diff options
Diffstat (limited to 'test-suite/success/Injection.v')
| -rw-r--r-- | test-suite/success/Injection.v | 36 |
1 files changed, 34 insertions, 2 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 25e464d6..da218384 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -4,6 +4,7 @@ Require Eqdep_dec. (* Check that Injection tries Intro until *) +Unset Structural Injection. Lemma l1 : forall x : nat, S x = S (S x) -> False. injection 1. apply n_Sn. @@ -37,6 +38,7 @@ intros. injection H. exact (fun H => H). Qed. +Set Structural Injection. (* Test injection as *) @@ -65,7 +67,13 @@ Qed. Goal (forall x y : nat, x = y -> S x = S y) -> True. intros. einjection (H O). -instantiate (1:=O). +2:instantiate (1:=O). +Abort. + +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +einjection (H O ?[y]) as H0. +instantiate (y:=O). Abort. (* Test the injection intropattern *) @@ -79,12 +87,21 @@ Qed. (* Basic case, using sigT *) Scheme Equality for nat. +Unset Structural Injection. Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, existT P n H1 = existT P n H2 -> H1 = H2. intros. injection H. intro H0. exact H0. Abort. +Set Structural Injection. + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H as H0. +exact H0. +Abort. (* Test injection using K, knowing that an equality is decidable *) (* Basic case, using sigT, with "as" clause *) @@ -118,7 +135,22 @@ intros * [= H]. exact H. Abort. -(* Injection does not projects at positions in Prop... allow it? +(* Test the Keep Proof Equalities option. *) +Set Keep Proof Equalities. +Unset Structural Injection. + +Inductive pbool : Prop := Pbool1 | Pbool2. + +Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell. + +Goal Pbsc Pbool1 = Pbsc Pbool2 -> True. +injection 1. +match goal with + |- Pbool1 = Pbool2 -> True => idtac | |- True => fail +end. +Abort. + +(* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. Goal forall p q : True\/True, c _ p = c _ q -> False. |