Agda-stdlib: Add true <-Reasoning

[MatthewDaggitt]

Ulf has come up with how to do it here

• [ ] Fix the proof of +-mono-< in Data.Integer.Properties (https://github.com/agda/agda-stdlib/pull/491/commits/613908c11b2fe75259d287dad7a568ba63e45e90)
• [ ] Fix the proof of n<s[n/ℕd]*d in Data.Integer.DivMod (https://github.com/agda/agda-stdlib/pull/491/commits/6a57cc12db74f8ec07adae0066356b0bec040709)

[MatthewDaggitt]

Have messed around with this a bit. It turns out that Ulf's solution above has the major drawback that it doesn't work when the _<_ and _≈_ have different universe levels. This means that it can't be used for Relation.Binary.NonStrictToStrict for example. I don't suppose @UlfNorell or anyone with more knowledge of universe hackery than I know a way around this?

I have come up with a working solution here. It works by defining two versions of each chaining operator, for when you're taking in a strict/non-strict proof. However it's pretty ugly and requires greater understanding by a new user.

If we could get a version of @UlfNorell's working that'd be preferable.

[MatthewDaggitt]

Just a bit of context. The current Relation.Binary.StrictPartialOrderReasoning module is misnamed, as it's still reasoning about partial order relations. All it does is add a chaining operator that takes a strict proof and converts it to a non-strict proof. Hence why we need to come up with a way of implementing true strict partial order reasoning.

[MatthewDaggitt]

Got it! Took me a while but the following variant works for relations with different universe levels. It also has the advantage that the same set of primitives work for both strict and nonstrict proofs. Hence you only need to change the begin statement.

The trick was to use True to enforce the constraint when trying to prove a strict inequality, the inequality must actually be strict. The only downside is that the error messages aren't very nice as you might imagine...

open import Relation.Binary hiding (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse)
open import Function using (case_of_)
open import Level using (_⊔_)

module Relation.Binary.Reasoning.Core.Strict
  {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} (≈-sym   : Symmetric _≈_)
  {_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-refl  : Reflexive _≤_)
  {_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
  (≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where


  -- Useful tools

  data _≲_ (x y : A) : Set (ℓ₂ ⊔ ℓ₃) where
    strict    : x < y → x ≲ y
    nonstrict : x ≤ y → x ≲ y

  data IsStrict {x y} : x ≲ y → Set (ℓ₂ ⊔ ℓ₃) where
    isStrict : ∀ x<y → IsStrict (strict x<y)

  IsStrict? : ∀ {x y} (x≲y : x ≲ y) → Dec (IsStrict x≲y)
  IsStrict? (strict x<y)  = yes (isStrict x<y)
  IsStrict? (nonstrict _) = no λ()

  extractStrict : ∀ {x y} {x≲y : x ≲ y} → IsStrict x≲y → x < y
  extractStrict (isStrict x<y) = x<y


  -- Actual implementation

  infix -1 <-begin_ begin_
  infixr 0 _<⟨_⟩_ _≤⟨_⟩_ _≈⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
  infix  1 _∎ 

  begin_ : ∀ {x y : A} (x≲y : x ≲ y) → x ≤ y
  begin strict    x<y = <⇒≤ x<y
  begin nonstrict x≤y = x≤y

  <-begin_ : ∀ {x y : A} (x≲y : x ≲ y) {eq : True (IsStrict? x≲y)}  → x < y
  (<-begin p) {eq} = extractStrict (toWitness eq)

  _<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y ≲ z → x ≲ z
  x <⟨ x<y ⟩ strict    y<z = strict (<-trans x<y y<z)
  x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-trans x<y y≤z)

  _≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y ≲ z → x ≲ z
  x ≤⟨ x≤y ⟩ strict    y<z = strict    (≤-<-trans x≤y y<z)
  x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (≤-trans x≤y y≤z)

  _≈⟨_⟩_ : ∀ (x : A) {y z} → x ≈ y → y ≲ z → x ≲ z
  x ≈⟨ x≈y ⟩ strict    y<z = strict    (<-respˡ-≈ (≈-sym x≈y) y<z)
  x ≈⟨ x≈y ⟩ nonstrict y≤z = nonstrict (≤-respˡ-≈ (≈-sym x≈y) y≤z)

  _≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y ≲ z → x ≲ z
  x ≡⟨ x≡y ⟩ strict    y<z = strict    (case x≡y of λ where refl → y<z)
  x ≡⟨ x≡y ⟩ nonstrict y≤z = nonstrict (case x≡y of λ where refl → y≤z)
    -- ^ Note: don't match on the proof here, we need to decide strict vs nonstrict for neutral proofs

  _≡⟨⟩_ : ∀ (x : A) {y} → x ≲ y → x ≲ y
  x ≡⟨⟩ x≲y = x≲y

  _∎ : ∀ (x : A) → x ≲ x
  x ∎ = nonstrict ≤-refl


  -- Tests

  postulate
    u v w x y z b c : A
    u≈v : u ≈ v
    v≡w : v ≡ w
    w<x : w < x
    x≤y : x ≤ y
    y<z : y < z
    z≡b : z ≡ b
    b≈c : b ≈ c

  u≤c : u ≤ c
  u≤c = begin
    u ≈⟨ u≈v ⟩
    v ≡⟨ v≡w ⟩
    w <⟨ w<x ⟩
    x ≤⟨ x≤y ⟩
    y <⟨ y<z ⟩
    z ≡⟨ z≡b ⟩
    b ≈⟨ b≈c ⟩
    c ∎

  u<c : u < c
  u<c = <-begin
    u ≈⟨ u≈v ⟩
    v ≡⟨ v≡w ⟩
    w <⟨ w<x ⟩
    x ≤⟨ x≤y ⟩
    y <⟨ y<z ⟩
    z ≡⟨ z≡b ⟩
    b ≈⟨ b≈c ⟩
    c ∎

[HuStmpHrrr]

I think we can add another case to this definition:

  data _≲_ (x y : A) : Set (ℓ₂ ⊔ ℓ₃) where
    strict    : x < y → x ≲ y
    nonstrict : x ≤ y → x ≲ y
    eq : x ≈ y → x ≲ y

Then the reasoning steps can maintain the variance that eq can convert to nonstrict, nonstrict can convert to strict. We then should be able to obtain an API on all three relations.

c.f. #471

[MatthewDaggitt]

Hmm interesting idea! Not sure off the top of my head if that would work. Feel free to copy my code and give it a go at integrating it.

Even if it does work out, then I'm undecided at first glance whether we should include in a module for reasoning about orders. I'll give it some thought. Also can we transfer this discussion to #185 please!

[HuStmpHrrr]

I quickly worked out a version that is slightly diferent:

open import Relation.Binary

module Reasoning {c ℓ₁ ℓ₂} (P : Poset c ℓ₁ ℓ₂) where

open import Level using (Level; _⊔_; Lift; lift)
open import Function using (case_of_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open Poset P renaming (Carrier to A)
import Relation.Binary.NonStrictToStrict _≈_ _≤_ as S
open S using (_<_)

private
  isStrictPartialOrder = S.<-isStrictPartialOrder isPartialOrder

  l : Level
  l = c ⊔ ℓ₁ ⊔ ℓ₂

  module Lt = IsStrictPartialOrder isStrictPartialOrder

  <-≤-trans : Trans _<_ _≤_ _<_
  <-≤-trans = S.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈

  ≤-<-trans : Trans _≤_ _<_ _<_
  ≤-<-trans = S.≤-<-trans trans antisym ≤-respˡ-≈

data _∼_ (x y : A) : Set l where
  strict    : (x<y : x < y) → x ∼ y
  nonstrict : (x≤y : x ≤ y) → x ∼ y
  eq        : (x≈y : x ≈ y) → x ∼ y


⟦_⟧ : ∀ {x y} → x ∼ y → Set l
⟦_⟧ {x} {y} (strict x<y)    = Lift l (x < y)
⟦_⟧ {x} {y} (nonstrict x≤y) = Lift l (x ≤ y)
⟦_⟧ {x} {y} (eq x≈y)        = Lift l (x ≈ y)


infix -2 result_
infix -1 of_
infixr 0 _<⟨_⟩_ _≤⟨_⟩_ _≈⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
infix  1 _∎ 

of_ : ∀ {x y} → (rel : x ∼ y) → ⟦ rel ⟧
of strict x<y    = lift x<y
of nonstrict x≤y = lift x≤y
of eq x≈y        = lift x≈y

result_ : ∀ {a l} {A : Set a} → Lift {a} l A → A
result (lift lower) = lower

_<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y ∼ z → x ∼ z
x <⟨ x<y ⟩ strict y<z    = strict (Lt.trans x<y y<z)
x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-trans x<y y≤z)
x <⟨ x<y ⟩ eq y≈z        = strict (Lt.<-respʳ-≈ y≈z x<y)


_≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y ∼ z → x ∼ z
x ≤⟨ x≤y ⟩ strict y<z    = strict (≤-<-trans x≤y y<z)
x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (trans x≤y y≤z)
x ≤⟨ x≤y ⟩ eq y≈z        = nonstrict (≤-respʳ-≈ y≈z x≤y)

_≈⟨_⟩_ : ∀ (x : A) {y z} → x ≈ y → y ∼ z → x ∼ z
x ≈⟨ x≈y ⟩ strict y<z    = strict (Lt.<-respˡ-≈ (Eq.sym x≈y) y<z)
x ≈⟨ x≈y ⟩ nonstrict y≤z = nonstrict (≤-respˡ-≈ (Eq.sym x≈y) y≤z)
x ≈⟨ x≈y ⟩ eq y≈z        = eq (Eq.trans x≈y y≈z)


_≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y ∼ z → x ∼ z
x ≡⟨ x≡y ⟩ strict y<z    = strict (case x≡y of λ where refl → y<z)
x ≡⟨ x≡y ⟩ nonstrict y≤z = nonstrict (case x≡y of λ where refl → y≤z)
x ≡⟨ x≡y ⟩ eq y≈z        = eq (case x≡y of λ where refl → y≈z)

_≡⟨⟩_ : ∀ (x : A) {y} → x ∼ y → x ∼ y
x ≡⟨⟩ x∼y = x∼y

_∎ : ∀ x → x ∼ x
x ∎ = eq Eq.refl


private
  module Test where    
    postulate
      u v w x y z d e : A
      u≈v : u ≈ v
      v≡w : v ≡ w
      w<x : w < x
      x≤y : x ≤ y
      y<z : y < z
      z≡d : z ≡ d
      d≈e : d ≈ e

    u≤c : u < e
    u≤c = result of
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w <⟨ w<x ⟩
      x ≤⟨ x≤y ⟩
      y <⟨ y<z ⟩
      z ≡⟨ z≡d ⟩
      d ≈⟨ d≈e ⟩
      e ∎

    u≤y : u ≤ y
    u≤y = result of
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w ≤⟨ S.<⇒≤ (<-≤-trans w<x x≤y) ⟩
      y ∎

I did not worry about the eventual conversion between equivalence and ordering, but try to return the most accurate relation. Otherwise we can use Matthew's way to put the conversion into the APIs as well. Let me know what's your opinion.

(and I was very lazy on elaborate antecedents. but I hope it suffices for a proof of concept.)

[MatthewDaggitt]

So using Poset and then converting to the strict version runs into the problem that then you can't use this module to implement reasoning where the strict version of the relation is not defined in terms of less than and not equal (e.g. Data.Nat/Integer). Hence why I had all the requirements spelt out.

You'll then find that you need to deal with relations of different levels and therefore you'll need to tweak your lift function...

[HuStmpHrrr]

@MatthewDaggitt it's fine that we need to spell out antecedents eventually, I was just being lazy.

I've dealt with universes here already, haven't I? where will I need to tweak lift?

[HuStmpHrrr]

Just defined a full version:

open import Relation.Binary

module Reasoning {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} (≈-trans : Transitive _≈_) (≈-sym   : Symmetric _≈_) (≈-refl : Reflexive _≈_)
  {_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-respʳ-≈ : _≤_ Respectsʳ _≈_) (≤-refl  : Reflexive _≤_)
  {_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<-respʳ-≈ : _<_ Respectsʳ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
  (≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where

open import Level using (Level; _⊔_; Lift; lift)
open import Function using (case_of_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

private
  l : Level
  l = a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃

data _∼_ (x y : A) : Set l where
  strict    : (x<y : x < y) → x ∼ y
  nonstrict : (x≤y : x ≤ y) → x ∼ y
  eq        : (x≈y : x ≈ y) → x ∼ y


⟦_⟧ : ∀ {x y} → x ∼ y → Set l
⟦_⟧ {x} {y} (strict x<y)    = Lift l (x < y)
⟦_⟧ {x} {y} (nonstrict x≤y) = Lift l (x ≤ y)
⟦_⟧ {x} {y} (eq x≈y)        = Lift l (x ≈ y)


infix -2 result_
infix -1 of_
infixr 0 _<⟨_⟩_ _≤⟨_⟩_ _≈⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
infix  1 _∎ 

of_ : ∀ {x y} → (rel : x ∼ y) → ⟦ rel ⟧
of strict x<y    = lift x<y
of nonstrict x≤y = lift x≤y
of eq x≈y        = lift x≈y

result_ : ∀ {a l} {A : Set a} → Lift {a} l A → A
result (lift lower) = lower

_<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y ∼ z → x ∼ z
x <⟨ x<y ⟩ strict y<z    = strict (<-trans x<y y<z)
x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-trans x<y y≤z)
x <⟨ x<y ⟩ eq y≈z        = strict (<-respʳ-≈ y≈z x<y)

_≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y ∼ z → x ∼ z
x ≤⟨ x≤y ⟩ strict y<z    = strict (≤-<-trans x≤y y<z)
x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (≤-trans x≤y y≤z)
x ≤⟨ x≤y ⟩ eq y≈z        = nonstrict (≤-respʳ-≈ y≈z x≤y)

_≈⟨_⟩_ : ∀ (x : A) {y z} → x ≈ y → y ∼ z → x ∼ z
x ≈⟨ x≈y ⟩ strict y<z    = strict (<-respˡ-≈ (≈-sym x≈y) y<z)
x ≈⟨ x≈y ⟩ nonstrict y≤z = nonstrict (≤-respˡ-≈ (≈-sym x≈y) y≤z)
x ≈⟨ x≈y ⟩ eq y≈z        = eq (≈-trans x≈y y≈z)

_≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y ∼ z → x ∼ z
x ≡⟨ x≡y ⟩ strict y<z    = strict (case x≡y of λ where refl → y<z)
x ≡⟨ x≡y ⟩ nonstrict y≤z = nonstrict (case x≡y of λ where refl → y≤z)
x ≡⟨ x≡y ⟩ eq y≈z        = eq (case x≡y of λ where refl → y≈z)

_≡⟨⟩_ : ∀ (x : A) {y} → x ∼ y → x ∼ y
x ≡⟨⟩ x∼y = x∼y

_∎ : ∀ x → x ∼ x
x ∎ = eq ≈-refl


private
  module Test where    
    postulate
      u v w x y z d e : A
      u≈v : u ≈ v
      v≡w : v ≡ w
      w<x : w < x
      x≤y : x ≤ y
      y<z : y < z
      z≡d : z ≡ d
      d≈e : d ≈ e

    u≤c : u < e
    u≤c = result of
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w <⟨ w<x ⟩
      x ≤⟨ x≤y ⟩
      y <⟨ y<z ⟩
      z ≡⟨ z≡d ⟩
      d ≈⟨ d≈e ⟩
      e ∎

    u≤y : u ≤ y
    u≤y = result of
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w ≤⟨ <⇒≤ (<-≤-trans w<x x≤y) ⟩
      y ∎

[gallais]

Note that we can actually compute the level the result lives at:

levelOf : ∀ {x y} → x ∼ y → Level
levelOf (strict x<y)    = ℓ₃
levelOf (nonstrict x≤y) = ℓ₂
levelOf (eq x≈y)        = ℓ₁

⟦_⟧ : ∀ {x y} (r : x ∼ y) → Set (levelOf r)

We can then rename of_ to begin_ and drop result_ thus getting back the syntax
we are used to:

    u≤y : u ≤ y
    u≤y = begin
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w ≤⟨ <⇒≤ (<-≤-trans w<x x≤y) ⟩
      y ∎

[HuStmpHrrr]

ah ha, that's even better!

I was thinking about this couple days ago. The demo code above effectively wants following things:

1. a setoid
2. a partial order compatible with the setoid
3. a strict order compatible with the setoid and the partial order.

so we will just need 3 antecedents and this should make this api more applicable.

[MatthewDaggitt]

I've been thinking of that as well. Effective we want something like the following:

record IsOrderingPair
  {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) (_<_ : Rel A ℓ₃)
  : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where

  field
    isEquivalence : IsEquivalence _≈_
    isPartialOrder : IsPartialOrder _≈_ _≤_
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
    <⇒≤ : _<_ ⇒ _≤_
    ≤∧≉⇒< : ∀ {x y} → x ≤ y → ¬ (x ≈ y) → x < y

The name is rubbish though. Any ideas?

[HuStmpHrrr]

do we want to encapsulate those in a record, or would it be ok to enumerate them in the API? I think the API itself can be regarded as a template which will be further specialized when it comes to specific cases, wouldn't it?

[JacquesCarette]

@WolframKahl might have an idea about naming.

[WolframKahl]

I'd just go with the arrows that are actually there:
agda ≤→≉→< : ∀ {x y} → x ≤ y → ¬ (x ≈ y) → x < y
As a relation-algebraic statement, using ⇒ for inclusion as above, it would be:
agda ≤∩≉⇒< : ∀ {x y} → x ≤ y → ¬ (x ≈ y) → x < y
Possibly more readable with “spacing”:
agda ≤∩≉-⇒-< : ∀ {x y} → x ≤ y → ¬ (x ≈ y) → x < y

[JacquesCarette]

I meant the whole record... which I think is what Matthew was wondering about as well.

[WolframKahl]

IsPartialOrderWithCompatibleStrictPartialOrder

:wink:

[MatthewDaggitt]

I've just realised that the version proposed by @HuStmpHrrr above doesn't actually pass the tests in my original code. In particular you can't have a _<_ in the chain when trying to prove _≤_.

This was one of the key features I was after...

[HuStmpHrrr]

yeah, I wasn't trying to handle this. similarly we can't go from = to <=. but i think it's fine: <= is the weakest relation among three, and we are just one function call away.

I am not sure if we can turn it polymorphic while not changing the interface. I think type class can help, but not sure people would like it? any fancy way to solve this problem?

[WolframKahl]

I am using different start combinators like ≤-begin and ≈-begin to declare what the goal is (haven't needed <-begin yet), but let them act on a common datatype so that the step combinators can have the same names in all kinds of calculation.

The step combinators have to know that ≤ followed by < produces a <, which does not match the type expected by ≈-begin, but does match the type expected by ≤-begin, etc.

[HuStmpHrrr]

the step combinators have achieved it I believe. so are we good with different start combinators? do we want to try to achieve something fancier?

[gallais]

do we want to try to achieve something fancier?

Not sure we want to get down that road but this is possible:

levelOf : ∀ {x y} → x ∼ y → Level
levelOf (strict x<y)    = ℓ₃
levelOf (nonstrict x≤y) = ℓ₂
levelOf (eq x≈y)        = ℓ₁

relOf : ∀ {x y} (r : x ∼ y) → Rel A (levelOf r)
relOf (strict x<y)    = _<_
relOf (nonstrict x≤y) = _≤_
relOf (eq x≈y)        = _≈_

record Entails {r₁ r₂} (R₁ : Rel A r₁) (R₂ : Rel A r₂) : Set (a ⊔ r₁ ⊔ r₂) where
  field entails : R₁ ⇒ R₂
open Entails {{...}}

instance

  ≈-entails-≤ : Entails _≈_ _≤_
  ≈-entails-≤ = record { entails = λ z → ≤-respʳ-≈ z ≤-refl }

  <-entails-≤ : Entails _<_ _≤_
  <-entails-≤ = record { entails = <⇒≤ }

  id-Entails : ∀ {r} {R : Rel A r} → Entails R R
  id-Entails = record { entails = id }

begin_ : ∀ {r x y} {R : Rel A r} (r : x ∼ y) {{ _ : Entails (relOf r) R }} → R x y
begin (strict x<y)    = entails x<y
begin (nonstrict x≤y) = entails x≤y
begin (eq x≈y)        = entails x≈y

self-contained gist

[MatthewDaggitt]

I've tried @gallais suggestion and it results in unsolved metas when applying it in the Data.Integer.Properties file. See the reasoning2 branch for details.