diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/cc.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/cc.v')
-rw-r--r-- | test-suite/success/cc.v | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 94d827fd..b565183b 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -22,12 +22,12 @@ intros. congruence. Qed. -(* Examples that fail due to dependencies *) +(* Examples that fail due to dependencies *) (* yields transitivity problem *) Theorem dep : - forall (A : Set) (P : A -> Set) (f g : forall x : A, P x) + forall (A : Set) (P : A -> Set) (f g : forall x : A, P x) (x y : A) (e : x = y) (e0 : f y = g y), f x = g x. intros; dependent rewrite e; exact e0. Qed. @@ -42,12 +42,12 @@ intros; rewrite e; reflexivity. Qed. -(* example that Congruence. can solve - (dependent function applied to the same argument)*) +(* example that Congruence. can solve + (dependent function applied to the same argument)*) Theorem dep3 : forall (A : Set) (P : A -> Set) (f g : forall x : A, P x), - f = g -> forall x : A, f x = g x. intros. + f = g -> forall x : A, f x = g x. intros. congruence. Qed. @@ -61,7 +61,7 @@ Qed. Theorem inj2 : forall (A : Set) (a c d : A) (f : A -> A * A), - f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d. + f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d. intros. congruence. Qed. @@ -80,7 +80,7 @@ Qed. (* example with implications *) -Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D -> +Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D -> (A -> C) = (B -> D). congruence. Qed. @@ -101,7 +101,6 @@ Proof. congruence. auto. Qed. - - -
\ No newline at end of file + + |