I have to confess something. In the codebase of SpecCert lies a shameful
secret. It takes the form of a set of unnecessary axioms. I thought I
couldn’t avoid them at first, but it was before I heard about “generalized
rewriting,” setoids and morphisms. Now, I know the truth, and I will have
to update SpecCert eventually. But, in the meantime, let me try to explain
in this article originally published on May
13, 2017 how it is possible to rewrite a term in a proof using a
ad-hoc equivalence relation and, when necessary, a proper morphism.
According to this definition, a gate can be either open or closed. It can
also be locked, but if it is, it cannot be open at the same time. To express
this constrain, we embed the appropriate proposition inside the Record. By
doing so, we know for sure that we will never meet an ill-formed Gate
instance. The Coq engine will prevent it, because to construct a gate, one
will have to prove the lock_is_close predicate holds.
The program attribute makes it easy to work with embedded proofs. For
instance, defining the ”open gate” is as easy as:
When you write something like a=b in Coq, the = refers to the
eq function and this function relies on what is called the Leibniz
Equality: x and y are equal iff every property on A which is
true of x is also true of y
As for myself, when I first started to write some Coq code, the
Leibniz Equality was not really something I cared about and I tried to
prove something like this:
Because “equality” means something very specific in Coq, we won't say “two
gates are equal” anymore, but “two gates are equivalent”. That is, gate_eq is
an equivalence relation. But “equivalence relation” is also something very
specific. For instance, such relation needs to be symmetric (Rxy->Ryx),
reflexive (Rxx) and transitive (Rxy->Ryz->Rxz).
So here we are, with our ad-hoc definition of gate equivalence. We can use
symmetry, reflexivity and transitivity along with gate_eq and it works
fine because we have told Coq gate_eq is indeed an equivalence relation for
Can we do better? Can we actually use rewrite to replace an occurrence of g
by an occurrence of g’ as long as we can prove that gate_eqgg’? The answer
is “yes”, but it will not come for free.
Before moving forward, just consider the following function:
What Coq is trying to tell us here —in a very poor manner, I’d say— is actually
pretty simple. It cannot replace g by g’ because it does not know if two
equivalent gates actually give the same result when passed as the argument of
try_open. This is actually what we want to prove, so we cannot use rewrite
just yet, because it needs this result so it can do its magic. Chicken and egg
In other words, we are making the same mistake as before: not telling Coq what
it cannot guess by itself.
The rewrite tactic works out of the box with the Coq equality (eq, or most
likely =) because of the Leibniz Equality: x and y are equal iff every
property on A which is true of x is also true of y
This is a pretty strong property, and one a lot of equivalence relations do not
have. Want an example? Consider the relation R over A such that forall x
and y, Rxy holds true. Such relation is reflexive, symmetric and
reflexive. Yet, there is very little chance that given a function f:A->B
and R’ an equivalence relation over B, Rxy->R'(fx)(fy). Only if we
have this property, we would know that we could rewrite fx by fy, e.g. in
R'z(fx). Indeed, by transitivity of R’, we can deduce R'z(fy) from
R'z(fx) and R(fx)(fy).
If Rxy->R'(fx)(fy), then f is a morphism because it preserves an
equivalence relation. In our previous case, A is Gate, R is gate_eq,
f is try_open and therefore B is Gate and R’ is gate_eq. To make Coq
aware that try_open is a morphism, we can use the following syntax:
This notation is actually more generic because you can deal with functions
that take more than one argument. Hence, given g:A->B->C->D, R
(respectively R’, R’’ and R’’’) an equivalent relation of A
(respectively B, C and D), we can prove f is a morphism as follows:
Add Parametric Morphism: (g)
with signature (R) ==> (R') ==> (R'') ==> (R''')
Back to our try_open morphism. Coq needs you to prove the following
1 subgoal, subgoal 1 (ID 50)
forall x y : Gate, gate_eq x y -> gate_eq (try_open x) (try_open y)
Here is a way to prove that:
NextObligation. introsgg'Heq. assert (gate_eqgg') as [HopHlo] by (exactHeq). unfoldtry_open. rewrite <- Hlo. destruct (bool_dec (lockg) false) as [Hlock|Hnlock]; subst.
+ rewriteHlock. split; cbn; reflexivity.
+ applynot_false_is_trueinHnlock. rewriteHnlock. cbn. exactHeq. Defined.
Now, back to our gate_eq_try_open_eq, we now can use rewrite and