From 3638caa4c6f363c1adc7c931f65dea3104cae796 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 29 Mar 2021 14:52:02 +0100 Subject: Convert to terminating proof using well-founded induction. --- src/Cfe/Parse/Properties.agda | 130 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 107 insertions(+), 23 deletions(-) diff --git a/src/Cfe/Parse/Properties.agda b/src/Cfe/Parse/Properties.agda index 830b0f2..1b1d247 100644 --- a/src/Cfe/Parse/Properties.agda +++ b/src/Cfe/Parse/Properties.agda @@ -8,41 +8,125 @@ module Cfe.Parse.Properties open Setoid over renaming (Carrier to C) -open import Cfe.Context over -open import Cfe.Expression over -open import Cfe.Language over +open import Cfe.Context over hiding (_≋_) +open import Cfe.Expression over hiding (_≋_) +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 open import Cfe.Parse.Base over open import Cfe.Type over using (_⊛_; _⊨_) open import Data.Bool using (T; not; true; false) open import Data.Empty using (⊥-elim) -open import Data.Fin as F +open import Data.Fin as F hiding (_<_) open import Data.List hiding (null) open import Data.List.Relation.Binary.Equality.Setoid over -open import Data.Nat as ℕ hiding (_⊔_; _^_) -open import Data.Product -open import Data.Sum -open import Data.Vec +open import Data.Nat as ℕ hiding (_⊔_; _^_; _<_) +open import Data.Nat.Properties using (≤-step; m≤m+n; m≤n+m; ≤-refl; n<1+n; module ≤-Reasoning) +open import Data.Nat.Induction using () renaming (<-wellFounded to <ⁿ-wellFounded) +open import Data.Product as Product +open import Data.Product.Relation.Binary.Lex.Strict +open import Data.Sum as Sum +open import Data.Vec hiding (length; _++_) open import Data.Vec.Relation.Binary.Pointwise.Inductive open import Data.Vec.Relation.Binary.Pointwise.Extensional open import Function +open import Induction.WellFounded open import Level -open import Relation.Binary.PropositionalEquality hiding (subst₂; setoid) +open import Relation.Binary +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoid) + +private + infix 4 _<_ + _<_ : Rel (List C × Expression 0) _ + _<_ = ×-Lex _≡_ ℕ._<_ ℕ._<_ on (Product.map length rank) + + <-wellFounded : WellFounded _<_ + <-wellFounded = On.wellFounded (Product.map length rank) (×-wellFounded <ⁿ-wellFounded <ⁿ-wellFounded) l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l -l∈⟦e⟧⇒e⤇l Eps (lift refl) = Eps -l∈⟦e⟧⇒e⤇l (Char c) (lift (c∼y ∷ [])) = Char c∼y -l∈⟦e⟧⇒e⤇l {μ e} (Fix ∙,τ⊢e∶τ) (suc n , l∈⟦e⟧ⁿ⁺¹) = Fix (l∈⟦e⟧⇒e⤇l (subst₂ z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ)) l∈⟦e[μe]⟧) +l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧ where - open import Relation.Binary.Reasoning.PartialOrder (poset (c ⊔ ℓ)) - ⟦e⟧ⁿ⁺¹≤⟦e[μe]⟧ = begin - ⟦ e ⟧ (((λ X → ⟦ e ⟧ (X ∷ [])) ^ n) (⟦ ⊥ ⟧ []) ∷ []) ≤⟨ mono e ((fⁿ≤⋃f (λ X → ⟦ e ⟧ (X ∷ [])) n) ∷ []) ⟩ - ⟦ e ⟧ (⋃ (λ X → ⟦ e ⟧ (X ∷ [])) ∷ []) ≡⟨⟩ - ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) ≈˘⟨ subst-fun e (μ e) F.zero [] ⟩ - ⟦ e [ μ e / F.zero ] ⟧ [] ∎ - l∈⟦e[μe]⟧ = _≤_.f ⟦e⟧ⁿ⁺¹≤⟦e[μe]⟧ l∈⟦e⟧ⁿ⁺¹ -l∈⟦e⟧⇒e⤇l (Cat ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁⊛τ₂) record { l₁∈A = l₁∈⟦e₁⟧ ; l₂∈B = l₂∈⟦e₂⟧ ; eq = eq } = - Cat (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₁∶τ₁ l₁∈⟦e₁⟧) (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₂∶τ₂ l₂∈⟦e₂⟧) eq -l∈⟦e⟧⇒e⤇l (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₁ l∈⟦e₁⟧) = Veeˡ (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧) -l∈⟦e⟧⇒e⤇l (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₂ l∈⟦e₂⟧) = Veeʳ (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧) + Pred : List C × Expression 0 → Set _ + Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → l ∈ ⟦ e ⟧ [] → e ⤇ l + + e[μe/0]<μe : ∀ {e τ} l → ∙,∙ ⊢ μ e ∶ τ → (l , e [ μ e / F.zero ]) < (l , μ e) + e[μe/0]<μe {e} l (Fix ∙,τ⊢e∶τ)= inj₂ (≡.refl , (begin-strict + rank (e [ μ e / F.zero ]) ≡⟨ subst-preserves-rank z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ) ⟩ + rank e <⟨ n<1+n (rank e) ⟩ + ℕ.suc (rank e) ≡⟨⟩ + rank (μ e) ∎)) + where + open ≤-Reasoning + + l₁++l₂≋l⇒∣l₁∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₁ ℕ.< length l) ⊎ (length l₁ ≡ length l) + l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] [] = inj₂ ≡.refl + l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] (_ ∷ _) = inj₁ (s≤s z≤n) + l₁++l₂≋l⇒∣l₁∣≤∣l∣ (_ ∷ l₁) (_ ∷ eq) = Sum.map s≤s (cong ℕ.suc) (l₁++l₂≋l⇒∣l₁∣≤∣l∣ l₁ eq) + + l₁++l₂≋l⇒∣l₂∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₂ ℕ.< length l) ⊎ (length l₁ ≡ 0) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ [] _ = inj₂ ≡.refl + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ []) (_ ∷ []) = inj₁ (s≤s z≤n) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ _ ∷ eq) = inj₁ ([ s≤s , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ eq))) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ x ∷ l₁) (_ ∷ eq) = inj₁ ([ ≤-step , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ l₁) eq)) + + e₁