------------------------------------------------------------------------
-- Properties of machine states.
------------------------------------------------------------------------

open import Graded.Modality
open import Graded.Usage.Restrictions
open import Definition.Typed.Variant
open import Graded.Usage.Restrictions.Natrec

module Graded.Heap.Untyped.Properties
  {a} {M : Set a} {š•„ : Modality M}
  (type-variant : Type-variant)
  (UR : Usage-restrictions š•„)
  (open Usage-restrictions UR)
  (factoring-nr :
    ā¦ƒ has-nr : Nr-available ā¦„ ā†’
    Is-factoring-nr M (Natrec-mode-Has-nr š•„ has-nr))
  where

open Type-variant type-variant
open Modality š•„

open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat; 1+; 2+; +-suc) renaming (_+_ to _+āæ_)
open import Tools.PropositionalEquality
open import Tools.Product
open import Tools.Relation
open import Tools.Reasoning.PropositionalEquality
open import Tools.Sum

open import Graded.Modality.Nr-instances
open import Graded.Modality.Properties š•„
open import Graded.Usage.Erased-matches
open import Graded.Usage.Restrictions.Instance UR

open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M

open import Graded.Heap.Untyped type-variant UR factoring-nr

private variable
  k n nā€² nā€³ m mā€² mā€³ : Nat
  t tā€² tā€³ u v A z : Term _
  H Hā€² Hā€³ : Heap _ _
  Ļ Ļā€² Ļā€³ : Wk _ _
  S Sā€² Sā€³ : Stack _
  p pā€² q qā€² r rā€² : M
  y yā€² : Ptr _
  x : Fin _
  e eā€² : Entry _ _
  Ī“ : Con Term _
  c cā€² cā€³ : Cont _
  s sā€² : State _ _ _
  Ļƒ : Subst _ _
  em : Erased-matches

------------------------------------------------------------------------
-- Properties of states

opaque

  -- Injectivity of states

  State-injectivity :
    {H : Heap _ _} ā†’
    āŸØ H , t , Ļ , S āŸ© ā‰” āŸØ Hā€² , tā€² , Ļā€² , Sā€² āŸ© ā†’
    H ā‰” Hā€² Ɨ t ā‰” tā€² Ɨ Ļ ā‰” Ļā€² Ɨ S ā‰” Sā€²
  State-injectivity refl = refl , refl , refl , refl

------------------------------------------------------------------------
-- Properties of values

opaque

  -- Values applied to weakenings are values

  wkValue : (Ļ : Wk m n) ā†’ Value t ā†’ Value (wk Ļ t)
  wkValue Ļ lamįµ„ = lamįµ„
  wkValue Ļ zeroįµ„ = zeroįµ„
  wkValue Ļ sucįµ„ = sucįµ„
  wkValue Ļ starįµ„ = starįµ„
  wkValue Ļ prodįµ„ = prodįµ„
  wkValue Ļ rflįµ„ = rflįµ„
  wkValue Ļ Uįµ„ = Uįµ„
  wkValue Ļ Ī Ī£įµ„ = Ī Ī£įµ„
  wkValue Ļ ā„•įµ„ = ā„•įµ„
  wkValue Ļ Unitįµ„ = Unitįµ„
  wkValue Ļ Emptyįµ„ = Emptyįµ„
  wkValue Ļ Idįµ„ = Idįµ„
  wkValue Ļ (unitrec-Ī·įµ„ Ī·) = unitrec-Ī·įµ„ Ī·

opaque

  -- Values applied to substitutions are values

  substValue : (Ļƒ : Subst m n) ā†’ Value t ā†’ Value (t [ Ļƒ ])
  substValue Ļƒ lamįµ„ = lamįµ„
  substValue Ļƒ zeroįµ„ = zeroįµ„
  substValue Ļƒ sucįµ„ = sucįµ„
  substValue Ļƒ starįµ„ = starįµ„
  substValue Ļƒ prodįµ„ = prodįµ„
  substValue Ļƒ rflįµ„ = rflįµ„
  substValue Ļƒ Uįµ„ = Uįµ„
  substValue Ļƒ Ī Ī£įµ„ = Ī Ī£įµ„
  substValue Ļƒ ā„•įµ„ = ā„•įµ„
  substValue Ļƒ Unitįµ„ = Unitįµ„
  substValue Ļƒ Emptyįµ„ = Emptyįµ„
  substValue Ļƒ Idįµ„ = Idįµ„
  substValue Ļ (unitrec-Ī·įµ„ Ī·) = unitrec-Ī·įµ„ Ī·

opaque

  -- Values are non-neutrals

  Valueā†’Ā¬Neutral : Value t ā†’ Ā¬ Neutral t
  Valueā†’Ā¬Neutral lamįµ„ ()
  Valueā†’Ā¬Neutral zeroįµ„ ()
  Valueā†’Ā¬Neutral sucįµ„ ()
  Valueā†’Ā¬Neutral starįµ„ ()
  Valueā†’Ā¬Neutral prodįµ„ ()
  Valueā†’Ā¬Neutral rflįµ„ ()
  Valueā†’Ā¬Neutral Uįµ„ ()
  Valueā†’Ā¬Neutral Ī Ī£įµ„ ()
  Valueā†’Ā¬Neutral ā„•įµ„ ()
  Valueā†’Ā¬Neutral Unitįµ„ ()
  Valueā†’Ā¬Neutral Emptyįµ„ ()
  Valueā†’Ā¬Neutral Idįµ„ ()
  Valueā†’Ā¬Neutral (unitrec-Ī·įµ„ Ī·) (unitrecā‚™ no-Ī· _) = no-Ī· Ī·

opaque

  -- If t is a value, then either t is in WHNF, or t is an application
  -- of unitrec and Ī·-equality is allowed for weak unit types.

  Valueā†’Whnf :
    Value t ā†’
    Whnf t āŠŽ āˆƒā‚† Ī» l p q A u v ā†’ t ā‰” unitrec l p q A u v Ɨ UnitŹ·-Ī·
  Valueā†’Whnf lamįµ„ = injā‚ lamā‚™
  Valueā†’Whnf zeroįµ„ = injā‚ zeroā‚™
  Valueā†’Whnf sucįµ„ = injā‚ sucā‚™
  Valueā†’Whnf starįµ„ = injā‚ starā‚™
  Valueā†’Whnf prodįµ„ = injā‚ prodā‚™
  Valueā†’Whnf rflįµ„ = injā‚ rflā‚™
  Valueā†’Whnf Uįµ„ = injā‚ Uā‚™
  Valueā†’Whnf Ī Ī£įµ„ = injā‚ Ī Ī£ā‚™
  Valueā†’Whnf ā„•įµ„ = injā‚ ā„•ā‚™
  Valueā†’Whnf Unitįµ„ = injā‚ Unitā‚™
  Valueā†’Whnf Emptyįµ„ = injā‚ Emptyā‚™
  Valueā†’Whnf Idįµ„ = injā‚ Idā‚™
  Valueā†’Whnf (unitrec-Ī·įµ„ x) = injā‚‚ (_ , _ , _ , _ , _ , _ , refl , x)

------------------------------------------------------------------------
-- Properties of the lookup relations

opaque

  -- Variable lookup with heap update is deterministic.

  lookup-det : {H : Heap k m} {t : Term n} {u : Term nā€²}
             ā†’ H āŠ¢ y ā†¦[ r ] t , Ļ āؾ Hā€²
             ā†’ H āŠ¢ y ā†¦[ r ] u , Ļā€² āؾ Hā€³
             ā†’ Ī£ (n ā‰” nā€²) Ī» p ā†’ subst Term p t ā‰” u
               Ɨ subst (Wk m) p Ļ ā‰” Ļā€² Ɨ Hā€² ā‰” Hā€³
  lookup-det (here p-šŸ™ā‰”q) (here p-šŸ™ā‰”qā€²) =
    case -ā‰”-functional p-šŸ™ā‰”q p-šŸ™ā‰”qā€² of Ī» {
      refl ā†’
    refl , refl , refl , refl }
  lookup-det (there x) (there y) =
    case lookup-det x y of Ī» {
      (refl , refl , refl , refl) ā†’
    refl , refl , refl , refl }
  lookup-det (thereā— x) (thereā— y) =
    case lookup-det x y of Ī» {
      (refl , refl , refl , refl) ā†’
    refl , refl , refl , refl}

opaque

  -- Variable lookup without heap update is deterministic.

  lookup-detā€² : {H : Heap k m} {t : Term n} {u : Term nā€²}
             ā†’ H āŠ¢ y ā†¦ (t , Ļ)
             ā†’ H āŠ¢ y ā†¦ (u , Ļā€²)
             ā†’ Ī£ (n ā‰” nā€²) Ī» p ā†’ subst Term p t ā‰” u Ɨ subst (Wk m) p Ļ ā‰” Ļā€²
  lookup-detā€² here here = refl , refl , refl
  lookup-detā€² (there d) (there dā€²) =
    case lookup-detā€² d dā€² of Ī» {
      (refl , refl , refl) ā†’
    refl , refl , refl }
  lookup-detā€² (thereā— d) (thereā— dā€²) =
    case lookup-detā€² d dā€² of Ī» {
      (refl , refl , refl) ā†’
    refl , refl , refl }

