Skip to content

Instantly share code, notes, and snippets.

@dwarn

dwarn/stlc_in_ccc.lean

Created January 30, 2022 13:33
Download ZIP

Revisions

  1. dwarn created this gist Jan 30, 2022.
    102 changes: 102 additions & 0 deletions stlc_in_ccc.lean
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,102 @@
    import category_theory.closed.cartesian

    noncomputable theory

    open category_theory category_theory.limits tactic interactive interactive.types

    lemma tidy_prod_helper {C} [category C] [has_binary_products C] {X Y Z : C}
    (h : Π Γ, (Γ ⟶ X) → (Γ ⟶ Y) → (Γ ⟶ Z)) : X ⨯ Y ⟶ Z :=
    h (X ⨯ Y) limits.prod.fst limits.prod.snd

    lemma coprod_cases_helper {C} [category C] [has_finite_products C] [cartesian_closed C]
    [has_binary_coproducts C] {Γ X Y Z : C} (h1 : Γ ⟶ X ⨿ Y) (h2 : Γ ⨯ X ⟶ Z) (h3 : Γ ⨯ Y ⟶ Z) :
    Γ ⟶ Z :=
    prod.lift (𝟙 Γ) h1 ≫ (prod_coprod_distrib _ _ _).inv ≫ coprod.desc h2 h3

    namespace tactic

    -- from Flypitch
    meta def get_name : expr → name
    | (expr.const c []) := c
    | (expr.local_const _ c _ _) := c
    | _ := name.anonymous

    -- given `f : Δ → Γ` and `h : Γ ⟶ X`, replace `h` with `f ≫ h : Δ ⟶ Γ`
    meta def clear_hom (f Δ Γ h : expr) : tactic unit :=
    try $ do
    `(%%Γ ⟶ %%X) ← infer_type h,
    replace (get_name h) ``(%%f ≫ %%h)

    -- given `f : Δ → Γ`, replace all assumptions `Γ ⟶ X` with `Δ ⟶ Γ`,
    -- clear `f` and `Γ`, and rename `Δ` to `Γ`.
    meta def rebase_context (f : expr) : tactic unit :=
    do
    `(%%Δ ⟶ %%Γ) ← infer_type f,
    ctx ← local_context,
    ctx.for_each (clear_hom f Δ Γ),
    clear f,
    clear Γ,
    rename (get_name Δ) (get_name Γ)

    namespace interactive

    -- changes a goal `Γ ⨯ X ⟶ Y` to `Γ ⟶ Y` and adds an assumption `n : Γ ⟶ X` to context.
    meta def tidy_prod (n : parse $ optional ident_) : tactic unit :=
    do
    `[refine tidy_prod_helper _, intro],
    f ← intro1,
    nm ← n.elim (get_unused_name "H") pure,
    intro nm,
    rebase_context f

    -- changes a goal `Γ ⟶ X ⟹ Y` to `Γ ⟶ Y` and adds an assumption `n : Γ ⟶ X` to context.
    -- this gives the illusion that `(Γ ⟶ X) → (Γ ⟶ Y)` is sufficient to deduce `Γ ⟶ (X ⟹ Y)`.
    meta def c_intro (n : parse $ optional ident_) : tactic unit :=
    `[refine category_theory.cartesian_closed.curry _,
    refine limits.prod.lift limits.prod.snd limits.prod.fst ≫ _] >> tidy_prod n

    -- cases on an assumption `Γ ⟶ X ⨿ Y`.
    -- this gives the illusion that `Γ ⟶ (X ⨿ Y)` eliminates to `(Γ ⟶ X) ⊕ (Γ ⟶ Y)`.
    meta def coprod_cases (nm : parse ident_) : tactic unit :=
    do
    e ← resolve_name nm >>= to_expr,
    `[refine coprod_cases_helper %%e _ _],
    all_goals (tactic.clear e >> tidy_prod nm),
    pure ()

    end interactive
    end tactic

    variables {C : Type*} (Γ X Y Z W : C) [category C] [has_finite_products C] [cartesian_closed C]

    instance : has_coe_to_fun (Γ ⟶ X ⟹ Y) (λ _, (Γ ⟶ X) → (Γ ⟶ Y)) :=
    ⟨λ f g, prod.lift g f ≫ (ev X).app Y⟩

    -- the S combinator in SKI calculus
    example : Γ ⟶ (Z ⟹ Y ⟹ X) ⟹ (Z ⟹ Y) ⟹ Z ⟹ X :=
    begin
    c_intro x,
    c_intro y,
    c_intro z,
    exact x z (y z),
    end

    variable [has_binary_coproducts C]

    example : Γ ⟶ ((X ⨿ (X ⟹ Y)) ⟹ Y) ⟹ Y :=
    begin
    c_intro hn,
    refine hn (_ ≫ coprod.inr),
    c_intro hx,
    exact hn (hx ≫ coprod.inl),
    end

    example : Γ ⟶ (X ⟹ Z) ⟹ (Y ⟹ Z) ⟹ (X ⨿ Y) ⟹ Z :=
    begin
    c_intro xz,
    c_intro yz,
    c_intro h,
    coprod_cases h,
    { exact xz h },
    { exact yz h },
    end