Library Asm.Util.Vector

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.


Index
This page has been generated by coqdoc