opaque

  -- Lookup will either yield an entry or a dummy entry

  ā†¦āŠŽā†¦ā— : āˆ€ y ā†’ (āˆƒā‚‚ Ī» n (c : Entry _ n) ā†’ H āŠ¢ y ā†¦ c) āŠŽ H āŠ¢ y ā†¦ā—
  ā†¦āŠŽā†¦ā— {H = Īµ} ()
  ā†¦āŠŽā†¦ā— {H = H āˆ™ c} y0 = injā‚ (_ , _ , here)
  ā†¦āŠŽā†¦ā— {H = H āˆ™ā—} y0 = injā‚‚ here
  ā†¦āŠŽā†¦ā— {H = H āˆ™ c} (y +1) =
    case ā†¦āŠŽā†¦ā— y of Ī» where
      (injā‚ (_ , _ , d)) ā†’ injā‚ (_ , _ , there d)
      (injā‚‚ d) ā†’ injā‚‚ (there d)
  ā†¦āŠŽā†¦ā— {H = H āˆ™ā—} (y +1) =
    case ā†¦āŠŽā†¦ā— y of Ī» where
      (injā‚ (_ , _ , d)) ā†’ injā‚ (_ , _ , thereā— d)
      (injā‚‚ d) ā†’ injā‚‚ (thereā— d)

opaque

  -- Lookup cannot yield both an entry and a dummy entry.

  Ā¬ā†¦āˆ§ā†¦ā— : H āŠ¢ y ā†¦ e ā†’ H āŠ¢ y ā†¦ā— ā†’ āŠ„
  Ā¬ā†¦āˆ§ā†¦ā— here ()
  Ā¬ā†¦āˆ§ā†¦ā— (there d) (there dā€²) = Ā¬ā†¦āˆ§ā†¦ā— d dā€²
  Ā¬ā†¦āˆ§ā†¦ā— (thereā— d) (thereā— dā€²) = Ā¬ā†¦āˆ§ā†¦ā— d dā€²

opaque

  -- If a heap does not contain erased entries then lookup to ā— will
  -- always fail.

  Ā¬erased-heapā†’Ā¬ā†¦ā— : {H : Heap k _} ā†’ H āŠ¢ y ā†¦ā— ā†’ k ā‰” 0 ā†’ āŠ„
  Ā¬erased-heapā†’Ā¬ā†¦ā— here ()
  Ā¬erased-heapā†’Ā¬ā†¦ā— (there d) kā‰”0 = Ā¬erased-heapā†’Ā¬ā†¦ā— d kā‰”0
  Ā¬erased-heapā†’Ā¬ā†¦ā— (thereā— d) ()

opaque

  Ā¬erased-heapā†’ā†¦ :
    {H : Heap k m} ā†’ k ā‰” 0 ā†’ (y : Ptr m) ā†’
    āˆƒā‚‚ Ī» n (e : Entry m n) ā†’ H āŠ¢ y ā†¦ e
  Ā¬erased-heapā†’ā†¦ kā‰”0 y =
    case ā†¦āŠŽā†¦ā— y of Ī» where
      (injā‚ x) ā†’ x
      (injā‚‚ x) ā†’ āŠ„-elim (Ā¬erased-heapā†’Ā¬ā†¦ā— x kā‰”0)

opaque

  -- If heap lookup with update succeeds lookup without heap update
  -- succeeds with the same result.

  ā†¦[]ā†’ā†¦ : H āŠ¢ y ā†¦[ q ] e āؾ Hā€² ā†’ H āŠ¢ y ā†¦ e
  ā†¦[]ā†’ā†¦ (here x) = here
  ā†¦[]ā†’ā†¦ (there d) = there (ā†¦[]ā†’ā†¦ d)
  ā†¦[]ā†’ā†¦ (thereā— d) = thereā— (ā†¦[]ā†’ā†¦ d)

opaque

  -- Heap lookups match the corresponding substitution.

  heapSubstVar : H āŠ¢ y ā†¦[ q ] t , Ļ āؾ Hā€² ā†’ toSubstā‚• H y ā‰” wk Ļ t [ H ]ā‚•
  heapSubstVar {t} (here _) =
    sym (step-consSubst t)
  heapSubstVar {t} (there d) =
    trans (heapSubstVar d) (sym (step-consSubst t))
  heapSubstVar {H = H āˆ™ā—} {t} {Ļ = step Ļ} (thereā— d) =
    trans (cong wk1 (heapSubstVar d))
      (trans (sym (wk1-liftSubst (wk Ļ t)))
        (cong (_[ H ]ā‡‘ā‚•) (wk1-wk Ļ t)))

opaque

  -- Heap lookups match the corresponding substitution.

  heapSubstVarā€² : H āŠ¢ y ā†¦ (t , Ļ) ā†’ toSubstā‚• H y ā‰” wk Ļ t [ H ]ā‚•
  heapSubstVarā€² {t} here =
    sym (step-consSubst t)
  heapSubstVarā€² {t} (there d) =
    trans (heapSubstVarā€² d) (sym (step-consSubst t))
  heapSubstVarā€² {H = H āˆ™ā—} {t} {Ļ = step Ļ} (thereā— d) =
    trans (cong wk1 (heapSubstVarā€² d))
      (trans (sym (wk1-liftSubst (wk Ļ t)))
        (cong (_[ H ]ā‡‘ā‚•) (wk1-wk Ļ t)))

opaque

  -- If subtraction of the grade correspoding to a heap entry cannot
  -- by subtracted by q then lookup of q copies fails.

  -ā‰¢-no-lookup :
    (āˆ€ {r} ā†’ H āŸØ y āŸ©Ź° - q ā‰” r ā†’ āŠ„) ā†’
    H āŠ¢ y ā†¦[ q ] e āؾ Hā€² ā†’ āŠ„
  -ā‰¢-no-lookup p-qā‰¢r (here p-qā‰”r) =
    p-qā‰¢r p-qā‰”r
  -ā‰¢-no-lookup p-qā‰¢r (there d) =
    -ā‰¢-no-lookup p-qā‰¢r d
  -ā‰¢-no-lookup p-qā‰¢r (thereā— d) =
    -ā‰¢-no-lookup p-qā‰¢r d

------------------------------------------------------------------------
-- Properties of stacks and continuations

opaque

  -- Applying a single substitution to a term and then to a continuation

  ā¦…ā¦†į¶œ-sgSubst : āˆ€ c ā†’ ā¦… c ā¦†į¶œ (t [ u ]ā‚€) ā‰” ā¦… wk1į¶œ c ā¦†į¶œ t [ u ]ā‚€
  ā¦…ā¦†į¶œ-sgSubst (āˆ˜ā‚‘ p u Ļ) =
    cong (_ āˆ˜_) (sym (step-sgSubst _ _))
  ā¦…ā¦†į¶œ-sgSubst (fstā‚‘ p) = refl
  ā¦…ā¦†į¶œ-sgSubst (sndā‚‘ p) = refl
  ā¦…ā¦†į¶œ-sgSubst {u = v} (prodrecā‚‘ r p q A u Ļ) =
    congā‚‚ (Ī» u A ā†’ prodrec r p q A _ u)
      (lifts-step-sgSubst 2 u)
      (lifts-step-sgSubst 1 A)
  ā¦…ā¦†į¶œ-sgSubst {u} (natrecā‚‘ p q r A z s Ļ) =
    congā‚ƒ (Ī» A z s ā†’ natrec p q r A z s _)
      (lifts-step-sgSubst 1 A)
      (lifts-step-sgSubst 0 z)
      (lifts-step-sgSubst 2 s)
  ā¦…ā¦†į¶œ-sgSubst {u = v} (unitrecā‚‘ _ p q A u Ļ) =
    congā‚‚ (Ī» u A ā†’ unitrec _ p q A _ u)
      (sym (step-sgSubst _ _))
      (lifts-step-sgSubst 1 A)
  ā¦…ā¦†į¶œ-sgSubst (emptyrecā‚‘ p A Ļ) =
    cong (Ī» A ā†’ emptyrec p A _)
      (lifts-step-sgSubst 0 A)
  ā¦…ā¦†į¶œ-sgSubst (Jā‚‘ p q A t B u v Ļ) =
    sym (congā‚… (Ī» A t B u v ā†’ J p q A t B u v _)
      (step-sgSubst A _) (step-sgSubst t _)
      (sym (lifts-step-sgSubst 2 B))
      (step-sgSubst u _) (step-sgSubst v _))
  ā¦…ā¦†į¶œ-sgSubst (Kā‚‘ p A t B u Ļ) =
    sym (congā‚„ (Ī» A t B u ā†’ K p A t B u _)
      (step-sgSubst A _) (step-sgSubst t _)
      (sym (lifts-step-sgSubst 1 B))
      (step-sgSubst u _))
  ā¦…ā¦†į¶œ-sgSubst ([]-congā‚‘ s A t u Ļ) =
    sym (congā‚ƒ (Ī» A t u ā†’ []-cong s A t u _)
      (step-sgSubst A _) (step-sgSubst t _)
      (step-sgSubst u _))
  ā¦…ā¦†į¶œ-sgSubst sucā‚‘ = refl

opaque

  -- Applying a single substitution to a term and then to a stack

  ā¦…ā¦†Ė¢-sgSubst : āˆ€ S ā†’ ā¦… S ā¦†Ė¢ (t [ u ]ā‚€) ā‰” ā¦… wk1Ė¢ S ā¦†Ė¢ t [ u ]ā‚€
  ā¦…ā¦†Ė¢-sgSubst Īµ = refl
  ā¦…ā¦†Ė¢-sgSubst {t} {u} (e āˆ™ S) = begin
   ā¦… e āˆ™ S ā¦†Ė¢ (t [ u ]ā‚€)              ā‰”āŸØāŸ©
   ā¦… S ā¦†Ė¢ (ā¦… e ā¦†į¶œ (t [ u ]ā‚€))          ā‰”āŸØ cong ā¦… S ā¦†Ė¢_ (ā¦…ā¦†į¶œ-sgSubst e) āŸ©
   ā¦… S ā¦†Ė¢ (ā¦… wk1į¶œ e ā¦†į¶œ t [ u ]ā‚€)       ā‰”āŸØ ā¦…ā¦†Ė¢-sgSubst S āŸ©
   ā¦… wk1Ė¢ S ā¦†Ė¢ (ā¦… wk1į¶œ e ā¦†į¶œ t) [ u ]ā‚€  ā‰”āŸØāŸ©
   ā¦… wk1Ė¢ (e āˆ™ S) ā¦†Ė¢ t [ u ]ā‚€         āˆŽ

