Introduce < for Languages.

Move around some definitions.

6 files changed, 90 insertions, 29 deletions

diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda
index 1f2bb63..ce368d0 100644
--- a/src/Cfe/Derivation/Base.agda
+++ b/src/Cfe/Derivation/Base.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (REL; Setoid)
 
 module Cfe.Derivation.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -14,12 +14,31 @@ open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Level using (_⊔_)
 
-infix 4 _⤇_
+infix 5 _⤇_
+infix 4 _≈_
 
 data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where
   Eps : ε ⤇ []
-  Char : ∀ {c y} → c ∼ y → Char c ⤇ [ y ]
+  Char : ∀ {c y} → (c∼y : c ∼ y) → Char c ⤇ [ y ]
   Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l
   Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l
   Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l
   Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l
+
+data _≈_ : ∀ {e l l′} → REL (e ⤇ l) (e ⤇ l′) (c ⊔ ℓ) where
+  Eps : Eps ≈ Eps
+  Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′
+  Cat : ∀ {e₁ e₂ l l₁ l₂ l₁′ l₂′ e₁⤇l₁ e₁⤇l₁′ e₂⤇l₂ e₂⤇l₂′} →
+          (e₁⤇l₁≈e₁⤇l′ : _≈_ {e₁} {l₁} {l₁′} e₁⤇l₁ e₁⤇l₁′) →
+          (e₂⤇l₂≈e₂⤇l′ : _≈_ {e₂} {l₂} {l₂′} e₂⤇l₂ e₂⤇l₂′) →
+          (eq : l₁ ++ l₂ ≋ l) → (eq′ : l₁′ ++ l₂′ ≋ l) →
+          Cat e₁⤇l₁ e₂⤇l₂ eq ≈ Cat e₁⤇l₁′ e₂⤇l₂′ eq′
+  Veeˡ : ∀ {e₁ e₂ l l′ e₁⤇l e₁⤇l′} →
+         (e₁⤇l≈e₁⤇l′ : _≈_ {e₁} {l} {l′} e₁⤇l e₁⤇l′) →
+         Veeˡ {e₂ = e₂} e₁⤇l ≈ Veeˡ e₁⤇l′
+  Veeʳ : ∀ {e₁ e₂ l l′ e₂⤇l e₂⤇l′} →
+         (e₂⤇l≈e₂⤇l′ : _≈_ {e₂} {l} {l′} e₂⤇l e₂⤇l′) →
+         Veeʳ {e₁} e₂⤇l ≈ Veeʳ e₂⤇l′
+  Fix : ∀ {e l l′ e[μe/0]⤇l e[μe/0]⤇l′} →
+        (e[μe/0]⤇l≈e[μe/0]⤇l′ : _≈_ {e [ μ e / zero ]} {l} {l′} e[μe/0]⤇l e[μe/0]⤇l′) →
+        Fix {e} e[μe/0]⤇l ≈ Fix e[μe/0]⤇l′
diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda
index 303d2f9..e89d9f1 100644
--- a/src/Cfe/Derivation/Properties.agda
+++ b/src/Cfe/Derivation/Properties.agda
@@ -6,11 +6,11 @@ module Cfe.Derivation.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over renaming (Carrier to C)
+open Setoid over renaming (Carrier to C; _≈_ to _∼_)
 
 open import Cfe.Context over hiding (_≋_)
 open import Cfe.Expression over hiding (_≋_)
-open import Cfe.Language over hiding (≤-refl)
+open import Cfe.Language over hiding (≤-refl; _≈_; _<_)
 open import Cfe.Language.Construct.Concatenate over using (Concat)
 open import Cfe.Language.Indexed.Construct.Iterate over
 open import Cfe.Judgement over
@@ -40,10 +40,10 @@ open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoi
 private
   infix 4 _<_
   _<_ : Rel (List C × Expression 0) _
-  _<_ = ×-Lex _≡_ ℕ._<_ ℕ._<_ on (Product.map length rank)
+  _<_ = ×-Lex _≡_ ℕ._<_ _<ᵣₐₙₖ_ on (Product.map₁ length)
 
   <-wellFounded : WellFounded _<_
-  <-wellFounded = On.wellFounded (Product.map length rank) (×-wellFounded <ⁿ-wellFounded <ⁿ-wellFounded)
+  <-wellFounded = On.wellFounded (Product.map₁ length) (×-wellFounded <ⁿ-wellFounded <ᵣₐₙₖ-wellFounded)
 
 l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l
 l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧
