diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:44 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:44 +0000 |
commit | 88af5db4957e7e866ea507825ff0f08bd09c38ad (patch) | |
tree | e81971a4eb04ff5e0be67d8d5b9e93ae93a1d0ff /theories/Vectors | |
parent | f03aaca003d9903bb90493a472a5f3138572a30e (diff) |
Vector equalities first stuff
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Vectors')
-rw-r--r-- | theories/Vectors/Vector.v | 2 | ||||
-rw-r--r-- | theories/Vectors/VectorEq.v | 80 | ||||
-rw-r--r-- | theories/Vectors/VectorSpec.v | 2 | ||||
-rw-r--r-- | theories/Vectors/vo.itarget | 1 |
4 files changed, 84 insertions, 1 deletions
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v index f3e5e338f..672858fa5 100644 --- a/theories/Vectors/Vector.v +++ b/theories/Vectors/Vector.v @@ -18,5 +18,7 @@ Based on contents from Util/VecUtil of the CoLoR contribution *) Require Fin. Require VectorDef. Require VectorSpec. +Require VectorEq. Include VectorDef. Include VectorSpec. +Include VectorEq.
\ No newline at end of file diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v new file mode 100644 index 000000000..04c570731 --- /dev/null +++ b/theories/Vectors/VectorEq.v @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Equalities and Vector relations + + Author: Pierre Boutillier + Institution: PPS, INRIA 07/2012 +*) + +Require Import VectorDef. +Require Import VectorSpec. +Import VectorNotations. + +Section BEQ. + + Variables (A: Type) (A_beq: A -> A -> bool). + Hypothesis A_eqb_eq: forall x y, A_beq x y = true <-> x = y. + + Definition eqb: + forall {m n} (v1: t A m) (v2: t A n), bool := + fix fix_beq {m n} v1 v2 := + match v1, v2 with + |[], [] => true + |_ :: _, [] |[], _ :: _ => false + |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2 + end%bool. + + Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n) + (Hbeq: eqb v1 v2 = true), m = n. + Proof. + intros m n v1; revert n. + induction v1; destruct v2; + [now constructor | discriminate | discriminate | simpl]. + intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq. + f_equal; eauto. + Qed. + + Lemma eqb_eq: forall n (v1: t A n) (v2: t A n), + eqb v1 v2 = true <-> v1 = v2. + Proof. + refine (@rect2 _ _ _ _ _); [now constructor | simpl]. + intros ? ? ? Hrec h1 h2; destruct Hrec; destruct (A_eqb_eq h1 h2); split. + + intros Hbeq. apply andb_prop in Hbeq; destruct Hbeq. + f_equal; now auto. + + intros Heq. destruct (cons_inj Heq). apply andb_true_intro. + split; now auto. + Qed. + + Definition eq_dec n (v1 v2: t A n): {v1 = v2} + {v1 <> v2}. + Proof. + case_eq (eqb v1 v2); intros. + + left; now apply eqb_eq. + + right. intros Heq. apply <- eqb_eq in Heq. congruence. + Defined. + +End BEQ. + +Section CAST. + + Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n. + Proof. + refine (fix cast {A m} (v: t A m) {struct v} := + match v in t _ m' return forall n, m' = n -> t A n with + |[] => fun n => match n with + | 0 => fun _ => [] + | S _ => fun H => False_rect _ _ + end + |h :: w => fun n => match n with + | 0 => fun H => False_rect _ _ + | S n' => fun H => h :: (cast w n' (f_equal pred H)) + end + end); discriminate. + Defined. + +End CAST. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 2f4086e5c..2d0a75f32 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -16,7 +16,7 @@ Require Fin. Require Import VectorDef. Import VectorNotations. -Definition cons_inj A a1 a2 n (v1 v2 : t A n) +Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 := match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1 with | eq_refl => conj eq_refl eq_refl diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget index 7f00d0162..779b1821c 100644 --- a/theories/Vectors/vo.itarget +++ b/theories/Vectors/vo.itarget @@ -1,4 +1,5 @@ Fin.vo VectorDef.vo VectorSpec.vo +VectorEq.vo Vector.vo |