opaque

  -- Applying a double substitution to a term and then to a continuation

  ā¦…ā¦†į¶œ-[,] : āˆ€ e ā†’ ā¦… e ā¦†į¶œ (t [ u , v ]ā‚ā‚€) ā‰” ā¦… wk2į¶œ e ā¦†į¶œ t [ u , v ]ā‚ā‚€
  ā¦…ā¦†į¶œ-[,] (āˆ˜ā‚‘ p u Ļ) =
    cong (_ āˆ˜_) (lifts-step-[,] 0 u)
  ā¦…ā¦†į¶œ-[,] (fstā‚‘ x) = refl
  ā¦…ā¦†į¶œ-[,] (sndā‚‘ x) = refl
  ā¦…ā¦†į¶œ-[,] (prodrecā‚‘ r p q A u Ļ) =
    congā‚‚ (Ī» x y ā†’ prodrec r p q x _ y)
      (lifts-step-[,] 1 A)
      (lifts-step-[,] 2 u)
  ā¦…ā¦†į¶œ-[,] (natrecā‚‘ p q r A z s Ļ) =
    congā‚ƒ (Ī» A z s ā†’ natrec p q r A z s _)
      (lifts-step-[,] 1 A)
      (lifts-step-[,] 0 z)
      (lifts-step-[,] 2 s)
  ā¦…ā¦†į¶œ-[,] (unitrecā‚‘ _ p q A u Ļ) =
    congā‚‚ (Ī» x y ā†’ unitrec _ p q x _ y)
      (lifts-step-[,] 1 A) (lifts-step-[,] 0 u)
  ā¦…ā¦†į¶œ-[,] (emptyrecā‚‘ p A Ļ) =
    cong (Ī» A ā†’ emptyrec p A _) (lifts-step-[,] 0 A)
  ā¦…ā¦†į¶œ-[,] (Jā‚‘ p q A t B u v Ļ) =
    congā‚… (Ī» A t B u v ā†’ J p q A t B u v _)
      (lifts-step-[,] 0 A) (lifts-step-[,] 0 t)
      (lifts-step-[,] 2 B) (lifts-step-[,] 0 u)
      (lifts-step-[,] 0 v)
  ā¦…ā¦†į¶œ-[,] (Kā‚‘ p A t B u Ļ) =
    congā‚„ (Ī» A t B u ā†’ K p A t B u _)
      (lifts-step-[,] 0 A) (lifts-step-[,] 0 t)
      (lifts-step-[,] 1 B) (lifts-step-[,] 0 u)
  ā¦…ā¦†į¶œ-[,] ([]-congā‚‘ s A t u Ļ) =
    congā‚ƒ (Ī» A t u ā†’ []-cong s A t u _)
      (lifts-step-[,] 0 A) (lifts-step-[,] 0 t)
      (lifts-step-[,] 0 u)
  ā¦…ā¦†į¶œ-[,] sucā‚‘ = refl

opaque

  -- Applying a double substitution to a term and then to a stack

  ā¦…ā¦†Ė¢-[,] : āˆ€ S ā†’ ā¦… S ā¦†Ė¢ (t [ u , v ]ā‚ā‚€) ā‰” ā¦… wk2Ė¢ S ā¦†Ė¢ t [ u , v ]ā‚ā‚€
  ā¦…ā¦†Ė¢-[,] Īµ = refl
  ā¦…ā¦†Ė¢-[,] {t} {u} {v} (e āˆ™ S) = begin
    ā¦… e āˆ™ S ā¦†Ė¢ (t [ u , v ]ā‚ā‚€)             ā‰”āŸØāŸ©
    ā¦… S ā¦†Ė¢ (ā¦… e ā¦†į¶œ (t [ u , v ]ā‚ā‚€))         ā‰”āŸØ cong ā¦… S ā¦†Ė¢_ (ā¦…ā¦†į¶œ-[,] e) āŸ©
    ā¦… S ā¦†Ė¢ (ā¦… wk2į¶œ e ā¦†į¶œ t [ u , v ]ā‚ā‚€)      ā‰”āŸØ ā¦…ā¦†Ė¢-[,] S āŸ©
    ā¦… wk2Ė¢ S ā¦†Ė¢ (ā¦… wk2į¶œ e ā¦†į¶œ t) [ u , v ]ā‚ā‚€ ā‰”āŸØāŸ©
    ā¦… wk2Ė¢ (e āˆ™ S) ā¦†Ė¢ t [ u , v ]ā‚ā‚€        āˆŽ

opaque

  -- Weakening of a continuation applied to a Term

  wk-ā¦…ā¦†į¶œ : āˆ€ {Ļ : Wk m n} e ā†’ wk Ļ (ā¦… e ā¦†į¶œ t) ā‰” ā¦… wkį¶œ Ļ e ā¦†į¶œ (wk Ļ t)
  wk-ā¦…ā¦†į¶œ {Ļ} (āˆ˜ā‚‘ p u Ļā€²) =
    cong (_ āˆ˜_) (wk-comp Ļ Ļā€² u)
  wk-ā¦…ā¦†į¶œ (fstā‚‘ p) = refl
  wk-ā¦…ā¦†į¶œ (sndā‚‘ p) = refl
  wk-ā¦…ā¦†į¶œ {Ļ} (prodrecā‚‘ r p q A u Ļā€²) =
    congā‚‚ (Ī» A u ā†’ prodrec r p q A _ u)
      (wk-comp (lift Ļ) (lift Ļā€²) A)
      (wk-comp (liftn Ļ 2) (liftn Ļā€² 2) u)
  wk-ā¦…ā¦†į¶œ {Ļ} (natrecā‚‘ p q r A z s Ļā€²) =
    congā‚ƒ (Ī» A z s ā†’ natrec p q r A z s _)
      (wk-comp (lift Ļ) (lift Ļā€²) A)
      (wk-comp Ļ Ļā€² z)
      (wk-comp (liftn Ļ 2) (liftn Ļā€² 2) s)
  wk-ā¦…ā¦†į¶œ {Ļ} (unitrecā‚‘ _ p q A u Ļā€²) =
    congā‚‚ (Ī» A u ā†’ unitrec _ p q A _ u)
      (wk-comp (lift Ļ) (lift Ļā€²) A)
      (wk-comp Ļ Ļā€² u)
  wk-ā¦…ā¦†į¶œ {Ļ} (emptyrecā‚‘ p A Ļā€²) =
    cong (Ī» A ā†’ emptyrec p A _) (wk-comp Ļ Ļā€² A)
  wk-ā¦…ā¦†į¶œ {Ļ} (Jā‚‘ p q A t B u v Ļā€²) =
    congā‚… (Ī» A t B u v ā†’ J p q A t B u v _)
      (wk-comp Ļ Ļā€² A) (wk-comp Ļ Ļā€² t)
      (wk-comp (liftn Ļ 2) (liftn Ļā€² 2) B)
      (wk-comp Ļ Ļā€² u) (wk-comp Ļ Ļā€² v)
  wk-ā¦…ā¦†į¶œ {Ļ} (Kā‚‘ p A t B u Ļā€²) =
    congā‚„ (Ī» A t B u ā†’ K p A t B u _)
      (wk-comp Ļ Ļā€² A) (wk-comp Ļ Ļā€² t)
      (wk-comp (lift Ļ) (lift Ļā€²) B) (wk-comp Ļ Ļā€² u)
  wk-ā¦…ā¦†į¶œ {Ļ} ([]-congā‚‘ s A t u Ļā€²) =
    congā‚ƒ (Ī» A t u ā†’ []-cong s A t u _)
      (wk-comp Ļ Ļā€² A) (wk-comp Ļ Ļā€² t)
      (wk-comp Ļ Ļā€² u)
  wk-ā¦…ā¦†į¶œ {Ļ} sucā‚‘ = refl

