diff options
| author | corbinea | 2002-10-01 15:59:03 +0000 |
|---|---|---|
| committer | corbinea | 2002-10-01 15:59:03 +0000 |
| commit | 0e341ccec174154a1e3cd51b8928a2e85c1ce1c1 (patch) | |
| tree | dc65593b33143cdd0e9e078143197f3879a77f9a /test-suite | |
| parent | 5ec22b65a16f82a3816635c3a4857a5ae544d6db (diff) | |
Adding the congruence closure tactics (CC and CCsolve).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/cc.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v new file mode 100644 index 0000000000..881d6f9e5f --- /dev/null +++ b/test-suite/success/cc.v @@ -0,0 +1,49 @@ +Require CC. + + +Theorem t1: (A:Set)(a:A)(f:A->A) + (f a)=a->(f (f a))=a. +Intros. +CC. +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. +CC. +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. +CC. +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 with CCSolve *) + +Theorem t4 : (A:Set; P:(A->Prop); u,v:A)u=v->(P u)->(P v). +Intros. +CCsolve. +Save. |