From 88af5db4957e7e866ea507825ff0f08bd09c38ad Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Jul 2012 14:22:44 +0000
Subject: Vector equalities first stuff

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Vectors/Vector.v     |  2 ++
 theories/Vectors/VectorEq.v   | 80 +++++++++++++++++++++++++++++++++++++++++++
 theories/Vectors/VectorSpec.v |  2 +-
 theories/Vectors/vo.itarget   |  1 +
 4 files changed, 84 insertions(+), 1 deletion(-)
 create mode 100644 theories/Vectors/VectorEq.v

(limited to 'theories/Vectors')

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
-- 
cgit v1.2.3