An alternative style of metatheory which can reduce the need for entailments.

stlc.lean

-- Foundational logics tend to be stated in terms of derivations that produce valid sentences,
-- by replicating this with the style of proofs below we can encode a small implicational
-- calculus to get a lighter encoding of contexts.
-- 
-- this demo isn't complete yet, I still need to add all the normal results,
-- and to fully demonstrate the translation into contexts: we want a version of
-- cut elimination for the forall quantifier I've introduced.
-- generally, we can normalize all judgements required in typing derivations into the form `(forall x.)* (P =>)* C`,
-- removing the `forall`s via the IntroForall rule: This produces entailment directly.
--
-- the derivations here need the forall judgements to allow the implication rules to work without
-- constraint: It's true implication, so the forall needs to guard the scoping of additional
-- premises. Pay attention to the abstraction typing rule, it's asserting that a single typing judgement on the parameter
-- is sufficient to produce the typing of the body, which is what allows us to form the lambda typing on a universally
-- quantified parameter.

inductive Expr : Type where
| Var : String -> Expr
| Abs : String -> Expr -> Expr
| App : Expr -> Expr -> Expr
def Expr.DistinctFromAnyVar : Expr := Expr.App (Expr.Var "") (Expr.Var "")

inductive Ty : Type where
| Bool : Ty
| Fn : Ty -> Ty -> Ty

inductive Judgement where
| Typed : Expr -> Ty -> Judgement
| Imp : Judgement -> Judgement -> Judgement
-- This is a slight restriction on the paper proof form: Strictly speaking, we *could*
-- have forall generically quantifying over strings, but the structured AST we're working
-- with for expressions means we need to specifically substitute `Var`s.
-- still, in the metatheory these are still untyped `Expr`s, they're only constrained
-- by adding more assumptions to context.
| ForallVar : String -> Judgement -> Judgement
def Judgement.Irrelevant : Judgement := Judgement.Typed (.Var "") .Bool

infixr:30 "~>" => Judgement.Imp
abbrev with_context (premises : List Judgement) (conclusion : Judgement) : Judgement :=
  match premises with
  | [] => conclusion
  | x :: xs => x ~> with_context xs conclusion
infix:35 "has-type" => Judgement.Typed
infixr:30 "~>*" => with_context
def Expr.subst_var (r : Expr) (x : String) (e : Expr)  : Expr :=
  match r with
  | .Var y => if x = y then e else .Var y
  | .Abs y b => if y = x then (.Abs y b) else (.Abs y $ b.subst_var x e)
  | .App f a => .App (f.subst_var x e) (a.subst_var x e)
def Ty.subst_var (t : Ty) (_ : String) (_ : Expr) : Ty := t
def Judgement.subst_var (j : Judgement) (x : String) (e : Expr) :  Judgement :=
  match j with
  | .Imp p c => .Imp (p.subst_var x e) (c.subst_var x e)
  | .Typed in_e t => .Typed (in_e.subst_var x e) (t.subst_var x e)
  | .ForallVar y j => .ForallVar y $ if x = y then j else j.subst_var x e

def Judgement.not_free_var (j : Judgement) (x : String) : Prop := j.subst_var x (.DistinctFromAnyVar) = j

-- a has-type b = forall c.
--    (forall f e argt. a = (.App f e) ~> f has-type (.Fn argt b) ~> e has-type argt ~> c)
--    ~> (forall x a e b. a = (.Abs x e) ~> (.ForallVar x $ .Var x has-type a ~> e has-type b) ~> c)
--    ~> c
--
-- so the reason this is a rule is that we need to unfold the recursion in `has-type`.
-- by stating the axiom, we're asserting that that recursion is sound.
-- we disallow instances in negative position, because they'd (potentially) allow recursive uses
-- to be constructed...
-- let have_node := TheVariant (\ use_node. ?)
-- have_node (\variant_with_neg_use.  variant_with_neg_use have_node)
--
-- what's the soundness issue? well, this is a bit fix-y, isnt it? We've managed to construct
-- a function that's getting passed itself
--
-- let have_node := TheVariant (\ use_node. continue_loop use_node use_node)
-- have_node (\variant_with_neg_use.  variant_with_neg_use have_node)
--
-- yeah great there's the soundness problem. I think this is only abusable under
-- parametric calls with my `forall`s, but we have those so yey.
--
-- so yep! We assert that the recursive use of this type is sound here.
-- the statement of the inductive type can be somewhat mundanely just the -> and <- conversions
-- between them, as isorec.

