diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/success/Inversion.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/success/Inversion.v')
-rw-r--r-- | test-suite/success/Inversion.v | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v new file mode 100644 index 00000000..a9e4a843 --- /dev/null +++ b/test-suite/success/Inversion.v @@ -0,0 +1,85 @@ +Axiom magic:False. + +(* Submitted by Dachuan Yu (bug #220) *) +Fixpoint T[n:nat] : Type := + Cases n of + | O => (nat -> Prop) + | (S n') => (T n') + end. +Inductive R : (n:nat)(T n) -> nat -> Prop := + | RO : (Psi:(T O); l:nat) + (Psi l) -> (R O Psi l) + | RS : (n:nat; Psi:(T (S n)); l:nat) + (R n Psi l) -> (R (S n) Psi l). +Definition Psi00 : (nat -> Prop) := [n:nat] False. +Definition Psi0 : (T O) := Psi00. +Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). +Inversion 1. +Abort. + +(* Submitted by Pierre Casteran (bug #540) *) + +Set Implicit Arguments. +Parameter rule: Set -> Type. + +Inductive extension [I:Set]:Type := + NL : (extension I) +|add_rule : (rule I) -> (extension I) -> (extension I). + + +Inductive in_extension [I :Set;r: (rule I)] : (extension I) -> Type := + in_first : (e:?)(in_extension r (add_rule r e)) +|in_rest : (e,r':?)(in_extension r e) -> (in_extension r (add_rule r' e)). + +Implicits NL [1]. + +Inductive super_extension [I:Set;e :(extension I)] : (extension I) -> Type := + super_NL : (super_extension e NL) +| super_add : (r:?)(e': (extension I)) + (in_extension r e) -> + (super_extension e e') -> + (super_extension e (add_rule r e')). + + + +Lemma super_def : (I :Set)(e1, e2: (extension I)) + (super_extension e2 e1) -> + (ru:?) + (in_extension ru e1) -> + (in_extension ru e2). +Proof. + Induction 1. + Inversion 1; Auto. + Elim magic. +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. +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. |