alternative to BCD subtyping
This commit is contained in:
Jeremy Siek
parent
b2ec029852
commit
ed1d572450
1 changed files with 438 additions and 0 deletions
438
extra/extra/Value.agda
Normal file
438
extra/extra/Value.agda
Normal file
|
|
@ -0,0 +1,438 @@
|
|||
open import Data.Nat using (ℕ; suc ; zero; _+_; _≤′_; _<′_; _<_; _≤_;
|
||||
z≤n; s≤s; ≤′-refl; ≤′-step; _≟_) renaming (_⊔_ to max)
|
||||
open import Data.Nat.Properties
|
||||
using (n≤0⇒n≡0; ≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; ≤-step; ⊔-mono-≤;
|
||||
+-mono-≤; +-mono-≤-<; +-mono-<-≤; +-comm; +-assoc; n≤1+n;
|
||||
≤-pred; m≤m+n; n≤m+n; ≤-reflexive; ≤′⇒≤; ≤⇒≤′; +-suc)
|
||||
open Data.Nat.Properties.≤-Reasoning using (begin_; _≤⟨_⟩_; _∎)
|
||||
open import Data.Bool using (Bool) renaming (_≟_ to _=?_)
|
||||
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Data.Empty using (⊥-elim) renaming (⊥ to Bot)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Maybe
|
||||
open import Data.List using (List ; _∷_ ; []; _++_)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary using (Dec; yes; no)
|
||||
open import Relation.Nullary.Negation using (contradiction)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
|
||||
open Relation.Binary.PropositionalEquality.≡-Reasoning renaming (begin_ to start_; _∎ to _□)
|
||||
|
||||
|
||||
module extra.Value where
|
||||
|
||||
data Base : Set where
|
||||
Nat : Base
|
||||
𝔹 : Base
|
||||
|
||||
data Prim : Set where
|
||||
base : Base → Prim
|
||||
_⇒_ : Base → Prim → Prim
|
||||
|
||||
base-rep : Base → Set
|
||||
base-rep Nat = ℕ
|
||||
base-rep 𝔹 = Bool
|
||||
|
||||
rep : Prim → Set
|
||||
rep (base b) = base-rep b
|
||||
rep (b ⇒ p) = base-rep b → rep p
|
||||
|
||||
base-eq? : (B : Base) → (B' : Base) → Dec (B ≡ B')
|
||||
base-eq? Nat Nat = yes refl
|
||||
base-eq? Nat 𝔹 = no (λ ())
|
||||
base-eq? 𝔹 Nat = no (λ ())
|
||||
base-eq? 𝔹 𝔹 = yes refl
|
||||
|
||||
base-rep-eq? : ∀{B} → (k : base-rep B) (k′ : base-rep B) → Dec (k ≡ k′)
|
||||
base-rep-eq? {Nat} k k′ = k ≟ k′
|
||||
base-rep-eq? {𝔹} k k′ = k =? k′
|
||||
|
||||
infixr 7 _↦_
|
||||
infixl 6 _⊔_
|
||||
|
||||
data Value : Set
|
||||
|
||||
data Value where
|
||||
⊥ : Value
|
||||
const : {b : Base} → base-rep b → Value
|
||||
_↦_ : Value → Value → Value
|
||||
_⊔_ : (u : Value) → (v : Value) → Value
|
||||
|
||||
infix 5 _∈_
|
||||
|
||||
_∈_ : Value → Value → Set
|
||||
u ∈ ⊥ = u ≡ ⊥
|
||||
u ∈ const {B} k = u ≡ const {B} k
|
||||
u ∈ v ↦ w = u ≡ v ↦ w
|
||||
u ∈ (v ⊔ w) = u ∈ v ⊎ u ∈ w
|
||||
|
||||
infix 5 _⊆_
|
||||
|
||||
_⊆_ : Value → Value → Set
|
||||
v ⊆ w = ∀{u} → u ∈ v → u ∈ w
|
||||
|
||||
|
||||
AllFun : (u : Value) → Set
|
||||
AllFun ⊥ = Bot
|
||||
AllFun (const x) = Bot
|
||||
AllFun (v ↦ w) = ⊤
|
||||
AllFun (u ⊔ v) = AllFun u × AllFun v
|
||||
|
||||
dom : (u : Value) → Value
|
||||
dom ⊥ = ⊥
|
||||
dom (const k) = ⊥
|
||||
dom (v ↦ w) = v
|
||||
dom (u ⊔ v) = dom u ⊔ dom v
|
||||
|
||||
cod : (u : Value) → Value
|
||||
cod ⊥ = ⊥
|
||||
cod (const k) = ⊥
|
||||
cod (v ↦ w) = w
|
||||
cod (u ⊔ v) = cod u ⊔ cod v
|
||||
|
||||
infix 4 _⊑_
|
||||
|
||||
data _⊑_ : Value → Value → Set where
|
||||
|
||||
⊑-⊥ : ∀ {v} → ⊥ ⊑ v
|
||||
|
||||
⊑-const : ∀ {B}{k} → const {B} k ⊑ const {B} k
|
||||
|
||||
⊑-conj-L : ∀ {u v w}
|
||||
→ v ⊑ u
|
||||
→ w ⊑ u
|
||||
-----------
|
||||
→ v ⊔ w ⊑ u
|
||||
|
||||
⊑-conj-R1 : ∀ {u v w}
|
||||
→ u ⊑ v
|
||||
------------------
|
||||
→ u ⊑ v ⊔ w
|
||||
|
||||
⊑-conj-R2 : ∀ {u v w}
|
||||
→ u ⊑ w
|
||||
-----------
|
||||
→ u ⊑ v ⊔ w
|
||||
|
||||
⊑-fun : ∀ {u u′ v w}
|
||||
→ u′ ⊆ u
|
||||
→ AllFun u′
|
||||
→ dom u′ ⊑ v
|
||||
→ w ⊑ cod u′
|
||||
-------------------
|
||||
→ v ↦ w ⊑ u
|
||||
|
||||
|
||||
⊑-refl : ∀{v} → v ⊑ v
|
||||
⊑-refl {⊥} = ⊑-⊥
|
||||
⊑-refl {const k} = ⊑-const
|
||||
⊑-refl {v ↦ w} = ⊑-fun{v ↦ w}{v ↦ w} (λ {u} z → z) tt (⊑-refl{v}) ⊑-refl
|
||||
⊑-refl {v₁ ⊔ v₂} = ⊑-conj-L (⊑-conj-R1 ⊑-refl) (⊑-conj-R2 ⊑-refl)
|
||||
|
||||
factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set
|
||||
factor u u′ v w = AllFun u′ × u′ ⊆ u × dom u′ ⊑ v × w ⊑ cod u′
|
||||
|
||||
|
||||
⊑-fun-inv : ∀{u₁ u₂ v w}
|
||||
→ u₁ ⊑ u₂
|
||||
→ v ↦ w ∈ u₁
|
||||
→ Σ[ u₃ ∈ Value ] factor u₂ u₃ v w
|
||||
⊑-fun-inv {.⊥} {u₂} {v} {w} ⊑-⊥ ()
|
||||
⊑-fun-inv {.(const _)} {.(const _)} {v} {w} ⊑-const ()
|
||||
⊑-fun-inv {u11 ⊔ u12} {u₂} {v} {w} (⊑-conj-L u₁⊑u₂ u₁⊑u₃) (inj₁ x) =
|
||||
⊑-fun-inv u₁⊑u₂ x
|
||||
⊑-fun-inv {u11 ⊔ u12} {u₂} {v} {w} (⊑-conj-L u₁⊑u₂ u₁⊑u₃) (inj₂ y) =
|
||||
⊑-fun-inv u₁⊑u₃ y
|
||||
⊑-fun-inv {u₁} {u21 ⊔ u22} {v} {w} (⊑-conj-R1 u₁⊑u₂) v↦w∈u₁
|
||||
with ⊑-fun-inv {u₁} {u21} {v} {w} u₁⊑u₂ v↦w∈u₁
|
||||
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u3⊆u₁ , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
|
||||
⟨ u₃ , ⟨ afu₃ , ⟨ (λ {x} x₁ → inj₁ (u3⊆u₁ x₁)) , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩
|
||||
⊑-fun-inv {u₁} {u21 ⊔ u22} {v} {w} (⊑-conj-R2 u₁⊑u₂) v↦w∈u₁
|
||||
with ⊑-fun-inv {u₁} {u22} {v} {w} u₁⊑u₂ v↦w∈u₁
|
||||
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u3⊆u₁ , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
|
||||
⟨ u₃ , ⟨ afu₃ , ⟨ (λ {x} x₁ → inj₂ (u3⊆u₁ x₁)) , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩
|
||||
⊑-fun-inv {u11 ↦ u21} {u₂} {v} {w} (⊑-fun{u′ = u′} u′⊆u₂ afu′ du′⊑u11 u21⊑cu′)
|
||||
refl =
|
||||
⟨ u′ , ⟨ afu′ , ⟨ u′⊆u₂ , ⟨ du′⊑u11 , u21⊑cu′ ⟩ ⟩ ⟩ ⟩
|
||||
|
||||
|
||||
sub-inv-trans : ∀{u′ u₂ u : Value}
|
||||
→ AllFun u′ → u′ ⊆ u
|
||||
→ (∀{v′ w′} → v′ ↦ w′ ∈ u′ → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′)
|
||||
---------------------------------------------------------------
|
||||
→ Σ[ u₃ ∈ Value ] factor u₂ u₃ (dom u′) (cod u′)
|
||||
sub-inv-trans {⊥} {u₂} {u} () u′⊆u IH
|
||||
sub-inv-trans {const k} {u₂} {u} () u′⊆u IH
|
||||
sub-inv-trans {u₁′ ↦ u₂′} {u₂} {u} fu′ u′⊆u IH = IH refl
|
||||
sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} ⟨ afu₁′ , afu₂′ ⟩ u′⊆u IH
|
||||
with sub-inv-trans {u₁′} {u₂} {u} afu₁′
|
||||
(λ {u₁} z → u′⊆u (inj₁ z)) (λ {v′} {w′} z → IH (inj₁ z))
|
||||
| sub-inv-trans {u₂′} {u₂} {u} afu₂′
|
||||
(λ {u₁} z → u′⊆u (inj₂ z)) (λ {v′} {w′} z → IH (inj₂ z))
|
||||
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u₃⊆ , ⟨ du₃⊑ , ⊑cu₃ ⟩ ⟩ ⟩ ⟩
|
||||
| ⟨ u₄ , ⟨ afu₄ , ⟨ u₄⊆ , ⟨ du₄⊑ , ⊑cu₄ ⟩ ⟩ ⟩ ⟩ =
|
||||
|
||||
⟨ (u₃ ⊔ u₄) , ⟨ ⟨ afu₃ , afu₄ ⟩ , ⟨ G , ⟨ H , I ⟩ ⟩ ⟩ ⟩
|
||||
where
|
||||
G : ∀ {u₁} → u₁ ∈ u₃ ⊎ u₁ ∈ u₄ → u₁ ∈ u₂
|
||||
G {u₁} (inj₁ x) = u₃⊆ x
|
||||
G {u₁} (inj₂ y) = u₄⊆ y
|
||||
|
||||
H : dom u₃ ⊔ dom u₄ ⊑ dom u₁′ ⊔ dom u₂′
|
||||
H = ⊑-conj-L (⊑-conj-R1 du₃⊑) (⊑-conj-R2 du₄⊑)
|
||||
|
||||
I : cod u₁′ ⊔ cod u₂′ ⊑ cod u₃ ⊔ cod u₄
|
||||
I = ⊑-conj-L (⊑-conj-R1 ⊑cu₃) (⊑-conj-R2 ⊑cu₄)
|
||||
|
||||
|
||||
⊔⊑R : ∀{B C A}
|
||||
→ B ⊔ C ⊑ A
|
||||
→ B ⊑ A
|
||||
⊔⊑R (⊑-conj-L B⊔C⊑A B⊔C⊑A₁) = B⊔C⊑A
|
||||
⊔⊑R (⊑-conj-R1 B⊔C⊑A) = ⊑-conj-R1 (⊔⊑R B⊔C⊑A)
|
||||
⊔⊑R (⊑-conj-R2 B⊔C⊑A) = ⊑-conj-R2 (⊔⊑R B⊔C⊑A)
|
||||
|
||||
⊔⊑L : ∀{B C A}
|
||||
→ B ⊔ C ⊑ A
|
||||
→ C ⊑ A
|
||||
⊔⊑L (⊑-conj-L B⊔C⊑A B⊔C⊑A₁) = B⊔C⊑A₁
|
||||
⊔⊑L (⊑-conj-R1 B⊔C⊑A) = ⊑-conj-R1 (⊔⊑L B⊔C⊑A)
|
||||
⊔⊑L (⊑-conj-R2 B⊔C⊑A) = ⊑-conj-R2 (⊔⊑L B⊔C⊑A)
|
||||
|
||||
|
||||
u∈v⊑w→u⊑w : ∀{B A C} → C ∈ B → B ⊑ A → C ⊑ A
|
||||
u∈v⊑w→u⊑w {⊥} C∈B B⊑A rewrite C∈B = B⊑A
|
||||
u∈v⊑w→u⊑w {const k} C∈B B⊑A rewrite C∈B = B⊑A
|
||||
u∈v⊑w→u⊑w {B₁ ↦ B₂} C∈B B⊑A rewrite C∈B = B⊑A
|
||||
u∈v⊑w→u⊑w {B₁ ⊔ B₂}{A}{C} (inj₁ C∈B₁) B⊑A = u∈v⊑w→u⊑w {B₁}{A}{C} C∈B₁ (⊔⊑R B⊑A)
|
||||
u∈v⊑w→u⊑w {B₁ ⊔ B₂}{A}{C} (inj₂ C∈B₂) B⊑A = u∈v⊑w→u⊑w {B₂}{A}{C} C∈B₂ (⊔⊑L B⊑A)
|
||||
|
||||
u⊆v⊑w→u⊑w : ∀{u v w} → u ⊆ v → v ⊑ w → u ⊑ w
|
||||
u⊆v⊑w→u⊑w {⊥} {v} {w} u⊆v v⊑w = ⊑-⊥
|
||||
u⊆v⊑w→u⊑w {const k} {v} {w} u⊆v v⊑w
|
||||
with u⊆v refl
|
||||
... | k∈v = u∈v⊑w→u⊑w k∈v v⊑w
|
||||
u⊆v⊑w→u⊑w {u₁ ↦ u₂} {v} {w} u⊆v v⊑w
|
||||
with u⊆v refl
|
||||
... | u₁↦u₂∈v = u∈v⊑w→u⊑w u₁↦u₂∈v v⊑w
|
||||
u⊆v⊑w→u⊑w {u₁ ⊔ u₂} {v} {w} u⊆v v⊑w =
|
||||
⊑-conj-L (u⊆v⊑w→u⊑w u₁⊆v v⊑w) (u⊆v⊑w→u⊑w u₂⊆v v⊑w)
|
||||
where
|
||||
u₁⊆v : u₁ ⊆ v
|
||||
u₁⊆v {u′} u′∈u₁ = u⊆v (inj₁ u′∈u₁)
|
||||
u₂⊆v : u₂ ⊆ v
|
||||
u₂⊆v {u′} u′∈u₂ = u⊆v (inj₂ u′∈u₂)
|
||||
|
||||
depth : (v : Value) → ℕ
|
||||
depth ⊥ = zero
|
||||
depth (const k) = zero
|
||||
depth (v ↦ w) = suc (max (depth v) (depth w))
|
||||
depth (v₁ ⊔ v₂) = max (depth v₁) (depth v₂)
|
||||
|
||||
size : (v : Value) → ℕ
|
||||
size ⊥ = zero
|
||||
size (const k) = zero
|
||||
size (v ↦ w) = suc (size v + size w)
|
||||
size (v₁ ⊔ v₂) = suc (size v₁ + size v₂)
|
||||
|
||||
∈→depth≤ : ∀{v u : Value} → u ∈ v → depth u ≤ depth v
|
||||
∈→depth≤ {⊥} {u} u∈v rewrite u∈v = _≤_.z≤n
|
||||
∈→depth≤ {const x} {u} u∈v rewrite u∈v = _≤_.z≤n
|
||||
∈→depth≤ {v ↦ w} {u} u∈v rewrite u∈v = ≤-refl
|
||||
∈→depth≤ {v₁ ⊔ v₂} {u} (inj₁ x) =
|
||||
≤-trans (∈→depth≤ {v₁} {u} x) (m≤m⊔n (depth v₁) (depth v₂))
|
||||
∈→depth≤ {v₁ ⊔ v₂} {u} (inj₂ y) =
|
||||
≤-trans (∈→depth≤ {v₂} {u} y) (n≤m⊔n (depth v₁) (depth v₂))
|
||||
|
||||
max-lub : ∀{x y z : ℕ} → x ≤ z → y ≤ z → max x y ≤ z
|
||||
max-lub {.0} {y} {z} _≤_.z≤n y≤z = y≤z
|
||||
max-lub {suc x} {.0} {suc z} (_≤_.s≤s x≤z) _≤_.z≤n = _≤_.s≤s x≤z
|
||||
max-lub {suc x} {suc y} {suc z} (_≤_.s≤s x≤z) (_≤_.s≤s y≤z) =
|
||||
let max-xy≤z = max-lub {x}{y}{z} x≤z y≤z in
|
||||
_≤_.s≤s max-xy≤z
|
||||
|
||||
⊔⊆-inv : ∀{u v w : Value}
|
||||
→ (u ⊔ v) ⊆ w
|
||||
---------------
|
||||
→ u ⊆ w × v ⊆ w
|
||||
⊔⊆-inv uvw = ⟨ (λ x → uvw (inj₁ x)) , (λ x → uvw (inj₂ x)) ⟩
|
||||
|
||||
⊆→depth≤ : ∀{u v : Value} → u ⊆ v → depth u ≤ depth v
|
||||
⊆→depth≤ {⊥} {v} u⊆v = _≤_.z≤n
|
||||
⊆→depth≤ {const x} {v} u⊆v = _≤_.z≤n
|
||||
⊆→depth≤ {u₁ ↦ u₂} {v} u⊆v = ∈→depth≤ (u⊆v refl)
|
||||
⊆→depth≤ {u₁ ⊔ u₂} {v} u⊆v
|
||||
with ⊔⊆-inv u⊆v
|
||||
... | ⟨ u₁⊆v , u₂⊆v ⟩ =
|
||||
let u₁≤v = ⊆→depth≤ u₁⊆v in
|
||||
let u₂≤v = ⊆→depth≤ u₂⊆v in
|
||||
max-lub u₁≤v u₂≤v
|
||||
|
||||
dom-depth-≤ : ∀{u : Value} → depth (dom u) ≤ depth u
|
||||
dom-depth-≤ {⊥} = _≤_.z≤n
|
||||
dom-depth-≤ {const k} = _≤_.z≤n
|
||||
dom-depth-≤ {v ↦ w} = ≤-step (m≤m⊔n (depth v) (depth w))
|
||||
dom-depth-≤ {u ⊔ v} =
|
||||
let ih1 = dom-depth-≤ {u} in
|
||||
let ih2 = dom-depth-≤ {v} in
|
||||
⊔-mono-≤ ih1 ih2
|
||||
|
||||
cod-depth-≤ : ∀{u : Value} → depth (cod u) ≤ depth u
|
||||
cod-depth-≤ {⊥} = _≤_.z≤n
|
||||
cod-depth-≤ {const k} = _≤_.z≤n
|
||||
cod-depth-≤ {v ↦ w} = ≤-step (n≤m⊔n (depth v) (depth w))
|
||||
cod-depth-≤ {u ⊔ v} =
|
||||
let ih1 = cod-depth-≤ {u} in
|
||||
let ih2 = cod-depth-≤ {v} in
|
||||
⊔-mono-≤ ih1 ih2
|
||||
|
||||
≤′-trans : ∀{x y z} → x ≤′ y → y ≤′ z → x ≤′ z
|
||||
≤′-trans x≤′y y≤′z = ≤⇒≤′ (≤-trans (≤′⇒≤ x≤′y) (≤′⇒≤ y≤′z))
|
||||
|
||||
data _<<_ : ℕ × ℕ → ℕ × ℕ → Set where
|
||||
fst : ∀{x x' y y'} → x <′ x' → ⟨ x , y ⟩ << ⟨ x' , y' ⟩
|
||||
snd : ∀{x x' y y'} → x ≤′ x' → y <′ y' → ⟨ x , y ⟩ << ⟨ x' , y' ⟩
|
||||
|
||||
<<-nat-wf : (P : ℕ → ℕ → Set) →
|
||||
(∀ x y → (∀ {x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → P x' y') → P x y) →
|
||||
∀ x y → P x y
|
||||
<<-nat-wf P ih x y = ih x y (help x y)
|
||||
where help : (x y : ℕ) → ∀{ x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → P x' y'
|
||||
help .(suc x') y {x'}{y'} (fst ≤′-refl) =
|
||||
ih x' y' (help x' y')
|
||||
help .(suc x) y {x'}{y'} (fst (≤′-step {x} q)) =
|
||||
help x y {x'}{y'} (fst q)
|
||||
help x .(suc y) {x'}{y} (snd x'≤x ≤′-refl) =
|
||||
let h : ∀ {x₁} {x₂} → (⟨ x₁ , x₂ ⟩ << ⟨ x , y ⟩) → P x₁ x₂
|
||||
h = help x y in
|
||||
ih x' y G
|
||||
where
|
||||
G : ∀ {x'' y'} → ⟨ x'' , y' ⟩ << ⟨ x' , y ⟩ → P x'' y'
|
||||
G {x''} {y'} (fst x''<x') =
|
||||
help x y (fst {y = y'}{y' = y} (≤′-trans x''<x' x'≤x))
|
||||
G {x''} {y'} (snd x''≤x' y'<y) =
|
||||
help x y {x''}{y'} (snd (≤′-trans x''≤x' x'≤x) y'<y)
|
||||
help x .(suc y) {x'}{y'} (snd x′≤x (≤′-step {y} q)) =
|
||||
help x y {x'}{y'} (snd x′≤x q)
|
||||
|
||||
|
||||
⊑-trans-P : ℕ → ℕ → Set
|
||||
⊑-trans-P d s = ∀{u v w} → d ≡ depth u + depth w → s ≡ size u + size v
|
||||
→ u ⊑ v → v ⊑ w → u ⊑ w
|
||||
|
||||
⊑-trans-rec : ∀ d s → ⊑-trans-P d s
|
||||
⊑-trans-rec = <<-nat-wf ⊑-trans-P helper
|
||||
where
|
||||
helper : ∀ x y
|
||||
→ (∀ {x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → ⊑-trans-P x' y')
|
||||
→ ⊑-trans-P x y
|
||||
helper d s IH {.⊥} {v} {w} d≡ s≡ ⊑-⊥ v⊑w = ⊑-⊥
|
||||
helper d s IH {.(const _)} {.(const _)} {w} d≡ s≡ ⊑-const v⊑w = v⊑w
|
||||
helper d s IH {u₁ ⊔ u₂} {v} {w} d≡ s≡ (⊑-conj-L u₁⊑v u₂⊑v) v⊑w
|
||||
rewrite d≡ | s≡ =
|
||||
let u₁⊑w = IH M1 {u₁}{v}{w} refl refl u₁⊑v v⊑w in
|
||||
let u₂⊑w = IH M2 {u₂}{v}{w} refl refl u₂⊑v v⊑w in
|
||||
⊑-conj-L u₁⊑w u₂⊑w
|
||||
where
|
||||
M1a = begin
|
||||
depth u₁ + depth w
|
||||
≤⟨ +-mono-≤ (m≤m⊔n (depth u₁) (depth u₂)) ≤-refl ⟩
|
||||
max (depth u₁) (depth u₂) + depth w
|
||||
∎
|
||||
M1b = begin
|
||||
suc (size u₁ + size v)
|
||||
≤⟨ s≤s (+-mono-≤ ≤-refl (n≤m+n (size u₂) (size v))) ⟩
|
||||
suc (size u₁ + (size u₂ + size v))
|
||||
≤⟨ s≤s (≤-reflexive (sym (+-assoc (size u₁) (size u₂) (size v)))) ⟩
|
||||
suc (size u₁ + size u₂ + size v)
|
||||
∎
|
||||
M1 : ⟨ depth u₁ + depth w , size u₁ + size v ⟩ <<
|
||||
⟨ max (depth u₁) (depth u₂) + depth w ,
|
||||
suc (size u₁ + size u₂ + size v) ⟩
|
||||
M1 = snd (≤⇒≤′ M1a) (≤⇒≤′ M1b)
|
||||
M2a = begin
|
||||
depth u₂ + depth w
|
||||
≤⟨ +-mono-≤ (n≤m⊔n (depth u₁) (depth u₂)) ≤-refl ⟩
|
||||
max (depth u₁) (depth u₂) + depth w
|
||||
∎
|
||||
M2b = begin
|
||||
suc (size u₂ + size v)
|
||||
≤⟨ s≤s (+-mono-≤ (n≤m+n (size u₁) (size u₂)) ≤-refl) ⟩
|
||||
suc ((size u₁ + size u₂) + size v)
|
||||
∎
|
||||
M2 : ⟨ depth u₂ + depth w , size u₂ + size v ⟩ <<
|
||||
⟨ max (depth u₁) (depth u₂) + depth w ,
|
||||
suc (size u₁ + size u₂ + size v) ⟩
|
||||
M2 = snd (≤⇒≤′ M2a) (≤⇒≤′ M2b)
|
||||
helper d s IH {u} {v₁ ⊔ v₂} {w} d≡ s≡ (⊑-conj-R1 u⊑v₁) v₁⊔v₂⊑w
|
||||
rewrite d≡ | s≡ =
|
||||
let v₁⊑w = ⊔⊑R v₁⊔v₂⊑w in
|
||||
IH M {u}{v₁}{w} refl refl u⊑v₁ v₁⊑w
|
||||
where
|
||||
Ma = begin
|
||||
suc (size u + size v₁)
|
||||
≤⟨ ≤-reflexive (sym (+-suc (size u) (size v₁))) ⟩
|
||||
size u + suc (size v₁)
|
||||
≤⟨ +-mono-≤ ≤-refl (s≤s (m≤m+n (size v₁) (size v₂))) ⟩
|
||||
size u + suc (size v₁ + size v₂)
|
||||
∎
|
||||
M : ⟨ depth u + depth w , size u + size v₁ ⟩ <<
|
||||
⟨ depth u + depth w , size u + suc (size v₁ + size v₂) ⟩
|
||||
M = snd (≤⇒≤′ ≤-refl) (≤⇒≤′ Ma)
|
||||
helper d s IH {u} {v₁ ⊔ v₂} {w} d≡ s≡ (⊑-conj-R2 u⊑v₂) v₁⊔v₂⊑w
|
||||
rewrite d≡ | s≡ =
|
||||
let v₂⊑w = ⊔⊑L v₁⊔v₂⊑w in
|
||||
IH M {u}{v₂}{w} refl refl u⊑v₂ v₂⊑w
|
||||
where
|
||||
Ma = begin
|
||||
suc (size u + size v₂)
|
||||
≤⟨ ≤-reflexive (sym (+-suc (size u) (size v₂))) ⟩
|
||||
size u + suc (size v₂)
|
||||
≤⟨ +-mono-≤ ≤-refl (s≤s (n≤m+n (size v₁) (size v₂))) ⟩
|
||||
size u + suc (size v₁ + size v₂)
|
||||
∎
|
||||
M : ⟨ depth u + depth w , size u + size v₂ ⟩ <<
|
||||
⟨ depth u + depth w , size u + suc (size v₁ + size v₂) ⟩
|
||||
M = snd (≤⇒≤′ ≤-refl) (≤⇒≤′ Ma)
|
||||
helper d s IH {u₁ ↦ u₂}{v}{w}d≡ s≡ (⊑-fun{u′ = v′}v′⊆v afv′ dv′⊑u₁ u₂⊑cv′) v⊑w
|
||||
rewrite d≡ | s≡
|
||||
with sub-inv-trans afv′ v′⊆v
|
||||
(λ {v₁}{v₂} v₁↦v₂∈v′ → ⊑-fun-inv {v′} {w} (u⊆v⊑w→u⊑w v′⊆v v⊑w)
|
||||
v₁↦v₂∈v′)
|
||||
... | ⟨ w′ , ⟨ afw′ , ⟨ w′⊆w , ⟨ dw′⊑dv′ , cv′⊑cw′ ⟩ ⟩ ⟩ ⟩ =
|
||||
let dw′⊑u₁ = IH M1 {dom w′}{dom v′}{u₁} refl refl dw′⊑dv′ dv′⊑u₁ in
|
||||
let u₂⊑cw′ = IH M2 {u₂}{cod v′}{cod w′} refl refl u₂⊑cv′ cv′⊑cw′ in
|
||||
⊑-fun{u′ = w′} w′⊆w afw′ dw′⊑u₁ u₂⊑cw′
|
||||
where
|
||||
dw′≤w : depth (dom w′) ≤ depth w
|
||||
dw′≤w = ≤-trans (dom-depth-≤{w′}) (⊆→depth≤ w′⊆w)
|
||||
cw′≤w : depth (cod w′) ≤ depth w
|
||||
cw′≤w = ≤-trans (cod-depth-≤{w′}) (⊆→depth≤ w′⊆w)
|
||||
|
||||
M1a = begin
|
||||
suc (depth (dom w′) + depth u₁)
|
||||
≤⟨ s≤s (≤-reflexive (+-comm (depth (dom w′)) (depth u₁))) ⟩
|
||||
suc (depth u₁ + depth (dom w′))
|
||||
≤⟨ s≤s (+-mono-≤ (m≤m⊔n (depth u₁) (depth u₂)) dw′≤w) ⟩
|
||||
suc (max (depth u₁) (depth u₂) + depth w)
|
||||
∎
|
||||
M1 : ⟨ depth (dom w′) + depth u₁ , size (dom w′) + size (dom v′) ⟩
|
||||
<< ⟨ suc (max (depth u₁) (depth u₂) + depth w) ,
|
||||
suc (size u₁ + size u₂ + size v) ⟩
|
||||
M1 = fst (≤⇒≤′ M1a)
|
||||
M2a = begin
|
||||
suc (depth u₂ + depth (cod w′))
|
||||
≤⟨ s≤s (+-mono-≤ (n≤m⊔n (depth u₁) (depth u₂)) cw′≤w) ⟩
|
||||
suc (max (depth u₁) (depth u₂) + depth w)
|
||||
∎
|
||||
M2 : ⟨ depth u₂ + depth (cod w′) ,
|
||||
size u₂ + size (cod v′) ⟩
|
||||
<< ⟨ suc (max (depth u₁) (depth u₂) + depth w) ,
|
||||
suc (size u₁ + size u₂ + size v) ⟩
|
||||
M2 = fst (≤⇒≤′ M2a)
|
||||
|
||||
|
||||
⊑-trans : ∀{u v w} → u ⊑ v → v ⊑ w → u ⊑ w
|
||||
⊑-trans {u} {v} {w} u⊑v v⊑w =
|
||||
⊑-trans-rec (depth u + depth w) (size u + size v) refl refl u⊑v v⊑w
|
||||
Loading…
Reference in a new issue