Hi, I’m **lthms**.

I don’t like syntax highlighting, but I like types and functional programming languages. He/him.

Interested in starting a discussion? Don’t hesitate to shoot me an email.

# Rewriting in Coq

## Gate: Our Case Study §

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
The program attribute makes it easy to work with embedded proofs. For
instance, defining the ”open gate” is as easy as:

*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.Require Import Coq.Program.Tactics.

#[program]

Definition open_gate :=

{| open := true

; lock := false

|}.

Under the hood, program proves what needs to be proven, that is the
lock_is_close proposition. Just have a look at its output:
In this case, using

open_gate has type-checked, generating 1 obligation(s) Solving obligations automatically... open_gate_obligation_1 is defined No more obligations remaining open_gate is defined

`Program`

is a bit like cracking a nut with a
sledgehammer. We can easily do it ourselves using the refine tactic.
Definition open_gate': Gate.

refine ({| open := true

; lock := false

|}).

intro Hfalse.

discriminate Hfalse.

Defined.

## Gate Equality §

### Leibniz Equality Is Too Strong §

Basically, it means that if two doors are open, then they are equal. That
made sense to me, because by definition of Gate, a locked door is closed,
meaning an open door cannot be locked.
Here is an attempt to prove the open_gates_are_equal lemmas.

Proof.

assert (forall g, open g = true -> lock g = false). {

intros [o l h] equo.

cbn in *.

case_eq l; auto.

intros equl.

now rewrite (h equl) in equo.

}

assert (lock g = false) by apply (H _ equ).

assert (lock g' = false) by apply (H _ equ').

destruct g; destruct g'; cbn in *; subst.

The term to prove is now:
The next tactic I wanted to use reflexivity, because I'd basically proven
open g = open g' and lock g = lock g', which meets my definition of equality
at that time.
Except Coq wouldn’t agree. See how it reacts:
It cannot unify the two records. More precisely, it cannot unify
lock_is_close1 and lock_is_close0. So we abort and try something
else.

{| open := true; lock := false; lock_is_close := lock_is_close0 |} = {| open := true; lock := false; lock_is_close := lock_is_close1 |}

Unable to unify "{| open := true; lock := false; lock_is_close := lock_is_close1 |}" with "{| open := true; lock := false; lock_is_close := lock_is_close0 |}".

Abort.

### Ah hoc Equivalence Relation §

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 (R x y -> R y x),
reflexive (R x x) and transitive (R x y -> R y z -> R x z).

Require Import Coq.Classes.Equivalence.

#[program]

Instance Gate_Equivalence

: Equivalence gate_eq.

Next Obligation.

split; reflexivity.

Defined.

Next Obligation.

intros g g' [Hop Hlo].

symmetry in Hop; symmetry in Hlo.

split; assumption.

Defined.

Next Obligation.

intros g g' g'' [Hop Hlo] [Hop' Hlo'].

split.

+ transitivity (open g'); [exact Hop|exact Hop'].

+ transitivity (lock g'); [exact Hlo|exact Hlo'].

Defined.

Afterwards, the symmetry, reflexivity and transitivity tactics also
works with gate_eq, in addition to eq. We can try again to prove the
open_gate_are_the_same lemma and it will workfn:lemma.

Lemma open_gates_are_the_same:

forall (g g': Gate),

open g = true

-> open g' = true

-> gate_eq g g'.

Proof.

induction g; induction g'.

cbn.

intros H0 H2.

assert (lock0 = false).

+ case_eq lock0; [ intro H; apply lock_is_close0 in H;

rewrite H0 in H;

discriminate H

| reflexivity

].

+ assert (lock1 = false).

* case_eq lock1; [ intro H'; apply lock_is_close1 in H';

rewrite H2 in H';

discriminate H'

| reflexivity

].

* subst.

split; reflexivity.

Qed.

fn:lemma I know I should have proven an intermediate lemma to avoid code
duplication. Sorry about that, it hurts my eyes too.
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
Gate.
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_eq g g’? The answer
is “yes”, but it will not come for free.
Before moving forward, just consider the following function:

## Equivalence Relations and Rewriting §

Require Import Coq.Bool.Bool.

Program Definition try_open

(g: Gate)

: Gate :=

if eqb (lock g) false

then {| lock := false

; open := true

|}

else g.

It takes a gate as an argument and returns a new gate. If the former is not
locked, the latter is open. Otherwise the argument is returned as is.

Lemma gate_eq_try_open_eq

: forall (g g': Gate),

gate_eq g g'

-> gate_eq (try_open g) (try_open g').

Proof.

intros g g' Heq.

Abort.

What we could have wanted to do is: rewrite Heq. Indeed, g and g’
“are the same” (gate_eq g g’), so,
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
problem.
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, R x y 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, R x y -> R' (f x) (f y). Only if we
have this property, we would know that we could rewrite f x by f y, e.g. in
R' z (f x). Indeed, by transitivity of R’, we can deduce R' z (f y) from
R' z (f x) and R (f x) (f y).
If R x y -> R' (f x) (f y), 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:

*of course*, the results of try_open g and try_open g’ have to be the same. Except...Error: Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints: UNDEFINED EVARS: ?X49==[g g' Heq |- relation Gate] (internal placeholder) {?r} ?X50==[g g' Heq (do_subrelation:=Morphisms.do_subrelation) |- Morphisms.Proper (gate_eq ==> ?X49@{__:=g; __:=g'; __:=Heq}) try_open] (internal placeholder) {?p} ?X52==[g g' Heq |- relation Gate] (internal placeholder) {?r0} ?X53==[g g' Heq (do_subrelation:=Morphisms.do_subrelation) |- Morphisms.Proper (?X49@{__:=g; __:=g'; __:=Heq} ==> ?X52@{__:=g; __:=g'; __:=Heq} ==> Basics.flip Basics.impl) eq] (internal placeholder) {?p0} ?X54==[g g' Heq |- Morphisms.ProperProxy ?X52@{__:=g; __:=g'; __:=Heq} (try_open g')] (internal placeholder) {?p1}

#[local]

Open Scope signature_scope.

Require Import Coq.Classes.Morphisms.

#[program]

Instance try_open_Proper

: Proper (gate_eq ==> gate_eq) try_open.

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:
Back to our try_open morphism. Coq needs you to prove the following
goal:
Here is a way to prove that:

Add Parametric Morphism: (g) with signature (R) ==> (R') ==> (R'') ==> (R''') as <name>.

1 subgoal, subgoal 1 (ID 50) ============================ forall x y : Gate, gate_eq x y -> gate_eq (try_open x) (try_open y)

Next Obligation.

intros g g' Heq.

assert (gate_eq g g') as [Hop Hlo] by (exact Heq).

unfold try_open.

rewrite <- Hlo.

destruct (bool_dec (lock g) false) as [Hlock|Hnlock]; subst.

+ rewrite Hlock.

split; cbn; reflexivity.

+ apply not_false_is_true in Hnlock.

rewrite Hnlock.

cbn.

exact Heq.

Defined.

Now, back to our gate_eq_try_open_eq, we now can use rewrite and
reflexivity.

Require Import Coq.Setoids.Setoid.

Lemma gate_eq_try_open_eq

: forall (g g': Gate),

gate_eq g g'

-> gate_eq (try_open g) (try_open g').

Proof.

intros g g' Heq.

rewrite Heq.

reflexivity.

Qed.

We did it! We actually rewrite g as g’, even if we weren’t able to prove
g = g’.