[Agda] `<' reasoning

[Sergei Meshveliani]

On Fri, 2017-12-08 at 09:45 +0100, Ulf Norell wrote:
> Here's how you can do it:
> 
> 
> https://gist.github.com/UlfNorell/102f8e59744de8a69f94b39f09f70c1d
> 
> [..]


Great! It works.
Thanks to people for the references.
I just start with the first one. 

Ulf, it remains a minor question about including there the functionality
of
  Relation.Binary.PropositionalEquality.≡-Reasoning

In the below example, the equality goal  test4   needs using ≡-Reasoning
and renaming the operators  begin_ and _∎.

Can  InequalityReasoning  be fixed so as to include the functionality of
≡-Reasoning 
(so that  import Relation.Binary.PropositionalEquality  to be canceled)
?

------------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE
                                                  using (_≡_; refl; sym)
open import Data.List using ([])

open import Bin0     using (0#; 1bin; _<_; _≤_; _+_)  -- of application
open import BinProp0 using (0<bs1; 0≤)                --
open import BinProp1 using (0+; +0; +-comm)           --

open import LtReasoning using (module InequalityReasoning)  
                                                        -- by U. Norell

open PE.≡-Reasoning renaming (begin_ to begin≡_; _∎ to _end≡)
                                                    -- renaming forced
postulate
  leq-refl     :  ∀ {x y} → x ≡ y → x ≤ y
  lt-trans     :  ∀ {x y z} → x < y → y < z → x < z
  leq-trans    :  ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
  lt/leq-trans :  ∀ {x y z} → x < y → y ≤ z → x < z
  leq/lt-trans :  ∀ {x y z} → x ≤ y → y < z → x < z

open InequalityReasoning _<_ _≤_
                         (\ {x y} → leq-refl {x} {y})
                         (\ {x y z} → lt-trans {x} {y} {z})
                         (\ {x y z} → leq-trans {x} {y} {z})
                         (\ {x y z} → lt/leq-trans {x} {y} {z})
                         (\ {x y z} → leq/lt-trans {x} {y} {z})
test1 : 0# < 1bin
test1 = begin
          0#     ≤[ 0≤ 0#  ]
          0#     ≡[ refl ]
          0#     <[ 0<bs1 [] ]
          1bin
        ∎

test2 :  0# + 1bin ≡ 1bin + 0#
test2 =  +-comm 0# 1bin

test3 :  0# ≤ 0# + 0#
test3 =  begin 0#        ≡[ sym (0+ 0#) ]
               0# + 0#
         ∎

test4 :  1bin ≡ 0# + 1bin   -- InequalityReasoning is not enough here

test4 =  begin≡ 1bin        ≡⟨ sym (+0 1bin) ⟩
                1bin + 0#   ≡⟨ +-comm 1bin 0# ⟩
                0# + 1bin
         end≡
----------------------------------------------------------------------


Thanks,

------
Sergei


> 
> 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
> 
>