inductive Valid : Judgement -> Prop where
| Apply : Valid $ f has-type .Fn a b ~> e has-type a ~> (.App f e) has-type b
| Abs {x a e b} : Valid $ (.ForallVar x $ .Var x has-type a ~> e has-type b) ~> .Abs x e has-type .Fn a b
| Cut : Valid (a ~> b) -> Valid a -> Valid b

-- internal mp would be (a ~> b) ~> a ~> b, and we can derive it.
| Weakening : Valid $ a ~> b ~> a
| Contraction : Valid $ (a ~> b ~> c) ~> (a ~> b) ~> a ~> c

-- `Judgement`s are the language's metatheory, lean is working as a meta-metatheory for use here.
-- this is an axiom of internalizing the parametericity into the metatheory:
-- it can otherwise be proven that `Valid a -> Valid (subst a x b)`
| IntroForall : Valid a -> Valid (.ForallVar x a)
| ForallExchange : Valid $ (.ForallVar x (.ForallVar y a)) ~> (.ForallVar y (.ForallVar x a))
| ForallNarrow : 
  -- substitutions *can* be encoded into the theory if we wish, as long as we
  -- has a sym-not-equal primitive, which is easy enough (can also be internal)
  -- generally there's just little sense in doing with with an embedded formalization
  -- though.
  j.not_free_var x -> (Valid $ (.ForallVar x (j ~> c)) ~> (j ~> .ForallVar x c))

/-
B = S (K S) K
C = S (S (K (S (K S) K)) S) (K K)
-/

theorem contraction2_lift : Valid (a ~> b ~> c) -> Valid (a ~> b) -> Valid (a ~> c) := 
  fun abc ab => Valid.Cut (Valid.Cut Valid.Contraction abc) ab
theorem Valid.weaken : Valid a -> Valid (b ~> a) := fun c => Valid.Cut Valid.Weakening c
theorem imp_trans_rev : Valid $ (b ~> c) ~> (a ~> b) ~> a ~> c := 
  contraction2_lift Valid.Contraction.weaken Valid.Weakening

theorem exchange : Valid $ (a ~> b ~> c) ~> (b ~> a ~> c) :=
  contraction2_lift (contraction2_lift imp_trans_rev.weaken Valid.Contraction) (Valid.Weakening.weaken)
theorem taut : Valid $ a ~> a :=
  -- (A => (B => A) => A) => (A => (B => A)) => A => A
  contraction2_lift (@Valid.Weakening _ (.Irrelevant ~> _)) Valid.Weakening

-- first nontrivial proof :)
theorem identity_fn : Valid $ (.Abs x (.Var x)) has-type (.Fn t t) := by
  apply Valid.Cut Valid.Abs
  apply Valid.IntroForall
  exact taut

theorem internal_mp : Valid $ (a ~> b) ~> a ~> b := taut

theorem imp_trans : Valid (b ~> c) -> Valid (a ~> b) -> Valid (a ~> c) :=
  fun bc ab => (Valid.Cut (Valid.Cut imp_trans_rev bc) ab)
theorem under_premise : Valid (b ~> c) -> Valid ((a ~> b) ~> (a ~> c)) :=
  Valid.Cut imp_trans_rev
