Skip to content

Commit

Permalink
SCP-2908 (#4102)
Browse files Browse the repository at this point in the history 
This PR adds the final missing CK => CEK direction of the behavioural equivalence proof: Reduction <=> CC <=> CK <=> CEK. Subject limitations described in the PR.
  • Loading branch information
@jmchapman
jmchapman committed Oct 17, 2021
1 parent 7e42d6b commit 42dcece
Show file tree
Hide file tree
Showing 2 changed files with 244 additions and 28 deletions.
260 changes: 232 additions & 28 deletions plutus-metatheory/src/Algorithmic/CEKV.lagda.md
View file
Expand Up @@ -29,7 +29,7 @@ open import Builtin
open import Utils hiding (TermCon)
open import Builtin.Constant.Type Ctx⋆ (_⊢Nf⋆ *)
open import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con
open import Data.Empty
open import Algorithmic.ReductionEC using (_<>>_∈_;start;bubble;saturated;<>>2<>>';lemma<>2;unique<>>;<>>-cancel-both;<>>-cancel-both')
Expand Down Expand Up @@ -1013,47 +1013,251 @@ postulate ival-lem : ∀ b {A}{s : CK.Stack A _} → (s CK.◅ Red.ival b) ≡ (
postulate dischargeBody-lem : ∀{A B}{Γ}{C}{s : CK.Stack A B}(M : Γ , C ⊢ _) ρ V → (s CK.▻ (dischargeBody M ρ [ CK.discharge (cek2ckVal V) ])) ≡ (s CK.▻ cek2ckClos M (ρ ∷ V))
postulate dischargeBody-lem' : ∀{B}{Γ}{C}(M : Γ , C ⊢ B) ρ V → (dischargeBody M ρ [ CK.discharge (cek2ckVal V) ]) ≡ cek2ckClos M (ρ ∷ V)
postulate discharge-lem : ∀{A}(V : Value A) → Red.deval (cek2ckVal V) ≡ discharge V
postulate dischargeBody⋆-lem : ∀{Γ K B A C}{s : CK.Stack C _}(M : Γ ,⋆ K ⊢ B) ρ → (s CK.▻ (dischargeBody⋆ M ρ [ A ]⋆)) ≡ (s CK.▻ cek2ckClos (M [ A ]⋆) ρ)
postulate dischargeBody⋆-lem' : ∀{Γ K B A}(M : Γ ,⋆ K ⊢ B) ρ → dischargeBody⋆ M ρ [ A ]⋆ ≡ (cek2ckClos (M [ A ]⋆) ρ)
postulate dischargeB-lem : ∀ {K A}{B : ∅ ,⋆ K ⊢Nf⋆ *}{C b}{as a as'}{p : as <>> Type ∷ a ∷ as' ∈ arity b}{x : BAPP b p (Π B)} (s : CK.Stack C (B [ A ]Nf)) → s CK.◅ Red.V-I b (bubble p) (Red.step⋆ p (cek2ckBAPP x)) ≡ (s CK.◅ cek2ckVal (V-I b (bubble p) (app⋆ p x refl)))
postulate dischargeB'-lem : ∀ {A}{C b}{as a as'}{p : as <>> a ∷ as' ∈ arity b}{x : BAPP b p A} (s : CK.Stack C _) → s CK.◅ Red.V-I b p (cek2ckBAPP x) ≡ (s CK.◅ cek2ckVal (V-I b p x))
postulate dischargeB-lem' : ∀ {A}{b}{as a as'}{p : as <>> a ∷ as' ∈ arity b}{x : BAPP b p A} → dischargeB x ≡ discharge (V-I b p x)
postulate dischargeB-lem'' : ∀ {A}{b}{as a as'}{p : as <>> a ∷ as' ∈ arity b}{x : BAPP b p A} → substEq Red.Value dischargeB-lem' (Red.V-I b p (cek2ckBAPP x)) ≡ cek2ckVal (V-I b p x)
-- assuming that buitins work the same way for CEK and red/CK
postulate BUILTIN-lem : ∀ b {A}{az}(p : az <>> [] ∈ arity b)(q : BAPP b p A) → Red.BUILTIN' b p (cek2ckBAPP q) ≡ cek2ckClos (BUILTIN' b p q) []
import Algorithmic.CC as CC
thm64 : ∀{A}(s s' : State A) → s -→s s' → cek2ckState s CK.-→s cek2ckState s'
thm64 s s base = CK.base
thm64 (s ; ρ ▻ ` x) s' (step* refl q) = CK.step** (CK.lemV (discharge (lookup x ρ)) (cek2ckVal (lookup x ρ)) (cek2ckStack s)) (thm64 _ s' q)
thm64 (s ; ρ ▻ ƛ L) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ (L · M)) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ Λ L) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ (L ·⋆ A)) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ wrap A B L) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ unwrap L) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ con c) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (s ; ρ ▻ ibuiltin b) s' (step* refl q) = CK.step* (ival-lem b) (thm64 _ s' q)
thm64 (s ; ρ ▻ error _) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (ε ◅ V) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 ((s , -· L ρ) ◅ V) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 ((s , (V-ƛ M ρ ·-)) ◅ V) s' (step* refl q) = CK.step*
thm65a : ∀{A}(s s' : State A) → s -→s s' → cek2ckState s CK.-→s cek2ckState s'
thm65a s s base = CK.base
thm65a (s ; ρ ▻ ` x) s' (step* refl q) = CK.step** (CK.lemV (discharge (lookup x ρ)) (cek2ckVal (lookup x ρ)) (cek2ckStack s)) (thm65a _ s' q)
thm65a (s ; ρ ▻ ƛ L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ (L · M)) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ Λ L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ (L ·⋆ A)) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ wrap A B L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ unwrap L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ con c) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (s ; ρ ▻ ibuiltin b) s' (step* refl q) = CK.step* (ival-lem b) (thm65a _ s' q)
thm65a (s ; ρ ▻ error _) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (ε ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a ((s , -· L ρ) ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a ((s , (V-ƛ M ρ ·-)) ◅ V) s' (step* refl q) = CK.step*
(dischargeBody-lem M ρ V)
(thm64 _ s' q)
thm64 ((s , (V-I⇒ b {as' = []} p x ·-)) ◅ V) s' (step* refl q) = CK.step*
(thm65a _ s' q)
thm65a ((s , (V-I⇒ b {as' = []} p x ·-)) ◅ V) s' (step* refl q) = CK.step*
(cong (cek2ckStack s CK.▻_) (BUILTIN-lem b (bubble p) (app p x V)))
(thm64 _ s' q)
thm64 ((s , (V-I⇒ b {as' = x₁ ∷ as'} p x ·-)) ◅ V) s' (step* refl q) = CK.step* (dischargeB'-lem (cek2ckStack s)) (thm64 _ s' q)
thm64 ((s , -·⋆ A) ◅ V-Λ M ρ) s' (step* refl q) = CK.step* (dischargeBody⋆-lem M ρ) (thm64 _ s' q)
thm64 ((s , -·⋆ A) ◅ V-IΠ b {as' = []} p x) s' (step* refl q) = CK.step*
(thm65a _ s' q)
thm65a ((s , (V-I⇒ b {as' = x₁ ∷ as'} p x ·-)) ◅ V) s' (step* refl q) = CK.step* (dischargeB'-lem (cek2ckStack s)) (thm65a _ s' q)
thm65a ((s , -·⋆ A) ◅ V-Λ M ρ) s' (step* refl q) = CK.step* (dischargeBody⋆-lem M ρ) (thm65a _ s' q)
thm65a ((s , -·⋆ A) ◅ V-IΠ b {as' = []} p x) s' (step* refl q) = CK.step*
(cong (cek2ckStack s CK.▻_) (BUILTIN-lem b (bubble p) (app⋆ p x refl)))
(thm64 _ s' q)
thm64 ((s , -·⋆ A) ◅ V-IΠ b {as' = x₁ ∷ as'} p x) s' (step* refl q) = CK.step* (dischargeB-lem (cek2ckStack s)) (thm64 _ s' q)
thm64 ((s , wrap-) ◅ V) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 ((s , unwrap-) ◅ V-wrap V) s' (step* refl q) = CK.step* (cong (cek2ckStack s CK.▻_) (discharge-lem V)) (CK.step** (CK.lemV _ (cek2ckVal V) (cek2ckStack s)) (thm64 _ s' q))
thm64 (□ V) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
thm64 (◆ A) s' (step* refl q) = CK.step* refl (thm64 _ s' q)
(thm65a _ s' q)
thm65a ((s , -·⋆ A) ◅ V-IΠ b {as' = x₁ ∷ as'} p x) s' (step* refl q) = CK.step* (dischargeB-lem (cek2ckStack s)) (thm65a _ s' q)
thm65a ((s , wrap-) ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a ((s , unwrap-) ◅ V-wrap V) s' (step* refl q) = CK.step* (cong (cek2ckStack s CK.▻_) (discharge-lem V)) (CK.step** (CK.lemV _ (cek2ckVal V) (cek2ckStack s)) (thm65a _ s' q))
thm65a (□ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
thm65a (◆ A) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
postulate clos-lem : ∀{A}(M : ∅ ⊢ A) → M ≡ cek2ckClos M []
lem□ : ∀{A}(W V : Value A) → □ W -→s □ V → W ≡ V
lem□ W .W base = refl
lem□ W V (step* refl p) = lem□ W V p
postulate discharge-lem' : ∀{A}{M : ∅ ⊢ A}(V : Red.Value M) → M ≡ discharge (ck2cekVal V)
postulate inv-lem : ∀{A}{M : ∅ ⊢ A}(x₁ : Red.Value M)
→ (p : M ≡ discharge (ck2cekVal x₁))
→ substEq Red.Value p x₁ ≡ cek2ckVal (ck2cekVal x₁)
-- the below lemmas/assumptions consider the case that where M is a
-- variable in M' == clos M ρ, but I am not sure if these cases ever
-- occur when the CEK machine is in value mode. This may be overkill
-- for our machine, in the textbook there is not such a clear
-- distinction between term and value mode and this analysis is needed.
-- note N cannot be a variable because if it was then the result of
-- the lookup in ρ would be a value that is then discharged which
-- couldn't be an application as applications are not values
postulate cek2ckClos-·lem : ∀{A B}{L : ∅ ⊢ A ⇒ B}{M : ∅ ⊢ A}{Γ}{ρ : Env Γ}{N : Γ ⊢ B} → L · M ≡ cek2ckClos N ρ → ∃ λ L' → ∃ λ M' → N ≡ L' · M' × L ≡ cek2ckClos L' ρ × M ≡ cek2ckClos M' ρ
-- as ƛ is a value, it can be the result of a variable lookup
postulate cek2ckClos-ƛlem : ∀{A B}{L : ∅ , A ⊢ B}{Γ}{ρ : Env Γ}{N : Γ ⊢ A ⇒ B} → (p : ƛ L ≡ cek2ckClos N ρ) → (∃ λ L' → N ≡ ƛ L' × L ≡ dischargeBody L' ρ) ⊎ ∃ λ x → N ≡ ` x × ∃ λ (p : ƛ L ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.V-ƛ L) ≡ cek2ckVal (lookup x ρ)
postulate cek2ckClos-·⋆lem : ∀{K B}{L : ∅ ⊢ Π B}{A : ∅ ⊢Nf⋆ K}{Γ}{ρ : Env Γ}{N : Γ ⊢ B [ A ]Nf} → L ·⋆ A ≡ cek2ckClos N ρ → ∃ λ L' → N ≡ L' ·⋆ A × L ≡ cek2ckClos L' ρ
postulate cek2ckClos-Λlem : ∀{K B}{L : ∅ ,⋆ K ⊢ B}{Γ}{ρ : Env Γ}{N : Γ ⊢ Π B} → (p : Λ L ≡ cek2ckClos N ρ) → (∃ λ L' → N ≡ Λ L' × L ≡ dischargeBody⋆ L' ρ) ⊎ ∃ λ x → N ≡ ` x × ∃ λ (p : Λ L ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.V-Λ L) ≡ cek2ckVal (lookup x ρ)
postulate cek2ckClos-wraplem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}{L}{Γ}{ρ : Env Γ}{N : Γ ⊢ μ A B} → (p : wrap A B L ≡ cek2ckClos N ρ) → (∃ λ L' → N ≡ wrap A B L' × L ≡ cek2ckClos L' ρ) ⊎ ∃ λ x → N ≡ ` x × ∃ λ V → ∃ λ (q : V-wrap V ≡ lookup x ρ) → discharge V ≡ L × substEq Red.Value (cong discharge q) (Red.V-wrap (cek2ckVal V)) ≡ cek2ckVal (lookup x ρ)
postulate cek2ckClos-unwraplem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}{L : ∅ ⊢ μ A B}{Γ}{ρ : Env Γ}{N : Γ ⊢ _} → (p : unwrap L ≡ cek2ckClos N ρ) → (∃ λ L' → N ≡ unwrap L' × L ≡ cek2ckClos L' ρ)
postulate cek2ckClos-conlem : ∀{tc : TyCon ∅}(c : TermCon (con tc)){Γ}{M' : Γ ⊢ con tc}{ρ : Env Γ} → con c ≡ cek2ckClos M' ρ → M' ≡ con c ⊎ ∃ λ x → M' ≡ ` x × V-con c ≡ lookup x ρ
postulate cek2ckClos-ibuiltinlem : ∀{b}{Γ}{M' : Γ ⊢ itype b}{ρ : Env Γ} → ibuiltin b ≡ cek2ckClos M' ρ → (M' ≡ ibuiltin b × ∃ λ p → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (ival b)) ⊎ ∃ λ x → M' ≡ ` x × ∃ λ (p : ibuiltin b ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (lookup x ρ)
cek2ckStack-εlem : ∀{A}(s : Stack A A) → CK.ε ≡ cek2ckStack s → s ≡ ε
cek2ckStack-εlem ε p = refl
cek2ckStack-εlem (s , f) ()
cek2ckStack-,lem : ∀{A B C}(s : CK.Stack A B)(s' : Stack A C)(f : Red.Frame B C)
→ s CK., f ≡ cek2ckStack s' →
∃ λ (s'' : Stack A B) → ∃ λ (f' : Frame B C) → s' ≡ (s'' Stack., f')
× s ≡ cek2ckStack s'' × f ≡ cek2ckFrame f'
cek2ckStack-,lem _ (s' , f) _ refl =
_ ,, _ ,, refl ,, refl ,, refl
cek2ckFrame-·-lem : ∀{A B} f {M : ∅ ⊢ A ⇒ B}(W : Red.Value M)
→ W Red.·- ≡ cek2ckFrame f →
∃ λ W' → f ≡ (W' ·-) × ∃ λ (p : M ≡ discharge W') → substEq Red.Value p W ≡ cek2ckVal W'
cek2ckFrame-·-lem (x ·-) .(cek2ckVal x) refl = _ ,, refl ,, refl ,, refl
postulate cek2ckFrame--·lem : ∀{A B}(f : Frame B (A ⇒ B)){M : ∅ ⊢ A} → (Red.-· M) ≡ cek2ckFrame f → ∃ λ Γ → ∃ λ (M' : Γ ⊢ A) → ∃ λ (ρ : Env Γ) → f ≡ (-· M' ρ) × M ≡ cek2ckClos M' ρ
postulate cek2ckFrame--·⋆lem : ∀{K A}{B : ∅ ,⋆ K ⊢Nf⋆ *}(f : Frame (B [ A ]Nf) (Π B)) → Red.-·⋆ A ≡ cek2ckFrame f → f ≡ -·⋆ A
postulate cek2ckFrame-unwrap-lem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}(f : Frame _ (μ A B)) → Red.unwrap- {A = A}{B = B} ≡ cek2ckFrame f → f ≡ unwrap-
postulate cek2ckFrame-wrap-lem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}(f : Frame (μ A B) _) → Red.wrap- {A = A}{B = B} ≡ cek2ckFrame f → f ≡ wrap-
thm65bV : ∀{A B}{L : ∅ ⊢ A}{M}{s : CK.Stack A B}{V : Red.Value L}
{W : Red.Value M}{W'}{s'}
→ (p : M ≡ discharge W')
→ substEq Red.Value p W ≡ cek2ckVal W'
→ s ≡ cek2ckStack s'
→ (s CK.◅ W) CK.-→s CK.□ V
→ ∃ λ V' → ((s' ◅ W') -→s □ V') × ∃ λ p → cek2ckVal V' ≡ substEq Red.Value p V
substLem : {A : Set}(P : A → Set){a a' : A}(p q : a ≡ a')(x : P a) →
substEq P p x ≡ substEq P q x
substLem P refl refl x = refl
postulate fast-forward : ∀{A B}(s : CK.Stack A B)(s' : CK.State A)(M : ∅ ⊢ B)
→ (V : Red.Value M)
→ (s CK.▻ M) CK.-→s s' → (s CK.◅ V) CK.-→s s'
{-# TERMINATING #-}
-- this is needed as in the wrap case we fast-forward the CK machine state
-- and recurse on something which is quite a bit shorter
thm65b : ∀{A B}{L : ∅ ⊢ A}{Γ M}{s : CK.Stack A B}{V : Red.Value L}
{M'}{ρ : Env Γ}{s'}
→ M ≡ cek2ckClos M' ρ
→ s ≡ cek2ckStack s'
→ (s CK.▻ M) CK.-→s CK.□ V
→ ∃ λ V' → ((s' ; ρ ▻ M') -→s □ V') × ∃ λ p → cek2ckVal V' ≡ substEq Red.Value p V
thm65b {M = ƛ M} {s = s} {M' = N} {ρ} {s'} p q (CK.step* refl r)
with cek2ckClos-ƛlem {ρ = ρ}{N = N} p
thm65b {M = ƛ M} {s = s} {M' = N} {ρ} {s'} refl q (CK.step* refl r) | inj₁ (L' ,, refl ,, z) with thm65bV refl refl q r
... | V ,, r' ,, y ,, y' = V ,, step* refl r' ,, y ,, y'
thm65b {Γ = _} {ƛ M} {s = s} {M' = .(` x)} {ρ} {s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y' ,, y'') with thm65bV p (trans (substLem Red.Value p y' _) y'') q r
... | V ,, r' ,, y ,, y' = V ,, step* refl r' ,, y ,, y'
thm65b {M = L · M} {s = s} {M' = N}{ρ}{s'} p q (CK.step* refl r)
with cek2ckClos-·lem {ρ = ρ}{N = N} p
... | L' ,, M' ,, refl ,, Lp ,, refl
with thm65b Lp (cong (CK._, (Red.-· M)) q) r
... | x ,, y ,, z ,, z' = x ,, step* refl y ,, z ,, z'
thm65b {M = Λ M} {s = s}{M' = N}{ρ}{s'} p q (CK.step* refl r)
with cek2ckClos-Λlem {ρ = ρ}{N = N} p
thm65b {M' = .(Λ L')} {ρ} {s'} refl q (CK.step* refl r) | inj₁ (L' ,, refl ,, z) with thm65bV refl refl q r
... | V ,, r' ,, y ,, y' = V ,, step* refl r' ,, y ,, y'
thm65b {M = Λ M} {s = s}{M' = N}{ρ}{s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y' ,, y'') with thm65bV p (trans (substLem Red.Value p y' _) y'') q r
... | V ,, r' ,, y ,, y' = V ,, step* refl r' ,, y ,, y'
thm65b {M = M ·⋆ A} {s = s}{M' = N}{ρ}{s' = s'} p q (CK.step* refl r)
with cek2ckClos-·⋆lem {ρ = ρ}{N = N} p
... | L' ,, refl ,, y'
with thm65b y' (cong (CK._, (Red.-·⋆ A)) q) r
... | x ,, y ,, z ,, z' = x ,, step* refl y ,, z ,, z'
thm65b {M = wrap A B M} {s = s}{M' = N}{ρ}{s' = s'} p q (CK.step* refl r)
with cek2ckClos-wraplem {ρ = ρ}{N = N} p
thm65b {M = wrap A B M} {s = s}{M' = N}{ρ}{s' = s'} p refl r | inj₂ (x ,, refl ,, W ,, y1 ,, refl ,, y3) with thm65bV (cong discharge y1) y3 refl (fast-forward _ _ _ (cek2ckVal (V-wrap W)) r)
... | V ,, r' ,, z ,, z' = V ,, step* refl r' ,, z ,, z'
thm65b {Γ = _} {wrap _ _ .(cek2ckClos V ρ)} {s = s} {M' = .(wrap _ _ V)} {ρ} {s' = s'} refl refl (CK.step* refl r) | inj₁ (V ,, refl ,, y) with thm65b refl refl r
... | x ,, y ,, z ,, z' = x ,, step* refl y ,, z ,, z'
thm65b {M = unwrap M} {s = s}{M' = N}{ρ = ρ} {s' = s'} p q (CK.step* refl r)
with cek2ckClos-unwraplem {ρ = ρ}{N = N} p
... | L' ,, refl ,, x2 with thm65b x2 (cong (CK._, Red.unwrap-) q) r
... | V' ,, r' ,, y1 ,, y2 = _ ,, step* refl r' ,, y1 ,, y2
thm65b {M = con c}{s = s}{M' = M'}{ρ = ρ}{s' = s'} p q (CK.step* refl r)
with thm65bV refl refl q r
... | W ,, r' ,, x1 ,, x2
with cek2ckClos-conlem c {M' = M'}{ρ = ρ} p
... | inj₁ refl = _ ,, step* refl r' ,, x1 ,, x2
... | inj₂ (var ,, refl ,, y2) = _ ,, step* (cong (s' ◅_) (sym y2)) r' ,, x1 ,, x2
thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r)
with cek2ckClos-ibuiltinlem {M' = N}{ρ = ρ} p
thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y2 ,, y3) with thm65bV y2 y3 q r
... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₁ (refl ,, x1 ,, x2)
with thm65bV x1 x2 q r
... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
thm65b {M = error _} {s = s} {s' = s'} p q (CK.step* refl r) = ⊥-elim (CK.lem◆' _ r)
thm65bV {s = CK.ε} {W = W} {s' = s'} refl refl r (CK.step* refl x)
rewrite cek2ckStack-εlem s' r
with CK.lem□ _ _ x
... | refl ,, refl = _ ,, step* refl base ,, refl ,, refl
thm65bV {s = s CK., (Red.-· x₁)} {W = W} {s' = s'} refl refl r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | _ ,, _ ,, refl ,, refl ,, z1
with cek2ckFrame--·lem _ z1
... | Γ ,, M' ,, ρ ,, refl ,, z2
with thm65b z2 refl x
... | _ ,, x' ,, refl ,, refl = _ ,, step* refl x' ,, refl ,, refl
thm65bV {s = s CK., (x₁ Red.·-)} {W = W} {s' = s'} p q r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | _ ,, _ ,, refl ,, refl ,, z1
with cek2ckFrame-·-lem _ _ z1
thm65bV {M = _} {.(cek2ckStack fst) CK., (.(cek2ckVal (V-ƛ M x₁)) Red.·-)} {W = W} {_} {.(fst , (V-ƛ M x₁ ·-))} refl refl r (CK.step* refl x) | fst ,, .(V-ƛ M x₁ ·-) ,, refl ,, refl ,, z1 | V-ƛ M x₁ ,, refl ,, refl ,, refl
with thm65b (dischargeBody-lem' M x₁ _) refl x
... | V'' ,, x' ,, refl ,, refl = _ ,, step* refl x' ,, refl ,, refl
thm65bV {M = _} {.(cek2ckStack fst) CK., (.(cek2ckVal (V-I⇒ b p₁ x₁)) Red.·-)} {W = W} {_} {.(fst , (V-I⇒ b p₁ x₁ ·-))} refl refl r (CK.step* refl x) | fst ,, .(V-I⇒ b p₁ x₁ ·-) ,, refl ,, refl ,, z1 | V-I⇒ b {as' = []} p₁ x₁ ,, refl ,, refl ,, refl with thm65b (BUILTIN-lem b (bubble p₁) (app p₁ x₁ _)) refl x
... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
thm65bV {M = _} {.(cek2ckStack fst) CK., (.(cek2ckVal (V-I⇒ b p₁ x₁)) Red.·-)} {W = W} {_} {.(fst , (V-I⇒ b p₁ x₁ ·-))} refl refl r (CK.step* refl x) | fst ,, .(V-I⇒ b p₁ x₁ ·-) ,, refl ,, refl ,, z1 | V-I⇒ b {as' = x₂ ∷ as'} p₁ x₁ ,, refl ,, refl ,, refl with thm65bV dischargeB-lem' dischargeB-lem'' refl x
... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
thm65bV {s = s CK., Red.-·⋆ A} {W = .(cek2ckVal (V-Λ M x₁))} {V-Λ M x₁} {s' = s'} refl refl r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | x1 ,, x2 ,, refl ,, z0 ,, z1
with thm65b {M' = M [ A ]⋆}{ρ = x₁} (dischargeBody⋆-lem' M x₁) z0 x
... | f ,, x' ,, refl ,, z2
with cek2ckFrame--·⋆lem x2 z1
... | refl = _ ,, step* refl x' ,, refl ,, z2
thm65bV {s = s CK., Red.-·⋆ A} {W = .(cek2ckVal (V-IΠ b p x₁))} {V-IΠ b {as' = []} p x₁} {s' = s'} refl refl r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | x1 ,, x2 ,, refl ,, z0 ,, z1
with cek2ckFrame--·⋆lem x2 z1
... | refl
with thm65b (BUILTIN-lem b (bubble p) (app⋆ p x₁ refl)) z0 x
... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
thm65bV {s = s CK., Red.-·⋆ A} {W = .(cek2ckVal (V-IΠ b p x₁))} {V-IΠ b {as' = x₂ ∷ as'} p x₁} {s' = s'} refl refl r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | x1 ,, x2 ,, refl ,, z0 ,, z1
with cek2ckFrame--·⋆lem x2 z1
... | refl with thm65bV (dischargeB-lem' {b = b}{x = app⋆ p x₁ refl}) dischargeB-lem'' z0 x
... | V' ,, x' ,, y1 ,, y2 = V' ,, step* refl x' ,, y1 ,, y2
thm65bV {s = s CK., Red.wrap- } {W = W} {s' = s'} refl q r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
... | s' ,, f' ,, refl ,, x2 ,, x3
with cek2ckFrame-wrap-lem _ x3
... | refl with thm65bV refl (cong Red.V-wrap q) x2 x
... | _ ,, x' ,, _ ,, y1 = _ ,, step* refl x' ,, _ ,, y1
thm65bV {s = s CK., Red.unwrap- } {W = W} {s' = s'} p q r (CK.step* refl x)
with cek2ckStack-,lem _ _ _ r
thm65bV {M = wrap _ _ M} {.(cek2ckStack s') CK., Red.unwrap- } {W = Red.V-wrap W} {W' = V-wrap W'} refl refl r (CK.step* refl x) | s' ,, f' ,, refl ,, refl ,, x3
with thm65bV refl refl refl (fast-forward (cek2ckStack s') (CK.□ _) (Red.deval (cek2ckVal W')) (cek2ckVal W') x)
... | _ ,, x' ,, _ ,, y1
with cek2ckFrame-unwrap-lem _ x3
thm65bV {L = _} {.(wrap _ _ _)} {.(cek2ckStack s') CK., Red.unwrap- } {_} {Red.V-wrap W} {V-wrap W'} {.(s' , unwrap-)} p q r (CK.step* refl x) | s' ,, .unwrap- ,, refl ,, refl ,, x1 | _ ,, x' ,, _ ,, y1 | refl = _ ,, step* refl x' ,, _ ,, y1

0 comments on commit 42dcece

Please sign in to comment.