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.