diff options
Diffstat (limited to 'test-suite/success/Injection.v')
-rw-r--r-- | test-suite/success/Injection.v | 44 |
1 files changed, 24 insertions, 20 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index fd80cec6..f8f7c996 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -2,33 +2,37 @@ (* Check that Injection tries Intro until *) -Lemma l1 : (x:nat)(S x)=(S (S x))->False. -Injection 1. -Apply n_Sn. +Lemma l1 : forall x : nat, S x = S (S x) -> False. + injection 1. +apply n_Sn. Qed. -Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False. -Injection H. -Intros. -Apply (n_Sn x H0). +Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False. + injection H. +intros. +apply (n_Sn x H0). Qed. (* Check that no tuple needs to be built *) -Lemma l3 : (x,y:nat) - (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))= - (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y))) - -> x=y. -Intros x y H. -Injection H. -Exact [H]H. +Lemma l3 : + forall x y : nat, + existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) = + existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> + x = y. +intros x y H. + injection H. +exact (fun H => H). Qed. (* Check that a tuple is built (actually the same as the initial one) *) -Lemma l4 : (p1,p2:{O=O}+{O=O}) - (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2) - ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2). -Intros. -Injection H. -Exact [H]H. +Lemma l4 : + forall p1 p2 : {0 = 0} + {0 = 0}, + existS (fun n : nat => {n = n} + {n = n}) 0 p1 = + existS (fun n : nat => {n = n} + {n = n}) 0 p2 -> + existS (fun n : nat => {n = n} + {n = n}) 0 p1 = + existS (fun n : nat => {n = n} + {n = n}) 0 p2. +intros. + injection H. +exact (fun H => H). Qed. |