opaque

  -- A congruence property for continuations

  ā¦…ā¦†į¶œ-cong : āˆ€ e ā†’ t [ Ļƒ ] ā‰” u [ Ļƒ ]
         ā†’ ā¦… e ā¦†į¶œ t [ Ļƒ ] ā‰” ā¦… e ā¦†į¶œ u [ Ļƒ ]
  ā¦…ā¦†į¶œ-cong (āˆ˜ā‚‘ p u Ļ) tā‰”u =
    cong (_āˆ˜ _) tā‰”u
  ā¦…ā¦†į¶œ-cong (fstā‚‘ x) tā‰”u =
    cong (fst _) tā‰”u
  ā¦…ā¦†į¶œ-cong (sndā‚‘ x) tā‰”u =
    cong (snd _) tā‰”u
  ā¦…ā¦†į¶œ-cong (prodrecā‚‘ r p q A u Ļ) tā‰”u =
    cong (Ī» t ā†’ prodrec _ _ _ _ t _) tā‰”u
  ā¦…ā¦†į¶œ-cong (natrecā‚‘ p q r A z s Ļ) tā‰”u =
    cong (Ī» t ā†’ natrec _ _ _ _ _ _ t) tā‰”u
  ā¦…ā¦†į¶œ-cong (unitrecā‚‘ _ p q A u Ļ) tā‰”u =
    cong (Ī» t ā†’ unitrec _ _ _ _ t _) tā‰”u
  ā¦…ā¦†į¶œ-cong (emptyrecā‚‘ p A Ļ) tā‰”u =
    cong (emptyrec _ _) tā‰”u
  ā¦…ā¦†į¶œ-cong (Jā‚‘ p q A t B u v Ļ) tā‰”u =
    cong (J _ _ _ _ _ _ _) tā‰”u
  ā¦…ā¦†į¶œ-cong (Kā‚‘ p A t B u Ļ) tā‰”u =
    cong (K _ _ _ _ _) tā‰”u
  ā¦…ā¦†į¶œ-cong ([]-congā‚‘ s A t u Ļ) tā‰”u =
    cong ([]-cong _ _ _ _) tā‰”u
  ā¦…ā¦†į¶œ-cong sucā‚‘ tā‰”u =
    cong suc tā‰”u

opaque

  -- A congruence property for stacks

  ā¦…ā¦†Ė¢-cong : āˆ€ S ā†’ t [ Ļƒ ] ā‰” u [ Ļƒ ]
         ā†’ ā¦… S ā¦†Ė¢ t [ Ļƒ ] ā‰” ā¦… S ā¦†Ė¢ u [ Ļƒ ]
  ā¦…ā¦†Ė¢-cong Īµ tā‰”u = tā‰”u
  ā¦…ā¦†Ė¢-cong (e āˆ™ S) tā‰”u = ā¦…ā¦†Ė¢-cong S (ā¦…ā¦†į¶œ-cong e tā‰”u)

opaque

  -- Weakening of sucā‚›Ā k

  wk-sucā‚› : (Ļ : Wk m n) (k : Nat) ā†’ wkĖ¢ Ļ (sucā‚› k) ā‰” sucā‚› k
  wk-sucā‚› Ļ 0 = refl
  wk-sucā‚› Ļ (1+ k) = cong (sucā‚‘ āˆ™_) (wk-sucā‚› Ļ k)

opaque

  -- An inversion lemma for multiplicity of non-empty stacks

  āˆ£āˆ£āˆ™-inv : āˆ£ c āˆ™ S āˆ£ā‰” p ā†’ āˆƒā‚‚ Ī» q r ā†’ āˆ£ c āˆ£į¶œā‰” q Ɨ āˆ£ S āˆ£ā‰” r Ɨ p ā‰” r Ā· q
  āˆ£āˆ£āˆ™-inv (e āˆ™ S) = _ , _ , e , S , refl

opaque

  -- Continuation weakening preserves multiplicity

  wk-āˆ£āˆ£į¶œ : āˆ£ c āˆ£į¶œā‰” p ā†’ āˆ£ wkį¶œ Ļ c āˆ£į¶œā‰” p
  wk-āˆ£āˆ£į¶œ āˆ˜ā‚‘ = āˆ˜ā‚‘
  wk-āˆ£āˆ£į¶œ fstā‚‘ = fstā‚‘
  wk-āˆ£āˆ£į¶œ sndā‚‘ = sndā‚‘
  wk-āˆ£āˆ£į¶œ (natrecā‚‘ x) = natrecā‚‘ x
  wk-āˆ£āˆ£į¶œ prodrecā‚‘ = prodrecā‚‘
  wk-āˆ£āˆ£į¶œ unitrecā‚‘ = unitrecā‚‘
  wk-āˆ£āˆ£į¶œ emptyrecā‚‘ = emptyrecā‚‘
  wk-āˆ£āˆ£į¶œ (Jā‚‘ x) = Jā‚‘ x
  wk-āˆ£āˆ£į¶œ (Kā‚‘ x) = Kā‚‘ x
  wk-āˆ£āˆ£į¶œ []-congā‚‘ = []-congā‚‘
  wk-āˆ£āˆ£į¶œ sucā‚‘ = sucā‚‘

opaque

  -- Stack weakening preserves multiplicity

  wk-āˆ£āˆ£ : āˆ£ S āˆ£ā‰” p ā†’ āˆ£ wkĖ¢ Ļ S āˆ£ā‰” p
  wk-āˆ£āˆ£ Īµ = Īµ
  wk-āˆ£āˆ£ (e āˆ™ S) = wk-āˆ£āˆ£į¶œ e āˆ™ wk-āˆ£āˆ£ S

opaque

  -- The multiplicity relation for natrecā‚‘ is functional

  āˆ£natrecāˆ£į¶œ-functional :
    āˆ£natrec p , r āˆ£ā‰” q ā†’ āˆ£natrec p , r āˆ£ā‰” qā€² ā†’ q ā‰” qā€²
  āˆ£natrecāˆ£į¶œ-functional
    (has-nrā‚‘ ā¦ƒ has-nr ā¦„) (has-nrā‚‘ ā¦ƒ has-nr = has-nrā€² ā¦„) =
    case Nr-available-propositional _ has-nr has-nrā€² of Ī» where
      refl ā†’ refl
  āˆ£natrecāˆ£į¶œ-functional (has-nrā‚‘ ā¦ƒ has-nr ā¦„) (no-nrā‚‘ ā¦ƒ no-nr ā¦„ x) =
    āŠ„-elim (Ā¬[Nrāˆ§No-nr-glb] _ has-nr no-nr)
  āˆ£natrecāˆ£į¶œ-functional (no-nrā‚‘ ā¦ƒ no-nr ā¦„ x) (has-nrā‚‘ ā¦ƒ has-nr ā¦„) =
    āŠ„-elim (Ā¬[Nrāˆ§No-nr-glb] _ has-nr no-nr)
  āˆ£natrecāˆ£į¶œ-functional (no-nrā‚‘ x) (no-nrā‚‘ y) =
    GLB-unique x y

opaque

  -- The multiplicity relation for Jā‚‘ is functional

  āˆ£Jāˆ£į¶œ-functional : āˆ£J em , p , q āˆ£ā‰” r ā†’ āˆ£J em , p , q āˆ£ā‰” rā€² ā†’ r ā‰” rā€²
  āˆ£Jāˆ£į¶œ-functional J-all J-all = refl
  āˆ£Jāˆ£į¶œ-functional (J-someā‚€ _ _) (J-someā‚€ _ _) = refl
  āˆ£Jāˆ£į¶œ-functional (J-someā‚€ pā‰”šŸ˜ qā‰”šŸ˜) (J-some false) =
    āŠ„-elim (false (pā‰”šŸ˜ , qā‰”šŸ˜))
  āˆ£Jāˆ£į¶œ-functional (J-some false) (J-someā‚€ pā‰”šŸ˜ qā‰”šŸ˜) =
    āŠ„-elim (false (pā‰”šŸ˜ , qā‰”šŸ˜))
  āˆ£Jāˆ£į¶œ-functional (J-some _) (J-some _) = refl
  āˆ£Jāˆ£į¶œ-functional J-none J-none = refl

opaque

  -- The multiplicity relation for Kā‚‘ is functional

  āˆ£Kāˆ£į¶œ-functional : āˆ£K em , p āˆ£ā‰” r ā†’ āˆ£K em , p āˆ£ā‰” rā€² ā†’ r ā‰” rā€²
  āˆ£Kāˆ£į¶œ-functional K-all K-all = refl
  āˆ£Kāˆ£į¶œ-functional (K-someā‚€ _) (K-someā‚€ _) = refl
  āˆ£Kāˆ£į¶œ-functional (K-someā‚€ pā‰”šŸ˜) (K-some pā‰¢šŸ˜) =
    āŠ„-elim (pā‰¢šŸ˜ pā‰”šŸ˜)
  āˆ£Kāˆ£į¶œ-functional (K-some pā‰¢šŸ˜) (K-someā‚€ pā‰”šŸ˜) =
    āŠ„-elim (pā‰¢šŸ˜ pā‰”šŸ˜)
  āˆ£Kāˆ£į¶œ-functional (K-some _) (K-some _) = refl
  āˆ£Kāˆ£į¶œ-functional K-none K-none = refl

opaque

  -- The multiplicity relation for continuations is functional

  āˆ£āˆ£į¶œ-functional : āˆ£ c āˆ£į¶œā‰” p ā†’ āˆ£ c āˆ£į¶œā‰” q ā†’ p ā‰” q
  āˆ£āˆ£į¶œ-functional āˆ˜ā‚‘ āˆ˜ā‚‘ = refl
  āˆ£āˆ£į¶œ-functional fstā‚‘ fstā‚‘ = refl
  āˆ£āˆ£į¶œ-functional sndā‚‘ sndā‚‘ = refl
  āˆ£āˆ£į¶œ-functional prodrecā‚‘ prodrecā‚‘ = refl
  āˆ£āˆ£į¶œ-functional (natrecā‚‘ x) (natrecā‚‘ y) =
    āˆ£natrecāˆ£į¶œ-functional x y
  āˆ£āˆ£į¶œ-functional unitrecā‚‘ unitrecā‚‘ = refl
  āˆ£āˆ£į¶œ-functional emptyrecā‚‘ emptyrecā‚‘ = refl
  āˆ£āˆ£į¶œ-functional (Jā‚‘ x) (Jā‚‘ y) = āˆ£Jāˆ£į¶œ-functional x y
  āˆ£āˆ£į¶œ-functional (Kā‚‘ x) (Kā‚‘ y) = āˆ£Kāˆ£į¶œ-functional x y
  āˆ£āˆ£į¶œ-functional []-congā‚‘ []-congā‚‘ = refl
  āˆ£āˆ£į¶œ-functional sucā‚‘ sucā‚‘ = refl

