/-!
# Infinite domains (footnotes 12 and 16)

`Q = infinitely many`, an arbitrary domain `D`.  A set is *infinite* iff no finite list covers it.
World-wise statement (one world `w`; `P`, `R` are the extensions of `P^w`, `R^w`, `γ` ranges over
all sets of individuals).  This is a simplified (single-world, semantic) rendering of the
Transparency condition for `(Q P . R̲R')`, with `γ` ranging over all properties.
-/

namespace AntiDyn
namespace InfiniteDomain

variable {D : Type}

/-- Not covered by any finite list. -/
def Inf (s : D → Prop) : Prop := ∀ l : List D, ∃ x, s x ∧ x ∉ l
/-- Covered by a finite list. -/
def Fin' (s : D → Prop) : Prop := ∃ l : List D, ∀ x, s x → x ∈ l

/-- `(Q P . (R and γ)) ⇔ (Q P . γ)` for all `γ` at a world, `Q = infinitely many`. -/
def TranspInf (P R : D → Prop) : Prop :=
  ∀ γ : D → Prop, Inf (fun d => P d ∧ (R d ∧ γ d)) ↔ Inf (fun d => P d ∧ γ d)

/-- **Footnote 12, sufficiency**: if `P^w ∖ R^w` is finite, Transparency holds at `w`. -/
theorem transpInf_of_finite (P R : D → Prop) (h : Fin' (fun d => P d ∧ ¬ R d)) : TranspInf P R := by
  intro γ
  constructor
  · intro hi l
    obtain ⟨x, hx, hxl⟩ := hi l
    exact ⟨x, ⟨hx.1, hx.2.2⟩, hxl⟩
  · intro hi l
    obtain ⟨l0, hl0⟩ := h
    obtain ⟨x, hx, hxl⟩ := hi (l ++ l0)
    have hxR : R x := by
      apply Classical.byContradiction
      intro hR
      exact hxl (List.mem_append_right _ (hl0 x ⟨hx.1, hR⟩))
    exact ⟨x, ⟨hx.1, hxR, hx.2⟩, fun hm => hxl (List.mem_append_left _ hm)⟩

/-- **Converse (new)**: if `P^w ∖ R^w` is infinite, Transparency fails at `w`
(take `γ = P ∖ R`). -/
theorem not_transpInf_of_infinite (P R : D → Prop) (h : ¬ Fin' (fun d => P d ∧ ¬ R d)) :
    ¬ TranspInf P R := by
  intro ht
  have h1 := (ht (fun d => ¬ R d)).2
  have hinf : Inf (fun d => P d ∧ ¬ R d) := by
    intro l
    apply Classical.byContradiction
    intro hn
    apply h
    exact ⟨l, fun x hx => Classical.byContradiction fun hxl => hn ⟨x, hx, hxl⟩⟩
  have := h1 hinf []
  obtain ⟨x, ⟨_, hR, hnR⟩, _⟩ := this
  exact hnR hR

/-- Hence, at a world: Transparency holds iff `P^w ∖ R^w` is finite,
whereas Heim's presupposition (`∀d [P(d) ⇒ R(d)]`) requires `P^w ∖ R^w = ∅`. -/
theorem transpInf_iff (P R : D → Prop) : TranspInf P R ↔ Fin' (fun d => P d ∧ ¬ R d) :=
  ⟨fun h => Classical.byContradiction fun hn => not_transpInf_of_infinite P R hn h,
   transpInf_of_finite P R⟩

/-- Footnote 16: integers, `P` = all integers (here: naturals), `R d` = `d ≠ 13`
("is lucky not to be the number 13" presupposes `d ≠ 13`).  `P ∖ R = {13}` is finite, so
Transparency holds although Heim's presupposition (every integer differs from 13) fails. -/
theorem footnote16 :
    TranspInf (D := Nat) (fun _ => True) (fun d => d ≠ 13) ∧
      ¬ ∀ d : Nat, True → d ≠ 13 := by
  refine ⟨transpInf_of_finite _ _ ⟨[13], ?_⟩, ?_⟩
  · intro x ⟨_, hx⟩
    have : x = 13 := Classical.byContradiction hx
    simp [this]
  · intro h; exact h 13 trivial rfl

end InfiniteDomain
end AntiDyn