diff --git a/plutus-metatheory/src/Algorithmic.lagda b/plutus-metatheory/src/Algorithmic.lagda index 9d68a26f4b7..9ab3e9fac58 100644 --- a/plutus-metatheory/src/Algorithmic.lagda +++ b/plutus-metatheory/src/Algorithmic.lagda @@ -240,27 +240,30 @@ data _⊢_ (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where → Γ ⊢ C constr : ∀{n} - → (i : Fin n) -- The tag + → (i : Fin n) -- The tag - → (A : Vec (List (Φ ⊢Nf⋆ *)) n) -- The sum of products. We make it a Vector - -- of lists, so that the tag is statically correct. + → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) -- The types of the sum of products. + -- We make it a Vector of lists, so that + -- the tag is statically correct. + -- We use the name `Tss` as it stands for a + -- a container of containers of types. - → ∀ {ts} → ts ≡ lookup A i -- The reason to define it like this, rather than - → ConstrArgs Γ ts -- simply ConstrArgs Γ (lookup A e) - -- is so that it is easier to construct terms (avoids using subst) - -- as often the result of a function will not match definitionally - -- with (lookup A e) but only propositionally. + → ∀ {ts} → ts ≡ lookup Tss i -- The reason to define it like this, rather than + → ConstrArgs Γ ts -- simply ConstrArgs Γ (lookup Tss i) is so that it + -- is easier to construct terms (helps to avoid the use of subst) + -- as often the result of a function will not match definitionally + -- with (lookup Tss i) but only propositionally. -------------------------------------- - → Γ ⊢ SOP A + → Γ ⊢ SOP Tss - case : ∀{n}{tss : Vec _ n}{A : Φ ⊢Nf⋆ *} - → (t : Γ ⊢ SOP tss) - → (cases : Cases Γ A tss) + case : ∀{n}{Tss : Vec _ n}{A : Φ ⊢Nf⋆ *} + → (t : Γ ⊢ SOP Tss) -- The term we case on + → (cases : Cases Γ A Tss) -------------------------- - → Γ ⊢ A + → Γ ⊢ A con : ∀{A : ∅ ⊢Nf⋆ ♯}{B} - → ⟦ A ⟧ + → ⟦ A ⟧ → B ≡ subNf∅ A --------------------- → Γ ⊢ con B @@ -276,17 +279,18 @@ data _⊢_ (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where -------------- → Γ ⊢ A +-- The type of arguments to a `constr` constructor ConstrArgs Γ = IList (Γ ⊢_) -- Cases is indexed by a vector -- so it can't be an IList data Cases Γ B where [] : Cases Γ B [] - _∷_ : ∀{n}{AS}{ASS : Vec _ n}( - c : Γ ⊢ (mkCaseType B AS)) - → (cs : Cases Γ B ASS) + _∷_ : ∀{n}{Ts}{Tss : Vec _ n}( + c : Γ ⊢ (mkCaseType B Ts)) + → (cs : Cases Γ B Tss) --------------------- - → Cases Γ B (AS ∷ ASS) + → Cases Γ B (Ts ∷ Tss) \end{code} Utility functions @@ -306,21 +310,21 @@ conv⊢ : ∀ {Γ Γ'}{A A' : Φ ⊢Nf⋆ *} → Γ' ⊢ A' conv⊢ refl refl t = t -lookupCase : ∀{n Φ}{Γ : Ctx Φ}{B}{TSS : Vec _ n} → (i : Fin n) → Cases Γ B TSS → Γ ⊢ mkCaseType B (Vec.lookup TSS i) +lookupCase : ∀{n Φ}{Γ : Ctx Φ}{A}{Tss : Vec _ n} → (i : Fin n) → Cases Γ A Tss → Γ ⊢ mkCaseType A (Vec.lookup Tss i) lookupCase Fin.zero (c ∷ cs) = c lookupCase (Fin.suc i) (c ∷ cs) = lookupCase i cs bwdMkCaseType : ∀{Φ} → Bwd (Φ ⊢Nf⋆ *) → (A : Φ ⊢Nf⋆ *) → Φ ⊢Nf⋆ * bwdMkCaseType bs A = bwd-foldr _⇒_ A bs -lemma-bwdfwdfunction' : ∀{Φ} {B : Φ ⊢Nf⋆ *} TS → mkCaseType B TS ≡ bwdMkCaseType ([] <>< TS) B -lemma-bwdfwdfunction' {B = B} TS = trans (cong (mkCaseType B) (sym (lemma<>1 [] TS))) (lemma-bwd-foldr _⇒_ B ([] <>< TS)) +lemma-bwdfwdfunction' : ∀{Φ} {B : Φ ⊢Nf⋆ *} Ts → mkCaseType B Ts ≡ bwdMkCaseType ([] <>< Ts) B +lemma-bwdfwdfunction' {B = B} Ts = trans (cong (mkCaseType B) (sym (lemma<>1 [] Ts))) (lemma-bwd-foldr _⇒_ B ([] <>< Ts)) -constr-cong : ∀{Γ : Ctx Φ}{n}{i : Fin n}{A : Vec (List (Φ ⊢Nf⋆ *)) n}{ts} - → (p : ts ≡ lookup A i) +constr-cong : ∀{Γ : Ctx Φ}{n}{i : Fin n}{Tss : Vec (List (Φ ⊢Nf⋆ *)) n}{ts} + → (p : ts ≡ lookup Tss i) → {cs : ConstrArgs Γ ts} - → {cs' : ConstrArgs Γ (lookup A i)} + → {cs' : ConstrArgs Γ (lookup Tss i)} → (q : cs' ≡ subst (IList (Γ ⊢_)) p cs) - → constr i A refl cs' ≡ constr i A p cs + → constr i Tss refl cs' ≡ constr i Tss p cs constr-cong refl refl = refl \end{code} \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/CC.lagda.md b/plutus-metatheory/src/Algorithmic/CC.lagda.md index 646b4fd0b30..5a7d8641bfd 100644 --- a/plutus-metatheory/src/Algorithmic/CC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CC.lagda.md @@ -51,9 +51,9 @@ dissect (wrap E) with dissect E dissect (unwrap E / refl) with dissect E ... | inj₁ refl = inj₂ (_ ,, [] ,, unwrap-) ... | inj₂ (C ,, E' ,, F) = inj₂ (C ,, unwrap E' / refl ,, F) -dissect (constr i TSS p {tidx} vs ts E) with dissect E -... | inj₁ refl = inj₂ (_ ,, ([] ,, (constr- i TSS p {tidx} vs ts))) -... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((constr i TSS p {tidx} vs ts E') ,, F)) +dissect (constr i Tss p {tidx} vs ts E) with dissect E +... | inj₁ refl = inj₂ (_ ,, ([] ,, (constr- i Tss p {tidx} vs ts))) +... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((constr i Tss p {tidx} vs ts E') ,, F)) dissect (case cs E) with dissect E ... | inj₁ refl = inj₂ (_ ,, ([] ,, (case- cs))) ... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((case cs E') ,, F)) @@ -65,7 +65,7 @@ compEC (VM ·r E) E' = VM ·r compEC E E' compEC (E ·⋆ A / refl) E' = compEC E E' ·⋆ A / refl compEC (wrap E) E' = wrap (compEC E E') compEC (unwrap E / refl) E' = unwrap (compEC E E') / refl -compEC (constr i TSS p {tidx} vs ts E) E' = constr i TSS p {tidx} vs ts (compEC E E') +compEC (constr i Tss p {tidx} vs ts E) E' = constr i Tss p {tidx} vs ts (compEC E E') compEC (case cs E) E' = case cs (compEC E E') extEC : ∀{A B C}(E : EC A B)(F : Frame B C) → EC A C @@ -75,7 +75,7 @@ extEC [] (VM ·-) = VM ·r [] extEC [] (-·⋆ A) = [] ·⋆ A / refl extEC [] wrap- = wrap [] extEC [] unwrap- = unwrap [] / refl -extEC [] (constr- i TSS p {tidx} vs ts) = constr i TSS p {tidx} vs ts [] +extEC [] (constr- i Tss p {tidx} vs ts) = constr i Tss p {tidx} vs ts [] extEC [] (case- cs) = case cs [] extEC (E l· M') F = extEC E F l· M' extEC (VM ·r E) F = VM ·r extEC E F @@ -96,7 +96,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where □ : {t : ∅ ⊢ T} → Value t → State T ◆ : (A : ∅ ⊢Nf⋆ *) → State T -extValueFrames : ∀{T H BS XS} → EC T H → {xs : IBwd (∅ ⊢_) BS} → VList xs → XS ≡ bwdMkCaseType BS H → EC T XS +extValueFrames : ∀{T H Bs Xs} → EC T H → {xs : IBwd (∅ ⊢_) Bs} → VList xs → Xs ≡ bwdMkCaseType Bs H → EC T Xs extValueFrames E [] refl = E extValueFrames E (vs :< v) refl = extValueFrames (extEC E (-·v v)) vs refl @@ -116,15 +116,15 @@ stepV (V-IΠ b {σA = σ} q) (inj₂ (_ ,, E ,, -·⋆ A)) = E ◅ V-I b (step⋆ q refl {σ [ A ]SigTy}) stepV V (inj₂ (_ ,, E ,, wrap-)) = E ◅ V-wrap V stepV (V-wrap V) (inj₂ (_ ,, E ,, unwrap-)) = E ▻ deval V -- E ◅ V -stepV V (inj₂ (_ ,, E ,, constr- i A p vs ts)) with Vec.lookup A i in eq +stepV V (inj₂ (_ ,, E ,, constr- i Tss p vs ts)) with Vec.lookup Tss i in eq stepV V (inj₂ (_ ,, E ,, constr- i _ refl {tidx} vs ts)) | [] with no-empty-≣-<>> tidx ... | () -stepV V (inj₂ (_ ,, E ,, constr- {VS = VS} {H} i _ refl {r}{tidx} vs [])) | _ ∷ _ = - E ◅ V-constr i _ (sym eq) (sym (trans (cong ([] <><_) (lem-≣-<>> r)) (lemma<>2 VS (H ∷ [])))) (vs :< V) refl -stepV V (inj₂ (_ ,, E ,, constr- {VS = VS} i A refl {r} vs (t ∷ ts))) | _ ∷ _ +stepV V (inj₂ (_ ,, E ,, constr- {Vs = Vs} {H} i _ refl {r}{tidx} vs [])) | _ ∷ _ = + E ◅ V-constr i _ (sym eq) (sym (trans (cong ([] <><_) (lem-≣-<>> r)) (lemma<>2 Vs (H ∷ [])))) (vs :< V) refl +stepV V (inj₂ (_ ,, E ,, constr- {Vs = Vs} i A refl {r} vs (t ∷ ts))) | _ ∷ _ = extEC E (constr- i A (sym eq) {bubble r} (vs :< V) ts) ▻ t -stepV (V-constr e A refl refl vs x) (inj₂ (_ ,, E ,, case- cs)) = - extValueFrames E vs (lemma-bwdfwdfunction' (Vec.lookup A e)) ▻ lookupCase e cs +stepV (V-constr e Tss refl refl vs x) (inj₂ (_ ,, E ,, case- cs)) = + extValueFrames E vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ▻ lookupCase e cs stepT : ∀{A} → State A → State A stepT (E ▻ ƛ M) = E ◅ V-ƛ M @@ -133,10 +133,10 @@ stepT (E ▻ Λ M) = E ◅ V-Λ M stepT (E ▻ (M ·⋆ A / refl)) = extEC E (-·⋆ A) ▻ M stepT (E ▻ wrap A B M) = extEC E wrap- ▻ M stepT (E ▻ unwrap M refl) = extEC E unwrap- ▻ M -stepT (E ▻ constr e A refl z) with Vec.lookup A e in eq -stepT (E ▻ constr e A refl []) | [] = E ◅ V-constr e A (sym eq) refl [] refl -stepT (E ▻ constr e A refl (x ∷ xs)) | a ∷ as = - extEC E (constr- e A (sym eq) {start} [] xs) ▻ x +stepT (E ▻ constr e Tss refl z) with Vec.lookup Tss e in eq +stepT (E ▻ constr e Tss refl []) | [] = E ◅ V-constr e Tss (sym eq) refl [] refl +stepT (E ▻ constr e Tss refl (x ∷ xs)) | a ∷ as = + extEC E (constr- e Tss (sym eq) {start} [] xs) ▻ x stepT (E ▻ case M cases) = extEC E (case- cases) ▻ M stepT (E ▻ con c refl) = E ◅ V-con c stepT (E ▻ (builtin b / refl)) = E ◅ ival b diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md index 6244c542592..82c3a5fde05 100644 --- a/plutus-metatheory/src/Algorithmic/CEK.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CEK.lagda.md @@ -93,7 +93,7 @@ data Value where → {σB : SigTy (bubble pt) pa B} → BApp b (Π B) (sucΠ σB) → Value (Π B) - V-constr : ∀{n}(e : Fin n) A {ts} (vs : VList ts) → ts ≡ [] <>< Vec.lookup A e → Value (SOP A) + V-constr : ∀{n}(e : Fin n) Tss {ts} (vs : VList ts) → ts ≡ [] <>< Vec.lookup Tss e → Value (SOP Tss) data BApp b where base : BApp b (sig2type (signature b)) (sig2SigTy (signature b)) @@ -172,7 +172,7 @@ dischargeStack-aux : ∀{A B C} → (s : VList A) → IList (∅ ⊢_) B → A < dischargeStack-aux [] a refl = a dischargeStack-aux (s :< x) a refl = dischargeStack-aux s (discharge x ∷ a) refl -dischargeStack : ∀{TS} → IBwd Value ([] <>< TS) → IList (_⊢_ ∅) TS +dischargeStack : ∀{Ts} → IBwd Value ([] <>< Ts) → IList (_⊢_ ∅) Ts dischargeStack bs = dischargeStack-aux bs [] (lemma<>1 [] _) discharge (V-ƛ M ρ) = ƛ (dischargeBody M ρ) @@ -181,7 +181,7 @@ discharge (V-wrap V) = wrap _ _ (discharge V) discharge (V-con c) = con c refl discharge (V-I⇒ b bt) = dischargeB bt discharge (V-IΠ b bt) = dischargeB bt -discharge (V-constr i A s refl) = constr i A refl (dischargeStack s) +discharge (V-constr i Tss s refl) = constr i Tss refl (dischargeStack s) ``` ## Builtin Semantics @@ -357,14 +357,14 @@ data Frame : (T : ∅ ⊢Nf⋆ *) → (H : ∅ ⊢Nf⋆ *) → Set where unwrap- : ∀{K}{A : ∅ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}{B : ∅ ⊢Nf⋆ K} → Frame (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)) (μ A B) - constr- : ∀{Γ n VS H TS} + constr- : ∀{Γ n Vs H Ts} → (i : Fin n) - → (TSS : Vec _ n) + → (Tss : Vec _ n) → Env Γ - → ∀{XS} → (XS ≡ Vec.lookup TSS i) - → {tidx : XS ≣ VS <>> (H ∷ TS)} → VList VS → ConstrArgs Γ TS - → Frame (SOP TSS) H - case- : ∀{Γ A n}{TSS : Vec _ n} → (ρ : Env Γ) → Cases Γ A TSS → Frame A (SOP TSS) + → ∀{Xs} → (Xs ≡ Vec.lookup Tss i) + → {tidx : Xs ≣ Vs <>> (H ∷ Ts)} → VList Vs → ConstrArgs Γ Ts + → Frame (SOP Tss) H + case- : ∀{Γ A n}{Tss : Vec _ n} → (ρ : Env Γ) → Cases Γ A Tss → Frame A (SOP Tss) data Stack (T : ∅ ⊢Nf⋆ *) : (H : ∅ ⊢Nf⋆ *) → Set where ε : Stack T T @@ -379,7 +379,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where ival : ∀(b : Builtin) → Value (btype b) ival b = V-I b base -pushValueFrames : ∀{T H BS XS} → Stack T H → VList BS → XS ≡ bwdMkCaseType BS H → Stack T XS +pushValueFrames : ∀{T H Bs Xs} → Stack T H → VList Bs → Xs ≡ bwdMkCaseType Bs H → Stack T Xs pushValueFrames s [] refl = s pushValueFrames s (vs :< v) refl = pushValueFrames (s , -·v v) vs refl @@ -394,9 +394,9 @@ step (s ; ρ ▻ unwrap L refl) = (s , unwrap-) ; ρ ▻ L step (s ; ρ ▻ con c refl) = s ◅ V-con c step (s ; ρ ▻ (builtin b / refl)) = s ◅ ival b step (s ; ρ ▻ error A) = ◆ A -step (s ; ρ ▻ constr e A refl as) with Vec.lookup A e in eq -step (s ; ρ ▻ constr e A refl []) | [] = s ◅ V-constr e A [] (cong ([] <><_) (sym eq)) -step (_;_▻_ {Γ} s ρ (constr e A refl (_∷_ {xty} {xsty} x xs))) | _ ∷ _ = (s , constr- e A ρ (sym eq) {start} [] xs) ; ρ ▻ x +step (s ; ρ ▻ constr e Tss refl as) with Vec.lookup Tss e in eq +step (s ; ρ ▻ constr e Tss refl []) | [] = s ◅ V-constr e Tss [] (cong ([] <><_) (sym eq)) +step (_;_▻_ {Γ} s ρ (constr e Tss refl (_∷_ {xty} {xsty} x xs))) | _ ∷ _ = (s , constr- e Tss ρ (sym eq) {start} [] xs) ; ρ ▻ x step (s ; ρ ▻ case t ts) = (s , case- ρ ts) ; ρ ▻ t step (ε ◅ V) = □ V step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M @@ -408,14 +408,14 @@ step ((s , -·⋆ A) ◅ V-Λ M ρ) = s ; ρ ▻ (M [ A ]⋆) step ((s , -·⋆ A) ◅ V-IΠ b {σB = σ} bapp) = s ◅ V-I b (_$$_ bapp refl {σ [ A ]SigTy}) step ((s , wrap-) ◅ V) = s ◅ V-wrap V step ((s , unwrap-) ◅ V-wrap V) = s ◅ V -step ((s , constr- i TSS ρ refl {tidx} vs ts) ◅ v) - with Vec.lookup TSS i in eq +step ((s , constr- i Tss ρ refl {tidx} vs ts) ◅ v) + with Vec.lookup Tss i in eq ... | [] with no-empty-≣-<>> tidx ... | () -step ((s , constr- i TSS ρ refl {r} vs []) ◅ v) | A ∷ AS = s ◅ V-constr i TSS (vs :< v) +step ((s , constr- i Tss ρ refl {r} vs []) ◅ v) | A ∷ As = s ◅ V-constr i Tss (vs :< v) (sym (trans (cong ([] <><_) (trans eq (lem-≣-<>> r))) (lemma<>2 _ (_ ∷ [])))) -step ((s , constr- i TSS ρ refl {r} vs (t ∷ ts)) ◅ v) | A ∷ AS = (s , constr- i TSS ρ (sym eq) {bubble r} (vs :< v) ts) ; ρ ▻ t -step {t} ((s , case- ρ cases) ◅ V-constr e TSS vs refl) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup TSS e)) ; ρ ▻ (lookupCase e cases) +step ((s , constr- i Tss ρ refl {r} vs (t ∷ ts)) ◅ v) | A ∷ As = (s , constr- i Tss ρ (sym eq) {bubble r} (vs :< v) ts) ; ρ ▻ t +step {t} ((s , case- ρ cases) ◅ V-constr e Tss vs refl) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ; ρ ▻ (lookupCase e cases) step (□ V) = □ V step (◆ A) = ◆ A diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md index 0ae4128c3d0..bf32c1c0710 100644 --- a/plutus-metatheory/src/Algorithmic/CK.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CK.lagda.md @@ -66,7 +66,7 @@ closeState (◆ A) = error _ discharge : ∀{A : ∅ ⊢Nf⋆ *}{t : ∅ ⊢ A} → Value t → ∅ ⊢ A discharge {t = t} _ = t -pushValueFrames : ∀{T H BS XS} → Stack T H → {xs : IBwd (∅ ⊢_) BS} → VList xs → XS ≡ bwdMkCaseType BS H → Stack T XS +pushValueFrames : ∀{T H Bs Xs} → Stack T H → {xs : IBwd (∅ ⊢_) Bs} → VList xs → Xs ≡ bwdMkCaseType Bs H → Stack T Xs pushValueFrames s [] refl = s pushValueFrames s (vs :< v) refl = pushValueFrames (s , -·v v) vs refl @@ -78,9 +78,9 @@ step (s ▻ (L ·⋆ A / refl)) = (s , -·⋆ A) ▻ L step (s ▻ wrap A B L) = (s , wrap-) ▻ L step (s ▻ unwrap L refl) = (s , unwrap-) ▻ L step (s ▻ con cn refl) = s ◅ V-con cn -step (s ▻ constr e A refl xs) with Vec.lookup A e in eq -step (s ▻ constr e TSS refl []) | [] = s ◅ V-constr e TSS (sym eq) refl [] refl -step (s ▻ constr e TSS refl (x ∷ xs)) | _ ∷ _ = (s , constr- e TSS (sym eq) {tidx = start} [] xs) ▻ x +step (s ▻ constr e Tss refl xs) with Vec.lookup Tss e in eq +step (s ▻ constr e Tss refl []) | [] = s ◅ V-constr e Tss (sym eq) refl [] refl +step (s ▻ constr e Tss refl (x ∷ xs)) | _ ∷ _ = (s , constr- e Tss (sym eq) {tidx = start} [] xs) ▻ x step (s ▻ case t ts) = (s , case- ts) ▻ t step (s ▻ error A) = ◆ A step (ε ◅ V) = □ V @@ -90,19 +90,19 @@ step ((s , (V-ƛ t ·-)) ◅ V) = s ▻ (t [ discharge V ]) step ((s , (-·⋆ A)) ◅ V-Λ t) = s ▻ (t [ A ]⋆) step ((s , wrap-) ◅ V) = s ◅ (V-wrap V) step ((s , unwrap-) ◅ V-wrap V) = s ▻ deval V -step ((s , constr- i TSS refl {tidx} vs ts) ◅ v) with Vec.lookup TSS i in eq +step ((s , constr- i Tss refl {tidx} vs ts) ◅ v) with Vec.lookup Tss i in eq ... | [] with no-empty-≣-<>> tidx ... | () -step ((s , constr- {n} {VS} {H} i TSS refl {tidx}{tvs} vs []) ◅ v) | _ ∷ _ = s ◅ - V-constr i TSS +step ((s , constr- {n} {Vs} {H} i Tss refl {tidx}{tvs} vs []) ◅ v) | _ ∷ _ = s ◅ + V-constr i Tss (sym eq) - (trans (sym (lemma<>2 VS (H ∷ []))) (sym (cong ([] <><_) (lem-≣-<>> tidx)))) + (trans (sym (lemma<>2 Vs (H ∷ []))) (sym (cong ([] <><_) (lem-≣-<>> tidx)))) {tvs :< deval v} (vs :< v) refl -step ((s , constr- i TSS refl {r} vs (t ∷ ts)) ◅ v) | _ ∷ _ = - (s , constr- i TSS (sym eq) {bubble r} (vs :< v) ts) ▻ t -step ((s , case- cs) ◅ V-constr e TSS refl refl vs x) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup TSS e)) ▻ lookupCase e cs +step ((s , constr- i Tss refl {r} vs (t ∷ ts)) ◅ v) | _ ∷ _ = + (s , constr- i Tss (sym eq) {bubble r} (vs :< v) ts) ▻ t +step ((s , case- cs) ◅ V-constr e Tss refl refl vs x) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ▻ lookupCase e cs step (s ▻ (builtin b / refl)) = s ◅ ival b step ((s , (V-I⇒ b {am = 0} bt ·-)) ◅ vu) = s ▻ BUILTIN' b (app bt vu) step ((s , (V-I⇒ b {am = suc _} bt ·-)) ◅ vu) = s ◅ V-I b (app bt vu) diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda b/plutus-metatheory/src/Algorithmic/Completeness.lagda index d3a694c70d0..ae306ef3dcc 100644 --- a/plutus-metatheory/src/Algorithmic/Completeness.lagda +++ b/plutus-metatheory/src/Algorithmic/Completeness.lagda @@ -191,23 +191,23 @@ nfType : ∀{Φ Γ} → nfCtx Γ Norm.⊢ nf A nfType-ConstrArgs : ∀ {Φ} {Γ : Syn.Ctx Φ} - {TS : List (Φ ⊢⋆ *)} - → (cs : Syn.ConstrArgs Γ TS) - → Norm.ConstrArgs (nfCtx Γ) (eval-List TS (idEnv Φ)) + {Ts : List (Φ ⊢⋆ *)} + → (cs : Syn.ConstrArgs Γ Ts) + → Norm.ConstrArgs (nfCtx Γ) (eval-List Ts (idEnv Φ)) nfType-ConstrArgs [] = [] nfType-ConstrArgs (c ∷ cs) = (nfType c) ∷ (nfType-ConstrArgs cs) -lemma-mkCaseType : ∀{Φ}{B} AS → - nf (Syn.mkCaseType B AS) ≡ Norm.mkCaseType (nf B) (eval-List AS (idEnv Φ)) +lemma-mkCaseType : ∀{Φ}{B} As → + nf (Syn.mkCaseType B As) ≡ Norm.mkCaseType (nf B) (eval-List As (idEnv Φ)) lemma-mkCaseType [] = refl -lemma-mkCaseType (A ∷ AS) = cong (eval A (idEnv _) ⇒_) (lemma-mkCaseType AS) +lemma-mkCaseType (A ∷ As) = cong (eval A (idEnv _) ⇒_) (lemma-mkCaseType As) nfType-Cases : ∀ {Φ} {Γ : Syn.Ctx Φ} {A : Φ ⊢⋆ *} {n} - {tss : Vec (List (Φ ⊢⋆ *)) n} - (cases : Syn.Cases Γ A tss) → - Norm.Cases (nfCtx Γ) (nf A) (eval-VecList tss (idEnv Φ)) + {Tss : Vec (List (Φ ⊢⋆ *)) n} + (cases : Syn.Cases Γ A Tss) → + Norm.Cases (nfCtx Γ) (nf A) (eval-VecList Tss (idEnv Φ)) nfType-Cases Syn.[] = Norm.[] -nfType-Cases (Syn._∷_ {AS = AS} c cases) = substEq (nfCtx _ Norm.⊢_) (lemma-mkCaseType AS) (nfType c) +nfType-Cases (Syn._∷_ {Ts = Ts} c cases) = substEq (nfCtx _ Norm.⊢_) (lemma-mkCaseType Ts) (nfType c) Norm.∷ (nfType-Cases cases) nfType (Syn.` α) = Norm.` (nfTyVar α) @@ -231,7 +231,7 @@ nfType (Syn.conv p t) = Norm.conv⊢ refl (completeness p) (nfType t) nfType (Syn.con {A} t p) = Norm.con {A = nf A} t (trans (completeness p) (subNf∅-sub∅ A)) nfType (Syn.builtin b) = Norm.conv⊢ refl (btype-lem b) (Norm.builtin b / refl) nfType (Syn.error A) = Norm.error (nf A) -nfType (Syn.constr e TSS refl cs) = Norm.constr e (eval-VecList TSS (idEnv _)) (sym (lookup-eval-VecList e TSS (idEnv _))) (nfType-ConstrArgs cs) +nfType (Syn.constr e Tss refl cs) = Norm.constr e (eval-VecList Tss (idEnv _)) (sym (lookup-eval-VecList e Tss (idEnv _))) (nfType-ConstrArgs cs) nfType (Syn.case t cases) = Norm.case (nfType t) (nfType-Cases cases) completenessT : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ Syn.⊢ A diff --git a/plutus-metatheory/src/Algorithmic/Erasure.lagda b/plutus-metatheory/src/Algorithmic/Erasure.lagda index c4cf6f57db7..1758e212c90 100644 --- a/plutus-metatheory/src/Algorithmic/Erasure.lagda +++ b/plutus-metatheory/src/Algorithmic/Erasure.lagda @@ -73,15 +73,15 @@ eraseTC A t = tmCon (A.ty2sty A) (subst ⟦_⟧ (ty≅sty₁ A) t) erase : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ⊢ A → len Γ ⊢ erase-ConstrArgs : ∀ {Φ} {Γ : Ctx Φ} - {TS : List (Φ ⊢Nf⋆ *)} - (cs : ConstrArgs Γ TS) + {Ts : List (Φ ⊢Nf⋆ *)} + (cs : ConstrArgs Γ Ts) → List (len Γ ⊢) erase-ConstrArgs [] = [] erase-ConstrArgs (c ∷ cs) = (erase c) ∷ (erase-ConstrArgs cs) erase-Cases : ∀ {Φ} {Γ : Ctx Φ} {A : Φ ⊢Nf⋆ *} {n} - {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cs : Cases Γ A tss) → + {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cs : Cases Γ A Tss) → List (len Γ ⊢) erase-Cases [] = [] erase-Cases (c ∷ cs) = (erase c) ∷ (erase-Cases cs) @@ -96,7 +96,7 @@ erase (unwrap t refl) = erase t erase (con {A = A} t p) = con (eraseTC A t) erase (builtin b / refl) = builtin b erase (error A) = error -erase (constr e TSS p cs) = constr (toℕ e) (erase-ConstrArgs cs) +erase (constr e Tss p cs) = constr (toℕ e) (erase-ConstrArgs cs) erase (case t cases) = case (erase t) (erase-Cases cases) \end{code} @@ -200,9 +200,9 @@ same : ∀{Φ Γ}{A : Φ ⊢⋆ *}(t : Γ D.⊢ A) +cancel : ∀{m m' n n'} → m + n ≡ m' + n' → m ≡ m' → n ≡ n' +cancel p refl = +-cancelˡ-≡ _ p -same-ConstrArgs : ∀{Φ}{Γ : D.Ctx Φ}{TS : List (Φ ⊢⋆ *)} +same-ConstrArgs : ∀{Φ}{Γ : D.Ctx Φ}{Ts : List (Φ ⊢⋆ *)} - (xs : D.ConstrArgs Γ TS) + (xs : D.ConstrArgs Γ Ts) → D.erase-ConstrArgs xs ≡ map (subst _⊢ (lenLemma Γ)) (erase-ConstrArgs (nfType-ConstrArgs xs)) same-ConstrArgs {Γ = Γ} [] = refl same-ConstrArgs {Γ = Γ} (x ∷ xs) = cong₂ _∷_ (same x) (same-ConstrArgs xs) @@ -214,13 +214,13 @@ same-mkCaseType : ∀ {Φ} {Γ : Ctx Φ} {A B : Φ ⊢Nf⋆ *} same-mkCaseType c refl = refl same-Cases : ∀ {Φ} {Γ : D.Ctx Φ} {A : Φ ⊢⋆ *} {n} - {tss : Vec (List (Φ ⊢⋆ *)) n} - (cases : D.Cases Γ A tss) → + {Tss : Vec (List (Φ ⊢⋆ *)) n} + (cases : D.Cases Γ A Tss) → D.erase-Cases cases ≡ map (subst _⊢ (lenLemma Γ)) (erase-Cases (nfType-Cases cases)) same-Cases D.[] = refl -same-Cases {Γ = Γ}(D._∷_ {AS = AS} c cs) = cong₂ _∷_ (trans (same c) - (cong (subst _⊢ (lenLemma Γ)) (same-mkCaseType (nfType c) (lemma-mkCaseType AS)))) +same-Cases {Γ = Γ}(D._∷_ {Ts = As} c cs) = cong₂ _∷_ (trans (same c) + (cong (subst _⊢ (lenLemma Γ)) (same-mkCaseType (nfType c) (lemma-mkCaseType As)))) (same-Cases cs) same {Γ = Γ}(D.` x) = @@ -258,7 +258,7 @@ same {Γ = Γ} (D.builtin b) = trans (lembuiltin b (lenLemma Γ)) (cong (subst _⊢ (lenLemma Γ)) (lem-erase refl (btype-lem b) (builtin b / refl))) same {Γ = Γ} (D.error A) = lemerror (lenLemma Γ) -same {Γ = Γ} (D.constr e TSS refl xs) rewrite lemConstr (toℕ e) (erase-ConstrArgs (nfType-ConstrArgs xs)) (lenLemma Γ) +same {Γ = Γ} (D.constr e Tss refl xs) rewrite lemConstr (toℕ e) (erase-ConstrArgs (nfType-ConstrArgs xs)) (lenLemma Γ) = cong (constr (toℕ e)) (same-ConstrArgs xs) same {Γ = Γ} (D.case t cases) rewrite lemCase (erase (nfType t)) (erase-Cases (Algorithmic.Completeness.nfType-Cases cases)) (lenLemma Γ) = cong₂ case (same t) (same-Cases cases) @@ -291,8 +291,8 @@ same' : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *}(x : Γ A.⊢ A) → erase x ≡ subst _⊢ (same'Len Γ) (D.erase (emb x)) same'ConstrArgs : ∀ {Φ} {Γ : Ctx Φ} - {TS : List (Φ ⊢Nf⋆ *)} - (xs : ConstrArgs Γ TS) + {Ts : List (Φ ⊢Nf⋆ *)} + (xs : ConstrArgs Γ Ts) → erase-ConstrArgs xs ≡ map (subst _⊢ (same'Len Γ)) (D.erase-ConstrArgs (emb-ConstrArgs xs)) same'ConstrArgs [] = refl @@ -305,14 +305,14 @@ same-subst : ∀ {Φ} {Γ : D.Ctx Φ} {A B : Φ ⊢⋆ *} same-subst c refl = refl same'Case : ∀ {Φ} {Γ : Ctx Φ} {A : Φ ⊢Nf⋆ *} {n} - {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cases : Cases Γ A tss) + {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cases : Cases Γ A Tss) → erase-Cases cases ≡ map (subst _⊢ (same'Len Γ)) (D.erase-Cases (Algorithmic.Soundness.emb-Cases cases)) same'Case [] = refl -same'Case {Γ = Γ} (_∷_ {AS = AS} c cases) = +same'Case {Γ = Γ} (_∷_ {Ts = As} c cases) = cong₂ _∷_ (trans (same' c) - (cong (subst _⊢ (same'Len Γ)) (same-subst (emb c) (lema-mkCaseType AS)))) + (cong (subst _⊢ (same'Len Γ)) (same-subst (emb c) (lema-mkCaseType As)))) (same'Case cases) same' {Γ = Γ} (` x) = trans (cong ` (same'Var x)) (lemVar (same'Len Γ) (D.eraseVar (embVar x))) @@ -334,7 +334,7 @@ same' {Γ = Γ} (con {A = A} tcn refl) = trans (cong con (same'TC {Γ = Γ} A tc (lemcon' (same'Len Γ) (D.eraseTC (embNf A) (subst ⟦_⟧ (sym (stability A)) tcn))) same' {Γ = Γ} (builtin b / refl) = lembuiltin b (same'Len Γ) same' {Γ = Γ} (error A) = lemerror (same'Len Γ) -same' {Γ = Γ} (constr e TSS {ts} refl xs) rewrite lemConstr (toℕ e) (D.erase-ConstrArgs (Algorithmic.Soundness.emb-ConstrArgs xs)) (same'Len Γ) +same' {Γ = Γ} (constr e Tss {ts} refl xs) rewrite lemConstr (toℕ e) (D.erase-ConstrArgs (Algorithmic.Soundness.emb-ConstrArgs xs)) (same'Len Γ) = cong (constr (toℕ e)) (same'ConstrArgs xs) same' {Γ = Γ}(case t cases) rewrite lemCase (D.erase (emb t)) (D.erase-Cases (Algorithmic.Soundness.emb-Cases cases)) (same'Len Γ) = cong₂ case (same' t) (same'Case cases) diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md index c56f3efce0b..8f95dcaaab7 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md @@ -70,7 +70,7 @@ VList = IIBwd Value deval : {A : ∅ ⊢Nf⋆ *}{u : ∅ ⊢ A} → Value u → ∅ ⊢ A deval {u = u} _ = u -deval-VecList : ∀{n} → (A : Vec (List (∃ (∅ ⊢_))) n) → Vec (List (∅ ⊢Nf⋆ *)) n +deval-VecList : ∀{n} → (Vec (List (∃ (∅ ⊢_))) n) → Vec (List (∅ ⊢Nf⋆ *)) n deval-VecList [] = [] deval-VecList (xs ∷ xss) = map proj₁ xs ∷ (deval-VecList xss) @@ -132,13 +132,13 @@ data Value where → BApp b (sucΠ σA) t → Value t V-constr : ∀{n}(e : Fin n) - → (TSS : Vec (List ( ∅ ⊢Nf⋆ *)) n ) - → ∀{XS} → (p : XS ≡ Vec.lookup TSS e) - → ∀{YS} → (q : YS ≡ [] <>< XS) - → {ts : IBwd (∅ ⊢_) YS} + → (Tss : Vec (List ( ∅ ⊢Nf⋆ *)) n ) + → ∀{Xs} → (p : Xs ≡ Vec.lookup Tss e) + → ∀{Ys} → (q : Ys ≡ [] <>< Xs) + → {ts : IBwd (∅ ⊢_) Ys} → (vs : VList ts) - → ∀ {ts' : IList (∅ ⊢_) XS} → (IBwd2IList (lemma<>1' _ _ q) ts ≡ ts') - → Value (constr e TSS p ts') + → ∀ {ts' : IList (∅ ⊢_) Xs} → (IBwd2IList (lemma<>1' _ _ q) ts ≡ ts') + → Value (constr e Tss p ts') red2cekVal : ∀{A}{L : ∅ ⊢ A} → Value L → CEK.Value A red2cekBApp : ∀{b} @@ -152,7 +152,7 @@ red2cekBApp (base) = CEK.base red2cekBApp (step x x₁) = (red2cekBApp x) CEK.$ (red2cekVal x₁) red2cekBApp (step⋆ x refl) = (red2cekBApp x) CEK.$$ refl -red2cekVal-VList : ∀{TS}{ts : IBwd (_⊢_ ∅) TS} → (vs : VList ts) → CEK.VList TS +red2cekVal-VList : ∀{Ts}{ts : IBwd (_⊢_ ∅) Ts} → (vs : VList ts) → CEK.VList Ts red2cekVal-VList [] = [] red2cekVal-VList (vs :< x) = (red2cekVal-VList vs) :< (red2cekVal x) @@ -162,7 +162,7 @@ red2cekVal (V-wrap V) = CEK.V-wrap (red2cekVal V) red2cekVal (V-con {A} cn) = CEK.V-con cn red2cekVal (V-I⇒ b x) = CEK.V-I⇒ b (red2cekBApp x) red2cekVal (V-IΠ b x) = CEK.V-IΠ b (red2cekBApp x) -red2cekVal (V-constr e TSS refl refl vs refl) = CEK.V-constr e TSS (red2cekVal-VList vs) refl +red2cekVal (V-constr e Tss refl refl vs refl) = CEK.V-constr e Tss (red2cekVal-VList vs) refl BUILTIN' : ∀ b {A}{t : ∅ ⊢ A} → ∀{tn} → {pt : tn ∔ 0 ≣ fv (signature b)} @@ -196,13 +196,13 @@ data Frame : (T : ∅ ⊢Nf⋆ *) → (H : ∅ ⊢Nf⋆ *) → Set where → Frame (μ A B) (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)) unwrap- : ∀{K}{A : ∅ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}{B : ∅ ⊢Nf⋆ K} → Frame (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)) (μ A B) - constr- : ∀{n VS H TS} + constr- : ∀{n Vs H Ts} → (i : Fin n) - → (TSS : Vec _ n) - → ∀ {XS} → (XS ≡ Vec.lookup TSS i) - → {tidx : XS ≣ VS <>> (H ∷ TS)} → {tvs : IBwd (∅ ⊢_) VS} → VList tvs → ConstrArgs ∅ TS - → Frame (SOP TSS) H - case- : ∀{A n}{TSS : Vec _ n} → Cases ∅ A TSS → Frame A (SOP TSS) + → (Tss : Vec _ n) + → ∀ {Xs} → (Xs ≡ Vec.lookup Tss i) + → {tidx : Xs ≣ Vs <>> (H ∷ Ts)} → {tvs : IBwd (∅ ⊢_) Vs} → VList tvs → ConstrArgs ∅ Ts + → Frame (SOP Tss) H + case- : ∀{A n}{Tss : Vec _ n} → Cases ∅ A Tss → Frame A (SOP Tss) _[_]ᶠ : ∀{A B : ∅ ⊢Nf⋆ *} → Frame B A → ∅ ⊢ A → ∅ ⊢ B (-· M') [ L ]ᶠ = L · M' @@ -211,7 +211,7 @@ _[_]ᶠ : ∀{A B : ∅ ⊢Nf⋆ *} → Frame B A → ∅ ⊢ A → ∅ ⊢ B -·⋆ A [ L ]ᶠ = L ·⋆ A / refl wrap- [ L ]ᶠ = wrap _ _ L unwrap- [ L ]ᶠ = unwrap L refl -constr- i TSS refl {tidx} {tvs} _ ts [ L ]ᶠ = constr i TSS (sym (lem-≣-<>> tidx)) (tvs <>>I (L ∷ ts)) +constr- i Tss refl {tidx} {tvs} _ ts [ L ]ᶠ = constr i Tss (sym (lem-≣-<>> tidx)) (tvs <>>I (L ∷ ts)) case- cs [ L ]ᶠ = case L cs ``` @@ -231,15 +231,15 @@ data EC : (T : ∅ ⊢Nf⋆ *) → (H : ∅ ⊢Nf⋆ *) → Set where → EC (μ A B) C → X ≡ (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)) → EC X C - constr : ∀{n VS H TS C} + constr : ∀{n Vs H Ts C} → (i : Fin n) - → (TSS : Vec _ n) - → ∀ {XS} → (XS ≡ Vec.lookup TSS i) - → {tidx : XS ≣ VS <>> (H ∷ TS)} - → {tvs : IBwd (∅ ⊢_) VS} → VList tvs → ConstrArgs ∅ TS + → (Tss : Vec _ n) + → ∀ {Xs} → (Xs ≡ Vec.lookup Tss i) + → {tidx : Xs ≣ Vs <>> (H ∷ Ts)} + → {tvs : IBwd (∅ ⊢_) Vs} → VList tvs → ConstrArgs ∅ Ts → EC H C - → EC (SOP TSS) C - case : ∀{A C n}{TSS : Vec _ n} → Cases ∅ A TSS → EC (SOP TSS) C → EC A C + → EC (SOP Tss) C + case : ∀{A C n}{Tss : Vec _ n} → Cases ∅ A Tss → EC (SOP Tss) C → EC A C -- Plugging of evaluation contexts _[_]ᴱ : ∀{A B : ∅ ⊢Nf⋆ *} → EC B A → ∅ ⊢ A → ∅ ⊢ B @@ -249,7 +249,7 @@ _[_]ᴱ : ∀{A B : ∅ ⊢Nf⋆ *} → EC B A → ∅ ⊢ A → ∅ ⊢ B (E ·⋆ A / q) [ L ]ᴱ = E [ L ]ᴱ ·⋆ A / q (wrap E) [ L ]ᴱ = wrap _ _ (E [ L ]ᴱ) (unwrap E / q) [ L ]ᴱ = unwrap (E [ L ]ᴱ) q -constr i TSS p {idx} {tvs} vs ts E [ L ]ᴱ = constr i TSS (trans (sym (lem-≣-<>> idx)) p) (tvs <>>I (E [ L ]ᴱ ∷ ts)) +constr i Tss p {idx} {tvs} vs ts E [ L ]ᴱ = constr i Tss (trans (sym (lem-≣-<>> idx)) p) (tvs <>>I (E [ L ]ᴱ ∷ ts)) case cs E [ L ]ᴱ = case (E [ L ]ᴱ) cs ``` @@ -300,13 +300,13 @@ data _—→⋆_ : {A : ∅ ⊢Nf⋆ *} → (∅ ⊢ A) → (∅ ⊢ A) → Set β-case : ∀{n}{A : ∅ ⊢Nf⋆ *} → (e : Fin n) - → (TSS : Vec (List (∅ ⊢Nf⋆ *)) n) - → ∀{YS} → (q : YS ≡ [] <>< Vec.lookup TSS e) - → {ts : IBwd (∅ ⊢_) YS} + → (Tss : Vec (List (∅ ⊢Nf⋆ *)) n) + → ∀{Ys} → (q : Ys ≡ [] <>< Vec.lookup Tss e) + → {ts : IBwd (∅ ⊢_) Ys} → (vs : VList ts) - → ∀ {ts' : IList (∅ ⊢_) (Vec.lookup TSS e)} → (IBwd2IList (lemma<>1' _ _ q) ts ≡ ts') - → (cases : Cases ∅ A TSS) - → case (constr e TSS refl ts') cases —→⋆ applyCase (lookupCase e cases) ts' + → ∀ {ts' : IList (∅ ⊢_) (Vec.lookup Tss e)} → (IBwd2IList (lemma<>1' _ _ q) ts ≡ ts') + → (cases : Cases ∅ A Tss) + → case (constr e Tss refl ts') cases —→⋆ applyCase (lookupCase e cases) ts' -- -} ``` diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md index 3eadc82f8f8..feaef184d64 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md @@ -5,21 +5,24 @@ module Algorithmic.ReductionEC.Determinism where ``` open import Data.Nat using (suc) +open import Data.Fin using (Fin) open import Data.Empty using (⊥;⊥-elim) -open import Data.List as List using (List; _∷_; []) -open import Data.Product using (_×_;∃) renaming (_,_ to _,,_) +open import Data.Vec as Vec using (lookup) +open import Data.Product using (Σ;_×_;∃) renaming (_,_ to _,,_) +open import Data.List.Properties using (∷-injective) open import Relation.Nullary using (¬_;yes;no) open import Relation.Binary.PropositionalEquality - using (_≡_;refl;sym;trans;cong) + using (_≡_;refl;sym;trans;cong;cong₂;subst-subst;subst-injective) renaming (subst to substEq) open import Relation.Binary.HeterogeneousEquality using (_≅_;refl;≅-to-≡) -open import Utils hiding (_×_) +open import Utils hiding (_×_;List) +open import Utils.List open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z) open _⊢⋆_ import Type.RenamingSubstitution as T -open import Algorithmic using (Ctx;_⊢_;conv⊢) +open import Algorithmic using (Ctx;_⊢_;conv⊢;ConstrArgs;constr-cong) open Ctx open _⊢_ open import Algorithmic.RenamingSubstitution using (_[_];_[_]⋆) @@ -64,9 +67,13 @@ conv∔≣a : ∀{b b' an am an' am'} → an ∔ am ≣ args♯ (signature b) conv∔≣a refl pa = conv∔≣ pa refl - uniqueVal : ∀{A}(M : ∅ ⊢ A)(v v' : Value M) → v ≡ v' +uniqueVal-List : ∀{As : Bwd (∅ ⊢Nf⋆ *)}{cs : IBwd (∅ ⊢_) As} → (vs vs' : VList cs) → vs ≡ vs' +uniqueVal-List [] [] = refl +uniqueVal-List (vs :< x) (vs' :< x') = cong₂ _:<_ (uniqueVal-List vs vs') (uniqueVal _ x x') + + uniqueBApp : ∀{A b} → ∀{tn tm}{pt : tn ∔ tm ≣ fv (signature b)} → ∀{an am}{pa : an ∔ am ≣ args♯ (signature b)} @@ -106,6 +113,10 @@ uniqueVal M (V-I⇒ b {σB = s} x) (V-I⇒ b' {σB = s'} x') with uniqueBApp' M uniqueVal M (V-IΠ b {σA = s} x) (V-IΠ b' {σA = s'} x') with uniqueBApp' M x x' ... | refl ,, refl ,, refl ,, refl ,, refl ,, refl ,, refl with uniqueSigTy s s' ... | refl = cong (V-IΠ b) (uniqueBApp M x x') +uniqueVal _ (V-constr e Tss refl refl {ts} vs refl) (V-constr .e .Tss .refl refl {ts'} vs₁ q) + with inj-IBwd2IList {ts = ts'}{ts} (lemma<>1 [] (lookup Tss e)) q +uniqueVal _ (V-constr e Tss .refl refl {ts} vs refl) (V-constr _ _ .refl refl {.ts} vs₁ refl) | refl = + cong (λ vs → V-constr e Tss refl refl vs refl) (uniqueVal-List vs vs₁) ``` ``` @@ -152,15 +163,36 @@ lemVβ⋆ : ∀{K}{A : ∅ ⊢Nf⋆ K}{B}{M : ∅ ,⋆ K ⊢ B}{C}{p : C ≡ B [ lemVβ⋆ (V-I⇒ b q) = lemBAppβ⋆ q lemVβ⋆ (V-IΠ b q) = lemBAppβ⋆ q +VE-constr-lemma : ∀ {Vs} {H} {Ts} + {tvs : IBwd (_⊢_ ∅) Vs} + {M : ∅ ⊢ H} + (ts : Algorithmic.ConstrArgs ∅ Ts) + {ZS} + (p : ZS ≡ (Vs <>< (H ∷ Ts))) + {zs : IBwd (∅ ⊢_) ZS} + (q : substEq (IBwd (∅ ⊢_)) p zs ≡ (tvs <>2 Vs (H ∷ Ts)) + (trans (cong (substEq (IBwd (_⊢_ ∅)) (lemma<>2 Vs (H ∷ Ts))) + (trans (IBwd<>IList (lemma<>1 [] (Vs <>> (H ∷ Ts))) x) + ((≡-subst-removable (IBwd (_⊢_ ∅)) _ refl ([] <>>I ((E [ M ]ᴱ) ∷ ts))))))) + (lemma<>I2 tvs ((E [ M ]ᴱ) ∷ ts))) vs')) +lemVE M (EC.case cs E) (V-I⇒ b ()) +lemVE M (EC.case cs E) (V-IΠ b ()) lemBE : ∀{A B b} M (E : EC A B) → ∀{tn tm}{pt : tn ∔ tm ≣ fv (signature b)} @@ -172,7 +204,6 @@ lemBE M (E l· x) (step bt y) = lemBE _ E bt lemBE M (x ·r E) (step bt y) = lemVE _ E y lemBE M (E ·⋆ A / refl) (step⋆ bt refl) = lemBE _ E bt - -- these adhoc lemmas about subst are needed as do the uniqueness bits of -- lemma51! with pattern matching lambdas and can't use "with" @@ -191,6 +222,13 @@ proj· : ∀{A A' B}{t : ∅ ⊢ A ⇒ B}{t' : ∅ ⊢ A' ⇒ B}{u : ∅ ⊢ A}{ × substEq (∅ ⊢_) p u ≡ u' proj· refl = refl ,, refl ,, refl +subst-case : ∀ {B} {A} {B'} {n} + {Tss = Tss : Vec.Vec (List (∅ ⊢Nf⋆ *)) n} + (cs : Algorithmic.Cases ∅ A Tss) (E : EC (SOP Tss) B) + (X : B ≡ B') → + substEq (EC A) X (case cs E) ≡ case cs (substEq (EC (SOP Tss)) X E) +subst-case cs E refl = refl + valred : ∀{A}{L N : ∅ ⊢ A} → Value L → L —→⋆ N → ⊥ valred (V-I⇒ b (step () x₂)) (β-ƛ x) valred (V-I⇒ b (step⋆ () .p)) (β-Λ p) @@ -234,6 +272,9 @@ determinism⋆ (β-Λ refl) (β-Λ refl) = refl determinism⋆ (β-wrap _ refl) (β-wrap _ refl) = refl determinism⋆ (β-builtin b t bt u vu) (β-builtin b' .t bt' .u vu') = BUILTIN-eq _ (step bt vu) (step bt' vu') +determinism⋆ (β-case e Tss refl {ts} vs refl cases) (β-case e' Tss' refl {ts'} vs' q cases') + with inj-IBwd2IList {ts = ts'}{ts} (lemma<>1 [] (lookup Tss e)) q +... | refl = refl data Redex {A : ∅ ⊢Nf⋆ *} : ∅ ⊢ A → Set where β : {L N : ∅ ⊢ A} → L —→⋆ N → Redex L @@ -263,6 +304,34 @@ data RProgress {A : ∅ ⊢Nf⋆ *} (M : ∅ ⊢ A) : Set where ----------- → RProgress M +data FocusedRProgress : ∀{tot}(itot : IList (∅ ⊢_) tot) → Set + where + done : ∀{bs}{ibs : IBwd (∅ ⊢_) bs}{tot}{itot : IList (∅ ⊢_) tot} + {idx : tot ≣ bs <>> []} + (x : (itot ≣I ibs <>> []) idx) + (vs : VList ibs) + → FocusedRProgress itot + step : ∀{tot}{itot : IList (∅ ⊢_) tot} + → ∀{bs}{ibs : IBwd (∅ ⊢_) bs}(vs : VList ibs) --evaluated + → ∀{A : ∅ ⊢Nf⋆ *} {M : ∅ ⊢ A} + ---- + → (Value M → ⊥) + → ∀{B}(E : EC A B){L : ∅ ⊢ B} + → Redex L + → M ≡ E [ L ]ᴱ + → (∀{B'} + → (E' : EC A B') + → {L' : ∅ ⊢ B'} + → M ≡ E' [ L' ]ᴱ + → Redex L' + → ∃ λ (p : B ≡ B') + → substEq (EC A) p E ≡ E' × substEq (∅ ⊢_) p L ≡ L') + ---- + → ∀ {ls : List (∅ ⊢Nf⋆ *)}(cs : ConstrArgs ∅ ls) + → {idx : tot ≣ bs <>> (A ∷ ls)} + → (x : (itot ≣I ibs <>> (M ∷ cs)) idx) + → FocusedRProgress itot + -- these lemmas are needed for the uniqueness cases of lemma51! -- it might be cleaner to define every uniqueness case directly as a lemma @@ -280,45 +349,28 @@ U·⋆1 eq (E' ·⋆ A / r) p q with lem-·⋆ r eq p U·⋆1 {L = L} eq (E' ·⋆ A / r) {L'} p q | refl ,, Y ,, refl ,, refl with lemΛE'' E' Y U·⋆1 {_} {A} {L = L} eq (_·⋆_/_ {_} E' A r) {.(Λ L)} p (β ()) | refl ,, Y ,, refl ,, refl | refl ,, X ,, refl +U·⋆1 p (constr i _ refl vs ts E') () y + -- M is not a value, it has made a step U·⋆2 : ∀{K}{C}{A : ∅ ⊢Nf⋆ K}{B : ∅ ,⋆ K ⊢Nf⋆ *}{M : ∅ ⊢ Π B}{E : EC (Π B) C}{L : ∅ ⊢ C}{X} {B' : ∅ ⊢Nf⋆ *} → ¬ (Value M) - → (p : X ≡ B [ A ]Nf) → - (E' : EC X B') - {L' : ∅ ⊢ B'} → - M _⊢_.·⋆ A / p ≡ (E' [ L' ]ᴱ) → - Redex L' → - (U : {B' : ∅ ⊢Nf⋆ *} (E' : EC (Π B) B') {L' : ∅ ⊢ B'} → - M ≡ (E' [ L' ]ᴱ) → - Redex L' → - ∃ (λ (q : C ≡ B') → substEq (EC _) q E ≡ E' × substEq (_⊢_ ∅) q L ≡ L')) - → - ∃ - (λ (p₁ : C ≡ B') → - substEq - (EC X) - p₁ (E EC.·⋆ A / p) - ≡ E' + → (p : X ≡ B [ A ]Nf) + → (E' : EC X B') + → {L' : ∅ ⊢ B'} → M _⊢_.·⋆ A / p ≡ (E' [ L' ]ᴱ) + → Redex L' + → (U : {B' : ∅ ⊢Nf⋆ *} (E' : EC (Π B) B') {L' : ∅ ⊢ B'} + → M ≡ (E' [ L' ]ᴱ) + → Redex L' + → ∃ (λ (q : C ≡ B') → substEq (EC _) q E ≡ E' × substEq (_⊢_ ∅) q L ≡ L')) + → ∃ (λ (p₁ : C ≡ B') → + substEq (EC X) p₁ (E EC.·⋆ A / p) ≡ E' × substEq (_⊢_ ∅) p₁ L ≡ L') U·⋆2 ¬VM eq [] refl (β (β-Λ .eq)) U = ⊥-elim (¬VM (V-Λ _)) U·⋆2 ¬VM eq (E ·⋆ A / .eq) refl q U with U E refl q ... | refl ,, refl ,, refl = refl ,, refl ,, refl -U·⋆3 : ∀{K}{A : ∅ ⊢Nf⋆ K}{B}{M : ∅ ⊢ Π B}{B' : ∅ ⊢Nf⋆ *}{X} - → (p : X ≡ B [ A ]Nf) → - (E' : EC X B') - {L' : ∅ ⊢ B'} → - Value M → - M _⊢_.·⋆ A / p ≡ (E' [ L' ]ᴱ) → - Redex L' → - ∃ λ (q : X ≡ B') → substEq (EC X) q [] ≡ E' - × substEq (∅ ⊢_) q (M _⊢_.·⋆ A / p) ≡ L' -U·⋆3 eq (E ·⋆ A / .eq) V refl q = ⊥-elim (valredex (lemVE _ E V) q) -U·⋆3 refl [] V refl q = refl ,, refl ,, refl - - -- body of wrap made a step, it's not a value Uwrap : ∀{A C}{B : ∅ ⊢Nf⋆ K}{M : ∅ ⊢ nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)}{L : ∅ ⊢ C}{E}{B' : ∅ ⊢Nf⋆ *} → (E' : EC (μ A B) B') {L' : ∅ ⊢ B'} → @@ -362,7 +414,6 @@ Uunwrap1 ¬VM eq [] refl (β (β-wrap x .eq)) U = ⊥-elim (¬VM (V-wrap x)) Uunwrap1 ¬VM refl (unwrap E / refl) refl q U with U E refl q ... | refl ,, refl ,, refl = refl ,, refl ,, refl - -- beta step Uunwrap2 : ∀{A}{B : ∅ ⊢Nf⋆ K}{M : ∅ ⊢ nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B)}{B' : ∅ ⊢Nf⋆ *}{X} → Value M @@ -373,46 +424,116 @@ Uunwrap2 : ∀{A}{B : ∅ ⊢Nf⋆ K}{M : ∅ ⊢ nf (embNf A · ƛ (μ (embNf ( Redex L' → ∃ (λ (q : X ≡ B') → substEq (EC X) q [] ≡ E' × substEq (∅ ⊢_) q (unwrap (wrap A B M) p) ≡ L') +Uunwrap2 VM eq [] refl q = refl ,, refl ,, refl Uunwrap2 VM eq (unwrap E / x) p q with lem-unwrap p -... | refl ,, refl ,, refl ,, X4 = - ⊥-elim (valredex (lemVE - _ - E - (substEq Value (≅-to-≡ X4) - (V-wrap VM))) q) -Uunwrap2 VM refl [] refl q = refl ,, refl ,, refl - +... | refl ,, refl ,, refl ,, X4 = ⊥-elim (valredex (lemVE _ E (substEq Value (≅-to-≡ X4) (V-wrap VM))) q) + +Ucase2 : ∀ {n} {Tss : Vec.Vec (List (∅ ⊢Nf⋆ *)) n} + {M : (∅ ⊢ SOP Tss)} {A} + {cs : Algorithmic.Cases ∅ A Tss} + (VM : Value M) + {B'} {n'}{Tss' : Vec.Vec (List (∅ ⊢Nf⋆ *)) n'} {L' : ∅ ⊢ B'} + → (cs' : Algorithmic.Cases ∅ A Tss') + → (E' : EC (SOP Tss') B') + → _⊢_.case M cs ≡ _⊢_.case (E' [ L' ]ᴱ) cs' + → Redex L' + → Σ (A ≡ B') (λ p → Σ (substEq (EC A) p [] ≡ case cs' E') (λ x → substEq (_⊢_ ∅) p (case M cs) ≡ L')) +Ucase2 VM cs' E' refl r = ⊥-elim (valredex (lemVE _ E' VM) r) + +constr-helper : ∀ {Bs : Bwd (∅ ⊢Nf⋆ *)} + {bs} (ibs : IBwd (_⊢_ ∅) bs) + {A} (w : ∅ ⊢ A) + {ls} (ils : ConstrArgs ∅ ls) + {ts : IBwd (_⊢_ ∅) Bs} + → (vs : IIBwd Value ts) + → (p : Bs ≡ bs <>< (A ∷ ls)) + → (q : substEq (IBwd (_⊢_ ∅)) p ts ≡ ibs <>> (H ∷ ls)) + → (E : EC H B) (L : ∅ ⊢ B) + → Redex L + → tot ≡ substEq (IList (_⊢_ ∅)) (sym (lem-≣-<>> idx)) (ibs <>>I ((E [ L ]ᴱ) ∷ cs)) + -- Second + → ∀ {i' : Fin n} + {B'} {Vs} {H'} {Ts} + {tvs : IBwd (_⊢_ ∅) Vs} + → (vs' : IIBwd Value tvs) + → (cs' : ConstrArgs ∅ Ts) + → (idx' : lookup Tss i' ≣ Vs <>> (H' ∷ Ts)) + → (E' : EC H' B') (L' : ∅ ⊢ B') + → _≡_ {_}{∅ ⊢ SOP Tss} (constr i Tss refl tot) (constr i' Tss refl (substEq (IList (_⊢_ ∅)) ((sym (lem-≣-<>> idx'))) (tvs <>>I ((E' [ L' ]ᴱ) ∷ cs')))) + → Redex L' + → (∀ {B''} (E'' : EC H B'') {L' = L'' : ∅ ⊢ B''} → + (E [ L ]ᴱ) ≡ (E'' [ L'' ]ᴱ) + → Redex L'' + → Σ (B ≡ B'') (λ p → substEq (EC H) p E ≡ E'' × substEq (_⊢_ ∅) p L ≡ L'')) + → Σ (B ≡ B') (λ p → substEq (EC (SOP Tss)) p (constr i Tss refl {idx} {_} vs cs E) ≡ (constr i' Tss refl {idx'} vs' cs' E') × (substEq _ p L ≡ L')) +Uconstr {tot = tot} vs cs idx E L r p vs' cs' idx' E' L' refl r' U with subst-helper (IList (∅ ⊢_)) (lem-≣-<>> idx') (lem-≣-<>> idx) p +... | x ,, y with equalbyPredicateI tot Value (lem-≣-<>> idx) (lem-≣-<>> idx') p refl vs vs' (λ V → valredex (lemVE _ E V) r) (λ V' → valredex (lemVE _ E' V') r') +... | refl ,, refl ,, refl ,, refl with uniqueVal-List vs vs' | unique-≣-<>> idx idx' +Uconstr {ibs = ibs} vs cs idx E L r p .vs cs' idx' E' L' refl r' U + | refl ,, y | refl ,, refl ,, refl ,, refl | refl | refl with ∷-injectiveI refl (<>>I-cancelˡ ibs ((E' [ L' ]ᴱ) ∷ cs') ((E [ L ]ᴱ) ∷ cs) y) +... | pel ,, refl with U E' (sym pel) r' +... | refl ,, refl ,, refl = refl ,, refl ,, refl +---------- +-- Lemma inspired by Lemma 5.1 (Chapter 5) of Semantics Engineering with PLT Redex +-- by M. Felleisen, R.B. Findler, and M. Flatt rlemma51! : {A : ∅ ⊢Nf⋆ *} → (M : ∅ ⊢ A) → RProgress M + +rlemma51-List : ∀{tot}{itot : IList (∅ ⊢_) tot}{bs}{ibs : IBwd (∅ ⊢_) bs} + {ls}{idx : tot ≣ bs <>> ls} + → (cs : IList (∅ ⊢_) ls) + → (iidx : (itot ≣I ibs <>> cs) idx) + → VList ibs + → FocusedRProgress itot +rlemma51-List [] x Vs = done x Vs +rlemma51-List (c ∷ cs) x Vs with rlemma51! c +... | step ¬VM E p q U = step Vs ¬VM E p q U cs x +... | done V = rlemma51-List cs (bubble x) (Vs :< V) + rlemma51! (ƛ M) = done (V-ƛ M) rlemma51! (M · N) with rlemma51! M ... | step ¬VM E p q U = step (lemV· ¬VM) (E l· N) p - (cong (_· N) q) - λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VM (V-ƛ _)) - ; [] refl (β (β-builtin b .M bt .N vu)) → ⊥-elim (¬VM (V-I⇒ b bt)) - ; (E' l· N') refl r → let X ,, Y ,, Y' = U E' refl r in - X ,, trans ( subst-l· E N X) (cong (_l· N) Y) ,, Y' - ; (VM ·r E') refl r → ⊥-elim (¬VM VM) - } + (cong (_· N) q) + λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VM (V-ƛ _)) + ; [] refl (β (β-builtin b .M bt .N vu)) → ⊥-elim (¬VM (V-I⇒ b bt)) + ; (E' l· N') refl r → let X ,, Y ,, Y' = U E' refl r in X ,, trans ( subst-l· E N X) (cong (_l· N) Y) ,, Y' + ; (VM ·r E') refl rx → ⊥-elim (¬VM VM)} ... | done VM with rlemma51! N ... | step ¬VN E p q U = step (lemV'· ¬VN) (VM ·r E) p - (cong (M ·_) q) - λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VN VN) - ; [] refl (β (β-builtin b .M bt .N VN)) → ⊥-elim (¬VN VN) - ; (E' l· N') refl q → ⊥-elim (valredex (lemVE _ _ VM) q) - ; (VM' ·r E') refl q → let X ,, X'' ,, X''' = U E' refl q in - X - ,, - trans (subst-·r E M VM X) - (trans (cong (VM ·r_) X'') (cong (_·r E') (uniqueVal M VM VM'))) - ,, - X'''} + (cong (M ·_) q) + λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VN VN) + ; [] refl (β (β-builtin b .M bt .N VN)) → ⊥-elim (¬VN VN) + ; (E' l· N') refl q → ⊥-elim (valredex (lemVE _ _ VM) q) + ; (VM' ·r E') refl q → let X ,, X'' ,, X''' = U E' refl q in + X + ,, + trans (subst-·r E M VM X) + (trans (cong (VM ·r_) X'') (cong (_·r E') (uniqueVal M VM VM'))) + ,, + X'''} rlemma51! (.(ƛ M) · N) | done (V-ƛ M) | done VN = step lemVβ [] @@ -429,6 +550,7 @@ rlemma51! (M · N) | done (V-I⇒ b {am = 0} x) | done VN = step refl λ { [] refl (β (β-builtin b .M bt .N vu)) → refl ,, refl ,, refl ; (E' l· N') refl q → ⊥-elim (valredex (lemBE _ E' x) q) +-- ; (E' l·v VN') refl q → ⊥-elim (valredex (lemBE _ E' x) q) ; (VM' ·r E') refl q → ⊥-elim (valredex (lemVE _ E' VN) q)} rlemma51! (M · N) | done (V-I⇒ b {am = suc _} x) | done VN = done (V-I b (step x VN)) @@ -459,6 +581,57 @@ rlemma51! (unwrap M x) with rlemma51! M refl λ E p' q' → Uunwrap2 VM x E p' q' rlemma51! (con c refl) = done (V-con c) +rlemma51! (constr i Tss refl tot) with rlemma51-List tot start [] +... | done {bs}{ibs}{idx = idx} x vs = done + (V-constr i + Tss + refl + (sym (lemma<>2' _ _ (sym (lem-≣-<>> idx)))) + vs + (trans (≡-subst-removable (IList (_⊢_ ∅)) _ _ (ibs <>>I [])) + (sym (lem-≣I-<>>1' x)))) +... | step {bs = bs}{ibs} vs ¬VM E {L} r refl U {ls} cs {idx} x = step + (λ {(V-constr .i .Tss .refl refl {ts} vs' x') → + ¬VM (constr-helper ibs + (E [ L ]ᴱ) + cs + (substEq VList (IBwd<>IList (lemma<>1 [] (lookup Tss i)) {ts} x') vs') + (trans (cong ([] <><_) (lem-≣-<>> idx)) (lemma<>2 bs (_ ∷ ls))) + (trans (trans (trans + (trans (trans + (subst-subst (lemma<>2' ([] <>< lookup Tss i) (lookup Tss i) (lemma<>1 [] (lookup Tss i))) + {(trans (cong ([] <><_) (lem-≣-<>> idx)) (lemma<>2 bs (_ ∷ ls)))}) + (≡-subst-removable (IBwd (∅ ⊢_)) _ _ ([] <><_ []) (lem-≣-<>> idx)) {lemma<>2 bs (_ ∷ ls) } ))) + (cong (substEq (IBwd (_⊢_ ∅)) (lemma<>2 bs (_ ∷ ls))) (sym (lem-<>> idx))))) + (cong (substEq (IBwd (_⊢_ ∅)) (lemma<>2 bs (_ ∷ ls))) (cong ([] <>>1 x)))) + (lemma<>I2 ibs ((E [ L ]ᴱ) ∷ cs)))) }) + (constr i Tss refl { idx } vs cs E) + r + (constr-cong (trans (sym (lem-≣-<>> idx)) refl) (trans (lem-≣I-<>>1' x) (≡-subst-removable (IList (_⊢_ ∅)) _ _ (ibs <>>I ((E [ _ ]ᴱ) ∷ cs))))) + λ { [] refl (β ()) + ; (constr i' .Tss refl {idx'} {tvs} vs' cs' E') {L'} p' r' → + Uconstr vs cs idx E L r (lem-≣I-<>>1' x) + vs' cs' idx' E' L' (trans p' + (sym (constr-cong (trans (sym (lem-≣-<>> idx')) refl) + (≡-subst-removable (IList (_⊢_ ∅)) (sym (lem-≣-<>> idx')) (trans (sym (lem-≣-<>> idx')) refl) _)))) + r' U + } +rlemma51! (case M cs) with rlemma51! M +... | step ¬VM E p q U = step (λ V → ¬VM (lemVE _ (EC.case cs []) V)) + (EC.case cs E) + p + (cong₂ case q refl) + λ { [] refl (β (β-case e _ q vs x .cs)) → ⊥-elim (¬VM (V-constr e _ refl q vs x)) + ; (case x E') refl q' → let X ,, Y ,, Y' = U E' refl q' + in X ,, (trans (subst-case cs E X) (cong (case cs) Y)) ,, Y'} +... | done VM@(V-constr e Tss refl refl vs x) = + step (λ V → valred V (β-case e Tss refl vs x cs)) + [] + (β (β-case e Tss refl vs x cs)) + refl + λ { [] refl r → refl ,, refl ,, refl + ; (EC.case cs' E') p r → Ucase2 VM cs' E' p r} rlemma51! (builtin b / refl) = done (ival b) rlemma51! (error _) = step (valerr E-error) @@ -476,7 +649,6 @@ unique-EC E E' L p q with rlemma51! (E [ L ]ᴱ) ... | refl ,, refl ,, refl with U E refl p ... | refl ,, refl ,, refl = refl - unique-EC' : ∀{A B}(E : EC A B)(L : ∅ ⊢ B) → Redex L → E [ L ]ᴱ ≡ error _ → ∃ λ (p : B ≡ A) → E ≡ substEq (λ A → EC A B) p [] × L ≡ error _ unique-EC' E L p q with rlemma51! (E [ L ]ᴱ) @@ -512,3 +684,4 @@ determinism {L = L} (ruleErr E' p) (ruleErr E'' q) | step ¬VL E err r' U with U ... | refl ,, refl ,, refl | refl ,, refl ,, refl = refl -- -} ``` + \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md index 158998c79a3..e726bb099a0 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md @@ -114,22 +114,22 @@ progress (unwrap M refl) with progress M progress (con c refl) = done (V-con c) progress (builtin b / refl ) = done (ival b) progress (error A) = step (ruleErr [] refl) -progress (constr i TSS refl cs) with progress-focus cs start [] +progress (constr i Tss refl cs) with progress-focus cs start [] ... | done {bs}{ibs}{idx = idx} x Vs = done (V-constr i - TSS + Tss refl (trans (sym (lemma<>2 bs [])) (cong ([] <><_) (sym (lem-≣-<>> idx)))) Vs (trans (≡-subst-removable (IList (_⊢_ ∅)) _ _ (ibs <>>I [])) (sym (lem-≣I-<>>1' x)))) ... | step Vs (ruleEC E p refl refl) cs {idx} x = - step (ruleEC (constr i TSS refl {idx} Vs cs E) + step (ruleEC (constr i Tss refl {idx} Vs cs E) p (constr-cong (trans (sym (lem-≣-<>> idx)) refl) (trans (lem-≣I-<>>1' x) (≡-subst-removable (IList (_⊢_ ∅)) (sym (lem-≣-<>> idx)) (trans (sym (lem-≣-<>> idx)) refl) _))) refl) ... | step Vs (ruleErr E refl) cs {idx} x = - step (ruleErr (constr i TSS refl {idx} Vs cs E) + step (ruleErr (constr i Tss refl {idx} Vs cs E) (constr-cong (trans (sym (lem-≣-<>> idx)) refl) (trans (lem-≣I-<>>1' x) (≡-subst-removable (IList (_⊢_ ∅)) (sym (lem-≣-<>> idx)) (trans (sym (lem-≣-<>> idx)) refl) _))) @@ -137,6 +137,6 @@ progress (constr i TSS refl cs) with progress-focus cs start [] progress (case M cases) with progress M ... | step (ruleEC E p refl refl) = step (ruleEC (case cases E) p refl refl) ... | step (ruleErr E refl) = step (ruleErr (case cases E) refl) -... | done (V-constr e TSS refl refl vs refl) = step (ruleEC [] (β-case e TSS refl vs refl cases) refl refl) +... | done (V-constr e Tss refl refl vs refl) = step (ruleEC [] (β-case e Tss refl vs refl cases) refl refl) \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda index 7a48f9e9ef5..ea3f8eaa859 100644 --- a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda @@ -66,10 +66,10 @@ creating the case type and the renaming. \begin{code} ren-mkCaseType : ∀ {Φ Ψ} → (ρ⋆ : ⋆.Ren Φ Ψ) - → ∀{A} AS - → renNf ρ⋆ (Algorithmic.mkCaseType A AS) ≡ Algorithmic.mkCaseType (renNf ρ⋆ A) (renNf-List ρ⋆ AS) + → ∀{A} As + → renNf ρ⋆ (Algorithmic.mkCaseType A As) ≡ Algorithmic.mkCaseType (renNf ρ⋆ A) (renNf-List ρ⋆ As) ren-mkCaseType ρ⋆ [] = refl -ren-mkCaseType ρ⋆ (x ∷ AS) = cong (renNf ρ⋆ x ⇒_) (ren-mkCaseType ρ⋆ AS) +ren-mkCaseType ρ⋆ (x ∷ As) = cong (renNf ρ⋆ x ⇒_) (ren-mkCaseType ρ⋆ As) \end{code} The actual renaming definition @@ -85,27 +85,27 @@ ren-ConstrArgs : ∀ {Φ Ψ Γ Δ n} → (ρ⋆ : ⋆.Ren Φ Ψ) → (ρ : Ren ρ⋆ Γ Δ) → (e : Fin n) - → (A : Vec (List (Φ ⊢Nf⋆ *)) n) - → (x : ConstrArgs Γ (lookup A e)) + → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + → (x : ConstrArgs Γ (lookup Tss e)) -------------------------------------------- - → ConstrArgs Δ (lookup (renNf-VecList ρ⋆ A) e) + → ConstrArgs Δ (lookup (renNf-VecList ρ⋆ Tss) e) ren-ConstrArgs-List : ∀ {Φ Ψ Γ Δ} → (ρ⋆ : ⋆.Ren Φ Ψ) → (ρ : Ren ρ⋆ Γ Δ) - → {AS : List (Φ ⊢Nf⋆ *) } - → (x : ConstrArgs Γ AS) + → {As : List (Φ ⊢Nf⋆ *) } + → (x : ConstrArgs Γ As) ------------------------------- - → ConstrArgs Δ (renNf-List ρ⋆ AS) + → ConstrArgs Δ (renNf-List ρ⋆ As) ren-Cases : ∀ {Φ Ψ Γ Δ n} → (ρ⋆ : ⋆.Ren Φ Ψ) → (ρ : Ren ρ⋆ Γ Δ) → {A : Φ ⊢Nf⋆ *} - → {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - → (cases : Cases Γ A tss) + → {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + → (cases : Cases Γ A Tss) ------------------------------------------- - → Cases Δ (renNf ρ⋆ A) (renNf-VecList ρ⋆ tss) + → Cases Δ (renNf ρ⋆ A) (renNf-VecList ρ⋆ Tss) ren ρ⋆ ρ (` x) = ` (ρ x) ren ρ⋆ ρ (ƛ N) = ƛ (ren ρ⋆ (ext ρ⋆ ρ) N) @@ -126,18 +126,18 @@ ren ρ⋆ ρ (unwrap {A = A}{B} M refl) = conv⊢ ren ρ⋆ ρ (con {A} c refl) = con c (subNf∅-renNf ρ⋆ A) ren ρ⋆ ρ (builtin b / refl) = conv⊢ refl (btype-ren b ρ⋆) (builtin b / refl) ren ρ⋆ ρ (error A) = error (renNf ρ⋆ A) -ren ρ⋆ ρ (constr e A refl x) = constr e (renNf-VecList ρ⋆ A) refl (ren-ConstrArgs ρ⋆ ρ e A x) +ren ρ⋆ ρ (constr e Tss refl x) = constr e (renNf-VecList ρ⋆ Tss) refl (ren-ConstrArgs ρ⋆ ρ e Tss x) ren ρ⋆ ρ (case x cases) = case (ren ρ⋆ ρ x) (ren-Cases ρ⋆ ρ cases) ren-ConstrArgs-List ρ⋆ ρ [] = [] ren-ConstrArgs-List ρ⋆ ρ (t ∷ xs) = ren ρ⋆ ρ t ∷ ren-ConstrArgs-List ρ⋆ ρ xs -ren-ConstrArgs ρ⋆ ρ e A x - rewrite lookup-renNf-VecList ρ⋆ e A = ren-ConstrArgs-List ρ⋆ ρ x +ren-ConstrArgs ρ⋆ ρ e Tss x + rewrite lookup-renNf-VecList ρ⋆ e Tss = ren-ConstrArgs-List ρ⋆ ρ x ren-Cases ρ⋆ ρ [] = [] -ren-Cases {Δ = Δ} ρ⋆ ρ {tss = AS ∷ _} (c ∷ cases) = subst (Δ ⊢_) - (ren-mkCaseType ρ⋆ AS) +ren-Cases {Δ = Δ} ρ⋆ ρ {Tss = As ∷ _} (c ∷ cases) = subst (Δ ⊢_) + (ren-mkCaseType ρ⋆ As) (ren ρ⋆ ρ c) ∷ (ren-Cases ρ⋆ ρ cases) \end{code} @@ -211,33 +211,33 @@ sub-VecList : ∀ {Φ Ψ Γ Δ n} → (σ⋆ : SubNf Φ Ψ) → (σ : Sub σ⋆ Γ Δ) → (e : Fin n) - → (A : Vec (List (Φ ⊢Nf⋆ *)) n) - → (x : ConstrArgs Γ (lookup A e)) + → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + → (x : ConstrArgs Γ (lookup Tss e)) -------------------------------------- - → ConstrArgs Δ (lookup (eval-VecList (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList A)) (idEnv Ψ)) e) -sub-VecList σ⋆ σ e A x rewrite lookup-eval-VecList e (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList A)) (idEnv _) - | ⋆.lookup-sub-VecList (λ x₁ → embNf (σ⋆ x₁)) e (embNf-VecList A) - | lookup-embNf-VecList e A = sub-ConstrList σ⋆ σ x + → ConstrArgs Δ (lookup (eval-VecList (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList Tss)) (idEnv Ψ)) e) +sub-VecList σ⋆ σ e Tss x rewrite lookup-eval-VecList e (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList Tss)) (idEnv _) + | ⋆.lookup-sub-VecList (λ x₁ → embNf (σ⋆ x₁)) e (embNf-VecList Tss) + | lookup-embNf-VecList e Tss = sub-ConstrList σ⋆ σ x sub-mkCaseType : ∀ {Φ Ψ} → (σ⋆ : SubNf Φ Ψ) - → ∀{A} AS - → subNf σ⋆ (Algorithmic.mkCaseType A AS) - ≡ Algorithmic.mkCaseType (subNf σ⋆ A) (eval-List (⋆.sub-List (λ x₁ → embNf (σ⋆ x₁)) (embNf-List AS)) (idEnv Ψ)) + → ∀{A} As + → subNf σ⋆ (Algorithmic.mkCaseType A As) + ≡ Algorithmic.mkCaseType (subNf σ⋆ A) (eval-List (⋆.sub-List (λ x₁ → embNf (σ⋆ x₁)) (embNf-List As)) (idEnv Ψ)) sub-mkCaseType σ⋆ [] = refl -sub-mkCaseType σ⋆ (x ∷ AS) = cong (subNf σ⋆ x ⇒_) (sub-mkCaseType σ⋆ AS) +sub-mkCaseType σ⋆ (x ∷ As) = cong (subNf σ⋆ x ⇒_) (sub-mkCaseType σ⋆ As) sub-Cases : ∀ {Φ Ψ Γ Δ n} → (σ⋆ : SubNf Φ Ψ) → (σ : Sub σ⋆ Γ Δ) → {A : Φ ⊢Nf⋆ *} - → {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - → (cs : Cases Γ A tss) + → {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + → (cs : Cases Γ A Tss) --------------------------------- - → Cases Δ (subNf σ⋆ A) (eval-VecList (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList tss)) (idEnv Ψ)) + → Cases Δ (subNf σ⋆ A) (eval-VecList (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList Tss)) (idEnv Ψ)) sub-Cases σ⋆ σ [] = [] -sub-Cases {Δ = Δ} σ⋆ σ {tss = AS ∷ _} (c ∷ cs) = subst (Δ ⊢_) - (sub-mkCaseType σ⋆ AS) +sub-Cases {Δ = Δ} σ⋆ σ {Tss = As ∷ _} (c ∷ cs) = subst (Δ ⊢_) + (sub-mkCaseType σ⋆ As) (sub σ⋆ σ c) ∷ (sub-Cases σ⋆ σ cs) @@ -261,7 +261,7 @@ sub σ⋆ σ (unwrap {A = A}{B} M refl) = conv⊢ sub σ⋆ σ (con {A} c refl) = con c (subNf∅-subNf σ⋆ A) sub σ⋆ σ (builtin b / refl) = conv⊢ refl (btype-sub b σ⋆) (builtin b / refl) sub σ⋆ σ (error A) = error (subNf σ⋆ A) -sub σ⋆ σ (constr e A refl x) = constr e _ refl (sub-VecList σ⋆ σ e A x) +sub σ⋆ σ (constr e Tss refl x) = constr e _ refl (sub-VecList σ⋆ σ e Tss x) sub σ⋆ σ (case x cs) = case (sub σ⋆ σ x) (sub-Cases σ⋆ σ cs) \end{code} @@ -350,30 +350,30 @@ renˢ : ∀ {Φ Γ Δ} renˢ-List : ∀ {Φ Γ Δ} → (ρ : Renˢ Γ Δ) - → {AS : List (Φ ⊢Nf⋆ *)} - → ConstrArgs Γ AS + → {As : List (Φ ⊢Nf⋆ *)} + → ConstrArgs Γ As ---------------------- - → ConstrArgs Δ AS + → ConstrArgs Δ As renˢ-List ρ [] = [] renˢ-List ρ (x ∷ xs) = renˢ ρ x ∷ (renˢ-List ρ xs) renˢ-ConstrArgs : ∀ {Φ Γ Δ n} → (ρ : Renˢ Γ Δ) → (e : Fin n) - → (A : Vec (List (Φ ⊢Nf⋆ *)) n) - → (xs : ConstrArgs Γ (lookup A e)) + → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + → (xs : ConstrArgs Γ (lookup Tss e)) ----- - → ConstrArgs Δ (lookup A e) -renˢ-ConstrArgs ρ zero (AS ∷ ASS) xs = renˢ-List ρ xs -renˢ-ConstrArgs ρ (suc e) (AS ∷ ASS) xs = renˢ-ConstrArgs ρ e ASS xs + → ConstrArgs Δ (lookup Tss e) +renˢ-ConstrArgs ρ zero (As ∷ Tss) xs = renˢ-List ρ xs +renˢ-ConstrArgs ρ (suc e) (As ∷ Tss) xs = renˢ-ConstrArgs ρ e Tss xs renˢ-Cases : ∀ {Φ Γ Δ n} → (ρ : Renˢ Γ Δ) → {A : Φ ⊢Nf⋆ *} - → {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - → (cs : Cases Γ A tss) + → {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + → (cs : Cases Γ A Tss) ------------------------------ - → Cases Δ A tss + → Cases Δ A Tss renˢ-Cases ρ [] = [] renˢ-Cases ρ (c ∷ cs) = renˢ ρ c ∷ (renˢ-Cases ρ cs) @@ -387,7 +387,7 @@ renˢ ρ (unwrap M p) = unwrap (renˢ ρ M) p renˢ ρ (con c refl) = con c refl renˢ ρ (builtin b / p) = builtin b / p renˢ ρ (error _) = error _ -renˢ ρ (constr e A refl x) = constr e A refl (renˢ-ConstrArgs ρ e A x) +renˢ ρ (constr e Tss refl x) = constr e Tss refl (renˢ-ConstrArgs ρ e Tss x) renˢ ρ (case x cs) = case (renˢ ρ x) (renˢ-Cases ρ cs) weakenˢ : ∀ {Φ Γ}{A : Φ ⊢Nf⋆ *}{B : Φ ⊢Nf⋆ *} @@ -447,8 +447,8 @@ renˢ-cong : ∀{Φ}{Γ Δ : Ctx Φ}{ρ ρ' : Renˢ Γ Δ} renˢ-List-cong : ∀{Φ}{Γ Δ : Ctx Φ}{ρ ρ' : Renˢ Γ Δ} → (∀{A}(x : Γ ∋ A) → ρ x ≡ ρ' x) - → {AS : List (Φ ⊢Nf⋆ *)} - → (cs : ConstrArgs Γ AS) + → {As : List (Φ ⊢Nf⋆ *)} + → (cs : ConstrArgs Γ As) -------------------------------- → renˢ-List ρ cs ≡ renˢ-List ρ' cs renˢ-List-cong p [] = refl @@ -457,18 +457,18 @@ renˢ-List-cong p (t ∷ cs) = cong₂ _∷_ (renˢ-cong p t) (renˢ-List-cong p renˢ-ConstrArgs-cong : ∀{Φ}{Γ Δ : Ctx Φ}{ρ ρ' : Renˢ Γ Δ}{n} → (∀{A}(x : Γ ∋ A) → ρ x ≡ ρ' x) → (e : Fin n) - → (A : Vec (List (Φ ⊢Nf⋆ *)) n) - → (cs : ConstrArgs Γ (lookup A e)) + → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + → (cs : ConstrArgs Γ (lookup Tss e)) --------------------------------------------------- - → renˢ-ConstrArgs ρ e A cs ≡ renˢ-ConstrArgs ρ' e A cs -renˢ-ConstrArgs-cong p zero (x ∷ A) cs = renˢ-List-cong p cs -renˢ-ConstrArgs-cong p (suc e) (x ∷ A) cs = renˢ-ConstrArgs-cong p e A cs + → renˢ-ConstrArgs ρ e Tss cs ≡ renˢ-ConstrArgs ρ' e Tss cs +renˢ-ConstrArgs-cong p zero (_ ∷ _) cs = renˢ-List-cong p cs +renˢ-ConstrArgs-cong p (suc e) (_ ∷ Tss) cs = renˢ-ConstrArgs-cong p e Tss cs renˢ-Cases-cong : ∀ {Φ} {Γ Δ : Ctx Φ} {ρ ρ' : Renˢ Γ Δ} (p : {A : Φ ⊢Nf⋆ *} (x : Γ ∋ A) → ρ x ≡ ρ' x) {A : Φ ⊢Nf⋆ *} {n} - {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cs : Cases Γ A tss) + {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cs : Cases Γ A Tss) -------------------------------------------------- → renˢ-Cases ρ cs ≡ renˢ-Cases ρ' cs renˢ-Cases-cong p [] = refl @@ -484,7 +484,7 @@ renˢ-cong p (unwrap M q) = cong (λ M → unwrap M q) (renˢ-cong p M) renˢ-cong p (con c refl) = refl renˢ-cong p (builtin b / q) = refl renˢ-cong p (error _) = refl -renˢ-cong p (constr e A refl x) = cong (constr e A refl) (renˢ-ConstrArgs-cong p e A x) +renˢ-cong p (constr e Tss refl x) = cong (constr e Tss refl) (renˢ-ConstrArgs-cong p e Tss x) renˢ-cong p (case M cs) = cong₂ case (renˢ-cong p M) (renˢ-Cases-cong p cs) renˢ-id : ∀ {Φ Γ}{A : Φ ⊢Nf⋆ *}(M : Γ ⊢ A) @@ -498,16 +498,16 @@ renˢ-List-id (t ∷ cs) = cong₂ _∷_ (renˢ-id t) (renˢ-List-id cs) renˢ-ConstrArgs-id : ∀ {Φ} {Γ : Ctx Φ} {n} (e : Fin n) - (A : Vec (List (Φ ⊢Nf⋆ *)) n) - (cs : ConstrArgs Γ (lookup A e)) + (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + (cs : ConstrArgs Γ (lookup Tss e)) ----------------------------- - → renˢ-ConstrArgs id e A cs ≡ cs -renˢ-ConstrArgs-id zero (A ∷ AS) cs = renˢ-List-id cs -renˢ-ConstrArgs-id (suc e) (A ∷ AS) cs = renˢ-ConstrArgs-id e AS cs + → renˢ-ConstrArgs id e Tss cs ≡ cs +renˢ-ConstrArgs-id zero (_ ∷ _) cs = renˢ-List-id cs +renˢ-ConstrArgs-id (suc e) (_ ∷ Tss) cs = renˢ-ConstrArgs-id e Tss cs renˢ-Cases-id : ∀ {Φ} {Γ : Ctx Φ} {A : Φ ⊢Nf⋆ *} {n} - {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cases : Cases Γ A tss) → + {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cases : Cases Γ A Tss) → renˢ-Cases id cases ≡ cases renˢ-Cases-id [] = refl renˢ-Cases-id (c ∷ cases) = cong₂ _∷_ (renˢ-id c) (renˢ-Cases-id cases) @@ -522,7 +522,7 @@ renˢ-id (unwrap M p) = cong (λ M → unwrap M p) (renˢ-id M) renˢ-id (con c refl) = refl renˢ-id (builtin b / p) = refl renˢ-id (error _) = refl -renˢ-id (constr e A refl x) = cong (constr e A refl) (renˢ-ConstrArgs-id e A x) +renˢ-id (constr e Tss refl x) = cong (constr e Tss refl) (renˢ-ConstrArgs-id e Tss x) renˢ-id (case M cases) = cong₂ case (renˢ-id M) (renˢ-Cases-id cases) renˢ-comp : ∀ {Φ Γ Δ Θ}{A : Φ ⊢Nf⋆ *} @@ -541,16 +541,16 @@ renˢ-List-comp (t ∷ cs) = cong₂ _∷_ (renˢ-comp t) (renˢ-List-comp cs) renˢ-ConstrArgs-comp : ∀ {Φ} {Γ Δ Θ : Ctx Φ} {ρ : Renˢ Δ Θ} {ρ' : Renˢ Γ Δ} {n} (e : Fin n) - (A : Vec (List (Φ ⊢Nf⋆ *)) n) - (x : ConstrArgs Γ (lookup A e)) + (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) + (x : ConstrArgs Γ (lookup Tss e)) -------------------------------------------------------------------------------- - → renˢ-ConstrArgs (ρ ∘ ρ') e A x ≡ renˢ-ConstrArgs ρ e A (renˢ-ConstrArgs ρ' e A x) -renˢ-ConstrArgs-comp zero (A ∷ AS) x = renˢ-List-comp x -renˢ-ConstrArgs-comp (suc e) (A ∷ AS) x = renˢ-ConstrArgs-comp e AS x + → renˢ-ConstrArgs (ρ ∘ ρ') e Tss x ≡ renˢ-ConstrArgs ρ e Tss (renˢ-ConstrArgs ρ' e Tss x) +renˢ-ConstrArgs-comp zero (_ ∷ _) x = renˢ-List-comp x +renˢ-ConstrArgs-comp (suc e) (_ ∷ Tss) x = renˢ-ConstrArgs-comp e Tss x renˢ-Cases-comp : ∀ {Φ} {Γ Δ Θ : Ctx Φ} {A : Φ ⊢Nf⋆ *} - {ρ : Renˢ Δ Θ} {ρ' : Renˢ Γ Δ} {n} {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cs : Cases Γ A tss) + {ρ : Renˢ Δ Θ} {ρ' : Renˢ Γ Δ} {n} {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cs : Cases Γ A Tss) ------------------------------------------------------- → renˢ-Cases (ρ ∘ ρ') cs ≡ renˢ-Cases ρ (renˢ-Cases ρ' cs) renˢ-Cases-comp [] = refl @@ -566,7 +566,7 @@ renˢ-comp (unwrap M p) = cong (λ M → unwrap M p) (renˢ-comp M) renˢ-comp (con c refl) = refl renˢ-comp (builtin b / p) = refl renˢ-comp (error _) = refl -renˢ-comp (constr e A refl x) = cong (constr e A refl) (renˢ-ConstrArgs-comp e A x) +renˢ-comp (constr e Tss refl x) = cong (constr e Tss refl) (renˢ-ConstrArgs-comp e Tss x) renˢ-comp (case M cs) = cong₂ case (renˢ-comp M) (renˢ-Cases-comp cs) diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda b/plutus-metatheory/src/Algorithmic/Soundness.lagda index eed24d5e824..8653d9930ba 100644 --- a/plutus-metatheory/src/Algorithmic/Soundness.lagda +++ b/plutus-metatheory/src/Algorithmic/Soundness.lagda @@ -143,23 +143,23 @@ btype-lem≡β {Φ} b rewrite btype-lem {Φ} b = soundness (Dec.btype {Φ} b) emb : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A emb-ConstrArgs : ∀ {Φ} {Γ : Alg.Ctx Φ} - {TS : List (Φ ⊢Nf⋆ *)} - (cs : Alg.ConstrArgs Γ TS) → - Dec.ConstrArgs (embCtx Γ) (embNf-List TS) + {Ts : List (Φ ⊢Nf⋆ *)} + (cs : Alg.ConstrArgs Γ Ts) → + Dec.ConstrArgs (embCtx Γ) (embNf-List Ts) emb-ConstrArgs [] = [] emb-ConstrArgs (x ∷ cs) = (emb x) ∷ (emb-ConstrArgs cs) -lema-mkCaseType : ∀{Φ}{A : Φ ⊢Nf⋆ *} AS → - embNf (Alg.mkCaseType A AS) ≡ Dec.mkCaseType (embNf A) (embNf-List AS) +lema-mkCaseType : ∀{Φ}{A : Φ ⊢Nf⋆ *} As → + embNf (Alg.mkCaseType A As) ≡ Dec.mkCaseType (embNf A) (embNf-List As) lema-mkCaseType [] = refl -lema-mkCaseType (A ∷ AS) = cong (embNf A ⇒_) (lema-mkCaseType AS) +lema-mkCaseType (A ∷ As) = cong (embNf A ⇒_) (lema-mkCaseType As) emb-Cases : ∀ {Φ} {Γ : Alg.Ctx Φ} {A : Φ ⊢Nf⋆ *} {n} - {tss : Vec (List (Φ ⊢Nf⋆ *)) n} - (cases : Alg.Cases Γ A tss) - → Dec.Cases (embCtx Γ) (embNf A) (embNf-VecList tss) + {Tss : Vec (List (Φ ⊢Nf⋆ *)) n} + (cases : Alg.Cases Γ A Tss) + → Dec.Cases (embCtx Γ) (embNf A) (embNf-VecList Tss) emb-Cases Alg.[] = Dec.[] -emb-Cases (Alg._∷_ {AS = AS} c cases) = substEq (embCtx _ Dec.⊢_) (lema-mkCaseType AS) (emb c) +emb-Cases (Alg._∷_ {Ts = Ts} c cases) = substEq (embCtx _ Dec.⊢_) (lema-mkCaseType Ts) (emb c) Dec.∷ (emb-Cases cases) emb (Alg.` α) = Dec.` (embVar α) @@ -177,7 +177,7 @@ emb (Alg.unwrap {A = A}{B} t refl) = emb (Alg.con {A = A} t refl ) = Dec.con {A = embNf A} (substEq Alg.⟦_⟧ (sym (stability A)) t) (subNf∅-sub∅-lem _ A) emb (Alg.builtin b / refl) = Dec.conv (btype-lem≡β b) (Dec.builtin b) emb (Alg.error A) = Dec.error (embNf A) -emb (Alg.constr e TSS refl cs) = Dec.constr e (embNf-VecList TSS) (sym (lookup-embNf-VecList e TSS)) (emb-ConstrArgs cs) +emb (Alg.constr e Tss refl cs) = Dec.constr e (embNf-VecList Tss) (sym (lookup-embNf-VecList e Tss)) (emb-ConstrArgs cs) emb (Alg.case x cases) = Dec.case (emb x) (emb-Cases cases) soundnessT : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md index 877a01476cc..363f3b17406 100644 --- a/plutus-metatheory/src/Check.lagda.md +++ b/plutus-metatheory/src/Check.lagda.md @@ -81,7 +81,7 @@ data TypeError : Set where notMu : ∀{Φ}(A : Φ ⊢Nf⋆ *) → (∀{K}(A' : Φ ⊢Nf⋆ _)(B : Φ ⊢Nf⋆ K) → ¬ (A ≡ μ A' B)) → TypeError notFunType : ∀{Φ}(A : Φ ⊢Nf⋆ *) → ((A' B : Φ ⊢Nf⋆ *) → ¬ (A ≡ A' ⇒ B)) → TypeError - notSOP : ∀{Φ}(A : Φ ⊢Nf⋆ *) → (∀{n}(A' : Vec (List (Φ ⊢Nf⋆ *)) n) → ¬ (A ≡ SOP A')) → TypeError + notSOP : ∀{Φ}(A : Φ ⊢Nf⋆ *) → (∀{n}(Tss : Vec (List (Φ ⊢Nf⋆ *)) n) → ¬ (A ≡ SOP Tss)) → TypeError IndexOutOfBounds : ∀{i n} → ¬(i < n) → TypeError TooManyConstrArgs : TypeError TooFewConstrArgs : TypeError @@ -170,23 +170,23 @@ isMu (SOP x ,, _) = inj₁ (notMu (SOP x) (λ _ _ ())) isSOPType : ∀{Φ} → (Φ ⊢Nf⋆ *) - → Either TypeError (Σ ℕ (λ n → Vec (List (Φ ⊢Nf⋆ *)) n )) + → Either TypeError (Σ ℕ (Vec (List (Φ ⊢Nf⋆ *)))) isSOPType (Π A) = inj₁ (notSOP (Π A) (λ _ ())) isSOPType (A ⇒ B) = inj₁ (notSOP (A ⇒ B) (λ _ ())) isSOPType (ne A) = inj₁ (notSOP (ne A) (λ _ ())) isSOPType (con c) = inj₁ (notSOP (con c) (λ _ ())) isSOPType (μ A B) = inj₁ (notSOP (μ A B) (λ _ ())) -isSOPType (SOP {n = n} TSS) = return (n ,, TSS) +isSOPType (SOP {n = n} Tss) = return (n ,, Tss) isSOP : ∀{Φ Γ} → Σ (Φ ⊢Nf⋆ *) (Γ ⊢_) - → Either TypeError (Σ ℕ λ n → Σ (Vec (List (Φ ⊢Nf⋆ *)) n) λ TSS → Γ ⊢ SOP TSS) + → Either TypeError (Σ ℕ λ n → Σ (Vec (List (Φ ⊢Nf⋆ *)) n) λ Tss → Γ ⊢ SOP Tss) isSOP (Π A ,, _) = inj₁ (notSOP (Π A) (λ _ ())) isSOP ((A ⇒ B) ,, _) = inj₁ (notSOP (A ⇒ B) (λ _ ())) isSOP (ne A ,, _) = inj₁ (notSOP (ne A) (λ _ ())) isSOP (con c ,, _) = inj₁ (notSOP (con c) (λ _ ())) isSOP (μ A B ,, x) = inj₁ (notSOP (μ A B) (λ _ ())) -isSOP (SOP {n = n} TSS ,, x) = return (n ,, (TSS ,, x)) +isSOP (SOP {n = n} Tss ,, x) = return (n ,, (Tss ,, x)) chkIdx : ∀ (i n : ℕ) → Either TypeError (Fin n) chkIdx i n with i >-++ bs (lemma-bwd-foldr f (f b e) bs) ``` +Some cancellation lemmas + +``` +<><-cancelʳ : ∀{A : Set} (bs bs' : Bwd A) xs → bs <>< xs ≡ bs' <>< xs → bs ≡ bs' +<><-cancelʳ bs bs' [] p = p +<><-cancelʳ bs bs' (x ∷ xs) p with <><-cancelʳ (bs :< x) (bs' :< x) xs p +... | refl = refl + +<>>[]-cancelʳ : ∀{A : Set} (bs bs' : Bwd A) → bs <>> [] ≡ bs' <>> [] → bs ≡ bs' +<>>[]-cancelʳ bs bs' p = trans (sym (lemma<>2' bs (bs' <>> []) p)) (lemma<>2 bs' []) + +<>>-cancelʳ : ∀{A : Set} (bs bs' : Bwd A) xs → bs <>> xs ≡ bs' <>> xs → bs ≡ bs' +<>>-cancelʳ bs bs' xs p = <>>[]-cancelʳ bs bs' + (++-cancelʳ (bs <>> []) (bs' <>> []) (trans (sym (lemma-<>>-++ bs [] xs)) + (trans p (lemma-<>>-++ bs' [] xs)))) + +<>>-cancelˡ : ∀{A : Set} (bs : Bwd A) xs xs' → bs <>> xs ≡ bs <>> xs' → xs ≡ xs' +<>>-cancelˡ [] xs xs' p = p +<>>-cancelˡ (bs :< x) xs xs' p with <>>-cancelˡ bs (x ∷ xs) (x ∷ xs') p +... | refl = refl +``` + ## Indexed Lists Indexed lists `IList` are lists of elements of an indexed set. @@ -114,6 +140,14 @@ iGetIdx {ts = ts} ils = ts -- snoc for Indexed Lists. _:I2 : ∀{A}{B : A → Set}{xs : Bwd A}{ys : List A}(ixs : IBwd B xs)(iys lemma<>I2 [] iys = refl lemma<>I2 (ixs :< ix) iys = lemma<>I2 ixs (ix ∷ iys) +lemma<>I2' : ∀{A}{B : A → Set}{xs : Bwd A}{ys : List A}(ixs : IBwd B xs)(iys : IList B ys) + → ([] <>>I iys)) ≡ subst (IBwd B) (sym (lemma<>2 xs ys)) (ixs <>I2' [] iys = refl +lemma<>I2' (ixs :< ix) iys = lemma<>I2' ixs (ix ∷ iys) + +IBwd2IList' : ∀{A}{B : A → Set}{bs}{ts} → (bs ≡ [] <>< ts) → IBwd B bs → IList B ts +IBwd2IList' {ts = ts} p tbs = subst (IList _) (trans (cong (_<>> []) p) (lemma<>1 [] ts)) (tbs <>>I []) + IBwd2IList : ∀{A}{B : A → Set}{bs}{ts} → (bs <>> [] ≡ ts) → IBwd B bs → IList B ts IBwd2IList p tbs = subst (IList _) p (tbs <>>I []) + +IList2IBwd : ∀{A}{B : A → Set}{ts}{bs} → ([] <>< ts ≡ bs) → IList B ts → IBwd B bs +IList2IBwd {ts = ts} p tbs = subst (IBwd _) p ([] <>IList : ∀{A}{B : A → Set}{bs}{ts} → (p : bs <>> [] ≡ ts) → {ibs : IBwd B bs} + → {its : IList B ts} + → IBwd2IList p ibs ≡ its + → ibs ≡ IList2IBwd (lemma<>2' _ _ p) its +IBwd<>IList refl {ibs} refl rewrite lemma<>I2 ibs [] = refl + +split : ∀{A : Set} bs (ts : List A){B : A → Set} → IList B (bs <>> ts) → IBwd B bs × IList B ts +split [] ts vs = [] , vs +split (bs :< x) ts vs with split bs (x ∷ ts) vs +... | ls , (x ∷ rs) = ls :< x , rs + +bsplit : ∀{A : Set} bs (ts : List A){B : A → Set} → IBwd B (bs <>< ts) → IBwd B bs × IList B ts +bsplit bs [] vs = vs , [] +bsplit bs (x ∷ ts) vs with bsplit (bs :< x) ts vs +... | ls :< x , rs = ls , (x ∷ rs) + +inj-IBwd2IList : ∀{A}{B : A → Set}{Bs}{As : List A}{ts ts' : IBwd B Bs} + → (p : Bs <>> [] ≡ As) + → IBwd2IList {ts = As} p ts ≡ IBwd2IList p ts' + → ts ≡ ts' +inj-IBwd2IList refl q = trans (trans (sym (lemma<>I2 _ [])) (cong (IList2IBwd (lemma<>2' _ _ refl)) q)) (lemma<>I2 _ []) ``` ## A type for Zipper indexes @@ -160,7 +227,6 @@ data _≣_<>>_ {A : Set} : (as : List A) → Bwd A → List A → Set where --------------------------- → as ≣ (vs :< t) <>> ts - lem-≣-<>> : ∀{A : Set}{tot vs}{ts : List A} → tot ≣ vs <>> ts → tot ≡ vs <>> ts lem-≣-<>> start = refl lem-≣-<>> (bubble x) = lem-≣-<>> x @@ -174,6 +240,11 @@ done-≣-<>> = lem-≣-<>>' (sym (lemma<>1 [] _)) no-empty-≣-<>> : ∀{A : Set}{vs}{h : A}{ts} → [] ≣ vs <>> (h ∷ ts) → ⊥ no-empty-≣-<>> (bubble r) = no-empty-≣-<>> r + +unique-≣-<>> : ∀{A : Set}{tot vs}{ts : List A}(p q : tot ≣ vs <>> ts) → p ≡ q +unique-≣-<>> start start = refl +unique-≣-<>> (bubble p) (bubble q) with unique-≣-<>> p q +... | refl = refl ``` ## Lists indexed by an indexed list @@ -183,9 +254,61 @@ data IIList {A : Set}{B : A → Set}(C : ∀{a : A}(b : B a) → Set) : ∀{is} [] : IIList C [] _∷_ : ∀{a as}{i : B a}{is : IList B as} → C i → IIList C is → IIList C (i ∷ is) + data IIBwd {A : Set}{B : A → Set}(C : ∀{a : A}→ B a → Set) : ∀{is} → IBwd B is → Set where [] : IIBwd C [] _:<_ : ∀{a as}{i : B a}{is : IBwd B as} → IIBwd C is → C i → IIBwd C (is :< i) + +-- Chip for double indexed lists +_<>>II_ : ∀{A : Set}{B : A → Set}{C : ∀{a : A}(b : B a) → Set}{bs : Bwd A}{ts : List A} + {ibs : IBwd B bs}{its : IList B ts} + → IIBwd C ibs → IIList C its → IIList C (ibs <>>I its) +[] <>>II tls = tls +(tbs :< x) <>>II tls = tbs <>>II (x ∷ tls) + +-- Convert an IIBwd into an IIList +IIBwd2IIList : ∀{A}{B : A → Set}{C : ∀{a : A}(b : B a) → Set}{bs}{ts : List A} + {ibs : IBwd B bs}{its : IList B ts} + → (p : bs <>> [] ≡ ts) + → (q : subst (IList B) p (ibs <>>I []) ≡ its) + → IIBwd C ibs + → IIList C its +IIBwd2IIList refl refl tbs = tbs <>>II [] + +-- Split an IIList +splitI : ∀{A : Set}{bs}{ts : List A}{B : A → Set}{C : ∀{a : A}(b : B a) → Set} + (ibs : IBwd B bs)(its : IList B ts) + → IIList C (ibs <>>I its) → IIBwd C ibs × IIList C its +splitI [] its xs = [] , xs +splitI (ibs :< x) its xs with splitI ibs (x ∷ its) xs +... | ls , (y ∷ rs) = (ls :< y) , rs + +-- Split an IIBwd +bsplitI : ∀{A : Set}{bs}{ts : List A}{B : A → Set}{C : ∀{a : A}(b : B a) → Set} + (ibs : IBwd B bs)(its : IList B ts) + → IIBwd C (ibs <>>I (b ∷ fs)) + → C b +proj-IIList b bs fs xs with splitI bs (b ∷ fs) xs +... | _ , (Cb ∷ _) = Cb + +-- project from an IIBwd +proj-IIBwd : ∀{A : Set}{B : A → Set}{C : ∀{a : A}(b : B a) → Set} + {a} (b : B a) {Bs}{Fs} + (bs : IBwd B Bs) (fs : IList B Fs) + → IIBwd C (bs <>>2' {ibs = ibs :< x} refl refl = bubble (lem-≣I-<>>2' refl refl) done-≣I-<>> : ∀{A : Set}{B : A → Set}{tot : List A}(itot : IList B tot) → (itot ≣I ([] <>> []) done-≣-<>> done-≣I-<>> itot = lem-≣I-<>>2 (lemma<>1 [] _) (sym (lemma<>I1 [] itot)) + +lemma<>I3 : ∀{A}{B : A → Set}{bs : Bwd A} + → (ibs : IBwd B bs)(iys : IList B (bs <>> [])) + → ibs <>>I [] ≡ iys → subst (IBwd B) (lemma<>2 bs []) ([] <>I3 xs ys refl = lemma<>I2 xs [] + +lem-<><_) p) ([] <>>I-++I : ∀{A : Set}{B : A → Set}{bs}{as as' : List A} + → (ibs : IBwd B bs)(ias : IList B as)(ias' : IList B as') + → ibs <>>I (ias ++I ias') ≡ subst (IList B) (sym (lemma-<>>-++ bs as as')) ((ibs <>>I ias) ++I ias') +lemma-<>>I-++I [] ias ias' = refl +lemma-<>>I-++I (ibs :< x) ias ias' = lemma-<>>I-++I ibs (x ∷ ias) ias' ``` +Cancellation law for <>>I - \ No newline at end of file +``` +<>>I[]-cancelʳ : ∀{A : Set}{B : A → Set}{bs : Bwd A}(ibs ibs' : IBwd B bs) + → ibs <>>I [] ≡ ibs' <>>I [] → ibs ≡ ibs' +<>>I[]-cancelʳ ibs ibs' p = trans (sym (lemma<>I3 ibs (ibs' <>>I []) p)) (lemma<>I2 ibs' []) + +<>>I-cancelˡ : ∀{A : Set}{B : A → Set}{bs : Bwd A}{xs} + (ibs : IBwd B bs) + → (ixs ixs' : IList B xs) + → ibs <>>I ixs ≡ ibs <>>I ixs' → ixs ≡ ixs' +<>>I-cancelˡ [] ixs ixs' p = p +<>>I-cancelˡ (ibs :< x) ixs ixs' p with <>>I-cancelˡ ibs (x ∷ ixs) (x ∷ ixs') p +... | refl = refl + +``` +We may have that Bs <>>I (H :: Fs) ≡ Bs' <>>I (H' :: Fs'). +We cannot conclude that Bs ≡ Bs', H ≡ H' and Fs ≡ Fs', because the focus +could be at different places of the same indexed list. +However, if there is a predicate P such that P holds for every element of Bs and Bs', +but ¬(P H) and ¬(P H'), then this determines where the focus is and we may conclude that +Bs ≡ Bs', H ≡ H' and Fs ≡ Fs'. + +``` +equalbyPredicate++ : ∀{A : Set} + (P : A → Set) + {bs bs' : List A}{fs fs'} + {tot : List A} + {h h' : A} + → (p : tot ≡ bs ++ (h ∷ fs)) + → (p' : tot ≡ bs' ++ (h' ∷ fs')) + → (IList P bs) + → (IList P bs') + → (¬Ph : ¬(P h)) + → (¬Ph' : ¬(P h')) + → bs ≡ bs' +equalbyPredicate++ P p p' [] [] ¬Ph ¬Ph' = refl +equalbyPredicate++ P refl refl [] (x ∷ ps') ¬Ph ¬Ph' = ⊥-elim (¬Ph x) +equalbyPredicate++ P refl refl (x ∷ ps) [] ¬Ph ¬Ph' = ⊥-elim (¬Ph' x) +equalbyPredicate++ P {a ∷ as} refl p' (x ∷ ps) (x₁ ∷ ps') ¬Ph ¬Ph' with ∷-injective p' +... | refl , q = cong (a ∷_) (equalbyPredicate++ P {as} refl q ps ps' ¬Ph ¬Ph') + + +equalbyPredicate : ∀{A : Set} + (P : A → Set) + {bs bs' : Bwd A}{fs fs'}{tot} + {h h' : A} + → (p : tot ≡ bs <>> (h ∷ fs)) + → (p' : tot ≡ bs' <>> (h' ∷ fs')) + → (IBwd P bs) + → (IBwd P bs') + → (¬Ph : ¬(P h)) + → (¬Ph' : ¬(P h')) + → bs ≡ bs' +equalbyPredicate P {bs} {bs'} {fs} {fs'} {tot} {h} {h'} p p' ps ps' ¬Ph ¬Ph' = + <>>[]-cancelʳ _ _ (equalbyPredicate++ P + (trans p (lemma-<>>-++ bs [] (h ∷ fs))) + (trans p' (lemma-<>>-++ bs' [] (h' ∷ fs'))) + (IBwd2IList refl ps) + (IBwd2IList refl ps') + ¬Ph + ¬Ph') + +equalbyPredicate++I : ∀{A : Set}{B : A → Set}{bs bs' : List A}{fs fs'}{tot} + (TOT : IList B tot) + {Bs : IList B bs}{Bs' : IList B bs'} + {Fs : IList B fs}{Fs' : IList B fs'} + {h h' : A} + {H : B h}{H' : B h'} + → (P : {a : A} → B a → Set) + → (p : tot ≡ bs ++ (h ∷ fs)) + → (p' : tot ≡ bs' ++ (h' ∷ fs')) + → (q : TOT ≡ subst (IList B) (sym p) (Bs ++I (H ∷ Fs))) + → (q' : TOT ≡ subst (IList B) (sym p') (Bs' ++I (H' ∷ Fs'))) + → (ps : IIList P Bs) + → (ps' : IIList P Bs') + → (¬PH : ¬(P H)) + → (¬PH' : ¬(P H')) + → Σ (bs ≡ bs') (λ { refl → + Σ (h ≡ h') (λ { refl → + Σ (fs ≡ fs') (λ { refl → Bs ≡ Bs' }) }) }) +equalbyPredicate++I TOT P p p' q q' [] [] ¬PH ¬PH' with ∷-injective (trans (sym p) p') +... | refl , refl = refl , (refl , (refl , refl)) +equalbyPredicate++I TOT P refl refl refl refl [] (x ∷ ps') ¬PH ¬PH' = ⊥-elim (¬PH x) +equalbyPredicate++I TOT P refl refl refl refl (x ∷ ps) [] ¬PH ¬PH' = ⊥-elim (¬PH' x) +equalbyPredicate++I TOT P refl p' refl q' (x ∷ ps) (x₁ ∷ ps') ¬PH ¬PH' with ∷-injective p' +... | refl , pt with ∷-injectiveI (sym p') q' +... | refl , qt with equalbyPredicate++I _ P refl pt refl + (trans qt (≡-subst-removable (IList _) (proj₂ (∷-injective (sym p'))) (sym pt) _)) + ps ps' ¬PH ¬PH' +... | refl , refl , refl , refl = refl , (refl , (refl , refl)) + +equalbyPredicateI : ∀{A : Set}{B : A → Set}{bs bs' : Bwd A}{fs fs'}{tot} + (TOT : IList B tot) + {Bs : IBwd B bs}{Bs' : IBwd B bs'} + {Fs : IList B fs}{Fs' : IList B fs'} + {h h' : A} + {H : B h}{H' : B h'} + → (P : {a : A} → B a → Set) + → (p : tot ≡ bs <>> (h ∷ fs)) + → (p' : tot ≡ bs' <>> (h' ∷ fs')) + → (q : TOT ≡ subst (IList B) (sym p) (Bs <>>I (H ∷ Fs))) + → (q' : TOT ≡ subst (IList B) (sym p') (Bs' <>>I (H' ∷ Fs'))) + → (ps : IIBwd P Bs) + → (ps' : IIBwd P Bs') + → (¬PH : ¬(P H)) + → (¬PH' : ¬(P H')) + → Σ (bs ≡ bs') (λ { refl → + Σ (h ≡ h') (λ { refl → + Σ (fs ≡ fs') (λ { refl → Bs ≡ Bs' }) }) }) +equalbyPredicateI {bs = bs}{bs'}{fs}{fs'}{tot} TOT {Bs} {Bs'} {Fs} {Fs'} {h} {h'} {H} {H'} P refl p' refl q' ps ps' ¬PH ¬PH' with + equalbyPredicate++I TOT + P + (lemma-<>>-++ bs [] (h ∷ fs)) + (trans p' (lemma-<>>-++ bs' [] (h' ∷ fs'))) + ((lemma-<>>I-++I Bs [] (H ∷ Fs))) + (trans q' + (trans (cong (subst (IList _) (sym p')) (lemma-<>>I-++I Bs' [] (H' ∷ Fs'))) + (trans (subst-subst {P = IList _} (sym (lemma-<>>-++ bs' [] (h' ∷ fs'))) {sym p'} {(Bs' <>>I []) ++I (H' ∷ Fs')}) + (≡-subst-removable (IList _) (trans (sym (lemma-<>>-++ bs' [] (h' ∷ fs'))) (sym p')) (sym (trans p' (lemma-<>>-++ bs' [] (h' ∷ fs')))) _)))) + (IIBwd2IIList refl refl ps) + (IIBwd2IIList refl refl ps') + ¬PH + ¬PH' +... | pbs , snd with <>>[]-cancelʳ bs bs' pbs +equalbyPredicateI TOT {Bs} {Bs'} P p p' q q' ps ps' ¬PH ¬PH' + | refl , refl , refl , pBs | refl with <>>I[]-cancelʳ Bs Bs' pBs +... | refl = refl , refl , refl , refl \ No newline at end of file diff --git a/plutus-metatheory/src/index.lagda.md b/plutus-metatheory/src/index.lagda.md index dd00073cbc4..19f5326b1df 100644 --- a/plutus-metatheory/src/index.lagda.md +++ b/plutus-metatheory/src/index.lagda.md @@ -113,7 +113,6 @@ import Declarative.Examples.StdLib.Function import Declarative.Examples.StdLib.ChurchNat import Declarative.Examples.StdLib.Nat ``` - ## Algorithmic syntax Terms, reduction and evaluation where terms are indexed by normal @@ -143,9 +142,7 @@ Proof for Progress and Determinism of the Reduction Semantics: ``` import Algorithmic.ReductionEC.Progress - ---TODO : Finish proof for SOPs ---import Algorithmic.ReductionEC.Determinism +import Algorithmic.ReductionEC.Determinism ``` There are proofs of correspondence of the semantics of: @@ -165,7 +162,6 @@ There are proofs of correspondence of the semantics of: Extrinsically typed terms, reduction and evaluation ``` -import Scoped --TODO : Finish proof for SOPs --import Scoped.RenamingSubstitution --import Scoped.Extrication