[Agda] new InequalityReasoning

Sergei Meshveliani mechvel at botik.ru
Sun Mar 17 13:24:19 CET 2019


Dear standard library supporters,

I am trying to use  inequality reasoning  provided in lib-0.18, 
and have certain difficulties.

Currently I use a non-standard  InequalityReasoning  by Ulf Norell
(see LtReasoning.agda attached).

Now I need to replace it with the standard inequality reasoning  of  
lib-0.18-candidate.

I attach a file with small examples  test1 ... test6  

that work under InequalityReasoning by Ulf Norell.
They have been tested under  
                      Agda-2.6.0-candidate, ghc-8.6.3.

They show proofs for various combinations of the relations 
                                          _≡_, _≈_; _≤_, _<_.

Can you, please, demonstrate the corresponding code with using the 
inequality reasoning of lib-0.18 ?
 
Somehow 
  extract (poset : Poset)
  open Relation.Binary.Reasoning.PartialOrder poset using ...
  ...

Which modules to open, how to rename things, in order to have a module
with similar proofs for test1 ... test6 ?

Such an explanation can be, say, a part of the manual for the library.

Here I copy an essential part of the code:

----------------------------------------------------------------------
...
import Relation.Binary.EqReasoning as EqR                -- standard
open import LtReasoning using (module InequalityReasoning) 
                                                       -- nonstandard
-- the two "reasonings" imported
...
module _ {c ℓ₁ ℓ₂} (dto : DecTotalOrder c ℓ₁ ℓ₂)
         (open DecTotalOrder dto using () renaming (Carrier to C))
         (_<_ : Rel C ℓ₂)
  where
  open DecTotalOrder dto using (_≈_; _≤_; module Eq)
  open Eq using (decSetoid)
  open DecSetoid decSetoid using (setoid)

  postulate
    ≤-reflexive  :  {x y : C} → x ≡ y → x ≤ y
    ≤-reflexive≈ :  {x y : C} → x ≈ y → x ≤ y
    ≤-trans      :  Transitive _≤_
    <-trans      :  Transitive _<_
    <-≤-trans    :  {x y z : C} → x < y → y ≤ z → x < z
    ≤-<-trans    :  {x y z : C} → x ≤ y → y < z → x < z

  open InequalityReasoning {A = C} _<_ _≤_
                                   (\{x y}   → ≤-reflexive {x} {y})
                                   (\{x y z} → <-trans   {x} {y} {z})
                                   (\{x y z} → ≤-trans   {x} {y} {z})
                                   (\{x y z} → <-≤-trans {x} {y} {z})
                                   (\{x y z} → ≤-<-trans {x} {y} {z})

                 renaming (begin_ to begin-ineq_; _∎ to _end-ineq)

                 -- it imports  _<[_]_;  _≤[_]_;  _≡[_]_
  ...

  test5 : ∀ {x y z u} → x < y → y ≡ z → z ≤ u → x < u
  test5 {x} {y} {z} {u} x<y y≡z z≤u =
                                 begin-ineq x    <[ x<y ]
                                            y    ≡[ y≡z ]
                                            z    ≤[ z≤u ]
                                            u
                                 end-ineq

  test6 : ∀ {x y z u} → x < y → y ≈ z → z ≤ u → x < u    -- _≈_ used
  test6 {x} {y} {z} {u} x<y y≈z z≤u =
                                 begin-ineq x    <[ x<y ]
                                            y    ≤[ ≤-reflexive≈ y≈z ]
                                            z    ≤[ z≤u ]
                                            u
                                 end-ineq
----------------------------------------------------------------------------


Thanks,

------
Sergei

-------------- next part --------------

-- This is by  Ulf Norell:
--
-- a suport for reasoning with inequalities.

-- "In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html "


module LtReasoning where

open import Agda.Builtin.Equality

infix 0 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

-- Equality reasoning --

module InequalityReasoning {a b} {A : Set a}
              (_<_ : A → A → Set b)
              (_≤_ : A → A → Set b)
              (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)
  where

  data _≲_ (x y : A) : Set b where
    strict    : x < y → x ≲ y
    nonstrict : x ≤ y → x ≲ y

  module _ {x y : A} where
    ⟦_⟧ : x ≲ y → Set b
    ⟦ strict    _ ⟧ = x < y
    ⟦ nonstrict _ ⟧ = x ≤ y

    infix -1 begin_
    begin_ : (p : x ≲ y) → ⟦ p ⟧
    begin strict    p = p
    begin nonstrict p = p

  infixr 0 eqReasoningStep ltReasoningStep leqReasoningStep
  infix  1 _∎

  syntax eqReasoningStep x q p = x ≡[ p ] q
  eqReasoningStep : ∀ (x : A) {y z} → y ≲ z → x ≡ y → 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

  syntax ltReasoningStep x q p = x <[ p ] q
  ltReasoningStep : ∀ (x : A) {y z} → y ≲ z → x < y → x ≲ z
  x <[ x<y ] strict    y<z = strict (lt-trans x<y y<z)
  x <[ x<y ] nonstrict y≤z = strict (lt/leq-trans x<y y≤z)

  syntax leqReasoningStep x q p = x ≤[ p ] q
  leqReasoningStep : ∀ (x : A) {y z} → y ≲ z → x ≤ y → x ≲ z
  x ≤[ x≤y ] strict    y<z = strict    (leq/lt-trans x≤y y<z)
  x ≤[ x≤y ] nonstrict y≤z = nonstrict (leq-trans x≤y y≤z)

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


