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
168
169
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Tactics to generate Boolean-valued equalities *)
(** The [decide equality] tactic can generate a term of type
[forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type.
This term is a decidable equality function.
Similarly, this module defines a [boolean_equality] tactic that generates
a term of type [A -> A -> bool]. This term is a Boolean-valued equality
function over the inductive type [A]. Two internal tactics generate
proofs that show the correctness of this equality function [f], namely
proofs of the following two properties:
- [forall (x: A), f x x = true]
- [forall (x y: A), f x y = true -> x = y]
Finally, the [decide_equality_from f] tactic wraps [f] (the Boolean equality
generated by [boolean_equality]) and those proofs together, producing
a decidable equality of type [forall (x y: A), {x=y} + {x<>y}].
The advantage of the present tactics over the standard [decide equality]
tactic is that the former produce smaller transparent definitions than
the latter.
For a type [A] that has N constructors, [decide equality] produces a
single term of size O(N^3), which must be kept transparent so that
it computes and extracts as expected. Given such a big transparent
definition, the virtual machine compiler of Coq produces very big
chunks of VM code, causing memory overflows on 32-bit platforms.
In contrast, the term produced by [boolean_equality] has size O(N^2)
only (so to speak). The proofs that this term is a correct boolean
equality are still O(N^3), but those proofs are opaque and do not need
to be compiled to VM code. Only the boolean equality itself is defined
transparently and compiled.
The present tactics also have some restrictions:
- Constructors must have at most 4 arguments.
- Decidable equalities must be provided (as hypotheses in the context)
for all the types [T] of constructor arguments other than type [A].
- They probably do not work for mutually-defined inductive types.
*)
Require Import Coqlib.
Module BE.
Definition bool_eq {A: Type} (x y: A) : Type := bool.
Ltac bool_eq_base x y :=
change (bool_eq x y);
match goal with
| [ H: forall (x y: ?A), bool |- @bool_eq ?A x y ] => exact (H x y)
| [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq ?A x y ] => exact (proj_sumbool (H x y))
| _ => idtac
end.
Ltac bool_eq_case :=
match goal with
| |- bool_eq (?C ?x1 ?x2 ?x3 ?x4) (?C ?y1 ?y2 ?y3 ?y4) =>
refine (_ && _ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3|bool_eq_base x4 y4]
| |- bool_eq (?C ?x1 ?x2 ?x3) (?C ?y1 ?y2 ?y3) =>
refine (_ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3]
| |- bool_eq (?C ?x1 ?x2) (?C ?y1 ?y2) =>
refine (_ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2]
| |- bool_eq (?C ?x1) (?C ?y1) => bool_eq_base x1 y1
| |- bool_eq ?C ?C => exact true
| |- bool_eq _ _ => exact false
end.
Ltac bool_eq :=
match goal with
| [ |- ?A -> ?A -> bool ] =>
let f := fresh "rec" in let x := fresh "x" in let y := fresh "y" in
fix f 1; intros x y; change (bool_eq x y); destruct x, y; bool_eq_case
| [ |- _ -> _ ] =>
let eq := fresh "eq" in intro eq; bool_eq
end.
Lemma proj_sumbool_is_true:
forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A),
proj_sumbool (f x x) = true.
Proof.
intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto.
Qed.
Ltac bool_eq_refl_case :=
match goal with
| [ |- true = true ] => reflexivity
| [ |- proj_sumbool _ = true ] => apply proj_sumbool_is_true
| [ |- _ && _ = true ] => apply andb_true_iff; split; bool_eq_refl_case
| _ => auto
end.
Ltac bool_eq_refl :=
let Hrec := fresh "Hrec" in let x := fresh "x" in
fix Hrec 1; intros x; destruct x; simpl; bool_eq_refl_case.
Lemma false_not_true:
forall (P: Prop), false = true -> P.
Proof.
intros. discriminate.
Qed.
Lemma proj_sumbool_true:
forall (A: Type) (x y: A) (a: {x=y} + {x<>y}),
proj_sumbool a = true -> x = y.
Proof.
intros. destruct a. auto. discriminate.
Qed.
Ltac bool_eq_sound_case :=
match goal with
| [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case
| [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case
| [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto
| [ |- ?C ?x1 ?x2 ?x3 = ?C ?y1 ?y2 ?y3 ] => apply f_equal3; auto
| [ |- ?C ?x1 ?x2 = ?C ?y1 ?y2 ] => apply f_equal2; auto
| [ |- ?C ?x1 = ?C ?y1 ] => apply f_equal; auto
| [ |- ?x = ?x ] => reflexivity
| _ => idtac
end.
Ltac bool_eq_sound :=
let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in
let H := fresh "EQ" in
fix Hrec 1; intros x y; destruct x, y; intro H;
try (apply (false_not_true _ H)); simpl in H; bool_eq_sound_case.
Lemma dec_eq_from_bool_eq:
forall (A: Type) (f: A -> A -> bool)
(f_refl: forall x, f x x = true) (f_sound: forall x y, f x y = true -> x = y),
forall (x y: A), {x=y} + {x<>y}.
Proof.
intros. destruct (f x y) eqn:E.
left. apply f_sound. auto.
right; red; intros. subst y. rewrite f_refl in E. discriminate.
Defined.
End BE.
(** Applied to a goal of the form [t -> t -> bool], the [boolean_equality]
tactic defines a function with that type, returning [true] iff the two
arguments of type [t] are equal. [t] must be an inductive type.
For any type [u] other than [t] that appears in arguments of constructors
of [t], a decidable equality over [u] must be provided, as an hypothesis
of type [forall (x y: u), {x=y}+{x<>y}]. *)
Ltac boolean_equality := BE.bool_eq.
(** Given a function [beq] of type [t -> t -> bool] produced by [boolean_equality],
the [decidable_equality_from beq] produces a decidable equality with type
[forall (x y: t], {x=y}+{x<>y}. *)
Ltac decidable_equality_from beq :=
apply (BE.dec_eq_from_bool_eq _ beq); [abstract BE.bool_eq_refl|abstract BE.bool_eq_sound].
|