opaque

  -- The multiplicity relation for stacks is functional

  āˆ£āˆ£-functional : āˆ£ S āˆ£ā‰” p ā†’ āˆ£ S āˆ£ā‰” q ā†’ p ā‰” q
  āˆ£āˆ£-functional Īµ Īµ = refl
  āˆ£āˆ£-functional (e āˆ™ S) (eā€² āˆ™ Sā€²) =
    Ā·-cong (āˆ£āˆ£-functional S Sā€²) (āˆ£āˆ£į¶œ-functional e eā€²)

opaque

  -- The multiplicity for natrecā‚‘ always exists if e is not natrecā‚‘ when
  -- the usage rule with greatest lower bounds is used.

  āˆ£nrāˆ£ā‰” : ā¦ƒ has-nr : Nr-available ā¦„ ā†’ āˆƒ Ī» q ā†’ āˆ£natrec p , r āˆ£ā‰” q
  āˆ£nrāˆ£ā‰” = _ , has-nrā‚‘

opaque

  -- The multiplicity relation for Jā‚‘ always inhabited

  āˆ£Jāˆ£ā‰” : āˆƒ Ī» r ā†’ āˆ£J em , p , q āˆ£ā‰” r
  āˆ£Jāˆ£ā‰” {em = none} = _ , J-none
  āˆ£Jāˆ£ā‰” {em = all} = _ , J-all
  āˆ£Jāˆ£ā‰” {em = some} {p} {q} =
    case is-šŸ˜? p of Ī» where
      (yes pā‰”šŸ˜) ā†’
        case is-šŸ˜? q of Ī» where
          (yes qā‰”šŸ˜) ā†’ _ , J-someā‚€ pā‰”šŸ˜ qā‰”šŸ˜
          (no qā‰¢šŸ˜) ā†’ _ , J-some Ī» (_ , qā‰”šŸ˜) ā†’ qā‰¢šŸ˜ qā‰”šŸ˜
      (no pā‰¢šŸ˜) ā†’ _ , J-some (Ī» (pā‰”šŸ˜ , _) ā†’ pā‰¢šŸ˜ pā‰”šŸ˜)

opaque

  -- The multiplicity relation for Kā‚‘ always inhabited

  āˆ£Kāˆ£ā‰” : āˆƒ Ī» r ā†’ āˆ£K em , p āˆ£ā‰” r
  āˆ£Kāˆ£ā‰” {em = none} = _ , K-none
  āˆ£Kāˆ£ā‰” {em = all} = _ , K-all
  āˆ£Kāˆ£ā‰” {em = some} {p} =
    case is-šŸ˜? p of Ī» where
      (yes pā‰”šŸ˜) ā†’ _ , K-someā‚€ pā‰”šŸ˜
      (no pā‰¢šŸ˜) ā†’ _ , K-some pā‰¢šŸ˜

opaque

  -- The multiplicity for a continuation c always exists if when c is
  -- natrecā‚‘ then the usage rule for natrec using an nr function is used.

  āˆ£āˆ£į¶œā‰” :
    (āˆ€ {n p q r A u v Ļ} ā†’ c ā‰” natrecā‚‘ {n = n} p q r A u v Ļ ā†’ Nr-available) ā†’
    āˆƒ āˆ£ c āˆ£į¶œā‰”_
  āˆ£āˆ£į¶œā‰” {c = āˆ˜ā‚‘ p u Ļ} _ = šŸ™ , āˆ˜ā‚‘
  āˆ£āˆ£į¶œā‰” {c = fstā‚‘ x} _ = šŸ™ , fstā‚‘
  āˆ£āˆ£į¶œā‰” {c = sndā‚‘ x} _ = šŸ™ , sndā‚‘
  āˆ£āˆ£į¶œā‰” {c = prodrecā‚‘ r p q A u Ļ} _ = r , prodrecā‚‘
  āˆ£āˆ£į¶œā‰” {c = natrecā‚‘ p q r A z s Ļ} has-nr =
    _ , natrecā‚‘ (āˆ£nrāˆ£ā‰” ā¦ƒ has-nr refl ā¦„ .projā‚‚)
  āˆ£āˆ£į¶œā‰” {c = unitrecā‚‘ l p q A u Ļ} _ = p , unitrecā‚‘
  āˆ£āˆ£į¶œā‰” {c = emptyrecā‚‘ p A Ļ} _ = p , emptyrecā‚‘
  āˆ£āˆ£į¶œā‰” {c = Jā‚‘ p q A t B u v Ļ} _ = _ , Jā‚‘ (āˆ£Jāˆ£ā‰” .projā‚‚)
  āˆ£āˆ£į¶œā‰” {c = Kā‚‘ p A t B u Ļ} _ = _ , Kā‚‘ (āˆ£Kāˆ£ā‰” .projā‚‚)
  āˆ£āˆ£į¶œā‰” {c = []-congā‚‘ s A t u Ļ} _ = šŸ˜ , []-congā‚‘
  āˆ£āˆ£į¶œā‰” {c = sucā‚‘} _ = šŸ™ , sucā‚‘

opaque

  -- The multiplicity relation for stacks is always inhabited is whenever
  -- the stack contains natrecā‚‘ the usage rule for natrec using nr
  -- functions is used.

  āˆ£āˆ£ā‰” : (āˆ€ {p r} ā†’ natrec p , r āˆˆ S ā†’ Nr-available) ā†’ āˆƒ āˆ£ S āˆ£ā‰”_
  āˆ£āˆ£ā‰” {S = Īµ} _ = šŸ™ , Īµ
  āˆ£āˆ£ā‰” {S = e āˆ™ S} has-nr =
    let _ , āˆ£Sāˆ£ā‰” = āˆ£āˆ£ā‰” (has-nr āˆ˜ā†’ there)
        _ , āˆ£eāˆ£ā‰” = āˆ£āˆ£į¶œā‰” Ī» { refl ā†’ has-nr here}
    in  _ , āˆ£eāˆ£ā‰” āˆ™ āˆ£Sāˆ£ā‰”

opaque

  -- A variant of the above for it assumed that the stack does not
  -- contain any occurences of natrecā‚‘.

  nrāˆ‰-āˆ£āˆ£ā‰” : (āˆ€ {p r} ā†’ Ā¬ natrec p , r āˆˆ S) ā†’ āˆƒ āˆ£ S āˆ£ā‰”_
  nrāˆ‰-āˆ£āˆ£ā‰” nrāˆ‰ = āˆ£āˆ£ā‰” (Ī» nrāˆˆ ā†’ āŠ„-elim (nrāˆ‰ nrāˆˆ))

opaque

  -- An inequality satisfied by the multiplicity of natrecā‚‘

  āˆ£natrecāˆ£ā‰¤ : āˆ£natrec p , r āˆ£ā‰” q ā†’ q ā‰¤ p + r Ā· q
  āˆ£natrecāˆ£ā‰¤ has-nrā‚‘ = nrā‚‚ā‰¤
  āˆ£natrecāˆ£ā‰¤ (no-nrā‚‘ x) = nrįµ¢-GLB-ā‰¤ x

opaque

  -- Under some conditions, the multiplicity of Jā‚‘ is Ļ‰

  āˆ£Jāˆ£ā‰”Ļ‰ :
    em ā‰¤įµ‰įµ some ā†’ (em ā‰” some ā†’ Ā¬ (p ā‰” šŸ˜ Ɨ q ā‰” šŸ˜)) ā†’
    āˆ£J em , p , q āˆ£ā‰” Ļ‰
  āˆ£Jāˆ£ā‰”Ļ‰ {(none)} _ _ = J-none
  āˆ£Jāˆ£ā‰”Ļ‰ {(all)} () _
  āˆ£Jāˆ£ā‰”Ļ‰ {(some)} _ ā‰¢šŸ˜ = J-some (ā‰¢šŸ˜ refl)

opaque

  -- Under some conditions, the multiplicity of Kā‚‘ is Ļ‰

  āˆ£Kāˆ£ā‰”Ļ‰ :
    em ā‰¤įµ‰įµ some ā†’ (em ā‰” some ā†’ p ā‰¢ šŸ˜) ā†’
    āˆ£K em , p āˆ£ā‰” Ļ‰
  āˆ£Kāˆ£ā‰”Ļ‰ {(none)} _ _ = K-none
  āˆ£Kāˆ£ā‰”Ļ‰ {(all)} () _
  āˆ£Kāˆ£ā‰”Ļ‰ {(some)} _ ā‰¢šŸ˜ = K-some (ā‰¢šŸ˜ refl)

opaque

  āˆ£sucā‚›āˆ£ā‰”šŸ™ : āˆ€ k ā†’ āˆ£ sucā‚› {m} k āˆ£ā‰” šŸ™
  āˆ£sucā‚›āˆ£ā‰”šŸ™ 0 = Īµ
  āˆ£sucā‚›āˆ£ā‰”šŸ™ (1+ k) =
    subst (āˆ£ _ āˆ™ sucā‚› k āˆ£ā‰”_) (Ā·-identityŹ³ šŸ™) (sucā‚‘ āˆ™ āˆ£sucā‚›āˆ£ā‰”šŸ™ k)

