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.