diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 13:32:57 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 13:32:57 +0000 |
commit | 32c7a28aa909ed04993f4701702db5e6272bc7ab (patch) | |
tree | f1e593c8815efda6b5de46a4db3daac3786cb4c3 /theories/Vectors/VectorSpec.v | |
parent | bc40ebf338191699793500f73178707f35946faa (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
Diffstat (limited to 'theories/Vectors/VectorSpec.v')
-rw-r--r-- | theories/Vectors/VectorSpec.v | 6 |
1 files changed, 6 insertions, 0 deletions
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] *) |