[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