blob: 940aa75075d5a2880115cfe5987ea2c391b64e7d (
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
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.
|
