-- https://plfa.github.io/Properties/ import Plfl.Init import Plfl.Lambda open Lambda namespace Properties open Context Context.IsTy Term.Reduce open Sum -- https://plfa.github.io/Properties/#values-do-not-reduce def Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by introv v; is_empty; intro r cases v <;> try contradiction · case succ v => cases r; · case succξ => apply (empty_reduce v).false; trivial def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by intro r; is_empty; intro v have : ∀ {n}, IsEmpty (m —→ n) := Value.empty_reduce v exact this.false r -- https://plfa.github.io/Properties/#exercise-canonical--practice inductive Canonical : Term → Ty → Type where | canLam : ∅‚ x ⦂ t ⊢ n ⦂ u → Canonical (ƛ x : n) (t =⇒ u) | canZero : Canonical 𝟘 ℕt | canSucc : Canonical n ℕt → Canonical (ι n) ℕt namespace Canonical def ofIsTy : ∅ ⊢ m ⦂ t → Value m → Canonical m t | tyLam l, Value.lam => canLam l | tyZero, V𝟘 => canZero | tySucc t, Value.succ m => canSucc <| ofIsTy t m def wellTyped : Canonical v t → ∅ ⊢ v ⦂ t × Value v := by intro | canLam h => exact ⟨tyLam h, Value.lam⟩ | canZero => exact ⟨tyZero, V𝟘⟩ | canSucc h => have ⟨ty, v⟩ := wellTyped h; exact ⟨tySucc ty, Value.succ v⟩ def wellTypedInv : ∅ ⊢ v ⦂ t × Value v → Canonical v t := by intro | ⟨tyLam ty, Value.lam⟩ => exact canLam ty | ⟨tyZero, Value.zero⟩ => exact canZero | ⟨tySucc ty, Value.succ v⟩ => apply canSucc; exact wellTypedInv ⟨ty, v⟩ lemma wellTyped_left_inv (c : Canonical v t) : wellTypedInv (wellTyped c) = c := by cases c with simp_all only [wellTypedInv, Prod.mk.eta, canSucc.injEq] | canSucc c' => rename_i v'; exact @wellTyped_left_inv v' ℕt c' lemma wellTyped_right_inv (c : ∅ ⊢ v ⦂ t × Value v) : wellTyped (wellTypedInv c) = c := by match c with | ⟨tyLam ty, Value.lam⟩ => simp_all only [wellTyped] | ⟨tyZero, Value.zero⟩ => simp_all only [wellTyped] | ⟨tySucc ty, Value.succ n⟩ => rename_i v'; have := @wellTyped_right_inv v' ℕt ⟨ty, n⟩; rw [wellTypedInv, wellTyped]; split · simp_all only [Prod.mk.injEq] /-- The Canonical forms are exactly the well-typed values. -/ instance : Canonical v t ≃ (∅ ⊢ v ⦂ t) × Value v where toFun := wellTyped invFun := wellTypedInv left_inv := wellTyped_left_inv right_inv := wellTyped_right_inv end Canonical def canonical : ∅ ⊢ m ⦂ t → Value m → Canonical m t := Canonical.ofIsTy -- https://plfa.github.io/Properties/#progress /-- If a term `m` is not ill-typed, then it either is a value or can be reduced. -/ inductive Progress (m : Term) where | step : (m —→ n) → Progress m | done : Value m → Progress m --^ In general, the rule of thumb is to consider the easy case (`step`) before the hard case (`done`) for easier proofs. namespace Progress def ofIsTy : ∅ ⊢ m ⦂ t → Progress m := by intro | tyVar _ => contradiction | tyLam _ => exact done Value.lam | tyAp jl jm => cases ofIsTy jl with | step => apply step; · apply apξ₁; trivial | done vl => cases ofIsTy jm with | step => apply step; apply apξ₂ <;> trivial | done => cases vl with | lam => apply step; apply lamβ; trivial | _ => contradiction | tyZero => exact done V𝟘 | tySucc j => cases ofIsTy j with | step => apply step; apply succξ; trivial | done => apply done; apply Value.succ; trivial | tyCase jl jm jn => cases ofIsTy jl with | step => apply step; apply caseξ; trivial | done vl => cases vl with | lam => trivial | zero => exact step zeroβ | succ => apply step; apply succβ; trivial | tyMu _ => exact step muβ end Progress def progress : ∅ ⊢ m ⦂ t → Progress m := Progress.ofIsTy -- https://plfa.github.io/Properties/#exercise-value-practice def IsTy.isValue : ∅ ⊢ m ⦂ t → Decidable (Nonempty (Value m)) := by intro j; cases progress j · rename_i n r; have := Reduce.empty_value r apply isFalse; simp_all only [not_nonempty_iff] · exact isTrue ⟨by trivial⟩ def Progress' (m : Term) : Type := Value m ⊕ Σ n, m —→ n namespace Progress' -- https://plfa.github.io/Properties/#exercise-progress-practice def ofIsTy : ∅ ⊢ m ⦂ t → Progress' m := by intro | tyVar _ => contradiction | tyLam _ => exact inl Value.lam | tyAp jl jm => match ofIsTy jl with | inr ⟨n, r⟩ => exact inr ⟨_, apξ₁ r⟩ | inl vl => match ofIsTy jm with | inr ⟨n, r⟩ => apply inr; exact ⟨_, apξ₂ vl r⟩ | inl _ => cases canonical jl vl with | canLam => apply inr; refine ⟨_, lamβ ?_⟩; trivial | tyZero => exact inl V𝟘 | tySucc j => match ofIsTy j with | inl v => apply inl; exact Value.succ v | inr ⟨n, r⟩ => exact inr ⟨_, succξ r⟩ | tyCase jl jm jn => match ofIsTy jl with | inr ⟨n, r⟩ => exact inr ⟨_, caseξ r⟩ | inl vl => cases vl with | lam => trivial | zero => exact inr ⟨_, zeroβ⟩ | succ v => exact inr ⟨_, succβ v⟩ | tyMu _ => exact inr ⟨_, muβ⟩ end Progress' namespace Progress -- https://plfa.github.io/Properties/#exercise-progress--practice @[simp] def toProgress' : Progress m → Progress' m | step r => inr ⟨_, r⟩ | done v => inl v @[simp] def fromProgress' : Progress' m → Progress m | inl v => done v | inr ⟨_, r⟩ => step r instance : Progress m ≃ Progress' m where toFun := toProgress' invFun := fromProgress' left_inv := by intro x; cases x <;> simp_all only [fromProgress', Progress', toProgress'] right_inv := by intro x; cases x <;> simp_all only [Progress', toProgress', fromProgress'] end Progress -- https://plfa.github.io/Properties/#renaming namespace Renaming open Lookup /-- If one context maps to another, the mapping holds after adding the same variable to both contexts. -/ def ext : (∀ {x tx}, Γ ∋ x ⦂ tx → Δ ∋ x ⦂ tx) → (∀ {x y tx ty}, Γ‚ y ⦂ ty ∋ x ⦂ tx → Δ‚ y ⦂ ty ∋ x ⦂ tx) := by introv ρ; intro | z => exact z | s nxy lx => exact s nxy <| ρ lx def rename : (∀ {x t}, Γ ∋ x ⦂ t → Δ ∋ x ⦂ t) → (∀ {m t}, Γ ⊢ m ⦂ t → Δ ⊢ m ⦂ t) := by introv ρ; intro | tyVar j => apply tyVar; exact ρ j | tyLam j => apply tyLam; exact rename (ext ρ) j | tyAp jl jm => apply tyAp · exact rename ρ jl · exact rename ρ jm | tyZero => apply tyZero | tySucc j => apply tySucc; exact rename ρ j | tyCase jl jm jn => apply tyCase · exact rename ρ jl · exact rename ρ jm · exact rename (ext ρ) jn | tyMu j => apply tyMu; exact rename (ext ρ) j def Lookup.weaken : ∅ ∋ m ⦂ t → Γ ∋ m ⦂ t := by intro. def weaken : ∅ ⊢ m ⦂ t → Γ ⊢ m ⦂ t := by intro j; refine rename ?_ j; exact Lookup.weaken def drop : Γ‚ x ⦂ t'‚ x ⦂ t ⊢ y ⦂ u → Γ‚ x ⦂ t ⊢ y ⦂ u := by intro j; refine rename ?_ j intro y u j; cases j · exact z · case s j => cases j · contradiction · case s j => refine s ?_ j; trivial def Lookup.swap : (x ≠ x') → (Γ‚ x' ⦂ t'‚ x ⦂ t ∋ y ⦂ u) → (Γ‚ x ⦂ t‚ x' ⦂ t' ∋ y ⦂ u) := by intro n j; cases j · exact s n z · case s j => cases j · exact z · apply s · trivial · apply s <;> trivial def swap : x ≠ x' → Γ‚ x' ⦂ t'‚ x ⦂ t ⊢ y ⦂ u → Γ‚ x ⦂ t‚ x' ⦂ t' ⊢ y ⦂ u := by intro n j; refine rename ?_ j; introv; exact Lookup.swap n end Renaming -- https://plfa.github.io/Properties/#substitution def subst : ∅ ⊢ y ⦂ t → Γ‚ x ⦂ t ⊢ n ⦂ u → Γ ⊢ n[x := y] ⦂ u := open Renaming in by intro j; intro | tyVar k => rename_i y; by_cases y = x <;> simp_all only [Term.subst, ite_true] · have := weaken (Γ := Γ) j; cases k <;> try trivial · cases k <;> simp_all only [not_true]; · repeat trivial | tyLam k => rename_i y _ _ _; by_cases h : y = x <;> ( simp_all only [Term.subst, ite_true]; apply tyLam ) · subst h; apply drop; trivial · apply subst j; exact swap (by trivial) k | tyAp k l => apply tyAp <;> (apply subst j; trivial) | tyZero => exact tyZero | tySucc _ => apply tySucc; apply subst j; trivial | tyCase k l m => rename_i y _; by_cases h : y = x <;> simp_all only [Term.subst, ite_true] · apply tyCase · apply subst j; exact k · apply subst j; exact l · subst h; exact drop m · apply tyCase <;> (apply subst j; try trivial) · exact swap (by trivial) m | tyMu k => rename_i y _; by_cases h : y = x <;> simp_all only [Term.subst, ite_true] · subst h; apply tyMu; exact drop k · apply tyMu; apply subst j; exact swap (by trivial) k -- https://plfa.github.io/Properties/#preservation def preserve : ∅ ⊢ m ⦂ t → (m —→ n) → ∅ ⊢ n ⦂ t := by intro | tyAp jl jm, lamβ _ => apply subst jm; cases jl; · trivial | tyAp jl jm, apξ₁ _ => apply tyAp <;> try trivial · apply preserve jl; trivial | tyAp jl jm, apξ₂ _ _ => apply tyAp <;> try trivial · apply preserve jm; trivial | tySucc j, succξ r => apply tySucc; exact preserve j r | tyCase k l m, zeroβ => trivial | tyCase k l m, succβ _ => refine subst ?_ m; cases k; · trivial | tyCase k l m, caseξ _ => apply tyCase <;> try trivial · apply preserve k; trivial | tyMu j, muβ => refine subst ?_ j; apply tyMu; trivial -- https://plfa.github.io/Properties/#evaluation inductive Result n where | done (val : Value n) | dnf deriving BEq, DecidableEq, Repr inductive Steps (l : Term) where | steps : ∀{n : Term}, (l —↠ n) → Result n → Steps l deriving Repr open Result Steps def eval (gas : ℕ) (j : ∅ ⊢ l ⦂ t) : Steps l := open Clos in if gas = 0 then ⟨nil, dnf⟩ else match progress j with | Progress.done v => steps nil <| done v | Progress.step r => let ⟨rs, res⟩ := eval (gas - 1) (preserve j r) ⟨cons r rs, res⟩ section examples open Term -- def x : ℕ := x + 1 abbrev succμ := μ "x" : ι `"x" abbrev tySuccμ : ∅ ⊢ succμ ⦂ ℕt := by apply tyMu; apply tySucc; trivial #eval eval 3 tySuccμ |>.3 abbrev add_2_2 := add □ 2 □ 2 abbrev two_ty : ∅ ⊢ 2 ⦂ ℕt := by iterate 2 (apply tySucc) · exact tyZero abbrev tyAdd_2_2 : ∅ ⊢ add_2_2 ⦂ ℕt := by apply tyAp · apply tyAp · exact addTy · iterate 2 (apply tySucc) · exact tyZero · iterate 2 (apply tySucc) · exact tyZero #eval eval 100 tyAdd_2_2 |>.3 end examples section subject_expansion open Term -- https://plfa.github.io/Properties/#exercise-subject_expansion-practice example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by by_contra; simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] let illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add] have nty_ill : ∅ ⊬ illCase := by by_contra; simp_all only [not_isEmpty_iff]; rename_i t j cases t <;> (simp only [illCase] at j; cases j; · contradiction) rename_i f; have := f 𝟘 ℕt illCase tyZero zeroβ exact nty_ill.false this.some example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by by_contra; simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] let illAp := (ƛ "x" : 𝟘) □ illLam have nty_ill : ∅ ⊬ illAp := by by_contra; simp_all only [not_isEmpty_iff]; rename_i t j cases t <;> ( · cases j · rename_i j; simp only [illAp] at j; cases j · apply nty_illLam.false <;> trivial ) rename_i f; have := f 𝟘 ℕt illAp tyZero (lamβ Value.lam) exact nty_ill.false this.some end subject_expansion -- https://plfa.github.io/Properties/#well-typed-terms-dont-get-stuck abbrev Normal m := ∀ {n}, IsEmpty (m —→ n) abbrev Stuck m := Normal m ∧ IsEmpty (Value m) example : Stuck (` "x") := by unfold Stuck Normal; constructor · intro n; is_empty; nofun · is_empty; nofun -- https://plfa.github.io/Properties/#exercise-unstuck-recommended /-- No well-typed term can be stuck. -/ def unstuck : ∅ ⊢ m ⦂ t → IsEmpty (Stuck m) := by intro j; is_empty; simp_all only [and_imp] intro n ns; cases progress j · case step s => exact n.false s · case done v => exact ns.false v /-- After any number of steps, a well-typed term remains well typed. -/ def preserves : ∅ ⊢ m ⦂ t → (m —↠ n) → ∅ ⊢ n ⦂ t := by intro j; intro | Clos.nil => trivial | Clos.cons car cdr => refine preserves ?_ cdr; exact preserve j car /-- _Well-typed terms don't get stuck_ (WTTDGS): starting from a well-typed term, taking any number of reduction steps leads to a term that is not stuck. -/ def preserves_unstuck : ∅ ⊢ m ⦂ t → (m —↠ n) → IsEmpty (Stuck n) := by intro j r; have := preserves j r; exact unstuck this -- https://plfa.github.io/Properties/#reduction-is-deterministic def Reduce.det : (m —→ n) → (m —→ n') → n = n' := by intro r r'; cases r · case lamβ => cases r' <;> try trivial · case apξ₂ => exfalso; rename_i v _ _ r; exact (Value.empty_reduce v).false r · case apξ₁ => cases r' <;> try trivial · case apξ₁ => simp only [Term.ap.injEq, and_true]; apply det <;> trivial · case apξ₂ => exfalso; rename_i r _ v _; exact (Value.empty_reduce v).false r · case apξ₂ => cases r' <;> try trivial · case lamβ => exfalso; rename_i r _ _ _ v; exact (Value.empty_reduce v).false r · case apξ₁ => exfalso; rename_i v _ _ r; exact (Value.empty_reduce v).false r · case apξ₂ => simp only [Term.ap.injEq, true_and]; apply det <;> trivial · case zeroβ => cases r' <;> try trivial · case succβ => cases r' <;> try trivial · case caseξ => exfalso; rename_i v _ r; exact (Value.empty_reduce (Value.succ v)).false r · case succξ => cases r'; · case succξ => simp only [Term.succ.injEq]; apply det <;> trivial · case caseξ => cases r' <;> try trivial · case succβ => exfalso; rename_i v r; exact (Value.empty_reduce (Value.succ v)).false r · case caseξ => simp only [Term.case.injEq, and_self, and_true]; apply det <;> trivial · case muβ => cases r'; try trivial -- https://plfa.github.io/Properties/#quiz /- Suppose we add a new term zap with the following reduction rule -------- β-zap M —→ zap and the following typing rule: ----------- ⊢zap Γ ⊢ zap ⦂ A Which of the following properties remain true in the presence of these rules? For each property, write either "remains true" or "becomes false." If a property becomes false, give a counterexample: * Determinism Becomes false. The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via: · apξ₁, to zap □ 𝟘 · zepβ, to zap ... and they're not equal. * Progress/Preservation Remains true. -/ -- https://plfa.github.io/Properties/#quiz-1 /- Suppose instead that we add a new term foo with the following reduction rules: ------------------ β-foo₁ (λ x ⇒ ` x) —→ foo ----------- β-foo₂ foo —→ zero Which of the following properties remain true in the presence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample: * Determinism Becomes false. The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via: · apξ₁, to foo □ 𝟘 · lamβ, to `"x" ... and they're not equal. * Progress Becomes false. The term `(ƛ x ⇒ `"x") □ 𝟘` can be reduced via: · apξ₁ fooβ₁, to foo □ 𝟘 · then apξ₁ fooβ₂, to 𝟘 □ 𝟘 ... and now the term get's stuck. * Preservation Becomes false. The term `(ƛ x ⇒ `"x") ⦂ ℕt =⇒ ℕt` can be reduced via: · fooβ₁, to foo · then fooβ₂, 𝟘 ⦂ ℕt ... and (ℕt =⇒ ℕt) ≠ ℕt -/ -- https://plfa.github.io/Properties/#quiz-2 /- Suppose instead that we remove the rule ξ·₁ from the step relation. Which of the following properties remain true in the absence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample: * Determinism/Preservation Remains true. * Progress Becomes false. The term `(ƛ x ⇒ `"x") □ 𝟘` is well-typed but gets stucked. -/ -- https://plfa.github.io/Properties/#quiz-3 /- We can enumerate all the computable function from naturals to naturals, by writing out all programs of type `ℕ ⇒ `ℕ in lexical order. Write fᵢ for the i’th function in this list. NB: A ℕ → ℕ function can be seen as a stream of ℕ's, where the i'th ℕ stands for f(i). Say we add a typing rule that applies the above enumeration to interpret a natural as a function from naturals to naturals: Γ ⊢ L ⦂ `ℕ Γ ⊢ M ⦂ `ℕ -------------- _·ℕ_ Γ ⊢ L · M ⦂ `ℕ And that we add the corresponding reduction rule: fᵢ(m) —→ n ---------- δ i · m —→ n Which of the following properties remain true in the presence of these rules? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample: * Determinism/Preservation Remains true. The only change is that the terms that were once stuck now might continue to progress. * Progress Becomes false. Since a computable function can be partial, the reduction might not halt. Are all properties preserved in this case? Are there any other alterations we would wish to make to the system? -/