Utilities related to Coq.Bool.Bvector
|
| Most of this file is taken directly from or adapted from CoLoR: http://color.loria.fr/ As a result, it is distributed under the CeCILL license, in contrast to the rest of this distribution. That license can be found at: http://www.cecill.info/licences/Licence_CeCILL_V2-en.html |
Require Import Bool Bvector Eqdep.
Set Implicit Arguments.
Require Export Bvector.
Implicit Arguments Vnil [A].
Implicit Arguments Vcons.
Implicit Arguments Vhead.
Implicit Arguments Vtail.
Implicit Arguments Vconst.
Lemmas |
Section S.
Variable A : Set.
Notation vec := (vector A).
Lemma VO_eq : forall v : vec O, v = Vnil.
Definition Vid n : vec n -> vec n :=
match n return vec n -> vec n with
| O => fun _ => Vnil
| _ => fun v => Vcons (Vhead v) (Vtail v)
end.
Lemma Vid_eq : forall n (v : vec n), v = Vid v.
Lemma VSn_eq : forall n (v : vec (S n)), v = Vcons (Vhead v) (Vtail v).
Variable eq_dec : forall x y : A, {x=y}+{~x=y}.
Local tactics |
Ltac Veqtac := repeat
match goal with
| H : @Vcons ?B ?x _ ?v = Vcons ?x ?w |- _ =>
let H1 := fresh in let H3 := fresh in
(injection H; intro H1; assert (H3 : v = w);
[apply (inj_pair2 nat (fun n => @vector B n)); assumption | clear H H1])
| H : @Vcons ?B ?x _ ?v = Vcons ?y ?w |- _ =>
let H1 := fresh in let H2 := fresh in let H3 := fresh in
(injection H; intros H1 H2; subst x; assert (H3 : v = w);
[apply (inj_pair2 nat (fun n => @vector B n)); assumption | clear H H1])
end.
Replace all variables of type Bvector O with Vnil.
|
Ltac VOtac := repeat
match goal with
| v : vector _ O |- _ => assert (v = Vnil); [apply VO_eq | subst v]
end.
Equate a variable y of type Bvector (S n) with Vcons (Vhead y) (Vtail y).
|
Ltac VSntac y :=
match type of y with
| vector _ (S _) => let H := fresh in
(assert (H : y = Vcons (Vhead y) (Vtail y)); [apply VSn_eq | rewrite H])
end.
Decidable equality |
Lemma eq_vec_dec : forall n (v1 v2 : vec n), {v1=v2}+{~v1=v2}.
End S.
Exported tactics |
Replace all variables of type Bvector O with Vnil.
|
Ltac VOtac := repeat
match goal with
| v : vector _ O |- _ => assert (v = Vnil); [apply VO_eq | subst v]
end.
Equate a variable y of type Bvector (S n) with Vcons (Vhead y) (Vtail y).
|
Ltac VSntac H y :=
match type of y with
| vector _ (S _) =>
(assert (H : y = Vcons (Vhead y) (Vtail y)); [apply VSn_eq | rewrite H])
end.