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