module Tree where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; s≤s; z≤n; _<_; _⊓_)
open import Data.Nat.Properties
-- don't use the library version of ≤-<-connex
-- use m≤n⇒m≤1+n instead of ≤-step
using (suc-injective; ≤-reflexive; ≤-refl; ≤-trans; <-irrefl; <⇒≤;
m≤n⇒m≤1+n; <-transˡ; <-transʳ;
≤∧≢⇒<; +-monoˡ-<; m≤m+n; m≤n+m; m≤n⇒m≤o+n; +-mono-≤;
m<n⇒m⊓o<n; m≤n⇒m⊓n≡m; ⊓-comm; -- ≤-total;
m⊓n≤m;
m<m+n; ≤-pred; +-monoˡ-≤)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_; Satisfiable)
open import Function using (_∘_; id)
open import Data.List using (List; []; _∷_; _++_; length; sum; _ʳ++_)
import Data.Fin as F
open F using (Fin; toℕ; fromℕ<)
open import Data.Fin.Properties using
(pigeonhole; toℕ-mono-<; toℕ<n; fromℕ<-toℕ; fromℕ<-cong; toℕ-fromℕ<;
toℕ-injective; fromℕ<-injective)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Properties using (just-injective)
open import Relation.Binary.Core using (_⇒_)
open import Miscellaneous
-- open import Classical
open import WQO
-- open import MinimalBadSeq
import Higman as H
open import Fin
private
variable
A : Set
n : ℕ
Trees with leaf labels in A and interior node labels in Fin n. A tree
with no interior node has size 1.
data Tree (A : Set) (n : ℕ) : Set where
leaf : (a : A) → Tree A n
node : (i : Fin n) → (ts : List (Tree A n)) → {Nonempty ts} → Tree A n
module _ {A : Set} {n : ℕ} where
size : Tree A n → ℕ
size-list : (List (Tree A n)) → ℕ
size (leaf a) = 1
size (node i ts) = suc (size-list ts)
size-list [] = zero
size-list (x ∷ ts) = size x + size-list ts
size≥1 : (t : Tree A n) → 1 ≤ size t
size≥1 (leaf a) = ≤-refl
size≥1 (node i ts) = s≤s z≤n
size-list≥1 : (ts : List (Tree A n)) → {Nonempty ts} → 1 ≤ size-list ts
size-list≥1 [] {()}
size-list≥1 (t ∷ ts) {ts≢[]} = ≤-trans (size≥1 t) (m≤m+n (size t) (size-list ts))
elem-size-≤ : {t : Tree A n} {ts : List (Tree A n)} → t elem ts → size t ≤ size-list ts
elem-size-≤ {t} {.t ∷ ts} here = m≤m+n (size t) (size-list ts)
elem-size-≤ {t} {u ∷ ts} (there h) = ≤-trans (elem-size-≤ h) (m≤n+m (size-list ts) (size u))
size≡1 : (t : Tree A n) → size t ≡ 1 → ∃[ a ] t ≡ leaf a
size≡1 (leaf a) h = a , refl
size≡1 (node i ts {ts≢[]}) h =
⊥-elim (¬1≤0 (≤-trans (size-list≥1 ts {ts≢[]}) (≤-reflexive (suc-injective h))))
where
¬1≤0 : ¬ (1 ≤ 0)
¬1≤0 ()
size>1 : (t : Tree A n)
→ 1 < size t
→ ∃₂ λ i ts → Σ[ ts≢[] ∈ Nonempty ts ] t ≡ node i ts {ts≢[]}
size>1 (leaf a) (s≤s ())
size>1 (node i (t ∷ ts)) h = i , (t ∷ ts) , tt , refl
-- size>1 (leaf a) h = ⊥-elim (<-irrefl refl h)
-- size>1 (node i ts {ts≢[]}) h = i , ts , ts≢[] , refl
size′ : Tree A n → ℕ
size-list′ : (List (Tree A n)) → ℕ
size′ (leaf a) = 1
size′ (node i ts) = suc (size-list′ ts)
size-list′ [] = 1 -- hack to avoid the failure of Agda's termination check
size-list′ (x ∷ ts) = size′ x + size-list′ ts
size′≥1 : (t : Tree A n) → 1 ≤ size′ t
size′≥1 (leaf a) = ≤-refl
size′≥1 (node i ts) = s≤s z≤n
size-list′≥1 : (ts : List (Tree A n)) → 1 ≤ size-list′ ts
size-list′≥1 [] = s≤s z≤n
size-list′≥1 (t ∷ ts) = ≤-trans (size′≥1 t) (m≤m+n (size′ t) (size-list′ ts))
elem-size′-< : {t : Tree A n} {ts : List (Tree A n)} → t elem ts → size′ t < size-list′ ts
elem-size′-< {t} {.t ∷ ts} here = m<m+n (size′ t) (size-list′≥1 ts)
elem-size′-< {t} {u ∷ ts} (there h) = <-transˡ (elem-size′-< {t} {ts} h) (m≤n+m (size-list′ ts) (size′ u))
elem-size′-≤ : {t : Tree A n} {ts : List (Tree A n)} → t elem ts → size′ t ≤ size-list′ ts
elem-size′-≤ h = <⇒≤ (elem-size′-< h)
head-size′-< : (t : Tree A n) (ts : List (Tree A n)) → size′ t < size-list′ (t ∷ ts)
head-size′-< t ts = elem-size′-< {t} {t ∷ ts} here
tail-size-list′-< : (t : Tree A n) (ts : List (Tree A n)) → size-list′ ts < size-list′ (t ∷ ts)
tail-size-list′-< t ts = +-monoˡ-≤ (size-list′ ts) (size′≥1 t)
The subtree relation. The use of elem makes inductive
proofs about the relation difficult. An alternative is to use an
auxiliary relation relating trees and lists of trees, but it is tiring
to always use mutual induction.
data _⊑_ : Tree A n → Tree A n → Set where
⊑-refl : {t : Tree A n} → t ⊑ t
⊑-step : {t u : Tree A n} (i : Fin n) (ts : List (Tree A n)) {ts≢[] : Nonempty ts}
→ t ⊑ u → u elem ts → t ⊑ node i ts {ts≢[]}
data _⊑′_ : Tree A n → Tree A n → Set
data _⊑′-any_ : Tree A n → List (Tree A n) → Set
data _⊑′_ where
⊑′-refl : {t : Tree A n} → t ⊑′ t
⊑′-step : {t : Tree A n} (i : Fin n) (us : List (Tree A n)) {us≢[] : Nonempty us}
→ t ⊑′-any us → t ⊑′ node i us {us≢[]}
data _⊑′-any_ where
here : {t u : Tree A n} {us : List (Tree A n)} → t ⊑′ u →
t ⊑′-any (u ∷ us)
there : {t u : Tree A n} {ts : List (Tree A n)} → t ⊑′-any ts →
t ⊑′-any (u ∷ ts)
⊑′-elem⇔⊑′-any : (t : Tree A n) (us : List (Tree A n)) →
(∃[ u ] (t ⊑′ u × u elem us)) ⇔ t ⊑′-any us
⊑′-elem⇔⊑′-any t us = ⟨⇒⟩ {us} , ⟨⇐⟩ {us}
where
⟨⇒⟩ : ∀ {us} → ∃[ u ] (t ⊑′ u × u elem us) → t ⊑′-any us
⟨⇒⟩ {u ∷ us} (u , t⊑′u , here) = here t⊑′u
⟨⇒⟩ {u₁ ∷ us} (u , t⊑′u , there h) = there (⟨⇒⟩ {us} (u , t⊑′u , h))
⟨⇐⟩ : ∀ {us} → t ⊑′-any us → ∃[ u ] (t ⊑′ u × u elem us)
⟨⇐⟩ {u₁ ∷ _} (here x) = u₁ , x , here
⟨⇐⟩ {_ ∷ us} (there h) with ⟨⇐⟩ {us} h
... | (u₂ , t⊑′u₂ , h₁) = u₂ , t⊑′u₂ , there h₁
⊑⇔⊑′ : (t u : Tree A n) → (t ⊑ u ⇔ t ⊑′ u)
⊑⇔⊑′ t u = ⟨⇒⟩ {u} (size u) ≤-refl , ⟨⇐⟩ {u} (size u) ≤-refl
where
⟨⇒⟩ : ∀ {u} (k : ℕ) → size u ≤ k → t ⊑ u → t ⊑′ u
⟨⇒⟩ {u} k size[u]≤k ⊑-refl = ⊑′-refl
⟨⇒⟩ {u} (suc k) (s≤s (size-list[ts]≤k)) (⊑-step {u = u₂} i ts t⊑u₂ x) =
⊑′-step i ts (proj₁ (⊑′-elem⇔⊑′-any t ts) (u₂ , t⊑′u₂ , x))
where
size[u₂]≤k : size u₂ ≤ k
size[u₂]≤k = ≤-trans (elem-size-≤ x) size-list[ts]≤k
t⊑′u₂ : t ⊑′ u₂
t⊑′u₂ = ⟨⇒⟩ {u₂} k size[u₂]≤k t⊑u₂
⟨⇐⟩ : ∀ {u} (k : ℕ) → size u ≤ k → t ⊑′ u → t ⊑ u
⟨⇐⟩ {u} k size[u]≤k ⊑′-refl = ⊑-refl
⟨⇐⟩ {.(node i us)} (suc k) (s≤s size-list[us]≤k) (⊑′-step i us x)
with proj₂ (⊑′-elem⇔⊑′-any t us) x
... | u₁ , t⊑′u₁ , h = ⊑-step i us t⊑u₁ h
where
size[u₁]≤k : size u₁ ≤ k
size[u₁]≤k = ≤-trans (elem-size-≤ h) size-list[us]≤k
t⊑u₁ : t ⊑ u₁
t⊑u₁ = ⟨⇐⟩ {u₁} k size[u₁]≤k t⊑′u₁
⊑-transitive : Transitive _⊑_
⊑-transitive {x = x} {y = y} {z = .y} x⊑y ⊑-refl = x⊑y
⊑-transitive {x = x} {y = y} {z = .(node i ts)} x⊑y (⊑-step i ts y⊑u h) =
⊑-step i ts (⊑-transitive x⊑y y⊑u) h
⊑-size-≤ : {t u : Tree A n} → t ⊑ u → size t ≤ size u
⊑-size-≤ ⊑-refl = ≤-refl
⊑-size-≤ (⊑-step {u = u} i ts h h₁) = -- ≤-step (≤-trans (⊑-size-≤ h) (elem-size-≤ h₁))
m≤n⇒m≤1+n (≤-trans (⊑-size-≤ h) (elem-size-≤ h₁))
⊑-size-≡ : {t u : Tree A n} → t ⊑ u → size t ≡ size u → t ≡ u
⊑-size-≡ {t = t} {u = .t} ⊑-refl _ = refl
⊑-size-≡ {t = t} {u = .(node i ts)} (⊑-step {u = u} i ts t⊑u h) h₁ =
⊥-elim (<-irrefl refl [1])
where
[1] : size-list ts < size-list ts
[1] rewrite sym h₁ = ≤-trans (⊑-size-≤ t⊑u) (elem-size-≤ h)
data IsLeaf (a : A) : Tree A n → Set where
here : IsLeaf a (leaf a)
there : {i : Fin n} {ts : List (Tree A n)} {t : Tree A n}
(h : t elem ts) →
IsLeaf a t →
IsLeaf a (node i ts {elem-nonempty h})
isLeaf-nonempty : (t : Tree A n) → Satisfiable (λ a → IsLeaf a t)
isLeaf-nonempty (leaf a) = a , here
isLeaf-nonempty (node i (t ∷ ts)) with isLeaf-nonempty t
... | a , h = a , there here h
⊑-IsLeaf-⊆ : {t u : Tree A n} → t ⊑ u → {a : A} → IsLeaf a t → IsLeaf a u
⊑-IsLeaf-⊆ ⊑-refl h = h
⊑-IsLeaf-⊆ (⊑-step i (t ∷ ts) t⊑u h₁) h = there h₁ (⊑-IsLeaf-⊆ t⊑u h)
isLeaf-leaf : {a b : A} → IsLeaf a (leaf b) → a ≡ b
isLeaf-leaf here = refl
isLeaf-node : {a : A} {i : Fin n} {ts : List (Tree A n)}
{ts≢[] : Nonempty ts} → IsLeaf a (node i ts {ts≢[]}) →
∃[ t ] t elem ts × IsLeaf a t
isLeaf-node (there {t = t} h x) = t , h , x
_⊏_ : Tree A n → Tree A n → Set
t ⊏ u = t ⊑ u × t ≢ u
immediate-subtree-⊏ : (i : Fin n) (ts : List (Tree A n)) {ts≢[] : Nonempty ts}
(t : Tree A n) (h : t elem ts) →
t ⊏ node i ts {ts≢[]}
immediate-subtree-⊏ i ts t h =
⊑-step i ts ⊑-refl h , λ {eq → <-irrefl (cong size eq) (s≤s (elem-size-≤ h))}
⊏-size-< : {t u : Tree A n} → t ⊏ u → size t < size u
⊏-size-< t⊏u =
≤∧≢⇒< (⊑-size-≤ (proj₁ t⊏u)) (λ h → ⊥-elim (proj₂ t⊏u (⊑-size-≡ (proj₁ t⊏u) h)))
⊏-⊑-⊏ : {t u v : Tree A n} → t ⊏ u → u ⊑ v → t ⊏ v
⊏-⊑-⊏ {t} {u} {v} t⊏u@(t⊑u , t≢u) u⊑v =
⊑-transitive t⊑u u⊑v , (λ {refl → <-irrefl refl [1]})
where
[1] : size t < size v
[1] = <-transˡ (⊏-size-< t⊏u) (⊑-size-≤ u⊑v)
⊑-⊏-⊏ : {t u v : Tree A n} → t ⊑ u → u ⊏ v → t ⊏ v
⊑-⊏-⊏ {t} {u} {v} t⊑u u⊏v@(u⊑v , u≢v) =
⊑-transitive t⊑u u⊑v , (λ {refl → <-irrefl refl [1]})
where
[1] : size t < size v
[1] = <-transʳ (⊑-size-≤ t⊑u) (⊏-size-< u⊏v)
head : Tree A n → Maybe (Fin n) head (leaf a) = nothing head (node i _) = just iIf t is a tree, μ t is the minimal interior node label in t (if there is one).
module _ {A : Set} {n : ℕ} where
μ : Tree A n → Maybe (Fin n)
μ-list : List (Tree A n) → Maybe (Fin n)
μ (leaf a) = nothing
μ (node i ts) = just i ⊓′ μ-list ts
-- μ (node i ts) with μ-list ts
-- ... | just j = case-⊎ (λ _ → just i) (λ _ → just j) (≤-<-connex (toℕ i) (toℕ j))
-- ... | nothing = just i
μ-list [] = nothing
μ-list (t ∷ ts) = μ t ⊓′ μ-list ts
-- μ-list (t ∷ ts) with μ t | μ-list ts
-- ... | just j | just k = case-⊎ (λ _ → just j) (λ _ → just k) (≤-<-connex (toℕ j) (toℕ k))
-- ... | just j | nothing = just j
-- ... | nothing | x = x
This definition of μ is rather hard to reason with. We state many
obvious properties of the function.
μ-node-≤ : (ts : List (Tree A n)) (m i : Fin n) {ts≢[] : Nonempty ts}
→ μ-list ts ≡ just m
→ toℕ i ≤ toℕ m
→ μ (node i ts {ts≢[]}) ≡ just i
μ-node-≤ ts m i h i≤m rewrite h = ≤-⊓′ i≤m
-- μ-node-≤ x m i h i≤m rewrite h | ≤-<-connex-≤ (toℕ i) (toℕ m) i≤m = refl
μ-node-> : (ts : List (Tree A n)) (m i : Fin n) {ts≢[] : Nonempty ts}
→ μ-list ts ≡ just m
→ toℕ m < toℕ i
→ μ (node i ts {ts≢[]}) ≡ just m
μ-node-> x m i h i>m rewrite h = ≥-⊓′ (<⇒≤ i>m)
-- μ-node-> x m i h i>m rewrite h | ≤-<-connex-> (toℕ i) (toℕ m) i>m = refl
μ-node-nothing : (ts : List (Tree A n)) (i : Fin n) {ts≢[] : Nonempty ts}
→ μ-list ts ≡ nothing
→ μ (node i ts {ts≢[]}) ≡ just i
μ-node-nothing ts i h rewrite h = refl
-- μ-node-nothing ts i h with μ-list ts
-- ... | nothing = refl
μ-node : (i : Fin n) (ts : List (Tree A n)) {ts≢[] : Nonempty ts}
→ Σ[ m ∈ Fin n ] μ (node i ts {ts≢[]}) ≡ just m
μ-node i ts with μ-list ts
... | just j = k , refl
where
k = (fromℕ< (m<n⇒m⊓o<n (toℕ j) (toℕ<n i)))
... | nothing = i , refl
-- μ-node i ts with μ-list ts
-- μ-node i ts | just m₁ with ≤-<-connex (toℕ i) (toℕ m₁)
-- ... | inj₁ i≤m₁ = i , refl
-- ... | inj₂ i>m₁ = m₁ , refl
-- μ-node i ts | nothing = i , refl
μ-nothing : (t : Tree A n) → μ t ≡ nothing → ∃[ a ] t ≡ leaf a
μ-nothing (leaf a) refl = a , refl
μ-nothing (node i ts {ts≢[]}) h with μ-node i ts {ts≢[]}
... | m , eq = ⊥-elim (just≢nothing (trans (sym eq) h))
μ-just : (t : Tree A n) (m : Fin n)
→ μ t ≡ just m
→ Σ[ i ∈ Fin n ] Σ[ ts ∈ List (Tree A n) ] Σ[ ts≢[] ∈ Nonempty ts ]
t ≡ node i ts {ts≢[]}
μ-just (node i (t ∷ ts)) m h = i , (t ∷ ts) , tt , refl
μ-just′ : (t : Tree A n) (m : Fin n) →
μ t ≡ just m →
Σ[ i ∈ Fin n ] Σ[ t₁ ∈ Tree A n ] Σ[ ts ∈ List (Tree A n) ]
t ≡ node i (t₁ ∷ ts)
μ-just′ (node i (t₁ ∷ ts)) m h = i , t₁ , ts , refl
μ-≤-μ-list : (i m : Fin n) (ts : List (Tree A n)) {ts≢[] : Nonempty ts}
→ μ-list ts ≡ just m
→ μ (node i ts {ts≢[]}) ≤′ just m
μ-≤-μ-list i m ts h rewrite h = ⊓′-≤′₂ i m
-- μ-≤-μ-list i m (t ∷ ts) h with μ-list (t ∷ ts)
-- μ-≤-μ-list i .m₁ (t ∷ ts) refl | just m₁ with ≤-<-connex (toℕ i) (toℕ m₁)
-- ... | inj₁ i≤m₁ = i≤m₁
-- ... | inj₂ i>m₁ = ≤-refl
μ-≤-head : {i : Fin n} {ts : List (Tree A n)} {ts≢[] : Nonempty ts}
→ μ (node i ts {ts≢[]}) ≤′ just i
μ-≤-head {i} {t ∷ ts} with μ-list (t ∷ ts)
... | nothing = ≤-refl
... | just m = ⊓′-≤′₁ i m
-- ... | just m with ≤-<-connex (toℕ i) (toℕ m)
-- ... | inj₁ i≤m = ≤-refl
-- ... | inj₂ i>m = <⇒≤ i>m
μ-list-just-nonempty : {i : Fin n} {ts : List (Tree A n)} →
μ-list ts ≡ just i → Nonempty ts
μ-list-just-nonempty {ts = t ∷ ts} eq = tt
elem-μ-list-just : {u : Tree A n} {ts : List (Tree A n)} {m : Fin n} →
μ u ≡ just m → u elem ts → ∃[ k ] μ-list ts ≡ just k
elem-μ-list-just {u} {[]} h ()
elem-μ-list-just {.t} {t ∷ ts} {m} h here with μ-list ts
... | nothing rewrite h = m , refl
... | just j rewrite h with ⊓′-⊓ m j
... | k , eq₁ , eq₂ = k , eq₁
elem-μ-list-just {u} {t ∷ ts} {m} h (there h₁) with elem-μ-list-just {u} {ts} {m} h h₁
... | k , eq with μ t
... | nothing rewrite eq = k , refl
... | just j rewrite eq with ⊓′-⊓ j k
... | i , eq₁ , eq₂ = i , eq₁
elem-μ-list-≤-μ : {u : Tree A n} {ts : List (Tree A n)} {m : Fin n} →
μ u ≡ just m → u elem ts → μ-list ts ≤′ just m
elem-μ-list-≤-μ {u} {[]} h ()
elem-μ-list-≤-μ {.t} {t ∷ ts} h here with μ t | μ-list ts
... | just j | just k = subst ((just j ⊓′ just k) ≤′_) h (⊓′-≤′₁ j k)
... | just j | nothing rewrite just-injective h = ≤-refl
elem-μ-list-≤-μ {u} {t ∷ ts} {m} h (there h₁) with μ t in eq₁ | μ-list ts in eq₂
... | nothing | just k = subst (_≤′ just m) eq₂ (elem-μ-list-≤-μ {u} {ts} h h₁)
... | nothing | nothing = tt
... | just j | just k = ≤′-trans (⊓′-≤′₂ j k) [1]
where
[1] : just k ≤′ just m
[1] = subst (_≤′ just m) eq₂ (elem-μ-list-≤-μ {u} {ts} {m} h h₁)
... | just j | nothing with elem-μ-list-just {u} {ts} {m} h h₁
... | k , eq₃ = ⊥-elim (just≢nothing (trans (sym eq₃) eq₂))
Friedman’s tree embedding relation with a “gap” condition. There are two variants of the condition. The variant without the “+” requires that all nodes between two matched nodes in the embedding tree have labels that are not smaller than the label of the lower of the matched nodes. In addition, the variant with the “+” requires that all nodes above the highest matched node have labels that are not smaller than the label of that node. The two embedding relations are defined inductively.
Again, the use of elem in the constructor
pass makes inductive proofs about the relation difficult.
It might be better to define another predicate
Embedding-gap⁺-any, which means the same things as
Any (Embedding-gap⁺ x) ys, and redefine pass as
pass : {t u : Tree An n} {us : List (Tree A n)} {us≢[] : Nonempty us}
{j : Fin n} → (h : head t ≤' just j) →
Embedding-gap⁺-any : t us →
Embedding-gap⁺ t (node j us {js≢[]})module _ {A : Set} {n : ℕ} (_≼_ : A → A → Set) where
data Embedding-gap⁺ : Tree A n → Tree A n → Set
data Embedding-gap⁺-list : List (Tree A n) → List (Tree A n) → Set
data Embedding-gap⁺ where
leaf : ∀ {a b} (h : a ≼ b) → Embedding-gap⁺ (leaf a) (leaf b)
pass : {t u : Tree A n} {us : List (Tree A n)} {us≢[] : Nonempty us} {j : Fin n} →
(h : head t ≤′ just j) →
Embedding-gap⁺ t u →
u elem us →
Embedding-gap⁺ t (node j us {us≢[]})
match : {ts us : List (Tree A n)} {ts≢[] : Nonempty ts} {us≢[] : Nonempty us}
(i : Fin n) →
(h : Embedding-gap⁺-list ts us) →
Embedding-gap⁺ (node i ts {ts≢[]}) (node i us {us≢[]})
data Embedding-gap⁺-list where
[] : Embedding-gap⁺-list [] []
_∷ʳ_ : ∀ {ts us} → ∀ u → Embedding-gap⁺-list ts us →
Embedding-gap⁺-list ts (u ∷ us)
_∷_ : ∀ {t ts u us} →
Embedding-gap⁺ t u →
Embedding-gap⁺-list ts us →
Embedding-gap⁺-list (t ∷ ts) (u ∷ us)
Embedding-gap⁺-list is just the Higman embedding relation between lists of trees with Embedding-gap⁺ as ≼.
embedding-gap⁺-Higman : (ts us : List (Tree A n)) →
Embedding-gap⁺-list ts us ⇔ H.Embedding (Embedding-gap⁺) ts us
embedding-gap⁺-Higman ts us = ⟨⇒⟩ {ts} {us} , ⟨⇐⟩ {ts} {us}
where
⟨⇒⟩ : {ts us : List (Tree A n)} →
Embedding-gap⁺-list ts us → H.Embedding Embedding-gap⁺ ts us
⟨⇒⟩ [] = H.[]
⟨⇒⟩ (u ∷ʳ h) = u H.∷ʳ ⟨⇒⟩ h
⟨⇒⟩ (h₁ ∷ h) = h₁ H.∷ ⟨⇒⟩ h
⟨⇐⟩ : {ts us : List (Tree A n)} →
H.Embedding Embedding-gap⁺ ts us → Embedding-gap⁺-list ts us
⟨⇐⟩ H.[] = []
⟨⇐⟩ (y H.∷ʳ h) = y ∷ʳ ⟨⇐⟩ h
⟨⇐⟩ (x H.∷ h) = x ∷ ⟨⇐⟩ h
elem-embedding-gap⁺-list : ∀ {t ts us} → t elem ts → Embedding-gap⁺-list ts us →
∃[ u ] u elem us × Embedding-gap⁺ t u
elem-embedding-gap⁺-list {t} {ts} {us} h h₁ =
H.elem-embedding Embedding-gap⁺ h (proj₁ (embedding-gap⁺-Higman ts us) h₁)
embedding-gap⁺-list-[] : ∀ us → Embedding-gap⁺-list [] us
embedding-gap⁺-list-[] [] = []
embedding-gap⁺-list-[] (u ∷ us) = u ∷ʳ (embedding-gap⁺-list-[] us)
It takes some effort to prove the “+” version is transitive.
emb-gap⁺-head : {t u : Tree A n} → (h : Embedding-gap⁺ t u) →
head t ≤′ head u
emb-gap⁺-head (leaf _) = tt
emb-gap⁺-head (pass h _ _) = h
emb-gap⁺-head (match _ _) = ≤-refl
emb-gap⁺-transitive : (h : Transitive _≼_) {t u v : Tree A n} →
(h₁ : Embedding-gap⁺ t u) →
(h₂ : Embedding-gap⁺ u v) →
Embedding-gap⁺ t v
emb-gap⁺-list-transitive : (h : Transitive _≼_) {ts us vs : List (Tree A n)} →
(h₁ : Embedding-gap⁺-list ts us) →
(h₂ : Embedding-gap⁺-list us vs) →
Embedding-gap⁺-list ts vs
emb-gap⁺-transitive h (leaf h₁) (leaf h₂) = leaf (h h₁ h₂)
emb-gap⁺-transitive h (leaf h₁) (pass h₂ h₃ x) =
pass tt (emb-gap⁺-transitive h (leaf h₁) h₃) x
emb-gap⁺-transitive h h′@(pass _ _ _) (pass h₁ h₂ x) =
pass (≤′-trans (emb-gap⁺-head h′) h₁) (emb-gap⁺-transitive h h′ h₂) x
emb-gap⁺-transitive h (pass {us = us} h₁ h₂ x) (match {us = vs} _ h₃)
with elem-embedding-gap⁺-list x h₃
... | v , h₄ , h₅ = pass h₁ (emb-gap⁺-transitive h h₂ h₅) h₄
emb-gap⁺-transitive h h′@(match _ _) (pass h₁ h₂ x) =
pass (≤′-trans (emb-gap⁺-head h′) h₁) (emb-gap⁺-transitive h h′ h₂) x
emb-gap⁺-transitive h (match i h₁) (match .i h₂) =
match i (emb-gap⁺-list-transitive h h₁ h₂)
emb-gap⁺-list-transitive h h₁ [] = h₁
emb-gap⁺-list-transitive h h₁ (u₁ ∷ʳ h₂) =
u₁ ∷ʳ emb-gap⁺-list-transitive h h₁ h₂
emb-gap⁺-list-transitive h (u ∷ʳ h₁) (x ∷ h₂) =
_ ∷ʳ emb-gap⁺-list-transitive h h₁ h₂
emb-gap⁺-list-transitive h (x₁ ∷ h₁) (x ∷ h₂) =
emb-gap⁺-transitive h x₁ x ∷ emb-gap⁺-list-transitive h h₁ h₂
emb-gap⁺-reflexive : Reflexive _≼_ → Reflexive Embedding-gap⁺
emb-gap⁺-list-reflexive : Reflexive _≼_ → Reflexive Embedding-gap⁺-list
emb-gap⁺-reflexive h {leaf a} = leaf h
emb-gap⁺-reflexive h {node i ts {ts≢[]}} =
match i (emb-gap⁺-list-reflexive h {ts})
emb-gap⁺-list-reflexive h {[]} = []
emb-gap⁺-list-reflexive h {t ∷ ts} =
emb-gap⁺-reflexive h {t} ∷ emb-gap⁺-list-reflexive h {ts}
emb-gap⁺-isQO : IsQO {A = A} _≼_ → IsQO {A = Tree A n} Embedding-gap⁺
emb-gap⁺-isQO h = record
{ reflexive = emb-gap⁺-reflexive (IsQO.reflexive h)
; transitive = emb-gap⁺-transitive (IsQO.transitive h)
}
emb-gap⁺-size : {t u : Tree A n} → Embedding-gap⁺ t u → size t ≤ size u
emb-gap⁺-list-size : {ts us : List (Tree A n)} →
Embedding-gap⁺-list ts us →
size-list ts ≤ size-list us
emb-gap⁺-size {t} {u} (leaf _) = s≤s z≤n
emb-gap⁺-size {t} {node i us {us≢[]}} (pass h h₁ x) =
m≤n⇒m≤1+n (≤-trans (emb-gap⁺-size h₁) (elem-size-≤ x))
emb-gap⁺-size {.(node i _)} {.(node i _)} (match i h) =
s≤s (emb-gap⁺-list-size h)
emb-gap⁺-list-size {ts} {us} [] = z≤n
emb-gap⁺-list-size {ts} {u ∷ us} (u ∷ʳ h) =
m≤n⇒m≤o+n (size u) (emb-gap⁺-list-size h)
emb-gap⁺-list-size {t ∷ ts} {u ∷ us} (x ∷ h) =
+-mono-≤ (emb-gap⁺-size x) (emb-gap⁺-list-size h)
The version without the “+”.
data Embedding-gap : Tree A n → Tree A n → Set where
mk : {t u : Tree A n} → (h : Embedding-gap⁺ t u) → Embedding-gap t u
pass : {t u : Tree A n} {us : List (Tree A n)} {us≢[] : Nonempty us} (j : Fin n) →
Embedding-gap t u →
u elem us →
Embedding-gap t (node j us {us≢[]})
emb-gap-isQO : IsQO {A = A} _≼_ → IsQO {A = Tree A n} Embedding-gap
emb-gap-isQO h = record
{ reflexive = emb-gap-reflexive
; transitive = emb-gap-transitive
}
where
≼-transitive : Transitive _≼_
≼-transitive = IsQO.transitive h
emb-gap-reflexive : Reflexive Embedding-gap
emb-gap-reflexive = mk (IsQO.reflexive (emb-gap⁺-isQO h))
emb-gap-emb-gap⁺-emb-gap : ∀ {t u v} → Embedding-gap t u → Embedding-gap⁺ u v →
Embedding-gap t v
emb-gap-emb-gap⁺-emb-gap (mk tu) uv =
mk (emb-gap⁺-transitive ≼-transitive tu uv)
emb-gap-emb-gap⁺-emb-gap {t} {node j us {us≢[]}} {node k vs {vs≢[]}}
tu@(pass j _ _) (pass j≤k uv vvs) =
pass k (emb-gap-emb-gap⁺-emb-gap tu uv) vvs
emb-gap-emb-gap⁺-emb-gap {t} {node j us {us≢[]}} {node .j vs {vs≢[]}}
(pass j tu uus) (match .j usvs)
with elem-embedding-gap⁺-list uus usvs
... | v , vvs , uv = pass j (emb-gap-emb-gap⁺-emb-gap tu uv) vvs
emb-gap-transitive : Transitive Embedding-gap
emb-gap-transitive {t} {u} {v} tu (mk uv) = emb-gap-emb-gap⁺-emb-gap tu uv
emb-gap-transitive {t} {u} {node k vs} tu@(mk h) (pass k uv x) =
pass k (emb-gap-transitive tu uv) x
emb-gap-transitive {t} {node j us} {node k vs} tu@(pass _ _ _) (pass k uv x) =
pass k (emb-gap-transitive tu uv) x
emb-gap-size : {t u : Tree A n} → (h : Embedding-gap t u) → size t ≤ size u
emb-gap-size {t} {u} (mk h) = emb-gap⁺-size h
emb-gap-size {t} {node .j us} (pass j tu uus) =
m≤n⇒m≤1+n (≤-trans (emb-gap-size tu) (elem-size-≤ uus))
emb-gap-⊑-emb-gap : {t u v : Tree A n} (h : Embedding-gap t u) → u ⊑ v →
Embedding-gap t v
emb-gap-⊑-emb-gap {t} {u} {v} h ⊑-refl = h
emb-gap-⊑-emb-gap {t} {u} {node k vs} h (⊑-step i vs u⊑v vvs) =
pass k (emb-gap-⊑-emb-gap h u⊑v) vvs
emb-gap-μ-emb-gap⁺ :
{t u : Tree A n} (h₁ : head t ≤′ μ u) (h₂ : Embedding-gap t u) →
Embedding-gap⁺ t u
emb-gap-μ-emb-gap⁺ {t} {u} h₁ (mk h₂) = h₂
emb-gap-μ-emb-gap⁺ {t} {node .j us {us≢[]}} h₁ (pass {u = u} j tu uus) =
pass [1] (emb-gap-μ-emb-gap⁺ [2] tu) uus
where
[1] : head t ≤′ just j
[1] = ≤′-trans h₁ (μ-≤-head {A = A} {n = n} {j} {us} {us≢[]})
[2] : head t ≤′ μ u
[2] with head t in eq₁ | μ u in eq₂
... | nothing | just k = tt
... | nothing | nothing = tt
... | just i | nothing = ⊥-elim (just≢nothing [8])
where
[3] : ∃[ a ] u ≡ leaf a
[3] = μ-nothing u eq₂
a = proj₁ [3]
[4] : u ≡ leaf a
[4] = proj₂ [3]
[5] : (v : Tree A n) → Embedding-gap v (leaf a) → ∃[ b ] v ≡ leaf b
[5] (leaf b) (mk (leaf h)) = b , refl
[6] : ∃[ b ] t ≡ leaf b
[6] rewrite [4] = [5] t tu
[7] : head t ≡ nothing
[7] rewrite proj₂ [6] = refl
[8] : just i ≡ nothing
[8] = trans (sym eq₁) [7]
... | just i | just k = [14]
where
[9] : ∃[ m ] μ-list us ≡ just m
[9] = elem-μ-list-just eq₂ uus
m = proj₁ [9]
[10] : μ (node j us {us≢[]}) ≡ just j ⊓′ just m
[10] rewrite proj₂ [9] = refl
[11] : just i ≤′ (just j ⊓′ just m)
[11] = ≤′-trans h₁ (≤′-reflexive [10])
[12] : just i ≤′ just m
[12] = ≤′-trans [11] (⊓′-≤′₂ j m)
[13] : just m ≤′ just k
[13] = subst (_≤′ just k) (proj₂ [9]) (elem-μ-list-≤-μ eq₂ uus)
[14] : just i ≤′ just k
[14] = ≤′-trans [12] [13]