opaque

  āˆ£S++sucā‚›āˆ£ā‰”āˆ£Sāˆ£ : āˆ£ S āˆ£ā‰” p ā†’ āˆ£ S ++ sucā‚› k āˆ£ā‰” p
  āˆ£S++sucā‚›āˆ£ā‰”āˆ£Sāˆ£ Īµ = āˆ£sucā‚›āˆ£ā‰”šŸ™ _
  āˆ£S++sucā‚›āˆ£ā‰”āˆ£Sāˆ£ (e āˆ™ S) = e āˆ™ āˆ£S++sucā‚›āˆ£ā‰”āˆ£Sāˆ£ S

opaque

  -- If an erased prodrec token is on the stack then the stack
  -- multiplicity is zero (if it exists).

  prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ : āˆ£ S āˆ£ā‰” q ā†’ prodrec šŸ˜ , p āˆˆ S ā†’ q ā‰” šŸ˜
  prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ Īµ ()
  prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (prodrecā‚‘ āˆ™ āˆ£Sāˆ£ā‰”) here = Ā·-zeroŹ³ _
  prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (_ āˆ™ āˆ£Sāˆ£ā‰”) (there x) =
    trans (Ā·-congŹ³ (prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” x)) (Ā·-zeroĖ” _)

opaque

  -- If an erased unitrec token is on the stack then the stack
  -- multiplicity is zero (if it exists).

  urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ : āˆ£ S āˆ£ā‰” q ā†’ unitrec šŸ˜ āˆˆ S ā†’ q ā‰” šŸ˜
  urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ Īµ ()
  urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (unitrecā‚‘ āˆ™ āˆ£Sāˆ£ā‰”) here = Ā·-zeroŹ³ _
  urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (_ āˆ™ āˆ£Sāˆ£ā‰”) (there x) =
    trans (Ā·-congŹ³ (urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” x)) (Ā·-zeroĖ” _)

opaque

  -- If an erased emptyrec token is on the stack then the stack
  -- multiplicity is zero (if it exists).

  erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ : āˆ£ S āˆ£ā‰” q ā†’ emptyrec šŸ˜ āˆˆ S ā†’ q ā‰” šŸ˜
  erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ Īµ ()
  erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (emptyrecā‚‘ āˆ™ āˆ£Sāˆ£ā‰”) here = Ā·-zeroŹ³ _
  erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ (_ āˆ™ āˆ£Sāˆ£ā‰”) (there x) =
    trans (Ā·-congŹ³ (erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” x)) (Ā·-zeroĖ” _)

opaque

  -- Under some conditions, the stack multiplicity is šŸ˜ (if it exists).

  āˆ£āˆ£ā‰”šŸ˜ :
    āˆ£ S āˆ£ā‰” q ā†’ prodrec šŸ˜ , p āˆˆ S āŠŽ (unitrec šŸ˜ āˆˆ S) āŠŽ (emptyrec šŸ˜ āˆˆ S) ā†’
    q ā‰” šŸ˜
  āˆ£āˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” (injā‚ prā‚€āˆˆ) = prā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” prā‚€āˆˆ
  āˆ£āˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” (injā‚‚ (injā‚ urā‚€āˆˆ)) = urā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” urā‚€āˆˆ
  āˆ£āˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” (injā‚‚ (injā‚‚ erā‚€āˆˆ)) = erā‚€āˆˆā†’āˆ£Sāˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” erā‚€āˆˆ

opaque

  -- Under some conditions, the stack multiplicity is šŸ˜.

  nrāˆ‰ā†’āˆ£āˆ£ā‰”šŸ˜ :
    (āˆ€ {p r} ā†’ natrec p , r āˆˆ S ā†’ āŠ„) ā†’
    prodrec šŸ˜ , p āˆˆ S āŠŽ (unitrec šŸ˜ āˆˆ S) āŠŽ (emptyrec šŸ˜ āˆˆ S) ā†’ āˆ£ S āˆ£ā‰” šŸ˜
  nrāˆ‰ā†’āˆ£āˆ£ā‰”šŸ˜ nrāˆ‰ assumption =
    let _ , āˆ£Sāˆ£ā‰” = nrāˆ‰-āˆ£āˆ£ā‰” nrāˆ‰
    in  subst (āˆ£ _ āˆ£ā‰”_) (āˆ£āˆ£ā‰”šŸ˜ āˆ£Sāˆ£ā‰” assumption) āˆ£Sāˆ£ā‰”

opaque

  -- The multiplicity of natrecā‚‘ is not šŸ˜.

  āˆ£nrāˆ£ā‰¢šŸ˜ :
   ā¦ƒ Has-well-behaved-zero _ semiring-with-meet ā¦„ ā†’
   āˆ£natrec p , r āˆ£ā‰” q ā†’ q ā‰¢ šŸ˜
  āˆ£nrāˆ£ā‰¢šŸ˜ has-nrā‚‘ = nrā‚‚ā‰¢šŸ˜
  āˆ£nrāˆ£ā‰¢šŸ˜ (no-nrā‚‘ x) refl = šŸ˜ā‰°šŸ™ (x .projā‚ 0)

opaque

  -- If the stack multiplicity is šŸ˜ then the stack contains an erased
  -- prodrec, unitrec or emptyrec or J, K or []-cong.

  āˆ£āˆ£ā‰”šŸ˜ā†’erased-match :
    ā¦ƒ Has-well-behaved-zero _ semiring-with-meet ā¦„ ā†’
    āˆ£ S āˆ£ā‰” šŸ˜ ā†’
    (āˆƒ Ī» p ā†’ prodrec šŸ˜ , p āˆˆ S) āŠŽ (unitrec šŸ˜ āˆˆ S) āŠŽ (emptyrec šŸ˜ āˆˆ S) āŠŽ
    (āˆƒā‚‚ Ī» p q ā†’ J p , q āˆˆ S) āŠŽ (āˆƒ Ī» p ā†’ K p āˆˆ S) āŠŽ ([]-congāˆˆ S)
  āˆ£āˆ£ā‰”šŸ˜ā†’erased-match = lemma refl
    where
    thereā€² :
      (āˆƒ Ī» p ā†’ prodrec šŸ˜ , p āˆˆ S) āŠŽ (unitrec šŸ˜ āˆˆ S) āŠŽ (emptyrec šŸ˜ āˆˆ S) āŠŽ
      (āˆƒā‚‚ Ī» p q ā†’ J p , q āˆˆ S) āŠŽ (āˆƒ Ī» p ā†’ K p āˆˆ S) āŠŽ ([]-congāˆˆ S) ā†’
      (āˆƒ Ī» p ā†’ prodrec šŸ˜ , p āˆˆ (c āˆ™ S)) āŠŽ (unitrec šŸ˜ āˆˆ c āˆ™ S) āŠŽ (emptyrec šŸ˜ āˆˆ c āˆ™ S) āŠŽ
      (āˆƒā‚‚ Ī» p q ā†’ J p , q āˆˆ c āˆ™ S) āŠŽ (āˆƒ Ī» p ā†’ K p āˆˆ c āˆ™ S) āŠŽ ([]-congāˆˆ c āˆ™ S)
    thereā€² (injā‚ (_ , x)) = injā‚ (_ , there x)
    thereā€² (injā‚‚ (injā‚ x)) = injā‚‚ (injā‚ (there x))
    thereā€² (injā‚‚ (injā‚‚ (injā‚ x))) = injā‚‚ (injā‚‚ (injā‚ (there x)))
    thereā€² (injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , _ , x))))) = injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , _ , there x))))
    thereā€² (injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , x)))))) = injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , there x)))))
    thereā€² (injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ x))))) = injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (there x)))))
    hereā€² :
      q ā‰” šŸ˜ ā†’ āˆ£ c āˆ£į¶œā‰” q ā†’
      (āˆƒ Ī» p ā†’ prodrec šŸ˜ , p āˆˆ (c āˆ™ S)) āŠŽ (unitrec šŸ˜ āˆˆ c āˆ™ S) āŠŽ (emptyrec šŸ˜ āˆˆ c āˆ™ S) āŠŽ
      (āˆƒā‚‚ Ī» p q ā†’ J p , q āˆˆ c āˆ™ S) āŠŽ (āˆƒ Ī» p ā†’ K p āˆˆ c āˆ™ S) āŠŽ ([]-congāˆˆ c āˆ™ S)
    hereā€² qā‰” āˆ˜ā‚‘ = āŠ„-elim (non-trivial qā‰”)
    hereā€² qā‰” fstā‚‘ = āŠ„-elim (non-trivial qā‰”)
    hereā€² qā‰” sndā‚‘ = āŠ„-elim (non-trivial qā‰”)
    hereā€² refl prodrecā‚‘ = injā‚ (_ , here)
    hereā€² qā‰” (natrecā‚‘ x) = āŠ„-elim (āˆ£nrāˆ£ā‰¢šŸ˜ x qā‰”)
    hereā€² refl unitrecā‚‘ = injā‚‚ (injā‚ here)
    hereā€² refl emptyrecā‚‘ = injā‚‚ (injā‚‚ (injā‚ here))
    hereā€² qā‰” (Jā‚‘ x) = injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , _ , here))))
    hereā€² qā‰” (Kā‚‘ x) = injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚ (_ , here)))))
    hereā€² qā‰” []-congā‚‘ = injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ (injā‚‚ here))))
    hereā€² qā‰” sucā‚‘ = āŠ„-elim (non-trivial qā‰”)
    lemma :
      q ā‰” šŸ˜ ā†’ āˆ£ S āˆ£ā‰” q ā†’
      (āˆƒ Ī» p ā†’ prodrec šŸ˜ , p āˆˆ S) āŠŽ (unitrec šŸ˜ āˆˆ S) āŠŽ (emptyrec šŸ˜ āˆˆ S) āŠŽ
      (āˆƒā‚‚ Ī» p q ā†’ J p , q āˆˆ S) āŠŽ (āˆƒ Ī» p ā†’ K p āˆˆ S) āŠŽ ([]-congāˆˆ S)
    lemma qā‰” Īµ = āŠ„-elim (non-trivial qā‰”)
    lemma qā‰” (āˆ£eāˆ£ā‰” āˆ™ āˆ£Sāˆ£ā‰”) =
      case zero-product qā‰” of Ī» where
        (injā‚ x) ā†’ thereā€² (lemma x āˆ£Sāˆ£ā‰”)
        (injā‚‚ x) ā†’ hereā€² x āˆ£eāˆ£ā‰”