theorem subst_many : Valid $ (a ~> b) ~> (cx ~>* a) ~> (cx ~>* b) := 
  by 
    induction cx with
    | nil => 
      unfold with_context
      exact taut
    | cons x xs ih => 
      unfold with_context
      exact imp_trans imp_trans_rev ih
theorem exchange_under : Valid $ (a ~> b ~> c ~> d) ~> (a ~> c ~> b ~> d) := 
  Valid.Cut imp_trans_rev exchange
theorem exchange_under_cx : Valid $ (cx ~>* b ~> c ~> d) ~> (cx ~>* c ~> b ~> d) := 
  Valid.Cut subst_many exchange

theorem contraction : Valid $ (a ~> a ~> b) ~> a ~> b := (Valid.Cut (Valid.Cut exchange Valid.Contraction) taut)
theorem all_premises1 : Valid (a ~> b)
  -> Valid ((ps ~>* a) ~> ps ~>* b) :=
  by
    intro ab
    induction ps
    simp [with_context]
    exact ab
    case cons head tail ih =>
      simp [with_context]
      exact under_premise ih
theorem all_premises : Valid (a ~> b ~> c)
  -> Valid ((ps ~>* a) ~> (ps ~>* b) ~> ps ~>* c) :=
  by
    intro abc
    induction ps
    simp [with_context]
    exact abc
    case cons head tail ih =>
      simp [with_context]
      exact (
        let extend_e := imp_trans imp_trans_rev ih
        let extend_f := under_premise extend_e
        let ordered_correctly := imp_trans exchange extend_f
        imp_trans (under_premise contraction) ordered_correctly
      )

theorem Judgement.apply : Valid $
  (cx ~>* f has-type .Fn a b) ~> (cx ~>* e has-type a) ~> cx ~>* (.App f e) has-type b
  := all_premises Valid.Apply
theorem Judgement.abs : Valid $
  (cx ~>* (.ForallVar x $ .Var x has-type a ~> e has-type b)) ~> cx ~>* .Abs x e has-type .Fn a b
  := all_premises1 Valid.Abs
theorem Judgement.var_intro : Valid $ .Var x has-type a ~> .Var x has-type a := taut

theorem alpha_equiv : Valid j -> Valid (j.subst_var x e) := by
  -- might need to weaken this to only var substitution, let's see.
  intro proof
  induction proof
  
  · unfold Judgement.subst_var
    unfold Judgement.subst_var
    unfold Judgement.subst_var
    unfold Ty.subst_var
    rw [Expr.subst_var]
    next f _ _ e =>
    generalize f.subst_var x _ = f'
    generalize e.subst_var x _ = e'
    apply Valid.Apply
  · unfold Judgement.subst_var
    unfold Judgement.subst_var
    unfold Ty.subst_var
    unfold Expr.subst_var
    split
    · next h =>
      simp [h]
      apply Valid.Abs
    · next h=> 
      split 
      · next h2 => symm at h2; contradiction
      unfold Judgement.subst_var
      unfold Judgement.subst_var
      unfold Ty.subst_var
      next body _ _ =>
      generalize body.subst_var x e = body'
      unfold Expr.subst_var
      simp [h]
      apply Valid.Abs
  case Cut iF _ =>
    unfold Judgement.subst_var at iF
    apply Valid.Cut
    assumption
    assumption
  · unfold Judgement.subst_var
    rw (occs := [1]) [Judgement.subst_var]
    apply Valid.Weakening
  case Contraction a b c =>
    unfold Judgement.subst_var
    unfold Judgement.subst_var
    generalize hA : a.subst_var x e = a'
    unfold Judgement.subst_var
    generalize b.subst_var x e = b'
    generalize c.subst_var x e = c'
    rw [hA]
    apply Valid.Contraction
  case IntroForall aVal ih =>

    unfold Judgement.subst_var
    split
    · apply Valid.IntroForall
      assumption
    apply Valid.IntroForall
    assumption
  · sorry
  · sorry