import KleeneTheory
/-!
# Sanity checks (non-vacuity of the formalised definitions)
Standard projection facts, derived through Theorem 1 / `transpI_iff_lcCond`:
* `pp'` presupposes `p`;   * `(p and pp')` presupposes nothing;   * `(pp' and p)` presupposes `p`.
World type `Bool`; proposition `p` (name 0) is true exactly at `true`.
-/
namespace LCProp
def Isan : Nat → Bool → Bool
  | 0, w => w
  | _, _ => true

def Call : Bool → Prop := fun _ => True
def Cp : Bool → Prop := fun w => w = true

theorem sanity_trig_all : ¬ TranspI Isan Call (.trig 0 1 0) := by
  intro h
  have := h ([], 0, 1, 0) (by simp [occs]) [] F2.nil Form.tt false trivial
  simp [plug, ev, ev_tt, Isan, Bop.eval] at this

theorem sanity_trig_p : TranspI Isan Cp (.trig 0 1 0) := by
  rw [transpI_iff_lcCond]
  intro t ht w hw
  simp [occs] at ht; subst ht
  simpa [lcK, Cp, Isan] using hw

theorem sanity_and_left_no_presup : TranspI Isan Call (.bin .and (.atom 0) (.trig 0 1 0)) := by
  rw [transpI_iff_lcCond]
  intro t ht w hw
  simp [occs] at ht; subst ht
  simp [lcK, Frame.step, ev, Isan] at hw ⊢
  exact hw.2

theorem sanity_and_right_presup : ¬ TranspI Isan Call (.bin .and (.trig 0 1 0) (.atom 0)) := by
  rw [transpI_iff_lcCond]
  intro h
  have := h ([Frame.left .and (.atom 0)], 0, 1, 0) (by simp [occs]) false
    (by simp [lcK, Frame.step, Call])
  simp [Isan] at this

end LCProp