@@ -82,24 +82,6 @@ l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-well
   ... | inj₂ ∣l₁∣≡0 with Concat.l₁ l∈⟦e₁∙e₂⟧ | Concat.l₁∈A l∈⟦e₁∙e₂⟧ | (_⊛_.τ₁.Null τ₁⊛τ₂) | _⊛_.¬n₁ τ₁⊛τ₂ | _⊨_.n⇒n (soundness ∙,∙⊢e₁∶τ₁ [] (ext (λ ()))) | ∣l₁∣≡0
   ... | [] | ε∈A | false | _ | n⇒n | refl = ⊥-elim (n⇒n ε∈A)
 
-  e₁<e₁∨e₂ : ∀ l e₁ e₂ → (l , e₁) < (l , e₁ ∨ e₂)
-  e₁<e₁∨e₂ _ e₁ e₂ = inj₂ (≡.refl , (begin-strict
-    rank e₁                     ≤⟨ m≤m+n (rank e₁) (rank e₂) ⟩
-    rank e₁ ℕ.+ rank e₂         <⟨ n<1+n (rank e₁ ℕ.+ rank e₂ ) ⟩
-    ℕ.suc (rank e₁ ℕ.+ rank e₂) ≡⟨⟩
-    rank (e₁ ∨ e₂)              ∎))
-    where
-    open ≤-Reasoning
-
-  e₂<e₁∨e₂ : ∀ l e₁ e₂ → (l , e₂) < (l , e₁ ∨ e₂)
-  e₂<e₁∨e₂ _ e₁ e₂ = inj₂ (≡.refl , (begin-strict
-    rank e₂                     ≤⟨ m≤n+m (rank e₂) (rank e₁) ⟩
-    rank e₁ ℕ.+ rank e₂         <⟨ n<1+n (rank e₁ ℕ.+ rank e₂ ) ⟩
-    ℕ.suc (rank e₁ ℕ.+ rank e₂) ≡⟨⟩
-    rank (e₁ ∨ e₂)              ∎))
-    where
-    open ≤-Reasoning
-
   l∈⟦e⟧ⁿ⇒l∈⟦e[μe/0]⟧ : ∀ {l} e n → l ∈ ((λ X → ⟦ e ⟧ (X ∷ [])) ^ n) (⟦ ⊥ ⟧ []) → l ∈ ⟦ e [ μ e / F.zero ] ⟧ []
   l∈⟦e⟧ⁿ⇒l∈⟦e[μe/0]⟧ e (suc n) l∈⟦e⟧ⁿ = _≤_.f
     (begin
@@ -128,5 +110,7 @@ l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-well
       l∈⟦e⟧.eq
     where
     module l∈⟦e⟧ = Concat l∈⟦e⟧
-  go (l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ _ _) (inj₁ l∈⟦e₁⟧) = Veeˡ (rec (l , e₁) (e₁<e₁∨e₂ l e₁ e₂) ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧)
-  go (l , e₁ ∨ e₂) rec (Vee _ ∙,∙⊢e₂∶τ₂ _) (inj₂ l∈⟦e₂⟧) = Veeʳ (rec (l , e₂) (e₂<e₁∨e₂ l e₁ e₂) ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧)
+  go (l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ _ _) (inj₁ l∈⟦e₁⟧) =
+    Veeˡ (rec (l , e₁) (inj₂ (≡.refl , e₁<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧)
+  go (l , e₁ ∨ e₂) rec (Vee _ ∙,∙⊢e₂∶τ₂ _) (inj₂ l∈⟦e₂⟧) =
+    Veeʳ (rec (l , e₂) (inj₂ (≡.refl , e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧)
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index dd9e9b4..1cd57a7 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -97,3 +97,8 @@ rank (e₁ ∨ e₂) = suc (rank e₁ ℕ.+ rank e₂)
 rank (e₁ ∙ _) = suc (rank e₁)
 rank (Var _) = 0
 rank (μ e) = suc (rank e)
+
+infix 4 _<ᵣₐₙₖ_
+
+_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _
+_<ᵣₐₙₖ_ = ℕ._<_ on rank
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 22dc18f..d1e2869 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -17,6 +17,8 @@ import Cfe.Language.Indexed.Construct.Iterate over as ⋃
 open import Data.Fin as F
 open import Data.Fin.Properties
 open import Data.Nat as ℕ hiding (_⊔_)
+open import Data.Nat.Induction
+open import Data.Nat.Properties using (m≤m+n; m≤n+m; n<1+n; module ≤-Reasoning)
 open import Data.Product
 open import Data.Sum
 open import Data.Unit
@@ -24,8 +26,10 @@ open import Data.Vec
 open import Data.Vec.Properties
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 open import Function
+open import Induction.WellFounded
 open import Level renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+import Relation.Binary.Construct.On as On
 open import Relation.Nullary
 
 isEquivalence : ∀ n → IsEquivalence (_≋_ {n})
@@ -206,3 +210,24 @@ cast-involutive (Var x) k≡m m≡n k≡n = ≡.cong Var (toℕ-injective (begin
   where
   open ≡.≡-Reasoning
 cast-involutive (μ e) k≡m m≡n k≡n = ≡.cong μ (cast-involutive e (≡.cong suc k≡m) (≡.cong suc m≡n) (≡.cong suc k≡n))
+
+<ᵣₐₙₖ-wellFounded : ∀ {n} → WellFounded (_<ᵣₐₙₖ_ {n})
+<ᵣₐₙₖ-wellFounded = On.wellFounded rank <-wellFounded
+
+e₁<ᵣₐₙₖe₁∨e₂ : ∀ {n} → (e₁ e₂ : Expression n) → e₁ <ᵣₐₙₖ e₁ ∨ e₂
+e₁<ᵣₐₙₖe₁∨e₂ e₁ e₂ = begin-strict
+  rank e₁                   ≤⟨ m≤m+n (rank e₁) (rank e₂) ⟩
+  rank e₁ ℕ.+ rank e₂       <⟨ n<1+n (rank e₁ ℕ.+ rank e₂) ⟩
+  suc (rank e₁ ℕ.+ rank e₂) ≡⟨⟩
+  rank (e₁ ∨ e₂)            ∎
+  where
+  open ≤-Reasoning
+
+e₂<ᵣₐₙₖe₁∨e₂ : ∀ {n} → (e₁ e₂ : Expression n) → e₂ <ᵣₐₙₖ e₁ ∨ e₂
+e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂ = begin-strict
+  rank e₂                   ≤⟨ m≤n+m (rank e₂) (rank e₁) ⟩
+  rank e₁ ℕ.+ rank e₂       <⟨ n<1+n (rank e₁ ℕ.+ rank e₂) ⟩
+  suc (rank e₁ ℕ.+ rank e₂) ≡⟨⟩
+  rank (e₁ ∨ e₂)            ∎
+  where
+  open ≤-Reasoning
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index a3b5136..71ee7df 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -63,6 +63,13 @@ record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔
     f : ∀ {l} → l ∈ A → l ∈ B
     f⁻¹ : ∀ {l} → l ∈ B → l ∈ A
 
+record _<_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
+  field
+    f : ∀ {l} → l ∈ A → l ∈ B
+    l : List C
+    l∉A : l ∉ A
+    l∈B : l ∈ B
+
 null : ∀ {a} → Language a → Set a
 null A = [] ∈ A
 
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 756877c..52b5470 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -8,8 +8,6 @@ module Cfe.Language.Properties
 
 open Setoid over using () renaming (Carrier to C)
 open import Cfe.Language.Base over
--- open Language
-
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
@@ -95,6 +93,29 @@ setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
 poset a = record { isPartialOrder = ≤-isPartialOrder a }
 
+<-trans : ∀ {a b c} → Trans (_<_ {a}) (_<_ {b} {c}) _<_
+<-trans A<B B<C = record
+  { f = B<C.f ∘ A<B.f
+  ; l = A<B.l
+  ; l∉A = A<B.l∉A
+  ; l∈B = B<C.f A<B.l∈B
+  }
+  where
+  module A<B = _<_ A<B
+  module B<C = _<_ B<C
+
+<-irrefl : ∀ {a b} → Irreflexive (_≈_ {a} {b}) _<_
+<-irrefl A≈B A<B = A<B.l∉A (A≈B.f⁻¹ A<B.l∈B)
+  where
+  module A≈B = _≈_ A≈B
+  module A<B = _<_ A<B
+
+<-asym : ∀ {a} → Asymmetric (_<_ {a})
+<-asym A<B B<A = A<B.l∉A (B<A.f A<B.l∈B)
+  where
+  module A<B = _<_ A<B
+  module B<A = _<_ B<A
+
 lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
 lift-cong b L = record
   { f = lower