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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a.
intros.
congruence.
Qed.
Theorem t2 :
forall (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.
Qed.
(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
Theorem t3 :
forall (N : Set) (o : N) (s 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.
Qed.
(* Examples that fail due to dependencies *)
(* yields transitivity problem *)
Theorem dep :
forall (A : Set) (P : A -> Set) (f g : forall 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.
Qed.
(* yields congruence problem *)
Theorem dep2 :
forall (A B : Set)
(f : forall (A : Set) (b : bool), if b then unit else A -> unit)
(e : A = B), f A true = f B true.
intros; rewrite e; reflexivity.
Qed.
(* example that Congruence. can solve
(dependent function applied to the same argument)*)
Theorem dep3 :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x),
f = g -> forall x : A, f x = g x. intros.
congruence.
Qed.
(* Examples with injection rule *)
Theorem inj1 :
forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d.
intros.
split; congruence.
Qed.
Theorem inj2 :
forall (A : Set) (a c d : A) (f : A -> A * A),
f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
intros.
congruence.
Qed.
(* Examples with discrimination rule *)
Theorem discr1 : true = false -> False.
intros.
congruence.
Qed.
Theorem discr2 : Some true = Some false -> False.
intros.
congruence.
Qed.
(* example with implications *)
Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D ->
(A -> C) = (B -> D).
congruence.
Qed.
Set Implicit Arguments.
Parameter elt: Set.
Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
Definition t (A: Set) := elt -> A.
Definition get (A: Set) (x: elt) (m: t A) := m x.
Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
fun (y: elt) => if elt_eq y x then v else m y.
Lemma gsident:
forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Proof.
intros. unfold get, set. case (elt_eq j i); intro.
congruence.
auto.
Qed.
(* bug 2447 is now closed (PC, 2014) *)
Section bug_2447.
Variable T:Type.
Record R := mkR {x:T;y:T;z:T}.
Variables a a' b b' c c':T.
Lemma bug_2447: mkR a b c = mkR a' b c -> a = a'.
congruence.
Qed.
Lemma bug_2447_variant1: mkR a b c = mkR a b' c -> b = b'.
congruence.
Qed.
Lemma bug_2447_variant2: mkR a b c = mkR a b c' -> c = c'.
congruence.
Qed.
End bug_2447.
(* congruence was supposed to do discriminate but it was bugged for
types with indices *)
Inductive I : nat -> Type := C : I 0 | D : I 0.
Goal ~C=D.
congruence.
Qed.
(* Example by Jonathan Leivant, congruence up to universes *)
Section JLeivant.
Variables S1 S2 : Set.
Definition T1 : Type := S1.
Definition T2 : Type := S2.
Goal T1 = T1.
congruence.
Undo.
unfold T1.
congruence.
Qed.
End JLeivant.
(* An example with primitive projections *)
Module PrimitiveProjections.
Set Primitive Projections.
Record t (A:Type) := { f : A }.
Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
congruence.
Undo.
intros.
unfold f in H0. (* internally turn the projection to unfolded form *)
congruence.
Qed.
End PrimitiveProjections.
|
