[Agda] `<' reasoning

[Sandro Stucki]

Hi Sergei,

The usual preorder reasoning framework from the standard library does
not work for _<_ because strict orders are irreflexive, but
reflexivity is crucial in the implementation of
Relation.Binary.PreorderReasoning.

Ulf's gist gets around that by defining a different framework for
inequality reasoning that is not based on
Relation.Binary.PreorderReasoning.

Another solution is to relax the requirements of
Relation.Binary.PreorderReasoning to allow reasoning about arbitrary
transitive relations that respect the underlying equality but are not
necessarily reflexive. Here's a possible implementation:

  https://gist.github.com/sstucki/2ce758a6dc62883ecbe54e71c0177fd0

The drawback of this solution is that it's not specific to
strict/non-strict orders so it doesn't allow mixing strict and
non-strict steps in the way Ulf's framework does. I suspect that this
limitation could be overcome via the conversion modules
Relation.Binary.{StrictToNonStrict,NonStrictToStrict} but I have not
tried that.

Cheers
/Sandro


On Fri, Dec 8, 2017 at 9:45 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>