opaque

  -- If a certain greatest lower bound does not exist then the stack
  -- multiplicity does not necessarily exist.

  āˆ£āˆ£ā‰¢ :
    ā¦ƒ no-nr : Nr-not-available-GLB ā¦„ ā†’
    Ā¬ (āˆƒ Ī» q ā†’ Greatest-lower-bound q (nrįµ¢ r šŸ™ p)) ā†’
    āˆƒ Ī» (S : Stack m) ā†’ āˆ€ q ā†’ āˆ£ S āˆ£ā‰” q ā†’ āŠ„
  āˆ£āˆ£ā‰¢ {r} {p} ā¦ƒ no-nr ā¦„ Ā¬glb =
    (natrecā‚‘ p šŸ˜ r ā„• zero zero id āˆ™ Īµ) ,
    Ī» { _ (natrecā‚‘ (has-nrā‚‘ ā¦ƒ has-nr ā¦„) āˆ™ _) ā†’ Ā¬[Nrāˆ§No-nr-glb] _ has-nr no-nr
      ; _ (natrecā‚‘ (no-nrā‚‘ x) āˆ™ _) ā†’ Ā¬glb (_ , x)}

opaque

  -- Stack concatenation

  ā¦…ā¦†Ė¢++ : āˆ€ S Sā€² ā†’ ā¦… S ++ Sā€² ā¦†Ė¢ t ā‰” ā¦… Sā€² ā¦†Ė¢ (ā¦… S ā¦†Ė¢ t)
  ā¦…ā¦†Ė¢++ Īµ Sā€² = refl
  ā¦…ā¦†Ė¢++ (c āˆ™ S) Sā€² = ā¦…ā¦†Ė¢++ S Sā€²

opaque

  -- Weakening of stack concatenation

  wk-++ : (Ļ : Wk m n) (S : Stack n) ā†’ wkĖ¢ Ļ (S ++ Sā€²) ā‰” wkĖ¢ Ļ S ++ wkĖ¢ Ļ Sā€²
  wk-++ Ļ Īµ = refl
  wk-++ Ļ (c āˆ™ S) = cong (_ āˆ™_) (wk-++ Ļ S)

opaque

  -- A specialized version of the property above

  wk-++sucā‚› : (Ļ : Wk m n) (S : Stack n) ā†’ wkĖ¢ Ļ (S ++ sucā‚› k) ā‰” wkĖ¢ Ļ S ++ sucā‚› k
  wk-++sucā‚› {k} Ļ S = trans (wk-++ Ļ S) (cong (_ ++_) (wk-sucā‚› Ļ k))

opaque

  -- Concatenation of sucā‚›Ā k

  sucā‚›++sucā‚› : āˆ€ k kā€² ā†’ sucā‚› {m} k ++ sucā‚› kā€² ā‰” sucā‚› (k +āæ kā€²)
  sucā‚›++sucā‚› 0 kā€² = refl
  sucā‚›++sucā‚› (1+ k) kā€² = cong (sucā‚‘ āˆ™_) (sucā‚›++sucā‚› k kā€²)

