stlc_in_ccc.lean

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