aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-02-29 13:32:57 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-02-29 13:32:57 +0000
commit32c7a28aa909ed04993f4701702db5e6272bc7ab (patch)
treef1e593c8815efda6b5de46a4db3daac3786cb4c3
parentbc40ebf338191699793500f73178707f35946faa (diff)
Vector: missing injection lemmas and better impossible branches
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/Vectors/Fin.v10
-rw-r--r--theories/Vectors/VectorDef.v23
-rw-r--r--theories/Vectors/VectorSpec.v6
3 files changed, 27 insertions, 12 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 28e355fb6..a5e37f34b 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -14,7 +14,7 @@ Require Arith_base.
the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
Author: Pierre Boutillier
- Institution: PPS, INRIA 12/2010
+ Institution: PPS, INRIA 12/2010-01/2012
*)
Inductive t : nat -> Set :=
@@ -69,6 +69,13 @@ match a with
end.
End SCHEMES.
+Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
+match eq in _ = a return
+ match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
+ with @F1 _ => fun _ => True |@FS _ y => fun x' => x' = y end x with
+ eq_refl => eq_refl
+end.
+
(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
match n in t k return {i | i< k} with
@@ -167,6 +174,7 @@ end.
Lemma depair_sanity {m n} (o : t m) (p : t n) :
proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
+Proof.
induction o ; simpl.
rewrite L_sanity. now rewrite Mult.mult_0_r.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 0fee50ffb..30c0d4c0e 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,17 +40,17 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
(rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
fix rectS_fix {n} (v: t A (S n)) : P v :=
match v with
- |nil => @id
+ |nil => fun devil => False_rect (@ID) devil
|cons a 0 v =>
match v as vnn in t _ nn
return
match nn,vnn with
|0,vm => P (a :: vm)
- |S _,_ => ID
+ |S _,_ => _
end
with
|nil => bas a
- |_ :: _ => @id
+ |_ :: _ => fun devil => False_rect (@ID) devil
end
|cons a (S nn') v => rect a v (rectS_fix v)
end.
@@ -66,11 +66,11 @@ match v1 as v1' in t _ n1
|[] => fun v2 =>
match v2 with
|[] => bas
- |_ :: _ => @id
+ |_ :: _ => fun devil => False_rect (@ID) devil
end
|h1 :: t1 => fun v2 =>
match v2 with
- |[] => @id
+ |[] => fun devil => False_rect (@ID) devil
|h2 :: t2 => fun t1' =>
rect (rect2_fix t1' t2) h1 h2
end t1
@@ -83,10 +83,10 @@ match v with
end.
(** A vector of length [S _] is [cons] *)
-Definition caseS {A} (P : forall n, t A (S n) -> Type)
- (H : forall h {n} t, @P n (h :: t)) {n} v : P n v :=
-match v with
- |[] => @id (* Why needed ? *)
+Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
+ (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
+match v as v' in t _ m return match m, v' with |0, _ => False -> True |S _, v0 => P v' end with
+ |[] => fun devil => False_rect _ devil (* subterm !!! *)
|h :: t => H h t
end.
End SCHEMES.
@@ -111,11 +111,12 @@ Fixpoint const {A} (a:A) (n:nat) :=
Computational behavior of this function should be the same as
ocaml function. *)
-Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A :=
+Definition nth {A} :=
+fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
match p in Fin.t m' return t A m' -> A with
|Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
|Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
- (fun h n t p0 => nth t p0) v) p'
+ (fun h n t p0 => nth_fix t p0) v) p'
end v'.
(** An equivalent definition of [nth]. *)
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index a576315e6..2f4086e5c 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,6 +16,12 @@ Require Fin.
Require Import VectorDef.
Import VectorNotations.
+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
+ end.
+
(** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
is true for the one that use [lt] *)