<div dir="ltr">Cool, thanks! -- P</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">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 4 May 2018 at 13:01, Jacques Carette <span dir="ltr"><<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    <div class="m_-7836122407960409597moz-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.<span class="HOEnZb"><font color="#888888"><br>
      <br>
      Jacques</font></span><div><div class="h5"><br>
      <br>
      On 2018-05-04 11:55 AM, Philip Wadler wrote:<br>
    </div></div></div><div><div class="h5">
    <blockquote type="cite">
      
      <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="m_-7836122407960409597gmail_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">http://homepages.inf.ed.ac.uk/<wbr>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">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">https://gist.github.com/laMudr<wbr>i/8b98b85ce570a09b464c007b1325<wbr>ca1b</a><br>
            <div>
              <div class="m_-7836122407960409597h5"><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">https://wenkokke.github.io/s<wbr>f/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">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" target="_blank">Agda@lists.chalmers.se</a><br>
            > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
            > <br>
            <br>
          </blockquote>
        </div>
        <br>
      </div>
      <br>
      <fieldset class="m_-7836122407960409597mimeAttachmentHeader"></fieldset>
      <br>
      <pre>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
      <br>
      <fieldset class="m_-7836122407960409597mimeAttachmentHeader"></fieldset>
      <br>
      <pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-7836122407960409597moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-7836122407960409597moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <p><br>
    </p>
  </div></div></div>

</blockquote></div><br></div>