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
|
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.
|