opaque

  -- Applying a term to a continuation becomes neutral only if the
  -- term is neutral.

  ā¦…ā¦†į¶œ-neutral : āˆ€ c ā†’ Neutral (ā¦… c ā¦†į¶œ t) ā†’ Neutral t
  ā¦…ā¦†į¶œ-neutral (āˆ˜ā‚‘ p u Ļ) (āˆ˜ā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (fstā‚‘ x) (fstā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (sndā‚‘ x) (sndā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (prodrecā‚‘ r p q A u Ļ) (prodrecā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (natrecā‚‘ p q r A z s Ļ) (natrecā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (unitrecā‚‘ l p q A u Ļ) (unitrecā‚™ x n) = n
  ā¦…ā¦†į¶œ-neutral (emptyrecā‚‘ p A Ļ) (emptyrecā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (Jā‚‘ p q A t B u v Ļ) (Jā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral (Kā‚‘ p A t B u Ļ) (Kā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral ([]-congā‚‘ s A t u Ļ) ([]-congā‚™ n) = n
  ā¦…ā¦†į¶œ-neutral sucā‚‘ ()

opaque

  -- Injectivity of stacks

  stack-injective : {c : Cont m} {S : Stack m}
                  ā†’ c āˆ™ S ā‰” cā€² āˆ™ Sā€² ā†’ c ā‰” cā€² Ɨ S ā‰” Sā€²
  stack-injective refl = refl , refl

opaque

  -- Injectivity of the stack sucā‚›Ā k

  sucā‚›-injective : sucā‚› {m} n ā‰” sucā‚› nā€² ā†’ n ā‰” nā€²
  sucā‚›-injective {n = 0}    {nā€² = 0}    _ = refl
  sucā‚›-injective {n = 1+ _} {nā€² = 1+ _} x =
    cong 1+ (sucā‚›-injective (stack-injective x .projā‚‚))
  sucā‚›-injective {n = 0}    {nā€² = 1+ _} ()
  sucā‚›-injective {n = 1+ _} {nā€² = 0}    ()

------------------------------------------------------------------------
-- Properties of heap equality

opaque

  -- Heap equality is reflective

  ~Ź°-refl : H ~Ź° H
  ~Ź°-refl {H = Īµ} = Īµ
  ~Ź°-refl {H = H āˆ™ c} = ~Ź°-refl āˆ™ _
  ~Ź°-refl {H = H āˆ™ā—} = ~Ź°-refl āˆ™ā—

opaque

  -- Heap equality is symmetric

  ~Ź°-sym : H ~Ź° Hā€² ā†’ Hā€² ~Ź° H
  ~Ź°-sym Īµ = Īµ
  ~Ź°-sym (H~Hā€² āˆ™ c) = ~Ź°-sym H~Hā€² āˆ™ c
  ~Ź°-sym (H~Hā€² āˆ™ā—) = ~Ź°-sym H~Hā€² āˆ™ā—

opaque

  -- Heap equality is transitive

  ~Ź°-trans : H ~Ź° Hā€² ā†’ Hā€² ~Ź° Hā€³ ā†’ H ~Ź° Hā€³
  ~Ź°-trans Īµ Īµ = Īµ
  ~Ź°-trans (H~Hā€² āˆ™ c) (Hā€²~Hā€³ āˆ™ .c) = ~Ź°-trans H~Hā€² Hā€²~Hā€³ āˆ™ c
  ~Ź°-trans (H~Hā€² āˆ™ā—) (Hā€²~Hā€³ āˆ™ā—) = ~Ź°-trans H~Hā€² Hā€²~Hā€³ āˆ™ā—

opaque

  -- Heap lookup without update behaves the same on equal heaps

  ~Ź°-lookup : H ~Ź° Hā€² ā†’ H āŠ¢ y ā†¦ e ā†’ Hā€² āŠ¢ y ā†¦ e
  ~Ź°-lookup Īµ ()
  ~Ź°-lookup (H~Hā€² āˆ™ _) here = here
  ~Ź°-lookup (H~Hā€² āˆ™ _) (there d) = there (~Ź°-lookup H~Hā€² d)
  ~Ź°-lookup (H~Hā€² āˆ™ā—) (thereā— d) = thereā— (~Ź°-lookup H~Hā€² d)

opaque

  -- Heap lookup to ā— behaves the same on equal heaps

  ~Ź°-lookupā— : H ~Ź° Hā€² ā†’ H āŠ¢ y ā†¦ā— ā†’ Hā€² āŠ¢ y ā†¦ā—
  ~Ź°-lookupā— Īµ ()
  ~Ź°-lookupā— (H~Hā€² āˆ™ā—) here = here
  ~Ź°-lookupā— (H~Hā€² āˆ™ _) (there d) = there (~Ź°-lookupā— H~Hā€² d)
  ~Ź°-lookupā— (H~Hā€² āˆ™ā—) (thereā— d) = thereā— (~Ź°-lookupā— H~Hā€² d)

opaque

  -- Equal heaps are equal as substitutions

  ~Ź°-subst : H ~Ź° Hā€² ā†’ toSubstā‚• H ā‰” toSubstā‚• Hā€²
  ~Ź°-subst Īµ = refl
  ~Ź°-subst (H~Hā€² āˆ™ (t , Ļ)) =
    case ~Ź°-subst H~Hā€² of Ī»
      Hā‰”Hā€² ā†’
    congā‚‚ consSubst Hā‰”Hā€² (cong (wk Ļ t [_]) Hā‰”Hā€²)
  ~Ź°-subst (H~Hā€² āˆ™ā—) =
    cong liftSubst (~Ź°-subst H~Hā€²)

opaque

  -- An updated heap is equal to the original one (up to grades)

  update-~Ź° : H āŠ¢ y ā†¦[ q ] e āؾ Hā€² ā†’ H ~Ź° Hā€²
  update-~Ź° (here _) = ~Ź°-refl āˆ™ _
  update-~Ź° (there d) = update-~Ź° d āˆ™ _
  update-~Ź° (thereā— d) = update-~Ź° d āˆ™ā—

------------------------------------------------------------------------
-- Properties of states in normal form

opaque

  wk1-Normal : Normal āŸØ H , t , Ļ , S āŸ© ā†’ Normal āŸØ H āˆ™ (p , e) , t , step Ļ , wk1Ė¢ S āŸ©
  wk1-Normal (val x) = val x
  wk1-Normal (var d) = var (there d)

opaque

  wk1ā—-Normal : Normal āŸØ H , t , Ļ , S āŸ© ā†’ Normal āŸØ H āˆ™ā— , t , step Ļ , wk1Ė¢ S āŸ©
  wk1ā—-Normal (val x) = val x
  wk1ā—-Normal (var d) = var (thereā— d)

opaque

  -- The stack of a normal state can be replaced to give a normal state

  Normal-stack : Normal āŸØ H , t , Ļ , S āŸ© ā†’ Normal āŸØ H , t , Ļ , Sā€² āŸ©
  Normal-stack (val x) = val x
  Normal-stack (var x) = var x

opaque

  -- The heap of a normal state can be replaced by an equal heap and the
  -- stack can be replaced with any stack to give a normal state.

  ~Ź°-Normal : H ~Ź° Hā€² ā†’ Normal āŸØ H , t , Ļ , S āŸ© ā†’ Normal āŸØ Hā€² , t , Ļ , Sā€² āŸ©
  ~Ź°-Normal H~Hā€² (val x) = val x
  ~Ź°-Normal H~Hā€² (var x) = var (~Ź°-lookupā— H~Hā€² x)

------------------------------------------------------------------------
-- Properties of heaps as substitutions

opaque

  -- Weakenings of heaps as substitutions

  wk-[]ā‚• : Ļ āˆ· H āŠ‡Ź° Hā€² ā†’ (t : Term n) ā†’ t [ Hā€² ]ā‚• ā‰” wk Ļ t [ H ]ā‚•
  wk-[]ā‚• {H} id t = cong (_[ H ]ā‚•) (sym (wk-id t))
  wk-[]ā‚• (step Ļ) t = trans (wk-[]ā‚• Ļ t) (sym (step-consSubst t))
  wk-[]ā‚• (lift {Ļ} {H} {Hā€²} {e = u , Ļā€²} [Ļ]) t = begin
    t [ consSubst (toSubstā‚• Hā€²) (wk Ļā€² u [ Hā€² ]ā‚•) ]                     ā‰”Ė˜āŸØ singleSubstComp (wk Ļā€² u [ Hā€² ]ā‚•) (toSubstā‚• Hā€²) t āŸ©
    t [ liftSubst (toSubstā‚• Hā€²) ] [ wk Ļā€² u [ Hā€² ]ā‚• ]ā‚€                  ā‰”Ė˜āŸØ singleSubstLift t (wk Ļā€² u) āŸ©
    t [ wk Ļā€² u ]ā‚€ [ Hā€² ]ā‚•                                              ā‰”āŸØ wk-[]ā‚• [Ļ] (t [ wk Ļā€² u ]ā‚€) āŸ©
    wk Ļ (t [ wk Ļā€² u ]ā‚€) [ H ]ā‚•                                        ā‰”āŸØ cong (_[ H ]ā‚•) (wk-Ī² t) āŸ©
    wk (lift Ļ) t [ wk Ļ (wk Ļā€² u) ]ā‚€ [ H ]ā‚•                            ā‰”āŸØ cong (Ī» x ā†’ wk (lift Ļ) t [ x ]ā‚€ [ H ]ā‚•) (wk-comp Ļ Ļā€² u) āŸ©
    wk (lift Ļ) t [ wk (Ļ ā€¢ Ļā€²) u ]ā‚€ [ H ]ā‚•                             ā‰”āŸØ singleSubstLift (wk (lift Ļ) t) (wk (Ļ ā€¢ Ļā€²) u) āŸ©
    wk (lift Ļ) t [ liftSubst (toSubstā‚• H) ] [ wk (Ļ ā€¢ Ļā€²) u [ H ]ā‚• ]ā‚€  ā‰”āŸØ singleSubstComp (wk (Ļ ā€¢ Ļā€²) u [ H ]ā‚•) (toSubstā‚• H) (wk (lift Ļ) t) āŸ©
    wk (lift Ļ) t [ consSubst (toSubstā‚• H) (wk (Ļ ā€¢ Ļā€²) u [ H ]ā‚•) ]     āˆŽ

opaque

  -- A heap updated by a pointer lookup gives the same substitution
  -- as the original heap.

  heapUpdateSubst : H āŠ¢ y ā†¦[ q ] e āؾ Hā€² ā†’ toSubstā‚• H ā‰” toSubstā‚• Hā€²
  heapUpdateSubst d = ~Ź°-subst (update-~Ź° d)

opaque

  -- Erased heaps are identity substitutions

  erasedHeapā‰”idsubst : āˆ€ x ā†’ toSubstā‚• (erasedHeap n) x ā‰” idSubst x
  erasedHeapā‰”idsubst x0 = refl
  erasedHeapā‰”idsubst (x +1) = cong wk1 (erasedHeapā‰”idsubst x)

opaque

  -- A collorary to the above property

  erasedHeap-subst : āˆ€ t ā†’ t [ erasedHeap n ]ā‚• ā‰” t
  erasedHeap-subst t = trans (substVar-to-subst erasedHeapā‰”idsubst t) (subst-id t)

opaque

  -- The weakening toWkā‚•Ā H acts as an "inverse" to toSubstā‚•Ā H

  toWkā‚•-toSubstā‚•-var : (H : Heap k m) (x : Fin k)
        ā†’ toSubstā‚• H (wkVar (toWkā‚• H) x) ā‰” idSubst x
  toWkā‚•-toSubstā‚•-var Īµ ()
  toWkā‚•-toSubstā‚•-var (H āˆ™ c) x = toWkā‚•-toSubstā‚•-var H x
  toWkā‚•-toSubstā‚•-var (H āˆ™ā—) x0 = refl
  toWkā‚•-toSubstā‚•-var (H āˆ™ā—) (x +1) = cong wk1 (toWkā‚•-toSubstā‚•-var H x)

opaque

  -- The weakening toWkā‚•Ā H acts as an "inverse" to toSubstā‚•Ā H

  toWkā‚•-toSubstā‚• : (H : Heap k m) (t : Term k)
                 ā†’ wk (toWkā‚• H) t [ H ]ā‚• ā‰” t
  toWkā‚•-toSubstā‚• H t = begin
    wk (toWkā‚• H) t [ H ]ā‚•       ā‰”āŸØ subst-wk t āŸ©
    t [ toSubstā‚• H ā‚›ā€¢ toWkā‚• H ] ā‰”āŸØ substVar-to-subst (toWkā‚•-toSubstā‚•-var H) t āŸ©
    t [ idSubst ]               ā‰”āŸØ subst-id t āŸ©
    t                           āˆŽ

opaque

  -- Substituting a variable corresponding to a dummy entry

  toSubstā‚•-erased : (H : Heap k m) (y : Fin m)
                  ā†’ H āŠ¢ y ā†¦ā— ā†’ āˆƒ Ī» yā€² ā†’ toSubstā‚• H y ā‰” var yā€²
  toSubstā‚•-erased Īµ () _
  toSubstā‚•-erased (H āˆ™ c) y0 ()
  toSubstā‚•-erased (H āˆ™ c) (y +1) (there d) = toSubstā‚•-erased H y d
  toSubstā‚•-erased (H āˆ™ā—) y0 d = y0 , refl
  toSubstā‚•-erased (H āˆ™ā—) (y +1) (thereā— d) =
    case toSubstā‚•-erased H y d of Ī»
      (yā€² , ā‰”yā€²) ā†’
    yā€² +1 , cong wk1 ā‰”yā€²

opaque

  -- A term that is neutral at a variable with a dummy entry in the heap
  -- will still be neutral at the same variable after applying the heap
  -- substitution.

  toSubstā‚•-NeutralAt : (d : H āŠ¢ y ā†¦ā—)
                     ā†’ NeutralAt y t
                     ā†’ NeutralAt (toSubstā‚•-erased H y d .projā‚) (t [ H ]ā‚•)
  toSubstā‚•-NeutralAt d var with toSubstā‚•-erased _ _ d
  ā€¦ | (xā€² , ā‰”xā€²) =
    subst (NeutralAt _) (sym ā‰”xā€²) var
  toSubstā‚•-NeutralAt d (āˆ˜ā‚™ n) =
    āˆ˜ā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (fstā‚™ n) =
    fstā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (sndā‚™ n) =
    sndā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (natrecā‚™ n) =
    natrecā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (prodrecā‚™ n) =
    prodrecā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (emptyrecā‚™ n) =
    emptyrecā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (unitrecā‚™ x n) =
    unitrecā‚™ x (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (Jā‚™ n) =
    Jā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d (Kā‚™ n) =
    Kā‚™ (toSubstā‚•-NeutralAt d n)
  toSubstā‚•-NeutralAt d ([]-congā‚™ n) =
    []-congā‚™ (toSubstā‚•-NeutralAt d n)

opaque

  -- ā¦…_ā¦† is an inverse of initial.

  ā¦…initialā¦†ā‰” : ā¦… initial t ā¦† ā‰” t
  ā¦…initialā¦†ā‰” = trans (erasedHeap-subst (wk id _)) (wk-id _)