a more general version of unwind

IntersectMBO · Apr 8, 2021 · 905036d · 905036d
1 parent e1c7635
commit 905036d
Showing 1 changed file with 36 additions and 63 deletions.
diff --git a/plutus-metatheory/src/Type/CC.lagda.md b/plutus-metatheory/src/Type/CC.lagda.md
@@ -13,11 +13,11 @@ module Type.CC where
 open import Type
 open import Type.RenamingSubstitution
 open import Type.ReductionC hiding (step)
-
-open import Data.Product
 ```
 
 ```
+open import Data.Product
+open import Data.Empty
 open import Relation.Binary.PropositionalEquality renaming ([_] to I[_])
 open import Data.Sum
 
@@ -147,7 +147,6 @@ subst-step* : {s : State K J}{s' : State K J'}{s'' : State K I}
         → s -→s s''
 subst-step* refl q = q
 
-
 stepV·r-lem : ∀(E : EvalCtx K J) B {A : ∅ ,⋆ K' ⊢⋆ J}(V : Value⋆ B) → 
   stepV V (dissect (extendEvalCtx E (V-ƛ A ·-))) ≡ (J , E ▻ (A [ B ]))
 stepV·r-lem E B {A} V rewrite lemma E (V-ƛ A ·-) = refl
@@ -238,74 +237,48 @@ lem62 A B E (μl E' C) refl = step*
 lem-→⋆ : (A B : ∅ ⊢⋆ J)(E : EvalCtx K J) → A —→⋆ B → (E ▻ A) -→s (E ▻ B)
 lem-→⋆ (ƛ A · B) ._ E (β-ƛ V) = step* refl (step* refl (step* (stepV·l-lem E B (V-ƛ A) ) (step** (lemV B V (extendEvalCtx E (V-ƛ A ·-))) (step* (stepV·r-lem E B V) base))))
 
-open import Data.Empty
-
 -- I think this would be structurally recurisve on the depth of the
 -- EvalCtx. dissect (which rips out the inner frame) reduces this by
 -- one every time. The termination checker cannot see that the call to
 -- dissect returns an E' that is smaller than E.
 
 {-# TERMINATING #-}
-unwindV : (A : ∅ ⊢⋆ J)(VA : Value⋆ A)(A' : ∅ ⊢⋆ K)(E : EvalCtx K J)
-  → A' ≡ closeEvalCtx E A → (V : Value⋆ A') → (E ◅ VA) -→s ([] ◅ V)
-unwindV A VA A' E p V with dissect' E | inspect dissect' E
-unwindV A VA A' E refl V | inj₁ (refl , refl) | I[ eq ]
-  rewrite val-unique VA V
-  = base 
-unwindV A VA A' E p V | inj₂ (I , E'  , (-· B)) | I[ eq ]
-  rewrite dissect-lemma E E' (-· B) eq
-  = ⊥-elim (lemV· (lem0 _ E' (subst Value⋆ (trans p (closeEF E' (-· B) A)) V)))
-... | inj₂ (I , E'  , (W ·-)) | I[ eq ]
-  rewrite dissect-lemma E E' (W ·-) eq
-  = ⊥-elim (lemV· (lem0 _ E' (subst Value⋆ (trans p (closeEF E' (W ·-) A)) V)))
-... | inj₂ (.* , E' , (-⇒ B)) | I[ eq ]
-  rewrite dissect-lemma E E' (-⇒ B) eq with decVal B
-... | inj₁ VB  = step*
-  (cong (stepV VA) (lemma E' (-⇒ B)))
-  (step**
-    (lemV B VB (extendEvalCtx E' (VA ⇒-)))
-    (step*
-      (cong (stepV VB) (lemma E' (VA ⇒-)))
-      (unwindV _ (VA V-⇒ VB) A' E' (trans p (closeEF E' (-⇒ B) A)) V)))
-... | inj₂ ¬VB = ⊥-elim (¬VB VB)
-  where X : A' ≡ closeEvalCtx (extendEvalCtx E' (VA ⇒-)) B
-        X = trans (trans p (closeEF E' (-⇒ B) A)) (sym (closeEF E' (VA ⇒-) B))
-        VB : Value⋆ B
-        VB = lem0 B (extendEvalCtx E' (VA ⇒-)) (subst Value⋆ X V)
-unwindV A VA A' E p V | inj₂ (.* , E' , (W ⇒-)) | I[ eq ]
-  rewrite dissect-lemma E E' (W ⇒-) eq = step*
-  (cong (stepV VA) (lemma E' (W ⇒-)))
-  (unwindV _ (W V-⇒ VA) A' E' (trans p (closeEF E' (W ⇒-) A)) V)
-unwindV A VA A' E p V | inj₂ (.* , E' , (μ- B)) | I[ eq ]
-  rewrite dissect-lemma E E' (μ- B) eq with decVal B
-... | inj₁ VB  = step*
-  (cong (stepV VA) (lemma E' (μ- B)))
-  (step**
-    (lemV B VB _)
-    (step* (cong (stepV VB) (lemma E' (μ VA -)))
-    (unwindV _ (V-μ VA VB) A' E' (trans p (closeEF E' (μ- B) A)) V)))
-... | inj₂ ¬VB = ⊥-elim (¬VB VB)
-  where X : A' ≡ closeEvalCtx (extendEvalCtx E' (μ VA -)) B
-        X = trans (trans p (closeEF E' (μ- B) A)) (sym (closeEF E' (μ VA -) B))
-        VB : Value⋆ B
-        VB = lem0 B (extendEvalCtx E' (μ VA -)) (subst Value⋆ X V)
-
-unwindV A VA A' E p V | inj₂ (.* , E' , μ W -) | I[ eq ]
-  rewrite dissect-lemma E E' (μ W -) eq
-  = step* (cong (stepV VA) (lemma E' (μ W -)))
-          (unwindV _ (V-μ W VA) A' E' (trans p (closeEF E' (μ W -) A)) V)
+unwindVE : (A : ∅ ⊢⋆ I)(B : ∅ ⊢⋆ J)(E : EvalCtx K J)(E' : EvalCtx J I)
+      → B ≡ closeEvalCtx E' A
+      → (VA : Value⋆ A)
+      → (VB : Value⋆ B)
+      → (compEvalCtx E E' ◅ VA) -→s (E ◅ VB) 
+unwindVE A B E E' p VA VB with dissect' E' | inspect dissect' E'
+unwindVE A B E E' refl VA VB | inj₁ (refl , refl) | I[ eq ] rewrite compEvalCtx-eq E [] rewrite val-unique VA VB = base
+... | inj₂ (I , E'' , (-· C)) | I[ eq ] rewrite dissect-lemma E' E'' (-· C) eq =
+  ⊥-elim (lemV· (lem0 _ E'' (subst Value⋆ (trans p (closeEF E'' (-· C) A)) VB)))
+... | inj₂ (I , E'' , (V ·-)) | I[ eq ] rewrite dissect-lemma E' E'' (V ·-) eq =
+  ⊥-elim (lemV· (lem0 _ E'' (subst Value⋆ (trans p (closeEF E'' (V ·-) A)) VB)))
+unwindVE A B E E' refl VA VB | inj₂ (.* , E'' , (-⇒ C)) | I[ eq ] rewrite dissect-lemma E' E'' (-⇒ C) eq with decVal C
+... | inj₁ VC  = step*
+  (cong (stepV VA) (trans (cong dissect (compEF' E E'' (-⇒ C))) (lemma (compEvalCtx E E'') (-⇒ C))))
+  (step** (lemV C VC (extendEvalCtx (compEvalCtx E E'') (VA ⇒-)))
+          (step* (cong (stepV VC) (lemma (compEvalCtx E E'') (VA ⇒-))) (unwindVE _ _ E E'' (closeEF E'' (-⇒ C) A) (VA V-⇒ VC) VB)))
+... | inj₂ ¬VC = ⊥-elim (¬VC (lem0 C (extendEvalCtx E'' (VA ⇒-)) (subst Value⋆ (trans (closeEF E'' (-⇒ C) A) (sym (closeEF E'' (VA ⇒-) C))) VB)))
+unwindVE A B E E' refl VA VB | inj₂ (.* , E'' , (V ⇒-)) | I[ eq ] rewrite dissect-lemma E' E'' (V ⇒-) eq = step* (cong (stepV VA) (trans (cong dissect (compEF' E E'' (V ⇒-))) (lemma (compEvalCtx E E'') (V ⇒-)))) (unwindVE _ _ E E'' (closeEF E'' (V ⇒-) A) (V V-⇒ VA) VB)
+unwindVE A B E E' refl VA VB | inj₂ (.* , E'' , (μ- C)) | I[ eq ] rewrite dissect-lemma E' E'' (μ- C) eq with decVal C
+... | inj₁ VC  = step* (cong (stepV VA) (trans (cong dissect (compEF' E E'' (μ- C))) (lemma (compEvalCtx E E'') (μ- C)))) (step** (lemV C VC (extendEvalCtx (compEvalCtx E E'') (μ VA -))) (step* (cong (stepV VC) (lemma (compEvalCtx E E'') (μ VA -))) (unwindVE _ _ E E'' (closeEF E'' (μ- C) A) (V-μ VA VC) VB)))
+... | inj₂ ¬VC = ⊥-elim (¬VC (lem0 C (extendEvalCtx E'' (μ VA -)) (subst Value⋆ (trans (closeEF E'' (μ- C) A) (sym (closeEF E'' (μ VA -) C))) VB)))
+unwindVE A B E E' refl VA VB | inj₂ (.* , E'' , μ V -) | I[ eq ] rewrite dissect-lemma E' E'' (μ V -) eq = step* (cong (stepV VA) (trans (cong dissect (compEF' E E'' (μ V -))) (lemma (compEvalCtx E E'') (μ V -)))) (unwindVE _ _ E E'' (closeEF E'' (μ V -) A) (V-μ V VA) VB)
+
+unwindE : (A : ∅ ⊢⋆ I)(B : ∅ ⊢⋆ J)(E : EvalCtx K J)(E' : EvalCtx J I)
+      → B ≡ closeEvalCtx E' A
+      → (VB : Value⋆ B)
+      → (compEvalCtx' E E' ▻ A) -→s (E ◅ VB) 
+unwindE A B E E' refl VB = step**
+  (subst-step* (cong (λ E → _ , (E ▻ A)) (sym (compEvalCtx-eq E E')))
+               (lemV A (lem0 A E' VB) (compEvalCtx E E')))
+               (unwindVE A B E E' refl (lem0 A E' VB) VB)
 
 unwind : (A : ∅ ⊢⋆ J)(A' : ∅ ⊢⋆ K)(E : EvalCtx K J) → A' ≡ closeEvalCtx E A → (V : Value⋆ A') → (E ▻ A) -→s ([] ◅ V)
-unwind A A' E p VA' = step** (lemV A VA E) (unwindV A VA A' E p VA')
-  where VA = lem0 A E (subst Value⋆ p VA')
-
--- this is a counterpart to lem62 and a stronger version of unwind
--- I expect the proof would be similar to that of unwind
-postulate
-  unwindE : (A : ∅ ⊢⋆ I)(B : ∅ ⊢⋆ J)(E : EvalCtx K J)(E' : EvalCtx J I)
-      → B ≡ closeEvalCtx E' A
-      → Value⋆ B
-      → (compEvalCtx' E E' ▻ A) -→s (E ▻ B) 
+unwind A A' E p VA' = subst-step*
+  (cong (λ E → _ , E ▻ A) (compEvalCtx-eq [] E))
+  (unwindE A A' [] E p VA')
 
 β-lem : A ≡ ƛ A' · B' → A —→⋆ B → B ≡ A' [ B' ]
 β-lem refl (β-ƛ x) = refl