diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-13 11:07:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-13 11:07:59 +0000 |
| commit | fb3359d1fdd572066f17c70c33b22e88e71a0a3f (patch) | |
| tree | b34fea621f3412c9a5a2db708860f38ff923773c /test-suite/success/Inversion.v | |
| parent | 750dcf0d40fbd5feb58c3223aa1db44e3676083a (diff) | |
Nouvel exemple; correction du contexte du précédent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Inversion.v')
| -rw-r--r-- | test-suite/success/Inversion.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 04b395397..a9e4a8434 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -55,6 +55,7 @@ Qed. (* Example from Norbert Schirmer on Coq-Club, Sep 2000 *) +Unset Implicit Arguments. Definition Q[n,m:nat;prf:(le n m)]:=True. Goal (n,m:nat;H:(le (S n) m))(Q (S n) m H)==True. Intros. @@ -62,3 +63,23 @@ Dependent Inversion_clear H. Elim magic. Elim magic. Qed. + +(* Submitted by Boris Yakobowski (bug #529) *) +(* Check that Inversion does not fail due to unnormalized evars *) + +Set Implicit Arguments. +Require Import Bvector. + +Inductive I : nat -> Set := +| C1 : (I (S O)) +| C2 : (k,i:nat)(vector (I i) k) -> (I i). + +Inductive SI : (k:nat)(I k) -> (vector nat k) -> nat -> Prop := +| SC2 : (k,i,vf:nat) (v:(vector (I i) k))(xi:(vector nat i))(SI (C2 v) xi vf). + +Theorem SUnique : (k:nat)(f:(I k))(c:(vector nat k)) +(v,v':?) (SI f c v) -> (SI f c v') -> v=v'. +Proof. +NewInduction 1. +Intros H ; Inversion H. +Admitted. |