------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with two relations:
-- equality and some other ordering.
------------------------------------------------------------------------
--
-- See `Data.Nat.Properties` or `Relation.Binary.Reasoning.PartialOrder`
-- for examples of how to instantiate this module.
{-#
OPTIONS
--cubical-compatible
--safe
#-}
open
import
Level
using
(
_⊔_
)
open
import
Function.Base
using
(
case_of_
)
open
import
Relation.Nullary.Decidable.Core
using
(
Dec
;
yes
;
no
)
open
import
Relation.Binary.Core
using
(
Rel
;
_⇒_
)
open
import
Relation.Binary.Definitions
using
(
Reflexive
;
Trans
)
open
import
Relation.Binary.Structures
using
(
IsPreorder
)
open
import
Relation.Binary.PropositionalEquality.Core
as
≡
using
(
_≡_
)
open
import
Relation.Binary.Reasoning.Syntax
module
Relation.Binary.Reasoning.Base.Double
{
a
ℓ₁
ℓ₂
}
{
A
:
Set
a
}
{
_≈_
:
Rel
A
ℓ₁
}
{
_≲_
:
Rel
A
ℓ₂
}
(
isPreorder
:
IsPreorder
_≈_
_≲_
)
where
open
IsPreorder
isPreorder
------------------------------------------------------------------------
-- A datatype to hide the current relation type
infix
4
_IsRelatedTo_
data
_IsRelatedTo_
(
x
y
:
A
)
:
Set
(
a
⊔
ℓ₁
⊔
ℓ₂
)
where
nonstrict
:
(
x≲y
:
x
≲
y
)
→
x
IsRelatedTo
y
equals
:
(
x≈y
:
x
≈
y
)
→
x
IsRelatedTo
y
start
:
_IsRelatedTo_
⇒
_≲_
start
(
equals
x≈y
)
=
reflexive
x≈y
start
(
nonstrict
x≲y
)
=
x≲y
≡-go
:
Trans
_≡_
_IsRelatedTo_
_IsRelatedTo_
≡-go
x≡y
(
equals
y≈z
)
=
equals
(
case
x≡y
of
λ
where
≡.refl
→
y≈z
)
≡-go
x≡y
(
nonstrict
y≤z
)
=
nonstrict
(
case
x≡y
of
λ
where
≡.refl
→
y≤z
)
≲-go
:
Trans
_≲_
_IsRelatedTo_
_IsRelatedTo_
≲-go
x≲y
(
equals
y≈z
)
=
nonstrict
(
∼-respʳ-≈
y≈z
x≲y
)
≲-go
x≲y
(
nonstrict
y≲z
)
=
nonstrict
(
trans
x≲y
y≲z
)
≈-go
:
Trans
_≈_
_IsRelatedTo_
_IsRelatedTo_
≈-go
x≈y
(
equals
y≈z
)
=
equals
(
Eq.trans
x≈y
y≈z
)
≈-go
x≈y
(
nonstrict
y≲z
)
=
nonstrict
(
∼-respˡ-≈
(
Eq.sym
x≈y
)
y≲z
)
stop
:
Reflexive
_IsRelatedTo_
stop
=
equals
Eq.refl
------------------------------------------------------------------------
-- A record that is used to ensure that the final relation proved by the
-- chain of reasoning can be converted into the required relation.
data
IsEquality
{
x
y
}
:
x
IsRelatedTo
y
→
Set
(
a
⊔
ℓ₁
⊔
ℓ₂
)
where
isEquality
:
∀
x≈y
→
IsEquality
(
equals
x≈y
)
IsEquality?
:
∀
{
x
y
}
(
x≲y
:
x
IsRelatedTo
y
)
→
Dec
(
IsEquality
x≲y
)
IsEquality?
(
nonstrict
_)
=
no
λ()
IsEquality?
(
equals
x≈y
)
=
yes
(
isEquality
x≈y
)
extractEquality
:
∀
{
x
y
}
{
x≲y
:
x
IsRelatedTo
y
}
→
IsEquality
x≲y
→
x
≈
y
extractEquality
(
isEquality
x≈y
)
=
x≈y
equalitySubRelation
:
SubRelation
_IsRelatedTo_
_
_
equalitySubRelation
=
record
{
IsS
=
IsEquality
;
IsS?
=
IsEquality?
;
extract
=
extractEquality
}
------------------------------------------------------------------------
-- Reasoning combinators
open
begin-syntax
_IsRelatedTo_
start
public
open
begin-equality-syntax
_IsRelatedTo_
equalitySubRelation
public
open
≡-syntax
_IsRelatedTo_
≡-go
public
open
≈-syntax
_IsRelatedTo_
_IsRelatedTo_
≈-go
Eq.sym
public
open
≲-syntax
_IsRelatedTo_
_IsRelatedTo_
≲-go
public
open
end-syntax
_IsRelatedTo_
stop
public
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
open
∼-syntax
_IsRelatedTo_
_IsRelatedTo_
≲-go
public
{-#
WARNING_ON_USAGE
step-∼
"Warning: step-∼ and _∼⟨_⟩_ syntax was deprecated in v2.0. Please use step-≲ and _≲⟨_⟩_ instead. "
#-}