Logic.lean

import Mathlib.tactic

abbrev Var := Nat

structure Lang where
  Const : Type
  Func : Nat → Type
  Rel : Nat → Type

/------
Logic
------/

inductive term (L : Lang): Type
  | const : L.Const → term L
  | var : Var → term L
  | func {arity : ℕ} : L.Func arity  →  (Fin arity → term L) → term L

inductive form (L : Lang): Type
  | rel {arity} : L.Rel arity → (Fin arity → term L) → form L
  | bot : form L
  | imp : form L → form L → form L
  | all : form L → form L

def form.not {L : Lang} (p : form L) : form L := p.imp form.bot
def form.top {L : Lang} : form L := form.bot.not
def form.or {L : Lang} (p q : form L) : form L := (p.not).imp q
def form.and {L : Lang} (p q : form L) : form L := (p.imp q.not).not
def form.ex {L : Lang} (p : form L) : form L := (form.all (p.not )).not

/------
subst
------/

def I : Var → Var := λ x => x
def S : Var → Var := λ x => x + 1
def extension {T : Type} : T → (Var → T) → Var → T := λ t σ x => if x = 0 then t else σ (x - 1)
def ids {L : Lang} : Var → term L := term.var

notation f ">>>" g => λ x => g (f x)
notation:80 s ".:" σ => extension s σ