-- Example -----------------------------------

{-
  Bin : Set
  0# 0bs1 0bs'1 bs1 bs'1 2bin : Bin
  _*2 : Bin → Bin
  _+_ _*_ : Bin → Bin → Bin
  _<_ _≤_ : Bin → Bin → Set

  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


infix 7 _*2
infixl 7 _*_
infixl 6 _+_
infix 3 _<_ _≤_

open InequalityReasoning _<_ _≤_ leq-refl lt-trans leq-trans lt/leq-trans 
                                                             leq/lt-trans

  step-1 : 0bs1 ≡ bs1 * 2bin
  step-2 : bs1 * 2bin < bs'1 * 2bin
  step-3 : bs'1 * 2bin ≡ bs'1 *2
  step-4 : bs'1 *2 ≡ 0# + 0bs'1

goal : 0bs1 < 0# + 0bs'1
goal =
  begin 0bs1           ≡[ step-1 ]
        bs1 * 2bin     <[ step-2 ]
        bs'1 * 2bin    ≡[ step-3 ]
        bs'1 *2        ≡[ step-4 ]
        0# + 0bs'1
  ∎

goal' : 0bs1 < 0# + 0bs'1
goal' =
  begin 0bs1           ≤[ leq-refl step-1 ]
        bs1 * 2bin     <[ step-2 ]
        bs'1 * 2bin    ≤[ leq-refl step-3 ] 
        bs'1 *2        ≡[ step-4 ]
        0# + 0bs'1
  ∎

test : bs'1 * 2bin ≤ 0# + 0bs'1
test =
  begin bs'1 * 2bin  ≤[ leq-refl step-3 ]
        bs'1 *2      ≡[ step-4 ]
        0# + 0bs'1
  ∎
-}
-------------- next part --------------
module IneqReasoning where

open import Relation.Binary using
                            (Rel; Transitive; DecTotalOrder; DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using 
                                                     (_≡_; refl; sym; trans)
import Relation.Binary.EqReasoning as EqR
open import LtReasoning using (module InequalityReasoning)  -- by U. Norell



--****************************************************************************
module _ {c ℓ₁ ℓ₂} (dto : DecTotalOrder c ℓ₁ ℓ₂)
                   (open DecTotalOrder dto using () renaming (Carrier to C))
                   (_<_ : Rel C ℓ₂)
  where
  open DecTotalOrder dto using (_≈_; _≤_; module Eq)
  open Eq using (decSetoid)
  open DecSetoid decSetoid using (setoid)
  
  postulate
    ≤-reflexive  :  {x y : C} → x ≡ y → x ≤ y
    ≤-reflexive≈ :  {x y : C} → x ≈ y → x ≤ y
    ≤-trans      :  Transitive _≤_
    <-trans      :  Transitive _<_
    <-≤-trans    :  {x y z : C} → x < y → y ≤ z → x < z
    ≤-<-trans    :  {x y z : C} → x ≤ y → y < z → x < z

  open InequalityReasoning {A = C} _<_ _≤_
                                   (\{x y}   → ≤-reflexive {x} {y})
                                   (\{x y z} → <-trans   {x} {y} {z})
                                   (\{x y z} → ≤-trans   {x} {y} {z})
                                   (\{x y z} → <-≤-trans {x} {y} {z})
                                   (\{x y z} → ≤-<-trans {x} {y} {z})

                 renaming (begin_ to begin-ineq_; _∎ to _end-ineq)

  test1 : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z 
  test1 {x} {y} {z} x≈y y≈z =
                            begin x   ≈⟨ x≈y ⟩
                                  y   ≈⟨ y≈z ⟩
                                  z
                            ∎
                            where open EqR setoid

  test2 : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z 
  test2 {x} {y} {z} x≡y y≡z =
                              begin x   ≡⟨ x≡y ⟩
                                    y   ≡⟨ y≡z ⟩
                                    z
                              ∎
                              where open PE.≡-Reasoning {A = C}

  test3 : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
  test3 {x} {y} {z} x≤y y≤z =
                            begin-ineq x   ≤[ x≤y ]
                                       y   ≤[ y≤z ]
                                       z
                            end-ineq

  test4 : ∀ {x y z} → x ≤ y → y < z → x < z
  test4 {x} {y} {z} x≤y y<z =
                            begin-ineq x   ≤[ x≤y ]
                                       y   <[ y<z ]
                                       z
                            end-ineq

  test5 : ∀ {x y z u} → x < y → y ≡ z → z ≤ u → x < u
  test5 {x} {y} {z} {u} x<y y≡z z≤u =
                                 begin-ineq x    <[ x<y ]
                                            y   ≡[ y≡z ]
                                            z    ≤[ z≤u ]
                                            u
                                 end-ineq

  test6 : ∀ {x y z u} → x < y → y ≈ z → z ≤ u → x < u
  test6 {x} {y} {z} {u} x<y y≈z z≤u =
                                 begin-ineq x    <[ x<y ]
                                            y    ≤[ ≤-reflexive≈ y≈z ]
                                            z    ≤[ z≤u ]
                                            u
                                 end-ineq


More information about the Agda mailing list