blob: 881d6f9e5f0f91e251f7a344a25f4af54f3a7e88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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.
|
