[Agda] `<' reasoning

[Ulf Norell]

Here's how you can do it:

https://gist.github.com/UlfNorell/102f8e59744de8a69f94b39f09f70c1d

I'll leave it as an exercise to hook it up to the relevant structures in
the standard library.

/ Ulf

On Thu, Dec 7, 2017 at 9:14 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> People,
>
> I meet the following difficulty in Agda reasoning about _<_.
>
> For  Nat,  it is all right, because  m < n  is defined as  suc m ≤ n,
> and it works the construct
>
>  e[1]<e[n] =
>      begin suc e[1]    ≤⟨ .. ⟩
>            ...
>            ...         ≡⟨ .. ⟩
>            ...
>            e[n]
>      ∎
>
> formed with standard functions
>                      begin_ , _∎ , _≡⟨_⟩_ , _≤⟨_⟩_
>
> But there are domains without  suc  operator (agreed with _≤_, _<_).
> For example, consider the proof
>
> ----------------------------------------------
> postulate  bs1<bs'1 :  bs1 < bs'1
>
> goal :  0bs1 < 0# + 0bs'1
> goal =  subst₂ _<_ (sym eq0) eq1 le
>      where
>      eq0 :  0bs1 ≡ bs1 * 2bin
>      eq0 =  *2≗*2bin bs1
>
>      eq1 = begin bs'1 * 2bin    ≡⟨ sym (*2≗*2bin bs'1) ⟩
>                  bs'1 *2        ≡⟨ sym (0+ 0bs'1) ⟩
>                  0# + 0bs'1
>            ∎
>
>      le :  bs1 * 2bin < bs'1 * 2bin
>      le =  *bs1-mono-< [ 0b ] bs1<bs'1
> ----------------------------------------------
>
> _≤_  is defined as   x ≤ y =  x < y ⊎ x ≡ y.
> And imagine that we do not use  suc  for redefining  _≤_.
>
> This is more difficult to compose and to read than the `linear'
> construct of
> goal =
>   begin< 0bs1          (1) ≡[ *2≗*2bin bs1 ]
>          bs1 * 2bin    (2) <[ *bs1-mono-< [ 0b ] bs1<bs'1 ]
>          bs'1 * 2bin   (3) ≡[ sym (*2≗*2bin bs'1) ]
>          bs'1 *2       (4) ≡[ sym (0+ 0bs'1) ]
>          0# + 0bs'1    (5)
>   end<
>
> Each next term in the column is less or is equal to the current one,
> and there is at least one line of the strict construct (that is of
> _<[_]_). Hence this proves the goal.
>
> Are there provers in Standard library that enable writing something like
> the above `linear' proofs with _<_ ?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171208/ffb45bd1/attachment.html>