From 9754a53fdc14f6ee4cf00f851cda68d69889bdcd Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Tue, 4 Feb 2020 18:13:38 +0100 Subject: Initial commit with previous content and a minimal theme --- site/posts/RewritingInCoq.v | 347 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 347 insertions(+) create mode 100644 site/posts/RewritingInCoq.v (limited to 'site/posts/RewritingInCoq.v') diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v new file mode 100644 index 0000000..5ebf6c6 --- /dev/null +++ b/site/posts/RewritingInCoq.v @@ -0,0 +1,347 @@ +(** # +

Rewriting in Coq

+ + # *) + +(** I have to confess something. In the published codebase of SpecCert lies a + shameful secret. It takes the form of a set of axioms which are not + required. I thought they were when I wrote them, but it was before I heard + about “generalized rewriting,” setoids and morphisms. + + Now, I know the truth. I will have to update SpecCert eventually. But, + in the meantime, let me try to explain how it is possible to rewrite a + term in a proof using a ad-hoc equivalence relation and, when + necessary, a proper morphism. *) + +(** #
# *) + +(** ** Gate: Our Case Study *) + +(** Now, why would anyone want such a thing as “generalized rewriting” when the + [rewrite] tactic works just fine. + + The thing is: it does not in some cases. To illustrate my statement, we will + consider the following definition of a gate in Coq: *) + +Record Gate := + { open: bool + ; lock: bool + ; lock_is_close: lock = true -> open = false + }. + +(** 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: *) + +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: + +<< +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 +>> + + In this case, using <> 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 + +What does it mean for two gates to be equal? Intuitively, we know they +have to share the same states ([open] and [lock] is our case). + +*** Leibniz Equality Is Too Strong + +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: *) + +Lemma open_gates_are_equal (g g': Gate) + (equ : open g = true) (equ' : open g' = true) + : g = g'. + +(** 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: + +<< +{| open := true; lock := false; lock_is_close := lock_is_close0 |} = +{| open := true; lock := false; lock_is_close := lock_is_close1 |} +>> + +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: + +<< +Unable to unify "{| open := true; lock := false; lock_is_close := lock_is_close1 |}" + with "{| open := true; lock := false; lock_is_close := lock_is_close0 |}". +>> + +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. *) + +Abort. + +(** *** Ah hoc Equivalence Relation + +This is a familiar pattern. Coq cannot guess what we have in mind. Giving a +formal definition of “our equality” is fortunately straightforward. *) + +Definition gate_eq + (g g': Gate) + : Prop := + open g = open g' /\ lock g = lock g'. + +(** 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 work[fn: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. + +** Equivalence Relations and Rewriting + +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: *) + +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, _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} +>> + +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: *) + +#[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: + +<< +Add Parametric Morphism: (g) + with signature (R) ==> (R') ==> (R'') ==> (R''') + as . +>> + +Back to our [try_open] morphism. Coq needs you to prove the following +goal: + +<< +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: *) + +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’]. *) -- cgit v1.2.3