import LCAbstract
/-!
# Example 23 : `(Infinitely-many P . QQ')`

Single world (`W = Unit`), infinite domain `D = Nat`, restrictor `P` = all of `D` (infinitely many),
quantifier `Inf`: `f(a,b) = 1` iff `b` is infinite.  The good final of `(Inf P . _` is just `)`.
`Envs` is the environment `x ↦ [[(Inf P . c'x)]]`.  Using the abstract theory `LCAbstract`:
  * 23a: `tr` has no bottom element, i.e. no local context exists;
  * 23b: `Q` = "different from 0" is transparent (so `Transp_i`, equivalently `Sat'_i`, holds) yet
    `(Every P . Q)` is false: the dynamic presupposition (`every P is Q`) is not entailed.
-/
namespace LCInf
open Classical

def Inf (S : Nat → Bool) : Prop := ∀ N, ∃ m, N ≤ m ∧ S m = true

noncomputable def Ψinf : LC.Env Unit Nat := fun x _ => decide (Inf (x ()))
def Envs : LC.Env Unit Nat → Prop := fun Ψ => Ψ = Ψinf
def C : Unit → Prop := fun _ => True

theorem Ψinf_ext : LC.Ext Ψinf := by
  intro x y w h; cases w; simp [Ψinf, h]

theorem inf_congr (S S' : Nat → Bool) (a : Nat) (h : ∀ m, m ≠ a → S m = S' m) (hS : Inf S) : Inf S' := by
  intro N
  obtain ⟨m, hm, hSm⟩ := hS (max N (a + 1))
  refine ⟨m, Nat.le_trans (Nat.le_max_left _ _) hm, ?_⟩
  have : m ≠ a := by have := Nat.le_max_right N (a + 1); omega
  rw [← h m this]; exact hSm

theorem inf_congr_iff (S S' : Nat → Bool) (a : Nat) (h : ∀ m, m ≠ a → S m = S' m) :
    Inf S ↔ Inf S' :=
  ⟨inf_congr S S' a h, inf_congr S' S a (fun m hm => (h m hm).symm)⟩

theorem tr_iff (x : LC.Val Unit Nat) :
    LC.Tr Envs C x ↔ ∀ γ : Nat → Bool, (Inf (fun d => x () d && γ d) ↔ Inf γ) := by
  constructor
  · intro H γ
    have := H Ψinf rfl (fun _ => γ) () trivial
    simp only [Ψinf, decide_eq_decide] at this
    exact this
  · intro H Ψ hΨ γ w _
    subst hΨ; cases w
    simp only [Ψinf, decide_eq_decide]
    exact H (γ ())

/-- **Example 23a**: the set of transparent restrictions has no bottom element:
`QQ'` has no local context in `{w}`. -/
theorem example23a : ¬ ∃ x, LC.IsLC Envs C x := by
  rintro ⟨x, hx, hmin⟩
  have hx' := (tr_iff x).mp hx
  -- x is infinite
  have hinf : Inf (x ()) := by
    have := (hx' (fun _ => true)).mpr (by intro N; exact ⟨N, Nat.le_refl _, rfl⟩)
    simpa using this
  obtain ⟨a, _, ha⟩ := hinf 0
  -- remove one element
  let y : LC.Val Unit Nat := fun _ d => x () d && decide (d ≠ a)
  have hy : LC.Tr Envs C y := by
    rw [tr_iff]
    intro γ
    have h1 := hx' γ
    refine Iff.trans ?_ h1
    apply inf_congr_iff _ _ a
    intro m hm
    simp [y, hm]
  have := hmin y hy () a ha
  simp [y] at this

/-- `Q d :⇔ d ≠ 0` (true of all P-individuals but one) -/
def Qinf : LC.Val Unit Nat := fun _ d => decide (d ≠ 0)

/-- **Example 23b**: `Q` is transparent (so `Transp_i` and `Sat'_i` hold, cf. Theorem 21) although
`(Every P . Q)` is false. -/
theorem example23b :
    LC.Tr Envs C Qinf ∧ LC.SatP Envs C Qinf ∧ ¬ (∀ d : Nat, Qinf () d = true) := by
  have hT : LC.Tr Envs C Qinf := by
    rw [tr_iff]
    intro γ
    apply inf_congr_iff _ _ 0
    intro m hm
    simp [Qinf, hm]
  refine ⟨hT, (LC.thm21 (by rintro Ψ rfl; exact Ψinf_ext) Qinf).mpr hT, ?_⟩
  intro h; have := h 0; simp [Qinf] at this

end LCInf