diff options
Diffstat (limited to 'test-suite/success/cc.v')
| -rw-r--r-- | test-suite/success/cc.v | 112 |
1 files changed, 54 insertions, 58 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 4d898da9..42df990f 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -1,83 +1,79 @@ -Theorem t1: (A:Set)(a:A)(f:A->A) - (f a)=a->(f (f a))=a. -Intros. -Congruence. -Save. - -Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A) - a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))-> - (g a b)=a. -Intros. -Congruence. -Save. +Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a. +intros. + congruence. +Qed. + +Theorem t2 : + forall (A : Set) (a b : A) (f : A -> A) (g : A -> A -> A), + a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a. +intros. + congruence. +Qed. (* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *) -Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N) - (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s o)))))))))))))))=o-> - (s (s (s (s (s (s (s (s (s (s o))))))))))=o-> - (s (s (s (s (s (s o))))))=o-> - o=(s o). -Intros. -Congruence. -Save. +Theorem t3 : + forall (N : Set) (o : N) (s d : N -> N), + s (s (s (s (s (s (s (s (s (s (s (s (s (s (s o)))))))))))))) = o -> + s (s (s (s (s (s (s (s (s (s o))))))))) = o -> + s (s (s (s (s (s o))))) = o -> o = s o. +intros. + congruence. +Qed. (* Examples that fail due to dependencies *) (* yields transitivity problem *) -Theorem dep:(A:Set)(P:A->Set)(f,g:(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. -Save. +Theorem dep : + 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. (* yields congruence problem *) -Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B) - (f A true)=(f B true). -Intros;Rewrite e;Reflexivity. -Save. +Theorem dep2 : + forall (A B : Set) + (f : forall (A : Set) (b : bool), if b then unit else A -> unit) + (e : A = B), f A true = f B true. +intros; rewrite e; reflexivity. +Qed. (* example that Congruence. can solve (dependent function applied to the same argument)*) -Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x). Intros. -Congruence. -Save. +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. + congruence. +Qed. (* Examples with injection rule *) -Theorem inj1 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d. -Intros. -Split;Congruence. -Save. +Theorem inj1 : + forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d. +intros. +split; congruence. +Qed. -Theorem inj2 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))-> - (Some ? (f c))=(Some ? (f d))->c=d. -Intros. -Congruence. -Save. +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. +intros. + congruence. +Qed. (* Examples with discrimination rule *) -Theorem discr1 : true=false->False. -Intros. -Congruence. -Save. +Theorem discr1 : true = false -> False. +intros. + congruence. +Qed. -Theorem discr2 : (Some ? true)=(Some ? false)->False. -Intros. -Congruence. -Save. - -(* example with Congruence.Solve (requires CCSolve.v)*) - -Require CCSolve. - -Theorem t4 : (A:Set; P:(A->Prop); a,b,c,d:A)a=b->c=d-> - (P a)->((P b)->(P c))->(P d). -Intros. -CCsolve. -Save. +Theorem discr2 : Some true = Some false -> False. +intros. + congruence. +Qed. |