diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /theories/Vectors/Fin.v | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'theories/Vectors/Fin.v')
-rw-r--r-- | theories/Vectors/Fin.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index 28e355fb..a5e37f34 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. |