-- https://plfa.github.io/Inference/ import Plfl.Init import Plfl.More namespace Inference -- https://plfa.github.io/Inference/#syntax open String def Sym : Type := String deriving BEq, DecidableEq, Repr inductive Ty where /-- Native natural type made of 𝟘 and ΞΉ. -/ | nat : Ty /-- Arrow type. -/ | fn : Ty β†’ Ty β†’ Ty /-- Product type. -/ | prod: Ty β†’ Ty β†’ Ty deriving BEq, DecidableEq, Repr namespace Notation open Ty scoped notation "β„•t" => nat scoped infixr:70 " =β‡’ " => fn instance : Mul Ty where mul := .prod end Notation open Notation abbrev Context : Type := List (Sym Γ— Ty) namespace Context abbrev extend (c : Context) (s : Sym) (t : Ty) : Context := ⟨s, t⟩ :: c end Context namespace Notation open Context -- The goal is to make `_β€š_⦂_` work like an `infixl`. -- https://matklad.github.io/2020/04/13/simple-but-powerful-pratt-parsing.html#From-Precedence-to-Binding-Power -- `β€š` is not a comma! See: notation:50 c "β€š " s:51 " ⦂ " t:51 => extend c s t end Notation open Notation /- An attribute is said to be Synthesized, if its parse tree node value is determined by the attribute value at its *child* nodes. An attribute is said to be Inherited, if its parse tree node value is determined by the attribute value at its *parent and/or siblings*. -/ mutual /-- A term with synthesized types. The main term in a constructor is typed via inheritance. -/ inductive TermS where | var : Sym β†’ TermS | ap : TermS β†’ TermI β†’ TermS | prod : TermS β†’ TermS β†’ TermS | syn : TermI β†’ Ty β†’ TermS deriving BEq, Repr -- * `DecidableEq` derivations are not yet supported in `mutual` blocks. -- See: /-- A term with inherited types. The main term in an eliminator is typed via synthesis. -/ inductive TermI where | lam : Sym β†’ TermI β†’ TermI | zero : TermI | succ : TermI β†’ TermI | case : TermS β†’ TermI β†’ Sym β†’ TermI β†’ TermI | mu : Sym β†’ TermI β†’ TermI | fst : TermS β†’ TermI | snd : TermS β†’ TermI | inh : TermS β†’ TermI deriving BEq, Repr end namespace Notation open TermS TermI scoped notation:50 "Ζ› " v " : " d => lam v d scoped notation:50 " ΞΌ " v " : " d => mu v d scoped notation:max "𝟘? " e " [zero: " o " |succ " n " : " i " ] " => case e o n i scoped infixr:min " $ " => ap -- scoped infix:60 " ↓ " => syn -- scoped postfix:60 "↑ " => inh scoped infixl:70 " β–‘ " => ap scoped prefix:80 "ΞΉ " => succ scoped prefix:90 "` " => var scoped notation "𝟘" => zero end Notation -- https://plfa.github.io/Inference/#example-terms abbrev two : TermI := ΞΉ ΞΉ 𝟘 -- * The coercion can only happen in this direction, -- since the other direction requires an extra type annotation. instance : Coe TermS TermI where coe := TermI.inh @[simp] abbrev TermI.the := TermS.syn abbrev add : TermS := (ΞΌ "+" : Ζ› "m" : Ζ› "n" : 𝟘? `"m" [zero: `"n" |succ "m" : ΞΉ (`"+" β–‘ `"m" β–‘ `"n")] ).the (β„•t =β‡’ β„•t =β‡’ β„•t) abbrev mul : TermS := (ΞΌ "*" : Ζ› "m" : Ζ› "n" : 𝟘? `"m" [zero: 𝟘 |succ "m": add β–‘ `"n" $ `"*" β–‘ `"m" β–‘ `"n"] ).the (β„•t =β‡’ β„•t =β‡’ β„•t) -- Note that the typing is only required for `add` due to the rule for `ap`. abbrev four : TermS := add β–‘ two β–‘ two /-- The Church numeral Ty. -/ @[simp] abbrev Ch (t : Ty := β„•t) : Ty := (t =β‡’ t) =β‡’ t =β‡’ t -- Church encoding... abbrev succC : TermI := Ζ› "n" : ΞΉ `"n" abbrev oneC : TermI := Ζ› "s" : Ζ› "z" : `"s" $ `"z" abbrev twoC : TermI := Ζ› "s" : Ζ› "z" : `"s" $ `"s" $ `"z" abbrev addC : TermS := (Ζ› "m" : Ζ› "n" : Ζ› "s" : Ζ› "z" : `"m" β–‘ `"s" $ `"n" β–‘ `"s" β–‘ `"z" ).the (Ch =β‡’ Ch =β‡’ Ch) -- Note that the typing is only required for `addC` due to the rule for `ap`. abbrev four' : TermS := addC β–‘ twoC β–‘ twoC β–‘ succC β–‘ 𝟘 -- https://plfa.github.io/Inference/#bidirectional-type-checking /-- A lookup judgement. `Lookup c s ts` means that `s` is of type `ts` by _looking up_ the context `c`. -/ inductive Lookup : Context β†’ Sym β†’ Ty β†’ Type where | z : Lookup (Ξ“β€š x ⦂ a) x a | s : x β‰  y β†’ Lookup Ξ“ x a β†’ Lookup (Ξ“β€š y ⦂ b) x a deriving DecidableEq namespace Lookup -- https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/d6a227a63c55bf13d49d443f47c54c7a500ea27b/md/main/tactics.md#tactics-by-macro-expansion /-- `elem` validates the type of a variable by looking it up in the current context. This tactic fails when the lookup fails. -/ scoped syntax "elem" : tactic macro_rules | `(tactic| elem) => `(tactic| repeat (first | apply Lookup.s (by trivial) | exact Lookup.z)) -- https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/d6a227a63c55bf13d49d443f47c54c7a500ea27b/md/main/macros.md#simplifying-macro-declaration scoped syntax "get_elem" (ppSpace term) : tactic macro_rules | `(tactic| get_elem $n) => match n.1.toNat with | 0 => `(tactic| exact Lookup.z) | n+1 => `(tactic| apply Lookup.s (by trivial); get_elem $(Lean.quote n)) end Lookup namespace Notation open Context Lookup scoped notation:40 Ξ“ " βˆ‹ " m " ⦂ " a:51 => Lookup Ξ“ m a scoped macro "β™― " n:term:90 : term => `(by get_elem $n) end Notation instance : Repr (Ξ“ βˆ‹ m ⦂ a) where reprPrec i n := "β™―" ++ reprPrec n (sizeOf i) #eval @Lookup.z (βˆ…β€š "x" ⦂ β„•t) "x" β„•t mutual /-- Typing of `TermS` terms. -/ inductive TyS : Context β†’ TermS β†’ Ty β†’ Type where | var : Ξ“ βˆ‹ x ⦂ a β†’ TyS Ξ“ (` x) a | ap: TyS Ξ“ l (a =β‡’ b) β†’ TyI Ξ“ m a β†’ TyS Ξ“ (l β–‘ m) b | prod: TyS Ξ“ m a β†’ TyS Ξ“ n b β†’ TyS Ξ“ (.prod m n) (a * b) | syn : TyI Ξ“ m a β†’ TyS Ξ“ (m.the a) a deriving Repr /-- Typing of `TermI` terms. -/ inductive TyI : Context β†’ TermI β†’ Ty β†’ Type where | lam : TyI (Ξ“β€š x ⦂ a) n b β†’ TyI Ξ“ (Ζ› x : n) (a =β‡’ b) | zero : TyI Ξ“ 𝟘 β„•t | succ : TyI Ξ“ m β„•t β†’ TyI Ξ“ (ΞΉ m) β„•t | case : TyS Ξ“ l β„•t β†’ TyI Ξ“ m a β†’ TyI (Ξ“β€š x ⦂ β„•t) n a β†’ TyI Ξ“ (𝟘? l [zero: m |succ x : n]) a | mu : TyI (Ξ“β€š x ⦂ a) n a β†’ TyI Ξ“ (ΞΌ x : n) a | fst: TyS Ξ“ p (a * b) β†’ TyI Ξ“ (.fst p) a | snd: TyS Ξ“ p (a * b) β†’ TyI Ξ“ (.snd p) b | inh : TyS Ξ“ m a β†’ TyI Ξ“ m a deriving Repr end instance : Coe (TyI Ξ“ m a) (TyS Ξ“ (m.the a) a) where coe := TyS.syn instance : Coe (TyS Ξ“ m a) (TyI Ξ“ m a) where coe := TyI.inh namespace Notation scoped notation:40 Ξ“ " ⊒ " m " ⇑ " a:51 => TyS Ξ“ m a scoped notation:40 Ξ“ " ⊒ " m " β†Ÿ " a:51 => TyS Ξ“ (TermS.syn m a) a scoped notation:40 Ξ“ " ⊒ " m " ⇣ " a:51 => TyI Ξ“ m a end Notation abbrev twoTy : Ξ“ ⊒ two β†Ÿ β„•t := open TyS TyI in by apply_rules [syn, succ, zero] abbrev addTy : Ξ“ ⊒ add ⇑ (β„•t =β‡’ β„•t =β‡’ β„•t) := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh] <;> elem -- https://plfa.github.io/Inference/#bidirectional-mul abbrev mulTy : Ξ“ ⊒ mul ⇑ (β„•t =β‡’ β„•t =β‡’ β„•t) := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, addTy] <;> elem abbrev twoCTy : Ξ“ ⊒ twoC ⇣ Ch := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh] <;> elem abbrev addCTy : Ξ“ ⊒ addC ⇑ (Ch =β‡’ Ch =β‡’ Ch) := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh] <;> elem -- https://plfa.github.io/Inference/#bidirectional-products example : Ξ“ ⊒ .prod (two.the β„•t) add ⇑ β„•t * (β„•t =β‡’ β„•t =β‡’ β„•t) := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, twoTy, addTy] <;> elem example : Ξ“ ⊒ .fst (.prod (two.the β„•t) add) β†Ÿ β„•t := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, twoTy] <;> elem example : Ξ“ ⊒ .snd (.prod (two.the β„•t) add) β†Ÿ (β„•t =β‡’ β„•t =β‡’ β„•t) := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, addTy] <;> elem -- https://plfa.github.io/Inference/#prerequisites /- Nothing to do. Relevant definitions have been derived. -/ -- https://plfa.github.io/Inference/#unique-types theorem Lookup.unique (i : Ξ“ βˆ‹ x ⦂ a) (j : Ξ“ βˆ‹ x ⦂ b) : a = b := by cases i with try trivial | z => cases j <;> trivial | s => cases j with try trivial | s => apply unique <;> trivial theorem TyS.unique (t : Ξ“ ⊒ x ⇑ a) (u : Ξ“ ⊒ x ⇑ b) : a = b := by match t with | .var i => cases u with | var j => apply Lookup.unique <;> trivial | .ap l _ => cases u with | ap l' _ => injection unique l l' | .prod m n => cases u with | prod m' n' => congr; exact unique m m'; exact unique n n' | .syn _ => cases u with | syn _ => trivial -- https://plfa.github.io/Inference/#lookup-type-of-a-variable-in-the-context lemma Lookup.empty_ext_empty : x β‰  y β†’ IsEmpty (Ξ£ a, Ξ“ βˆ‹ x ⦂ a) β†’ IsEmpty (Ξ£ a, Ξ“β€š y ⦂ b βˆ‹ x ⦂ a) := by intro n ai; is_empty; intro ⟨a, i⟩; apply ai.false; exists a cases i <;> trivial def Lookup.lookup (Ξ“ : Context) (x : Sym) : Decidable' (Ξ£ a, Ξ“ βˆ‹ x ⦂ a) := by match Ξ“, x with | [], _ => left; is_empty; nofun | ⟨y, b⟩ :: Ξ“, x => if h : x = y then right; subst h; exact ⟨b, .z⟩ else match lookup Ξ“ x with | .inr ⟨a, i⟩ => right; refine ⟨a, .s ?_ i⟩; trivial | .inl n => left; refine empty_ext_empty ?_ n; trivial -- https://plfa.github.io/Inference/#promoting-negations lemma TyS.empty_arg : Ξ“ ⊒ l ⇑ a =β‡’ b β†’ IsEmpty (Ξ“ ⊒ m ⇣ a) β†’ IsEmpty (Ξ£ b', Ξ“ ⊒ l β–‘ m ⇑ b') := by intro tl n; is_empty; intro ⟨b', .ap tl' tm'⟩ injection tl.unique tl'; rename_i h _; apply n.false; rwa [←h] at tm' lemma TyS.empty_switch : Ξ“ ⊒ m ⇑ a β†’ a β‰  b β†’ IsEmpty (Ξ“ ⊒ m ⇑ b) := by intro ta n; is_empty; intro tb; have := ta.unique tb; contradiction mutual def TermS.infer (m : TermS) (Ξ“ : Context) : Decidable' (Ξ£ a, Ξ“ ⊒ m ⇑ a) := by match m with | ` x => match Lookup.lookup Ξ“ x with | .inr ⟨a, i⟩ => right; exact ⟨a, .var i⟩ | .inl n => left; is_empty; intro ⟨a, .var _⟩; apply n.false; exists a | l β–‘ m => match l.infer Ξ“ with | .inr ⟨a =β‡’ b, tab⟩ => match m.infer Ξ“ a with | .inr ta => right; exact ⟨b, .ap tab ta⟩ | .inl n => left; exact tab.empty_arg n | .inr βŸ¨β„•t, t⟩ => left; is_empty; intro ⟨_, .ap tl _⟩; injection t.unique tl | .inr ⟨.prod _ _, t⟩ => left; is_empty; intro ⟨_, .ap tl _⟩; injection t.unique tl | .inl n => left; is_empty; intro ⟨a, .ap tl _⟩; rename_i b _; exact n.false ⟨b =β‡’ a, tl⟩ | .prod m n => match m.infer Ξ“, n.infer Ξ“ with | .inr ⟨a, tm⟩, .inr ⟨b, tn⟩ => right; exact ⟨a * b, tm.prod tn⟩ | .inr _, .inl nn => left; is_empty; intro ⟨_, tmn⟩; cases tmn; apply nn.false; constructor <;> trivial | .inl nm, _ => left; is_empty; intro ⟨_, .prod tm _⟩; apply nm.false; constructor <;> trivial | .syn m a => match m.infer Ξ“ a with | .inr t => right; exact ⟨a, t⟩ | .inl n => left; is_empty; intro ⟨a', t'⟩; cases t'; apply n.false; trivial def TermI.infer (m : TermI) (Ξ“ : Context) (a : Ty) : Decidable' (Ξ“ ⊒ m ⇣ a) := by match m with | Ζ› x : n => match a with | a =β‡’ b => match n.infer (Ξ“β€š x ⦂ a) b with | .inr t => right; exact .lam t | .inl n => left; is_empty; intro (.lam t); exact n.false t | β„•t => left; is_empty; nofun | .prod _ _ => left; is_empty; nofun | 𝟘 => match a with | β„•t => right; exact .zero | _ =β‡’ _ => left; is_empty; nofun | .prod _ _ => left; is_empty; nofun | ΞΉ n => match a with | β„•t => match n.infer Ξ“ β„•t with | .inr t => right; exact .succ t | .inl n => left; is_empty; intro (.succ t); exact n.false t | _ =β‡’ _ => left; is_empty; nofun | .prod _ _ => left; is_empty; nofun | .case l m x n => match l.infer Ξ“ with | .inr βŸ¨β„•t, tl⟩ => match m.infer Ξ“ a, n.infer (Ξ“β€š x ⦂ β„•t) a with | .inr tm, .inr tn => right; exact .case tl tm tn | .inl nm, _ => left; is_empty; intro (.case _ _ _); apply nm.false; trivial | .inr _, .inl nn => left; is_empty; intro (.case _ _ _); apply nn.false; trivial | .inr ⟨_ =β‡’ _, tl⟩ => left; is_empty; intro (.case t _ _); injection t.unique tl | .inr ⟨.prod _ _, tl⟩ => left; is_empty; intro (.case t _ _); injection t.unique tl | .inl nl => left; is_empty; intro (.case _ _ _); apply nl.false; constructor <;> trivial | ΞΌ x : n => match n.infer (Ξ“β€š x ⦂ a) a with | .inr t => right; exact .mu t | .inl n => left; is_empty; intro (.mu t); exact n.false t | .fst m => match m.infer Ξ“ with | .inr ⟨.prod b _, tm⟩ => if h : a = b then right; subst h; exact .fst tm else left; is_empty; intro (.fst t); injection t.unique tm; contradiction | .inr βŸ¨β„•t, tm⟩ => left; is_empty; intro (.fst t); injection t.unique tm | .inr ⟨_ =β‡’ _, tm⟩ => left; is_empty; intro (.fst t); injection t.unique tm | .inl n => left; is_empty; intro (.fst t); apply n.false; constructor <;> trivial | .snd m => match m.infer Ξ“ with | .inr ⟨.prod _ b, tm⟩ => if h : a = b then right; subst h; exact .snd tm else left; is_empty; intro (.snd t); injection t.unique tm; contradiction | .inr βŸ¨β„•t, tm⟩ => left; is_empty; intro (.snd t); injection t.unique tm | .inr ⟨_ =β‡’ _, tm⟩ => left; is_empty; intro (.snd t); injection t.unique tm | .inl n => left; is_empty; intro (.snd t); apply n.false; constructor <;> trivial | .inh m => match m.infer Ξ“ with | .inr ⟨b, tm⟩ => if h : a = b then right; subst h; exact .inh tm else left; rw [←Ne.def] at h; is_empty; intro (.inh _) apply (tm.empty_switch h.symm).false; trivial | .inl nm => left; is_empty; intro (.inh tm); apply nm.false; exists a end -- https://plfa.github.io/Inference/#testing-the-example-terms abbrev fourTy : Ξ“ ⊒ four ⇑ β„•t := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, addTy, twoTy] <;> elem example : four.infer βˆ… = .inr βŸ¨β„•t, fourTy⟩ := by rfl abbrev four'Ty : Ξ“ ⊒ four' ⇑ β„•t := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, addCTy, twoCTy] <;> elem example : four'.infer βˆ… = .inr βŸ¨β„•t, four'Ty⟩ := by rfl abbrev four'': TermS := mul β–‘ two β–‘ two abbrev four''Ty : Ξ“ ⊒ four'' ⇑ β„•t := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, addCTy, twoCTy] <;> elem example : four''.infer βˆ… = .inr βŸ¨β„•t, four''Ty⟩ := by rfl -- https://plfa.github.io/Inference/#testing-the-error-cases /- Sadly this won't work for now due to limitations with mutual recursions. See: -/ -- example := show ((Ζ› "x" : `"y").the (β„•t =β‡’ β„•t)).infer βˆ… = .inl _ by rfl /- This won't work either, probably due to similar reasons... -/ -- instance : Decidable (Nonempty (Ξ£ a, Ξ“ ⊒ m ⇑ a)) := (m.infer Ξ“).toDecidable -- example := let m := (Ζ› "x" : `"y").the (β„•t =β‡’ β„•t); show IsEmpty (Ξ£ a, βˆ… ⊒ m ⇑ a) by -- rw [←not_nonempty_iff]; decide -- Unbound variable: #eval ((Ζ› "x" : `"y").the (β„•t =β‡’ β„•t)).infer βˆ… -- Argument in application is ill typed: #eval (add β–‘ succC).infer βˆ… -- Function in application is ill typed: #eval (add β–‘ succC β–‘ two).infer βˆ… -- Function in application has type natural: #eval (two.the β„•t β–‘ two).infer βˆ… -- Abstraction inherits type natural: #eval (twoC.the β„•t).infer βˆ… -- Zero inherits a function type: #eval (𝟘.the (β„•t =β‡’ β„•t)).infer βˆ… -- Successor inherits a function type: #eval (two.the (β„•t =β‡’ β„•t)).infer βˆ… -- Successor of an ill-typed term: #eval ((ΞΉ twoC).the β„•t).infer βˆ… -- Case of a term with a function type: #eval ((𝟘? twoC.the Ch [zero: 𝟘 |succ "x" : `"x"]).the β„•t).infer βˆ… -- Case of an ill-typed term: #eval ((𝟘? twoC.the β„•t [zero: 𝟘 |succ "x" : `"x"]).the β„•t).infer βˆ… -- Inherited and synthesized types disagree in a switch: #eval ((Ζ› "x" : `"x").the (β„•t =β‡’ β„•t =β‡’ β„•t)).infer βˆ… -- https://plfa.github.io/Inference/#erasure def Ty.erase : Ty β†’ More.Ty | β„•t => .nat | a =β‡’ b => .fn a.erase b.erase | .prod a b => a.erase * b.erase def Context.erase : Context β†’ More.Context | [] => βˆ… | ⟨_, a⟩ :: Ξ“ => a.erase :: Context.erase Ξ“ def Lookup.erase : Ξ“ βˆ‹ x ⦂ a β†’ More.Lookup Ξ“.erase a.erase | .z => .z | .s _ i => .s i.erase mutual def TyS.erase : Ξ“ ⊒ m ⇑ a β†’ More.Term Ξ“.erase a.erase | .var i => .var i.erase | .ap l m => .ap l.erase m.erase | .prod m n => .prod m.erase n.erase | .syn m => m.erase def TyI.erase : Ξ“ ⊒ m ⇣ a β†’ More.Term Ξ“.erase a.erase | .lam m => .lam m.erase | .zero => .zero | .succ m => .succ m.erase | .case l m n => .case l.erase m.erase n.erase | .mu m => .mu m.erase | .fst m => .fst m.erase | .snd m => .snd m.erase | .inh m => m.erase end example : fourTy.erase (Ξ“ := βˆ…) = More.Term.four := by rfl -- https://plfa.github.io/Inference/#exercise-inference-multiplication-recommended example : mul.infer βˆ… = .inr βŸ¨β„•t =β‡’ β„•t =β‡’ β„•t, mulTy⟩ := by rfl -- ! BOOM! The commented lines below are very CPU/RAM-intensive, and might even make LEAN4 leak memory! -- example : mulTy.erase (Ξ“ := βˆ…) = More.Term.mul := by rfl -- example : four'Ty.erase (Ξ“ := βˆ…) = More.Term.four' := by rfl -- example : four''Ty.erase (Ξ“ := βˆ…) = More.Term.four'' := by rfl