diff options
Diffstat (limited to 'test-suite/success/cc.v')
-rw-r--r-- | test-suite/success/cc.v | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v new file mode 100644 index 00000000..4d898da9 --- /dev/null +++ b/test-suite/success/cc.v @@ -0,0 +1,83 @@ + +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. + +(* 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. + +(* 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. + +(* 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. + + +(* 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. + +(* 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 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. + +(* Examples with discrimination rule *) + +Theorem discr1 : true=false->False. +Intros. +Congruence. +Save. + +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. |