notboth for inductive eval ctx closure/factoring

plutus-metatheory/src/Type/ReductionC.lagda.md

@@ -211,15 +211,15 @@ variables in the empty context.
 progress⋆ : (A : ∅ ⊢⋆ K) → Progress⋆ A
 progress⋆ (` ())
 progress⋆ (μ A B) with progress⋆ A
-... | step p  = step (contextRule (μl [] B) p (~μl A A B [] (~[] A)) (~μl _ _ B [] (~[] _)))
+... | step p = step (contextRule (μl [] B) p (~μl A A B [] (~[] A)) (~μl _ _ B [] (~[] _)))
 ... | done VA with progress⋆ B
-... | step p  = step (contextRule (μr VA []) p (~μr B A VA [] B (~[] B)) (~μr _ A VA [] _ (~[] _)))
+... | step p = step (contextRule (μr VA []) p (~μr B A VA [] B (~[] B)) (~μr _ A VA [] _ (~[] _)))
 ... | done VB = done (V-μ VA VB)
 progress⋆ (Π A) = done (V-Π A)
 progress⋆ (A ⇒ B) with progress⋆ A
 ... | step p = step (contextRule ([] l⇒ B) p (~l⇒ A A B [] (~[] A)) (~l⇒ _ _ _ [] (~[] _)))
 ... | done VA with progress⋆ B
-... | step q  = step (contextRule (VA ⇒r []) q (~⇒r B _ VA [] B (~[] B)) (~⇒r _ A VA [] _ (~[] _)))
+... | step q = step (contextRule (VA ⇒r []) q (~⇒r B _ VA [] B (~[] B)) (~⇒r _ A VA [] _ (~[] _)))
 ... | done VB = done (VA V-⇒ VB)
 progress⋆ (ƛ A) = done (V-ƛ A)
 progress⋆ (A · B) with progress⋆ A
@@ -237,7 +237,23 @@ progress⋆ (con tcn) = done (V-con tcn)
 A type is a value or it can make a step, but not both:
 
 ```
---notboth : (A : ∅ ⊢⋆ K) → ¬ (Value⋆ A × (Σ (∅ ⊢⋆ K) (A —→⋆_)))
+lem0 : ∀ A B (E : EvalCtx K J) → B ~ E ⟦ A ⟧ → Value⋆ B → Value⋆ A
+lem0 A .A [] (~[] .A) V = V
+lem0 A .(_ · B) (x ·r E) (~·r .A .x B .E p) ()
+lem0 A .(A₁ · x) (E l· x) (~l· .A A₁ .x .E p) ()
+lem0 A .(_ ⇒ B) (x ⇒r E) (~⇒r .A _ .x .E B p) (V V-⇒ W) = lem0 A B E p W
+lem0 A .(A₁ ⇒ x) (E l⇒ x) (~l⇒ .A A₁ .x .E p) (V V-⇒ W) = lem0 A _ E p V
+lem0 A .(μ _ B) (μr x E) (~μr .A _ .x .E B p) (V-μ V W) = lem0 A B E p W
+lem0 A .(μ A₁ B₁) (μl E B₁) (~μl .A A₁ .B₁ .E p) (V-μ V W) = lem0 A _ E p V
+
+notboth : (A : ∅ ⊢⋆ K) → ¬ (Value⋆ A × (Σ (∅ ⊢⋆ K) (A —→⋆_)))
+notboth A (V , A' , contextRule [] p (~[] .A) (~[] .A')) = notboth A (V , A' , p)
+notboth .(_ · B) (() , .(_ · B₁) , contextRule (x₂ ·r E) p (~·r _ .x₂ B .E x) (~·r _ .x₂ B₁ .E x₁))
+notboth .(A · x₂) (() , .(A₁ · x₂) , contextRule (E l· x₂) p (~l· _ A .x₂ .E x) (~l· _ A₁ .x₂ .E x₁))
+notboth .(_ ⇒ B) ((V V-⇒ W) , .(_ ⇒ B₁) , contextRule (x₂ ⇒r E) p (~⇒r _ _ .x₂ .E B x) (~⇒r _ _ .x₂ .E B₁ x₁)) = notboth _ (W , _ , contextRule E p x x₁)
+notboth .(A ⇒ x₂) (V V-⇒ W , .(A₁ ⇒ x₂) , contextRule (E l⇒ x₂) p (~l⇒ _ A .x₂ .E x) (~l⇒ _ A₁ .x₂ .E x₁)) = notboth _ (V , _ , contextRule E p x x₁)
+notboth .(μ _ B) (V-μ V W , .(μ _ B₁) , contextRule (μr x₂ E) p (~μr _ _ .x₂ .E B x) (~μr _ _ .x₂ .E B₁ x₁)) = notboth _ (W , _ , contextRule E p x x₁)
+notboth .(μ A B) (V-μ V W , .(μ A₁ B) , contextRule (μl E B) p (~μl _ A .B .E x) (~μl _ A₁ .B .E x₁)) = notboth _ (V , _ , contextRule E p x x₁)
 ```
 
 Reduction is deterministic. There is only one possible reduction step