<div dir="ltr">Here's how you can do it:<div><br></div><div><a href="https://gist.github.com/UlfNorell/102f8e59744de8a69f94b39f09f70c1d">https://gist.github.com/UlfNorell/102f8e59744de8a69f94b39f09f70c1d</a><br></div><div><br></div><div>I'll leave it as an exercise to hook it up to the relevant structures in the standard library.<br></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 7, 2017 at 9:14 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
<br>
I meet the following difficulty in Agda reasoning about _<_.<br>
<br>
For  Nat,  it is all right, because  m < n  is defined as  suc m ≤ n,<br>
and it works the construct<br>
<br>
 e[1]<e[n] =<br>
     begin suc e[1]    ≤⟨ .. ⟩<br>
           ...<br>
           ...         ≡⟨ .. ⟩<br>
           ...<br>
           e[n]<br>
     ∎<br>
<br>
formed with standard functions<br>
                     begin_ , _∎ , _≡⟨_⟩_ , _≤⟨_⟩_<br>
<br>
But there are domains without  suc  operator (agreed with _≤_, _<_).<br>
For example, consider the proof<br>
<br>
------------------------------<wbr>----------------<br>
postulate  bs1<bs'1 :  bs1 < bs'1<br>
<br>
goal :  0bs1 < 0# + 0bs'1<br>
goal =  subst₂ _<_ (sym eq0) eq1 le<br>
     where<br>
     eq0 :  0bs1 ≡ bs1 * 2bin<br>
     eq0 =  *2≗*2bin bs1<br>
<br>
     eq1 = begin bs'1 * 2bin    ≡⟨ sym (*2≗*2bin bs'1) ⟩<br>
                 bs'1 *2        ≡⟨ sym (0+ 0bs'1) ⟩<br>
                 0# + 0bs'1<br>
           ∎<br>
<br>
     le :  bs1 * 2bin < bs'1 * 2bin<br>
     le =  *bs1-mono-< [ 0b ] bs1<bs'1<br>
------------------------------<wbr>----------------<br>
<br>
_≤_  is defined as   x ≤ y =  x < y ⊎ x ≡ y.<br>
And imagine that we do not use  suc  for redefining  _≤_.<br>
<br>
This is more difficult to compose and to read than the `linear'<br>
construct of<br>
goal =<br>
  begin< 0bs1          (1) ≡[ *2≗*2bin bs1 ]<br>
         bs1 * 2bin    (2) <[ *bs1-mono-< [ 0b ] bs1<bs'1 ]<br>
         bs'1 * 2bin   (3) ≡[ sym (*2≗*2bin bs'1) ]<br>
         bs'1 *2       (4) ≡[ sym (0+ 0bs'1) ]<br>
         0# + 0bs'1    (5)<br>
  end<<br>
<br>
Each next term in the column is less or is equal to the current one,<br>
and there is at least one line of the strict construct (that is of<br>
_<[_]_). Hence this proves the goal.<br>
<br>
Are there provers in Standard library that enable writing something like<br>
the above `linear' proofs with _<_ ?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>