[Agda] `<' reasoning

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Ulf Norell
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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Sandro Stucki
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
https://gist.github.com/sstucki/2ce758a6dc62883ecbe54e71c0177fd0

In a proof-relevant setting it can also be nice to avoid inserting extra
steps in proofs. I often use combinators of the following kind:

finally : ∀ {a} {A : Set a} (x y : A) → x ≡ y → x ≡ y
finally _ _ x≡y = x≡y

syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

I also have a library that allows you to mix different relations:

http://www.cse.chalmers.se/~nad/listings/up-to/Equational-reasoning.html

One key piece is the following abstraction of transitivity:

record Transitive {a b p q} {A : Set a} {B : Set b}
(P : A → A → Set p) (Q : A → B → Set q) :
Set (a ⊔ b ⊔ p ⊔ q) where
constructor is-transitive
field
transitive : ∀ {x y z} → P x y → Q y z → Q x z

(I also have one where transitivity goes from P and Q to P.) It is then
up to users of the library to define suitable instances.

[Sergei Meshveliani]

Post by Ulf Norell
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

Post by Ulf Norell
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
https://lists.chalmers.se/mailman/listinfo/agda