def rename' (ξ : Var → Var) (s : term L) : term L :=
  match s with
  | term.const c => term.const c
  | term.var x => term.var (ξ x)
  | term.func f ts => term.func f (λ i => rename' ξ (ts i))

def inst' (σ : Var → term L) (s : term L) : term L :=
  match s with
  | term.const c => term.const c
  | term.var x => σ x
  | term.func f ts => term.func f (λ i => inst' σ (ts i))

def rename {L : Lang} (ξ : Var → Var) (s : form L) : form L :=
  match s with
  | form.rel R ts => form.rel R (λ i => rename' ξ (ts i))
  | form.bot => form.bot
  | form.imp p q => form.imp (rename ξ p) (rename ξ q)
  | form.all p => form.all  (rename (0 .: (ξ >>> S)) p)

def up {L : Lang} (σ : Var → term L) := (ids 0 .:( σ >>> rename' S))

def inst {L : Lang} (σ : Var → term L) (s : form L) : form L :=
  match s with
  | form.rel R ts => form.rel R (λ i => inst' σ (ts i))
  | form.bot => form.bot
  | form.imp p q => form.imp (inst σ p) (inst σ q)
  | form.all p => form.all (inst (up σ) p)

def subst {L : Lang} (p : form L) (x : Var) (s : term L) : form L :=
  inst (λ y => if y = x then s else term.var y) p


def compose {L : Lang} (σ τ : Var → term L) : Var → term L := σ >>> inst' τ
infixr:90 " >> " => compose

notation s ".[" σ "]" => inst σ s
def ren {L : Lang} (ξ : Var → Var) : Var → term L := ξ >>> ids


/-
  subst lemma
-/

section subst_lemma

variable {L : Lang}

lemma rename'_inst'_ren (ξ : Var → Var) (t : term L) :
  rename' ξ t = inst' (ren ξ) t
:= by
  induction t generalizing ξ with
  | const c => simp [rename', inst']
  | var x => simp [rename', inst', ren, ids]
  | func f l IH =>
    simp [rename', inst']; ext i
    rw [IH]

lemma rename_inst_ren (ξ : Var → Var) (s : form L) :
  rename ξ s = inst (ren ξ) s
:= by
  induction s generalizing ξ with
  | rel R l =>
    simp [rename, inst]; ext i
    rw [rename'_inst'_ren]
  | bot => simp [rename, inst]
  | imp p q IHp IHq =>
    simp [rename, inst]; rw [IHp, IHq]; simp
  | all p IH =>
    simp [rename, inst]
    rw [IH]
    congr; ext i
    simp [ren, up, ids, rename', extension]
    split_ifs; simp; simp

variable (σ τ ρ : Var → term L) (p q : form L) (s t : term L)


lemma impr_inst :
  (p.imp q).[σ] = (p.[σ]).imp (q.[σ])
:= by
  simp [inst]

lemma all_inst :
  (form.all p).[σ] = form.all (p.[ids 0 .: (σ >> ren S)])
:= by
  simp [inst]
  congr
  simp [up]
  ext i; simp [extension]
  rcases i with _ | i
  · simp
  · simp [compose]
    rw [rename'_inst'_ren]





lemma all_inst' :
  (form.all p).[σ] = form.all (p.[up σ])
:= by
  simp [inst]

@[simp]
lemma zero_inst_extension :
  inst' (s .: σ) (ids 0) = s
:= by
  simp [inst', extension]

@[simp]
lemma S_extension_cancel :
  (ren S >> (s .: σ)) = σ
:= by
  ext i; simp [extension, compose, inst', S]

@[simp]
lemma rename'_I :
  rename' I s = s
:= by
  induction s with
  | const => simp [rename']
  | var x => simp [rename', I]
  | func f l IH =>
    simp [rename']; ext i
    rw [IH]

@[simp]
lemma rename_I :
  rename I p = p
:= by
  induction p with
  | rel R l =>
    simp [rename]
  | bot => simp [rename]
  | imp p q IHp IHq => simp [rename, IHp, IHq]
  | all a IH =>
    simp [rename, I]
    unfold extension
    have : (fun x => if x = 0 then 0 else (fun x => S x) (x - 1)) = I := by {
      ext i; simp [I]
      rcases i; simp; simp [S]
    }
    rw [this, IH]

@[simp]
lemma extension_compose :
  ((inst' σ (ids 0)) .: (ren S >> σ)) = σ
:= by
  ext i; simp [inst', extension]
  rcases i with _ | i'
  · simp
  · simp [S, compose, inst']

@[simp]
lemma I_compose :
  (ren I >> σ) = σ
:= by
  ext i; simp [compose, inst', I]

@[simp]
lemma compose_I :
  (σ >> ren I) = σ
:= by
  ext i; simp [compose]
  rw [<- rename'_inst'_ren]
  rw [rename'_I]

-- @[simp]
lemma compose_assoc :
  (σ >> ρ) >> τ = σ >> (ρ >> τ)
:= by
  ext i; simp [compose]
  set t := σ i
  induction t  with
  | const c => simp [inst']
  | var x =>
    simp [inst', compose]
  | func f l IH =>
    simp [inst']; ext j
    rw [IH]


-- @[simp]
lemma extension_copose_distriv :
  (s .: σ) >> τ = (inst' τ s) .: (σ >> τ)
:= by
  ext i; simp [compose, extension]
  rcases i with _ | i
  · simp
  · simp

@[simp]
lemma inst'_compose :
  inst' (σ >> τ) s = inst' τ (inst' σ s)
:= by
  induction s with
  | const c => simp [inst']
  | var x => simp [inst', compose]
  | func f l IH =>
    simp [inst']; ext i
    rw [IH]

-- @[simp]
lemma up_compose_distrib :
  up (σ >> τ) = (up σ) >> (up τ)
:= by
  ext i
  conv => arg 2; simp [compose]
  conv => arg 1; simp [up, ids, extension]
  rcases i with _ | i
  · simp
    conv => arg 2; arg 2; simp [up, extension, ids]
    simp [inst', up, extension, ids]
  · simp
    conv => arg 2; arg 2; simp [up, extension]
    conv => arg 1; arg 2; simp [compose]
    set t := σ i
    induction t with
    | const c => simp [inst', rename']
    | var x => simp [inst', up, extension, S]
    | func f l IH =>
      simp [inst', rename']; ext j
      rw [IH]

@[simp]
lemma inst_compose :
  p.[σ >> τ] = p.[σ].[τ]
:= by
  induction p generalizing σ τ with
  | rel R l =>
    simp [inst]
  | bot => simp [inst]
  | imp p q IHp IHq =>
    simp [inst]; rw [IHp, IHq]; simp
  | all p IH =>
    simp [inst]
    rw [<- IH]
    congr
    rw [up_compose_distrib]

@[simp]
lemma zero_extension :
  ((ids 0) .: ren S) = (ids : Var → term L)
:= by
  ext i; simp [ids, extension]
  rcases i with _ | i<;> simp
  simp [ren, ids, S]


end subst_lemma




/------
semantics
------/

structure Structure (L : Lang) where
  domain : Type
  interprConst : L.Const → domain
  nameOf : domain → L.Const
  isInverse : ∀ d : domain, interprConst (nameOf d) = d
  interpFunc {arity} : L.Func arity → (Fin arity → domain) → domain
  interpRel {arity} : L.Rel arity → (Fin arity → domain) → Prop


@[simp]
def evalt {L : Lang} {M : Structure L} (context : Var → M.domain): term L →  M.domain
  | .const c => M.interprConst c
  | .var x => context x
  | .func f ts => M.interpFunc f (fun i => evalt context (ts i))

@[simp]
def form.size {L : Lang} : form L → Nat
  | form.rel _ _ => 0
  | form.bot => 0
  | form.imp p q => 1 + max p.size q.size
  | form.all p => 1 + p.size



lemma form_size_inst {L : Lang} (p : form L) (σ : Var → term L) :
  (inst σ p).size = p.size
:= by
  induction p generalizing σ with
  | rel R l => simp
  | bot => simp
  | imp p q IHp IHq => simp [form.size]; rw [IHp, IHq]
  | all p IH => simp; rw [IH]


lemma form_size_subst {L : Lang} (p : form L) (x : Var) (s : term L) :
  (subst p x s).size = p.size
:= by
  simp [subst]
  rw [form_size_inst]


@[simp]
def evalf {L : Lang} {M : Structure L} (context : Var → M.domain) : form L → Prop
  | form.bot => False
  | form.rel R ts => M.interpRel R (fun i => evalt context (ts i))
  | form.imp p q => evalf context p → evalf context q
  | form.all p => ∀ c : M.domain, evalf context (subst p 0 (term.const (M.nameOf c)))
termination_by f => f.size
decreasing_by
  all_goals conv => arg 2; try simp
  · calc
      p.size ≤ max p.size q.size := by apply Nat.le_max_left
      max p.size q.size < 1 + max p.size q.size := by simp
  · calc
      q.size ≤ max p.size q.size := by apply Nat.le_max_right
      max p.size q.size < 1 + max p.size q.size := by simp
  · rw [form_size_subst]; simp