Skip to content

Commit b2e74a7

Browse files
hexwellLorenzoMolena
hexwell
and
LorenzoMolena
authored
Non-strict order equational reasoning (#1229)
* rename `begin` to `begin<`, add `begin≤` and weaken hypothesis, use pattern matching instead of with-abstraction, move examples to a module * Separate `<-≤-StrictReasoning` from `<-≤-Reasoning`, since the latter uses additional data * remove SubRelation record, cleanup * align with library code style, improve wording * improve doc wording * move Triple datatype to separate private module to hide it --------- Co-authored-by: Lorenzo Molena <[email protected]>
1 parent c4401c7 commit b2e74a7

File tree

1 file changed

+191
-95
lines changed

1 file changed

+191
-95
lines changed

‎Cubical/Relation/Binary/Order/QuosetReasoning.agda‎

Lines changed: 191 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,14 @@
1-
-- Example of usage:
2-
--
3-
-- open <-syntax
4-
-- open ≤-syntax
5-
-- open ≡-syntax
6-
--
7-
-- example : ∀ (x y z u v w α γ δ : P)
8-
-- → x < y
9-
-- → y ≤ z
10-
-- → z ≡ u
11-
-- → u < v
12-
-- → v ≤ w
13-
-- → w ≡ α
14-
-- → α ≡ γ
15-
-- → γ ≡ δ
16-
-- → x < δ
17-
-- example x y z u v w α γ δ x<y y≤z z≡u u<v v≤w w≡α α≡γ γ≡δ = begin
18-
-- x <⟨ x<y ⟩
19-
-- y ≤⟨ y≤z ⟩
20-
-- z ≡→≤⟨ z ≡⟨ z≡u ⟩
21-
-- u ≡⟨ sym z≡u ⟩
22-
-- z ≡[ i ]⟨ z≡u i ⟩
23-
-- u ∎ ⟩
24-
-- u <⟨ u<v ⟩
25-
-- v ≤⟨ v≤w ⟩
26-
-- w ≡→≤⟨
27-
-- w ≡⟨ w≡α ⟩
28-
-- α ≡⟨ α≡γ ⟩
29-
-- γ ≡[ i ]⟨ γ≡δ i ⟩
30-
-- δ ∎
31-
-- ⟩
32-
-- δ ◾
33-
341
{-
35-
Equational reasoning in a Quoset that is also a Poset, i.e.
36-
for writing a chain of <,≤,≡ with at least a <
2+
Equational reasoning in a Quoset that is also a Poset,
3+
i.e. for writing a chain of <, ≤, ≡.
4+
5+
Import <-≤-StrictReasoning if you only need to obtain strict inequalities,
6+
import <-≤-Reasoning otherwise.
7+
8+
Use begin< to obtain a strict inequality (in this case, at least one < is required in the chain).
9+
Use begin≤ to obtain a nonstrict inequality.
3710
-}
11+
3812
module Cubical.Relation.Binary.Order.QuosetReasoning where
3913

4014
open import Cubical.Foundations.Prelude
@@ -44,84 +18,76 @@ open import Cubical.Data.Empty.Base as ⊥
4418
open import Cubical.Relation.Nullary.Base
4519

4620
open import Cubical.Relation.Binary.Base
47-
open BinaryRelation
4821
open import Cubical.Relation.Binary.Order.Poset.Base
4922
open import Cubical.Relation.Binary.Order.Quoset.Base
5023

5124
private
5225
variable
5326
ℓ ℓ≤ ℓ< : Level
5427

55-
-- Record with all the parts needed to extract a subrelation from a relation
56-
-- (e.g. from a chain of <,≤,=, with at least a <, to a <)
57-
-- Note:
58-
-- It could be better to move this record in Relation.Binary.Base,
59-
-- but there isn't yet a proper module for subrelations.
60-
record SubRelation
61-
{ℓR}
62-
{P : Type ℓ}
63-
(_R_ : Rel P P ℓR ) ℓS ℓIsS : Type (ℓ-max ℓ (ℓ-max ℓR (ℓ-max (ℓ-suc ℓS) (ℓ-suc ℓIsS)))) where
64-
no-eta-equality
65-
field
66-
_S_ : Rel P P ℓS
67-
IsS : ∀ {x y} → x R y → Type ℓIsS
68-
IsS? : ∀ {x y} → (xRy : x R y) → Dec (IsS xRy)
69-
extract : ∀ {x y} → {xRy : x R y} → IsS xRy → x S y
70-
71-
module <-≤-Reasoning
72-
(P : Type ℓ)
73-
((posetstr (_≤_) isPoset) : PosetStr ℓ≤ P)
74-
((quosetstr (_<_) isQuoset) : QuosetStr ℓ< P)
75-
(<-≤-trans : ∀ x {y z} → x < y → y ≤ z → x < z)
76-
(≤-<-trans : ∀ x {y z} → x ≤ y → y < z → x < z) where
77-
78-
open IsPoset
79-
open IsQuoset
80-
open SubRelation
81-
82-
private
83-
variable
84-
x y z : P
85-
data _<≤≡_ : P → P → Type (ℓ-max ℓ (ℓ-max ℓ< ℓ≤)) where
86-
strict : x < y → x <≤≡ y
87-
nonstrict : x ≤ y → x <≤≡ y
88-
equal : x ≡ y → x <≤≡ y
89-
90-
sub : SubRelation _<≤≡_ ℓ< ℓ<
91-
sub ._S_ = _<_
92-
sub .IsS {x} {y} r with r
93-
... | strict x<y = x < y
94-
... | equal _ = ⊥*
95-
... | nonstrict _ = ⊥*
96-
sub .IsS? r with r
97-
... | strict x<y = yes x<y
98-
... | nonstrict _ = no λ ()
99-
... | equal _ = no λ ()
100-
sub .extract {xRy = strict _ } x<y = x<y
101-
102-
open SubRelation sub renaming (IsS? to Is<? ; extract to extract<)
103-
infix 1 begin_
104-
begin_ : (r : x <≤≡ y) → {True (Is<? r)} → x < y
105-
begin_ r {s} = extract< {xRy = r} (toWitness s)
28+
module Triple
29+
(P : Type ℓ)
30+
((posetstr (_≤_) isPoset ) : PosetStr ℓ≤ P)
31+
((quosetstr (_<_) isQuoset) : QuosetStr ℓ< P)
32+
where
33+
private variable
34+
x y : P
35+
36+
data _<≤≡_ : P → P → Type (ℓ-max ℓ (ℓ-max ℓ< ℓ≤)) where
37+
strict : x < y → x <≤≡ y
38+
nonstrict : x ≤ y → x <≤≡ y
39+
equal : x ≡ y → x <≤≡ y
40+
41+
Is< : ∀ {x y} → x <≤≡ y → Type ℓ<
42+
Is< {x} {y} (strict _) = x < y
43+
Is< (nonstrict _) = ⊥*
44+
Is< (equal _) = ⊥*
45+
46+
Is<? : (x<y : x <≤≡ y) → Dec(Is< x<y)
47+
Is<? (strict x<y) = yes x<y
48+
Is<? (nonstrict _) = no λ ()
49+
Is<? (equal _) = no λ ()
50+
51+
extract< : {xRy : x <≤≡ y} → Is< xRy → x < y
52+
extract< {xRy = strict _} x<y = x<y
53+
54+
module <-≤-StrictReasoning
55+
(P : Type ℓ)
56+
((posetstr (_≤_) isPoset ) : PosetStr ℓ≤ P)
57+
((quosetstr (_<_) isQuoset) : QuosetStr ℓ< P)
58+
(<-≤-trans : ∀ x {y z} → x < y → y ≤ z → x < z)
59+
(≤-<-trans : ∀ x {y z} → x ≤ y → y < z → x < z)
60+
where
61+
62+
open Triple P (posetstr (_≤_) isPoset) (quosetstr (_<_) isQuoset)
63+
64+
private variable
65+
x y z : P
66+
67+
infix 1 begin<_
68+
begin<_ : (r : x <≤≡ y) → {True (Is<? r)} → x < y
69+
begin<_ r {s} = extract< {xRy = r} (toWitness s)
10670

10771
-- Partial order syntax
10872
module ≤-syntax where
73+
open IsPoset
74+
10975
infixr 2 step-≤
11076
step-≤ : ∀ (x : P) → y <≤≡ z → x ≤ y → x <≤≡ z
111-
step-≤ x r x≤y with r
112-
... | strict y<z = strict (≤-<-trans x x≤y y<z)
113-
... | nonstrict y≤z = nonstrict (isPoset .is-trans x _ _ x≤y y≤z)
114-
... | equal y≡z = nonstrict (subst (x ≤_) y≡z x≤y)
77+
step-≤ x (strict y<z) x≤y = strict (≤-<-trans x x≤y y<z)
78+
step-≤ x (nonstrict y≤z) x≤y = nonstrict (isPoset .is-trans x _ _ x≤y y≤z)
79+
step-≤ x (equal y≡z) x≤y = nonstrict (subst (x ≤_) y≡z x≤y)
11580

11681
syntax step-≤ x yRz x≤y = x ≤⟨ x≤y ⟩ yRz
11782

11883
module <-syntax where
84+
open IsQuoset
85+
11986
infixr 2 step-<
12087
step-< : ∀ (x : P) → y <≤≡ z → x < y → x <≤≡ z
121-
step-< x r x<y with r
122-
... | strict y<z = strict (isQuoset .is-trans x _ _ x<y y<z)
123-
... | nonstrict y≤z = strict (<-≤-trans x x<y y≤z)
124-
... | equal y≡z = strict (subst (x <_) y≡z x<y)
88+
step-< x (strict y<z) x<y = strict (isQuoset .is-trans x _ _ x<y y<z)
89+
step-< x (nonstrict y≤z) x<y = strict (<-≤-trans x x<y y≤z)
90+
step-< x (equal y≡z) x<y = strict (subst (x <_) y≡z x<y)
12591

12692
syntax step-< x yRz x<y = x <⟨ x<y ⟩ yRz
12793

@@ -135,3 +101,133 @@ module <-≤-Reasoning
135101
infix 3 _◾
136102
_◾ : ∀ x → x <≤≡ x
137103
x ◾ = equal refl
104+
105+
106+
module <-≤-Reasoning
107+
(P : Type ℓ)
108+
((posetstr (_≤_) isPoset ) : PosetStr ℓ≤ P)
109+
((quosetstr (_<_) isQuoset) : QuosetStr ℓ< P)
110+
(<-≤-trans : ∀ x {y z} → x < y → y ≤ z → x < z)
111+
(≤-<-trans : ∀ x {y z} → x ≤ y → y < z → x < z)
112+
(<-≤-weaken : ∀ {x y} → x < y → x ≤ y)
113+
where
114+
115+
open <-≤-StrictReasoning P
116+
(posetstr (_≤_) isPoset) (quosetstr (_<_) isQuoset)
117+
<-≤-trans ≤-<-trans
118+
public
119+
120+
open Triple P (posetstr (_≤_) isPoset) (quosetstr (_<_) isQuoset)
121+
open IsPoset
122+
123+
infix 1 begin≤_
124+
begin≤_ : ∀ {x y} → (r : x <≤≡ y) → x ≤ y
125+
begin≤_ (strict x<y) = <-≤-weaken x<y
126+
begin≤_ (nonstrict x≤y) = x≤y
127+
begin≤_ (equal {x} x≡y) = subst (x ≤_) x≡y (isPoset .is-refl x)
128+
129+
-- Examples of usage:
130+
131+
module Examples (P : Type ℓ)
132+
((posetstr (_≤_) isPoset ) : PosetStr ℓ≤ P)
133+
((quosetstr (_<_) isQuoset) : QuosetStr ℓ< P)
134+
(<-≤-trans : ∀ x {y z} → x < y → y ≤ z → x < z)
135+
(≤-<-trans : ∀ x {y z} → x ≤ y → y < z → x < z)
136+
(<-≤-weaken : ∀ {x y} → x < y → x ≤ y)
137+
where
138+
139+
example< : ∀ x y z u v w α γ δ
140+
→ x < y
141+
→ y ≤ z
142+
→ z ≡ u
143+
→ u < v
144+
→ v ≤ w
145+
→ w ≡ α
146+
→ α ≡ γ
147+
→ γ ≡ δ
148+
→ x < δ
149+
example< x y z u v w α γ δ x<y y≤z z≡u u<v v≤w w≡α α≡γ γ≡δ = begin<
150+
x <⟨ x<y ⟩
151+
y ≤⟨ y≤z ⟩
152+
z ≡→≤⟨ z ≡⟨ z≡u ⟩
153+
u ≡⟨ sym z≡u ⟩
154+
z ≡[ i ]⟨ z≡u i ⟩
155+
u ∎ ⟩
156+
u <⟨ u<v ⟩
157+
v ≤⟨ v≤w ⟩
158+
w ≡→≤⟨
159+
w ≡⟨ w≡α ⟩
160+
α ≡⟨ α≡γ ⟩
161+
γ ≡[ i ]⟨ γ≡δ i ⟩
162+
δ ∎
163+
⟩
164+
δ ◾
165+
where
166+
open <-≤-StrictReasoning P
167+
(posetstr (_≤_) isPoset) (quosetstr (_<_) isQuoset)
168+
<-≤-trans ≤-<-trans
169+
170+
open <-syntax
171+
open ≤-syntax
172+
open ≡-syntax
173+
174+
open <-≤-Reasoning P
175+
(posetstr (_≤_) isPoset) (quosetstr (_<_) isQuoset)
176+
<-≤-trans ≤-<-trans <-≤-weaken
177+
178+
example≤ : ∀ x y z u v w α γ δ
179+
→ x < y
180+
→ y ≤ z
181+
→ z ≡ u
182+
→ u < v
183+
→ v ≤ w
184+
→ w ≡ α
185+
→ α ≡ γ
186+
→ γ ≡ δ
187+
→ x ≤ δ
188+
example≤ x y z u v w α γ δ x<y y≤z z≡u u<v v≤w w≡α α≡γ γ≡δ = begin≤
189+
x <⟨ x<y ⟩
190+
y ≤⟨ y≤z ⟩
191+
z ≡→≤⟨ z ≡⟨ z≡u ⟩
192+
u ≡⟨ sym z≡u ⟩
193+
z ≡[ i ]⟨ z≡u i ⟩
194+
u ∎ ⟩
195+
u <⟨ u<v ⟩
196+
v ≤⟨ v≤w ⟩
197+
w ≡→≤⟨
198+
w ≡⟨ w≡α ⟩
199+
α ≡⟨ α≡γ ⟩
200+
γ ≡[ i ]⟨ γ≡δ i ⟩
201+
δ ∎
202+
⟩
203+
δ ◾
204+
where
205+
open <-syntax
206+
open ≤-syntax
207+
open ≡-syntax
208+
209+
example≤' : ∀ y z u w α γ δ
210+
→ y ≤ z
211+
→ z ≡ u
212+
→ u ≤ w
213+
→ w ≡ α
214+
→ α ≡ γ
215+
→ γ ≡ δ
216+
→ y ≤ δ
217+
example≤' y z u w α γ δ y≤z z≡u u≤w w≡α α≡γ γ≡δ = begin≤
218+
y ≤⟨ y≤z ⟩
219+
z ≡→≤⟨ z ≡⟨ z≡u ⟩
220+
u ≡⟨ sym z≡u ⟩
221+
z ≡[ i ]⟨ z≡u i ⟩
222+
u ∎ ⟩
223+
u ≤⟨ u≤w ⟩
224+
w ≡→≤⟨
225+
w ≡⟨ w≡α ⟩
226+
α ≡⟨ α≡γ ⟩
227+
γ ≡[ i ]⟨ γ≡δ i ⟩
228+
δ ∎
229+
⟩
230+
δ ◾
231+
where
232+
open ≤-syntax
233+
open ≡-syntax

0 commit comments

Comments
 (0)