Stable propositions, i.e. (not necessarily decidable) propostions for which double negation elimination holds

stable.lean

-- https://plfa.github.io/Negation
-- https://www.youtube.com/watch?v=SJ-_zqw5UHk

-- A very interesting idea of the talk above is that there is no information in
-- a classical proposition. Note that `(p ↔ q) → p = q` imply that every
-- proposition is isomorphic to `true` or `false` and neither carry any
-- information. Constructive `or` and `exists` carry information, so `stable p`
-- and `stable q` imply `stable (p ∧ q)` but not `stable (p ∨ q)`.

section

variables {p q r : Prop}

@[class, simp] def stable (p : Prop) : Prop :=
¬¬p → p

instance : stable ¬p :=
mt not_not_intro

instance [hp : stable p] [hq : stable q] :
  stable (p ∧ q) :=
λ h₁, and.intro
  (hp $ λ h₂, h₁ $ λ ⟨hp, _⟩, h₂ hp)
  (hq $ λ h₂, h₁ $ λ ⟨_, hq⟩, h₂ hq)

instance impl_stable [hq : stable q] :
  stable (p → q) :=
λ h₁ hp, hq $ λ h₂, h₁ $ λ h₃, h₂ $ h₃ hp

instance decidable_stable [hp : decidable p] :
  stable p :=
λ h, decidable.cases_on hp (false.elim ∘ h) id

lemma em_of_stable (h : stable (p ∨ ¬p)) :
  p ∨ ¬p :=
h $ not_not_em p

@[simp] def stable_or (p q : Prop) : Prop :=
¬(¬p ∧ ¬q)

instance stable_or_stable : stable (stable_or p q) :=
λ h₁ h₂, h₁ $ not_not_intro h₂

def stable_or.inr (hp : p) : stable_or p q :=
λ ⟨h, _⟩, h hp

def stable_or.inl (hq : q) : stable_or p q :=
λ ⟨_, h⟩, h hq

def stable_or.cases_on [hr : stable r]
  (h : stable_or p q) (h₁ : p → r) (h₂ : q → r) : r :=
hr $ λ h₃, h ⟨mt h₁ h₃, mt h₂ h₃⟩

lemma stable_or_em : stable_or p ¬p :=
λ ⟨h₁, h₂⟩, h₂ h₁

end

section

universe u

variables {α : Sort u} {p : α → Prop} {q : Prop}

instance stable_forall (h : ∀ a, stable (p a)) :
  stable (∀ a, p a) :=
λ h₁ a, h a $ λ h₂, h₁ $ λ h₃, h₂ $ h₃ a

@[simp] def stable_exists (p : α → Prop) : Prop :=
¬∀ a, ¬p a

instance stable_exists_stable {p : α → Prop} :
  stable (stable_exists p) :=
λ h₁ h₂, h₁ $ λ h₃, h₃ h₂

def stable_exists.intro (a : α) (ha : p a) :
  stable_exists p :=
λ h, h a ha

def stable_exists.cases_on [hq : stable q]
  (h₁ : stable_exists p) (h₂ : ∀ a, p a → q) : q :=
hq $ λ h₃, h₁ $ λ a ha, h₃ $ h₂ a ha

end