<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">I have a Ph.D. student actively looking
into deriving various 'free' things from theories. Term languages
and term orders are included. No tool available yet, but I'm
hopeful we'll have something by the fall.<br>
<br>
Jacques<br>
<br>
On 2018-05-04 11:55 AM, Philip Wadler wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAESRbcqot=YFBuw7C8b+O-AVMnWutvnbVZupg+FWnQ17FaN0wg@mail.gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<div dir="ltr">Thanks, James. You note the proof of totality has
c^2 easy cases, but it is no easier than repeating the redundant
cases in a proof of determinism. Your suggestion fails to
simplify the proof, but would help if one had more than one
proof where one wished to exploit symmetry, or if one already
had a total order for some other reason. (I expect one could
derive a total order on reductions from a total order on terms,
which would also help.)
<div><br>
</div>
<div>Sounds like what Agda needs is a tool for deriving
lexicographic orders, *including* a proof that the
lexicographic order is a total order. Is anyone looking at
such a tool? I remember Ulf describing how deriving supports
decidable equality.</div>
<div><br>
</div>
<div>Cheers, -- P</div>
</div>
<div class="gmail_extra"><br clear="all">
<div>
<div class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of
Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a
href="http://homepages.inf.ed.ac.uk/wadler/"
target="_blank" moz-do-not-send="true">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 3 May 2018 at 18:34, James Wood <span
dir="ltr"><<a href="mailto:james.wood.100@strath.ac.uk"
target="_blank" moz-do-not-send="true">james.wood.100@strath.ac.uk</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">I believe
I've done the same sort of thing before by introducing a<br>
(constructively) total ordering between the things that
should be<br>
handled symmetrically. I'm not sure whether it really is
helpful, but it<br>
might be worth a try. I wrote up a simplified example at
[0], which I'll<br>
explain the approach of here.<br>
<br>
First, introduce a relation _≤_ : ∀ {M M′ M″} → (M ⟶ M′) →
(M ⟶ M″) →<br>
Set, and prove total : ∀ {M M′ M″} → (r0 : M ⟶ M′) (r1 : M ⟶
M″) → r0 ≤<br>
r1 ⊎ r1 ≤ r0. The relation _≤_ should roughly be what
deriving Ord would<br>
give in Haskell, though all of the data in the _⟶_
constructors except<br>
inductive positions can be ignored for simplicity. For
example, if you<br>
wanted this relation to be over List A, the definition could
be:<br>
<br>
data _≤_ : (xs ys : List A) → Set where<br>
[]≤[] : [] ≤ []<br>
[]≤∷ : ∀ {x xs} → [] ≤ x ∷ xs<br>
∷≤∷ : ∀ {x y xs ys} → xs ≤ ys → x ∷ xs ≤ y ∷ ys<br>
<br>
This does not assume any ordering on A. Notice that this
definition will<br>
have tr(c) constructors, where c is the number of
constructors of the<br>
original type (List, _⟶_).<br>
<br>
Next, prove the lemma det-≤ : ∀ {M M′ M″} (r0 : M ⟶ M′) (r1
: M ⟶ M″) →<br>
r0 ≤ r1 → M′ ≡ M″ by induction on the proof of r0 ≤ r1. This
will<br>
essentially contain only the cases you wanted to write, with
no<br>
duplicates. From this, the desired result det is proved by
cases on<br>
total r0 r1, using det-≤ in both cases (and sym in the
second case).<br>
<br>
The bottleneck in this is the proof of total, which requires
the full c²<br>
cases. However, this should be an easy proof. Wherever the
two head<br>
constructors differ, C-c C-a should find the solution, and
the c-many<br>
diagonal cases are by congruence.<br>
<br>
James<br>
<br>
[0]: <a
href="https://gist.github.com/laMudri/8b98b85ce570a09b464c007b1325ca1b"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://gist.github.com/<wbr>laMudri/<wbr>8b98b85ce570a09b464c007b1325ca<wbr>1b</a><br>
<div>
<div class="h5"><br>
On 03/05/18 12:49, Philip Wadler wrote:<br>
> Here is a proof that reduction is deterministic:<br>
> <br>
> -- Values do not reduce<br>
> Val-⟶ : ∀ {M N} → Value M → ¬ (M ⟶ N)<br>
> Val-⟶ Fun ()<br>
> Val-⟶ Zero ()<br>
> Val-⟶ (Suc VM) (ξ-suc M⟶N) = Val-⟶ VM M⟶N<br>
> <br>
> <br>
> -- Reduction is deterministic <br>
> <br>
> det : ∀ {M M′ M″}<br>
> → (M ⟶ M′)<br>
> → (M ⟶ M″)<br>
> ----------<br>
> → M′ ≡ M″<br>
> det (ξ-·₁ L⟶L′) (ξ-·₁ L⟶L″) = cong₂ _·_ (det
L⟶L′ L⟶L″) refl<br>
> det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL
L⟶L′)<br>
> det (ξ-·₁ L⟶L′) (β-→ _) = ⊥-elim (Val-⟶ Fun
L⟶L′)<br>
> det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL
L⟶L″)<br>
> det (ξ-·₂ _ M⟶M′) (ξ-·₂ _ M⟶M″) = cong₂ _·_
refl (det M⟶M′ M⟶M″)<br>
> det (ξ-·₂ _ M⟶M′) (β-→ VM) = ⊥-elim (Val-⟶ VM
M⟶M′)<br>
> det (β-→ VM) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ Fun
L⟶L″)<br>
> det (β-→ VM) (ξ-·₂ _ M⟶M″) = ⊥-elim (Val-⟶ VM
M⟶M″)<br>
> det (β-→ _) (β-→ _) = refl<br>
> det (ξ-suc M⟶M′) (ξ-suc M⟶M″) = cong `suc_ (det
M⟶M′ M⟶M″)<br>
> det (ξ-pred M⟶M′) (ξ-pred M⟶M″) = cong `pred_
(det M⟶M′ M⟶M″)<br>
> det (ξ-pred M⟶M′) β-pred-zero = ⊥-elim (Val-⟶
Zero M⟶M′)<br>
> det (ξ-pred M⟶M′) (β-pred-suc VM) = ⊥-elim
(Val-⟶ (Suc VM) M⟶M′)<br>
> det β-pred-zero (ξ-pred M⟶M′) = ⊥-elim (Val-⟶
Zero M⟶M′)<br>
> det β-pred-zero β-pred-zero = refl<br>
> det (β-pred-suc VM) (ξ-pred M⟶M′) = ⊥-elim
(Val-⟶ (Suc VM) M⟶M′)<br>
> det (β-pred-suc _) (β-pred-suc _) = refl<br>
> det (ξ-if0 L⟶L′) (ξ-if0 L⟶L″) = cong₃
`if0_then_else_ (det L⟶L′<br>
> L⟶L″) refl refl<br>
> det (ξ-if0 L⟶L′) β-if0-zero = ⊥-elim (Val-⟶
Zero L⟶L′)<br>
> det (ξ-if0 L⟶L′) (β-if0-suc VL) = ⊥-elim (Val-⟶
(Suc VL) L⟶L′)<br>
> det β-if0-zero (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶
Zero L⟶L″)<br>
> det β-if0-zero β-if0-zero = refl<br>
> det (β-if0-suc VL) (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶
(Suc VL) L⟶L″)<br>
> det (β-if0-suc _) (β-if0-suc _) = refl<br>
> det (ξ-Y M⟶M′) (ξ-Y M⟶M″) = cong `Y_ (det M⟶M′
M⟶M″)<br>
> det (ξ-Y M⟶M′) (β-Y refl) = ⊥-elim (Val-⟶ Fun
M⟶M′)<br>
> det (β-Y refl) (ξ-Y M⟶M″) = ⊥-elim (Val-⟶ Fun
M⟶M″)<br>
> det (β-Y refl) (β-Y refl) = refl<br>
> <br>
> <br>
> The proof and all relevant definitions are here:<br>
> <a href="https://wenkokke.github.io/sf/Typed"
rel="noreferrer" target="_blank"
moz-do-not-send="true">https://wenkokke.github.io/<wbr>sf/Typed</a><br>
> <br>
> Almost half the lines in the above proof are
redundant, for example<br>
> <br>
> det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL
L⟶L′)<br>
> det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL
L⟶L″)<br>
> <br>
> <br>
> are essentially identical.<br>
> <br>
> What I would like to do is delete the redundant
lines and add<br>
> <br>
> det M⟶M′ M⟶M″ = sym (det M⟶M″ M⟶M′)<br>
> <br>
> <br>
> to the bottom of the proof. But, of course, the
termination checker<br>
> complains.<br>
> <br>
> How can I rewrite the proof to exploit symmetry?
Cheers, -- P<br>
> <br>
> . \ Philip Wadler, Professor of Theoretical
Computer Science,<br>
> . /\ School of Informatics, University of
Edinburgh<br>
> . / \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/"
rel="noreferrer" target="_blank"
moz-do-not-send="true">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
> <br>
> <br>
</div>
</div>
> The University of Edinburgh is a charitable body,
registered in<br>
> Scotland, with registration number SC005336.<br>
> <br>
> <br>
> <br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
> <a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
> <br>
<br>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<p><br>
</p>
</body>
</html>