Implications involving choice principles, extensionality / quotient exactness, excluded middle, and classical/intermediate logics in type theory.

choice_and_excluded_middle.lean

import tactic data.setoid.basic
universes u v

def em (p) := p ∨ ¬p
def lem := ∀p, em p

def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β

theorem nonempty_choice : nonempty (Π {β : Sort v}, nonempty β → β) :=
  nonempty_pi _ (λα, nonempty_pi _ id)
-- first proposed by Mario Carneiro
-- without the outer "nonempty", this is [Lean] classical.choice or
-- [Coq] ID_epsilon = constructive version of indefinite description; combined with proof-irrelevance, it may be connected to Carlström's type theory with a constructive indefinite description operator

theorem np_of_nc {α : Sort u} (β : α → Sort v) :
  nonempty (Π {β : Sort v}, nonempty β → β) → np β :=  λ⟨c⟩ f, ⟨λa, c (f a)⟩

lemma cond_choice {α : Sort u} {β : Sort v} (r : α → β → Prop) :
  (∀a, ∃b, r a b) → ∃f:α→β, ∀a, r a (f a) :=
λh, let ⟨f⟩ := nonempty_pi (λa, {b // r a b}) (λa, nonempty_subtype.2 (h a))
  in ⟨λa,(f a).1, λa,(f a).2⟩
#print axioms cond_choice -- nonempty_pi
-- similar in form to the axiom for complete distributive lattice
-- [Coq] AC_fun = functional form of the (non extensional) axiom of choice (a "type-theoretic" axiom of choice)

-- nonempty_pi (with proof irrelevance (PI)) implies (the Prop version of) decidability of equality in any type
theorem deq {α : Sort u} : nonempty (decidable_eq α) :=
  nonempty_pi _ (λa₁, nonempty_pi _ (λa₂, by {
    /- variation on Diaconescu -/
    let s := {a // a₁ = a ∨ a₂ = a},
    cases cond_choice (λ(a:s) b, cond b (a₁ = a) (a₂ = a))
      (λ⟨a,h⟩, h.elim (λh,⟨tt,h⟩) (λh,⟨ff,h⟩)) with f hf,
    let A₁:s := ⟨a₁, or.inl rfl⟩, let A₂:s := ⟨a₂, or.inr rfl⟩,
    have : a₁ = a₂ ∨ f A₁ ≠ f A₂,
    { have h₁ := hf A₁, cases f A₁, left, exact h₁.symm,
      have h₂ := hf A₂, cases f A₂, right, triv, left, exact h₂ },
    refine this.elim (λh, ⟨decidable.is_true h⟩)
      (λh, ⟨decidable.is_false (mt (λe, _) h)⟩),
    subst e  /- uses PI for a₁ = a₂ ⇒ A₁ = A₂ -/ }))
#print axioms deq -- nonempty_pi
-- Thanks to Mario Carneiro for simplifying the proof, see https://leanprover-community.github.io/archive/stream/113488-general/topic/classical.2Eem.20without.20funext.20.2F.20quot.2Esound.html#207358170

-- LEM follows from nonempy_pi and proposition extensionality (and PI), no quot.sound or function extensionality required:
theorem em_of_propext : lem :=  let ⟨d⟩ := @deq Prop in
λp, by { cases d p true, right, exact mt eq_true_intro h, left, rw h, triv }
#print axioms em_of_propext -- nonempty_pi, propext used for eq_ture_intro

-- attempts to use quot.sound instead of propext failed, but the weaker principle, LEM for all negations, can be proved with quot.sound :

theorem wem_of_qsound : ∀p, em ¬p :=  λp, by {
  let m := @quot.mk bool (λ_ _,p),
  cases @deq (@quot bool (λ_ _,p)) with d,
  cases d (m ff) (m tt),
  left, refine mt _ h, exact λa, quot.sound a,
  right, intro n,
  cases congr_arg (@quot.lift bool (λ_ _,p) _ id (λ_ _ a, absurd a n)) h }
#print axioms wem_of_qsound -- nonempty_pi, quot.sound(, PI)


/- quotient exactness -/

def exact {α : Sort u} (s : setoid α) :=
  ∀{a a'}, quot.mk s.r a = quot.mk s.r a' → @setoid.r α s a a'
-- named quot.exact in Lean library; colloquially, means that for an equivalence relation, the quotient type is exactly the type of equivalence classes

def ker {α : Sort u} {β : Sort v} (f : α → β) : setoid α :=
  ⟨λa a', f a = f a', ⟨λ_,rfl, λ_ _,eq.symm, λ_ _ _,eq.trans⟩⟩
-- setoid.ker is defined in mathlib but only for Types

lemma exact_of_ker {α : Sort u} {β : Sort v} (f : α → β) : exact (ker f) :=
λa a' h, by {
  have := congr_arg (@quot.lift _ (ker f).r _ f (λ _ _, id)) h,
  exact this } -- why must do `have` then `exact`?
#print axioms exact_of_ker -- no axioms
-- Conversely, an equivalence relation is exact means exactly that it is the kernel of the quotient map, so an eqv rel is exact iff exist a sort and a map to that sort with the eqv rel as the kernel. The existence of such a map guarantees that the quotient cannot identify too many things. (In contrast, quot.sound ensures not too few are identified.) However, there is no obvious way to construct such a map for arbitrary eqv rels, or just for the iff relation.
-- quot α r is the initial object in the category of maps from α respecting r
-- quot α r and quot α (eqv_gen r) are canonically isomorphic (≃)

def funeqv {α : Sort u} (β : α → Sort v) : setoid (Π a, β a) :=
⟨λf g, ∀a, f a = g a,
 λf a, rfl,
 λf g r a, (r a).symm,
 λf g h r s a, (r a).trans (s a)⟩

-- funeqv is exact, no axiom required, because it's the intersection for all a:α of the kernels of the evaluation maps λf, f a (not necessarily the same as the kernel of the induced map to the Pi type over all a:α !)
example {α : Sort u} {β : α → Sort v} : exact (funeqv β) :=
λ_ _ h a, congr_arg (@quot.lift _ (funeqv β).r _ (λf, f a) (λ_ _ h, h a)) h
-- no axioms


/- Exactness of equivalence relations and excluded middle -/
-- show they are equivalent under nonempty_pi and quot.sound.

-- Excluded middle + nonempty_pi (or decidability of the relation s.r alone) implies exactness of any eqv rel, as any two inequivalent elements can be mapped to different things
theorem exact_of_em {α : Sort u} (s : setoid α) : lem → exact s :=
let r := s.r in λem a, by {
  cases cond_choice (λc x, cond x (r a c) (¬r a c))
    (λc, (em (r a c)).elim (λh,⟨tt,h⟩) (λh,⟨ff,h⟩)) with f hf,
  let f' := @quot.lift _ r _ f
    (λc d h, by { have hc := hf c, have hd := hf d,
      cases f c, cases f d, refl, cases hc (s.2.2.2 hd (s.2.2.1 h)),
                 cases f d, cases hd (s.2.2.2 hc h), refl }),
  intros b h, replace h := congr_arg f' h,
  have : f a = f b, exact h,
  have ha := hf a, cases f a, cases ha (s.2.1 a),
  have hb := hf b, rwa ← this at hb }
#print axioms exact_of_em -- nonempty_pi
#print axioms quot.exact -- the library proof of quot.exact uses propext and quot.sound instead, not em or choice

-- The eqv rel where two Props are equivalent iff both are equal or both are provable (hence iff-equivalent to true)
def teqv_setoid : setoid Prop :=
  ⟨λp q, p = q ∨ (p ∧ q),
   λ_, or.inl rfl,
   λ_ _, or.imp eq.symm and.symm,
   λ_ _ _ h' k', h'.elim (λh, h.symm ▸ k')
    (λh, k'.elim (λk, or.inr (k ▸ h)) (λk, or.inr ⟨h.1,k.2⟩))⟩
-- is the trivial relation assuming propext, because p ∧ q ⇒ p = q = true
-- trivial relation is the kernel of the identity map, hence exact
-- so propext ⇒ exact teqv_setoid

theorem em_of_exact : exact teqv_setoid → lem :=
  let ⟨d⟩ := @deq (quotient teqv_setoid) in
  let m := @quotient.mk _ teqv_setoid in
  λex p, by { cases d (m p) (m true),
    right, exact h ∘ (λa, quot.sound (or.inr ⟨a,trivial⟩)),
    left, cases ex h with a a, rw a, triv, exact a.1 }
#print axioms em_of_exact -- nonempty_pi, quot.sound
-- [Bell] Ackermann's Extensionality Principle (∀x,αx↔βx) → εα=εβ could be used as a replacement of exactness. Essentially eqv_choice w.r.t. the iff relation.



/- Other choice principles -/
-- that are not consequences of nonempty_pi without extensionality or excluded middle
-- Outline of implications : exact ⇒ eqv_choice ⇒ powersetoid_choice ⇒ partd_choice_fun ⇒ partd_choice_set ⇒ rep_choice_set ⇔ rep_choice_fun ⇒ exact
-- invokes nonempty_pi and quot.sound at some occasions; can go exact ⇒ eqv_choice ⇒ powersetoid_choice ⇒ partd_choice_fun ⇒ rep_choice_fun ⇒ exact, invoking them only at the first step

-- Reproduces a "setoid hell" (https://github.com/coq/coq/issues/10871) in Coq standard library https://coq.inria.fr/library/Coq.Logic.ChoiceFacts.html

def rep_choice_set {α : Sort u} (s : setoid α) := let r := s.r in
  ∃P:α→Prop, ∀a, ∃!a', P a' ∧ r a a'
-- can choose a set containing exactly one representative from each equivalence class
def rep_choice_fun {α : Sort u} (s : setoid α) := let r := s.r in
  ∃f:α→α, ∀a, r a (f a) ∧ ∀a', r a a' → f a = f a'
-- can map every element to its representative; clearly r is the kernel of any such function, so the existence of such choice function implies exactness of r
-- [Coq] AC_fun_repr = functional choice of a representative in an equivalence class
-- The function version is a special case of eqv_choice introduced below, and can also be stated with arbitrary relation r. Equivalent to considering the equivalence relation generated.
-- can get set as range of function, or function from set by choice ("reification")
-- [Coq] AC! = functional relation reification (known as axiom of unique choice in topos theory, sometimes called principle of definite description in the context of constructive type theory, sometimes called axiom of no choice)

def iff_setoid : setoid Prop := ⟨iff, iff.refl, λ_ _, iff.symm, λ_ _ _, iff.trans⟩
-- again, is the trivial relation under propext
def iff_rep_choice_set := rep_choice_set iff_setoid
-- ∃P:Prop→Prop, ∀p, ∃!q, P q ∧ (p ↔ q)
def iff_rep_choice_fun := rep_choice_fun iff_setoid
-- ∃f:Prop→Prop, ∀p q, (p ↔ f p) ∧ ((p ↔ q) → f p = f q)
def seteqv {α : Sort u} (P Q : α → Prop) := ∀a, P a ↔ Q a
def seteqv_setoid (α : Sort u) : setoid (α → Prop) :=
  @pi_setoid _ _ (λ_, iff_setoid)
#print axioms seteqv_setoid -- no axioms

theorem em_of_rcs : @rep_choice_set (ΣP:set bool, subtype P)
  ((seteqv_setoid bool).comap (λa, a.1)) → lem :=  λ⟨P,h⟩ p, by
  { rcases h ⟨λb,p∨b=ff,ff,or.inr rfl⟩ with ⟨⟨p₁,b₁,h₁⟩,⟨k₁,l₁⟩,u₁⟩,
    rcases h ⟨λb,p∨b=tt,tt,or.inr rfl⟩ with ⟨⟨p₂,b₂,h₂⟩,⟨k₂,l₂⟩,u₂⟩,
    cases (l₁ b₁).2 h₁ with a e₁, left, exact a,
    cases (l₂ b₂).2 h₂ with a e₂, left, exact a,
    right, intro hp, substs e₁ e₂,
    cases u₁ ⟨p₂,tt,h₂⟩ ⟨k₂,λb,⟨λ_,(l₂ b).1 (or.inl hp), λ_,or.inl hp⟩⟩ }
#print axioms em_of_rcs -- no axioms
/- [Coq] analogue :
Theorem repr_fun_choice_imp_excluded_middle :
  RepresentativeFunctionalChoice -> ExcludedMiddle. -/

example {α : Sort u} (s : setoid α) : rep_choice_fun s → rep_choice_set s := by
{ rintro ⟨f,hf⟩, use λa', ∃a, f a = a', intro a, use f a, split,
  split, use a, exact (hf a).1, intros b hb, rw (hf a).2 b hb.2,
  cases hb.1 with c hc, rw ← hc,
  exact (hf c).2 (f c) (hf c).1 }
-- no axioms

example {α : Sort u} (s : setoid α) : rep_choice_set s → rep_choice_fun s := by
{ let r := s.r, rintro ⟨P,hP⟩,
  cases cond_choice (λa b, P b ∧ r a b)
    (λa, exists_of_exists_unique (hP a)) with f hf,
  use f, intro a, split, exact (hf a).2,
  intros b h, cases hP a with c hc, rw hc.2 (f a) (hf a),
  rw hc.2 (f b) ⟨(hf b).1, s.2.2.2 h (hf b).2⟩ }
-- notice how idempotency f (f a) = f a is proved and used in the proof
-- axiom : nonempty_pi

lemma seteqv_eqvcls {α : Sort u} {s : setoid α} {a b : α} :
  let r := s.r in r a b ↔ seteqv (r a) (r b) :=
-- the equivalence class of a is simply r a
⟨λh _, ⟨s.2.2.2 (s.2.2.1 h), s.2.2.2 h⟩,  λh, (h b).2 (s.2.1 b)⟩

structure partd (α : Sort u) :=  -- partitionoid
  (ss : (α → Prop) → Prop)  -- set of subsets of α
  (is_partd : (∀a, ∃P, ss P ∧ P a) ∧
               ∀P, ss P → (∃a, P a) ∧ ∀Q a, ss Q → P a ∧ Q a → seteqv P Q)
def setoid.partd {α : Sort u} (s : setoid α) : partd α :=
  let r := s.r in ⟨λP, ∃a, P = r a,
    λa, ⟨r a, ⟨a, rfl⟩, s.2.1 a⟩,
    by { intros P hP, cases hP with a hP, split,
         use a, rw hP, apply s.2.1,
         intros Q b hQ PQa, cases hQ with c hQ,
         rw [hP,hQ] at PQa ⊢,
         exact seteqv_eqvcls.1 (s.2.2.2 PQa.1 (s.2.2.1 PQa.2)) }⟩

-- to-do? If you construct this "equivalence class" partitionoid from the setoid s, and then construct the equivalence relation of being in the same class in the partitionoid, then the new eqv rel is ∀∀↔ equivalent to the original s.

-- to-do? The quotient of α by s is canonically isomorphic to the quotient of the (subtype associated to the) partitinoid by seteqv, so the former quotient is exact iff the latter quotient is.

def partd_choice_set {α : Sort u} (p : partd α) :=
  ∃P:α→Prop, ∀Q, p.ss Q → ∃!a, P a ∧ Q a
def partd_choice_fun {α : Sort u} (p : partd α) :=
  let S := {P:α→Prop // p.ss P} in
    ∃f:S→α, ∀P:S, P.1 (f P) ∧ ∀Q:S, seteqv P.1 Q.1 → f P = f Q
-- also follows from eqv_choice

example {α : Sort u} (s : setoid α) :
  partd_choice_set s.partd → rep_choice_set s :=
λ ⟨P,hP⟩, ⟨P, λa, hP (@setoid.r α s a) ⟨a, rfl⟩⟩
-- no axioms

example {α : Sort u} (p : partd α) : partd_choice_fun p → partd_choice_set p :=
λ⟨f,hf⟩, ⟨λa, ∃P, a = f P, λP hP, ⟨f⟨P,hP⟩, by {
  use P, exact hP, exact (hf ⟨P,hP⟩).1, intros a ha,
  rcases ha with ⟨⟨⟨Q,hQ⟩,Qa⟩,ha⟩, rw Qa, apply (hf _).2,
  apply (p.is_partd.2 Q hQ).2, exact hP, split,
  exact (hf ⟨Q,hQ⟩).1, rw ← Qa, exact ha}⟩⟩
-- no axioms

def nesets (α : Sort u) := {P : α → Prop // ∃ a, P a} -- nonempty sets
def neseteqv_setoid (α : Sort u) :=
  @subtype.setoid _ (seteqv_setoid α) (λP, ∃a, P a)
def powersetoid_choice (α : Sort u) :=
  ∃f: nesets α → α, ∀P Q: nesets α, P.1 (f P) ∧ (seteqv P.1 Q.1 → f P = f Q)

example {α : Sort u} {p : partd α} : powersetoid_choice α → partd_choice_fun p :=
begin
  let : ΠP, p.ss P → nesets α := λP hP, ⟨P,(p.is_partd.2 P hP).1⟩,
  rintro ⟨f,hf⟩, fconstructor,
  exact λ⟨P,hP⟩, f (this P hP),
  rintro ⟨P,hP⟩, split, exact (hf (this P hP) (this P hP)).1,
  rintro ⟨Q,hQ⟩, exact (hf (this P hP) (this Q hQ)).2,
end
-- no axioms

def eqv_choice {α : Sort u} {β : Sort v} (s : setoid α) (r : α → β → Prop) :=
  let sr := s.r in
  (∀a, ∃b, r a b) → (∀a a' b, sr a a' → (r a b ↔ r a' b)) →
    ∃f:α→β, ∀a, r a (f a) ∧ ∀a', sr a a' → f a = f a'
-- [Coq] AC_fun_setoid = functional form of the (so-called extensional) axiom of choice from setoids. AC_fun_setoid = AC_fun + Ext_fun_repr + EM = AC_fun + Ext_pred_repr + PI : [Carlström04] Jesper Carlström, EM + Ext + AC_int is equivalent to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
-- Also interesting: AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of choice from setoids on locally compatible relations

example {α : Sort u} :
  eqv_choice (neseteqv_setoid α) (λP a, P.1 a) → powersetoid_choice α :=
λh, let ⟨f,hf⟩ := h (λ⟨P,a,ha⟩, ⟨a,ha⟩) (λP Q a hr, hr a)
  in ⟨f, λP Q, ⟨(hf P).1, (hf P).2 Q⟩⟩
-- no axioms

def seteqv_exact (α : Sort u) := exact (seteqv_setoid α)
-- could be seen as Axiom of Extensionality in ZF
def iff_exact := exact iff_setoid
/- Compare : [Coq] Extensional schemes
"iff_exact" Ext_prop_repr = choice of a representative among extensional propositions
"funeqv_exact" Ext_fun_repr = choice of a representative among extensional functions
"seteqv_exact" = "funeqv+iff_exact" Ext_pred_repr = choice of a representative among extensional predicates
(Coq has no quotient type or quot.sound) -/

example {α : Sort u} : iff_exact → seteqv_exact α :=
begin
  intros hi p q he a,
  let f := @quot.lift _ seteqv _ (λp:α→Prop, quot.mk iff (p a)) _,
  apply hi, have := congr_arg f he, exact this,
  exact λ_ _ h, quot.sound (h a),
end
-- axiom : quot.sound

example {α : Sort u} [s : setoid α] : seteqv_exact α → exact s :=
begin
  let r := s.r, -- why this works but s.r a doesn't work.
  let f := quot.lift (λa, quot.mk (@seteqv α) (r a))
    (λa b h, quot.sound (seteqv_eqvcls.1 h)),
  intros h a b he, apply seteqv_eqvcls.2, apply h,
  have := congr_arg f he, exact this,  -- why doesn't `exact congr_arg f he` work?
end
-- axiom : quot.sound

example {α : Sort u} {β : Sort v} (s : setoid α) (r : α → β → Prop) :
  exact s → eqv_choice s r :=
begin
  intros h hex heq,
  cases cond_choice (λ(ac: quotient s) b, ∀a, ⟦a⟧ = ac → r a b) _ with f hf,
  use λa, f⟦a⟧, intro a, split, exact hf⟦a⟧ a rfl,
  intros a' hr, rw quotient.sound hr,
  apply quot.ind, intro a, cases hex a with b hr,
  exact ⟨b, λa' he, (heq a' a b (h he)).2 hr⟩,
end
-- axioms : quot.sound, nonempty_pi

example {α : Sort u} (s : setoid α) : rep_choice_fun s → exact s :=
λh a b he, by { cases h with f hf,
  apply s.2.2.2 (hf a).1,
  have := congr_arg (quot.lift f (λa b, (hf a).2 b)) he,
  simp at this, rw this, exact s.2.2.1 (hf b).1 }
-- no axioms

/- Classical logic principles seen as choice principles -/
-- strong indefinite description / drinker paradox / independence of general premises / extension of function on subtype

-- [Bell] John L. Bell, Choice principles in intuitionistic set theory, http://publish.uwo.ca/~jbell/Choice%20Principles.pdf
-- I write " = [Bell] " to mean the form of the statements are the same, but the statements may not be of the same strength, since [Bell] quantifies over the whole universe while in Lean/Coq we quantify over any type.

-- [Coq] https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html
-- Independence of general premises and drinker's paradox
-- Independence of general premises is the unconstrained, non constructive, version of the Independence of Premises as considered in [Troelstra73].
-- It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle [KreiselPutnam57].

-- from https://eprints.illc.uva.nl/200/1/PP-2006-25.text.pdf, p.19
-- LC (Goedel--Dummett logic) axiomatized by [Bell] Lin : (φ→ψ)∨(ψ→φ). LC characterizes the linear frames and is complete with regard to the finite ones. Equivalent axiomatizations are (φ→ψ∨χ)→(φ→ψ)∨(φ→χ) or ((φ→ψ)→ψ)∧((ψ→φ)→φ) → φ∨ψ.
-- the reference says ((φ→ψ)→ψ) → φ∨ψ which is too strong: it readily implies LEM by taking ψ = ¬φ.
-- The stronger form (φ→ψ∨χ)→ψ∨(φ→χ) (classically valid) would directly imply LEM by taking ψ=φ and χ=false; it can be seen as (∀_:φ,ψ∨χ) → ψ∨∀_:φ,χ (proposition as type).
-- The more general form [Bell] Dis : ∀x,φ∨ψx → φ∨∀x,ψx is a predicate intermediate logic sound and complete for the frames with constant domains. The same formula axiomatizes dual frames / complete co-Heyting algebra according to https://en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_laws_for_complete_lattices.
-- [Bell] Dis is equivalent, over intuitionistic predicate logic, to what is called in [Lawvere & Rosebrugh, Sets for Mathematics, 2003] the higher dual distributive law HDDL: (∀a,ψa∨χa)  →  (∃a,ψa)∨∀a,χa
-- KC (de Morgan logic, logic of the weak excluded middle), axiomatized by [Bell] Stone : ¬φ ∨ ¬¬φ, complete with regard to the finite frames with a largest element. Implied by LC : (φ→ψ)∨(ψ→φ) by taking ψ=¬φ.

-- Outline of implications, the two implications involving "extendable" uses nonempty_pi.
-- sid' ⇒ sid ⇒ sid'' ⇒ extendable ⇒ sid'

def sid {α : Sort u} [nonempty α] (p : α → Prop) := ∃a, (∃b, p b) → p a
-- [Lean] noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop) (h : nonempty α) : {x : α // (∃ y : α, p y) → p x}
#print axioms classical.strong_indefinite_description -- all three (uses EM)
-- [Bell] Un = [Coq] Drinker = drinker's paradox (small form) (called Ex in Bell [Bell])
-- This is the Prop form, and the strong (Type) form is [Coq] D_epsilon = (weakly classical) indefinite description principle
-- equivalently, ∃a, ∀b, p b → p a

-- ∃a, p a → ∀b, p b ([Bell] Ex) is also called drinker paradox (e.g. on codewars), which implies ∃a, (∃ b, p b) → ¬¬p a; sid implies only ∃a, p a → ∀b, ¬¬p b
def drinker {α : Sort u} [nonempty α] (p : α → Prop) := ∃a, p a → ∀b, p b

theorem em_of_sid {p : Prop} :
  @sid {u:bool // p ∨ u=tt} ⟨⟨tt,or.inr rfl⟩⟩ (λu, ↑u=ff) → em p :=
λ⟨⟨u,h₁⟩,h₂⟩, h₁.imp id (λe h, by subst e; cases h₂ ⟨⟨ff,or.inl h⟩,rfl⟩)
#print axioms em_of_sid -- no axioms, not even proof irrelevance
-- this proof is slightly different from Diaconescu; it's rather equivalent to the derivation of EM from "relativized ε-scheme" in [Bell].

theorem em_of_drinker {p : Prop} :
  @drinker {u:bool // p ∨ u=tt} ⟨⟨tt,or.inr rfl⟩⟩ (λu, ↑u=tt) → em p :=
λ⟨⟨u,h₁⟩,h₂⟩, h₁.imp id (λe h, by subst e; cases h₂ rfl ⟨ff,or.inl h⟩)
#print axioms em_of_drinker -- no axioms

def sid' {α : Sort u} [nonempty α] (p : α → Prop) (r : Prop) :=
  (r → ∃a, p a) → ∃a, r → p a
-- [Coq] IGP = independence of general premises (an unconstrained generalisation of the constructive principle of independence of premises)
-- implies LC : (φ→ψ∨χ)→(φ→ψ)∨(φ→χ) immediately

-- Trivially interderivable:
example {α : Sort u} [nonempty α] (p : α → Prop) :
  sid' p (∃a, p a) → sid p :=  λs, s id
example {α : Sort u} [nonempty α] (p : α → Prop) (r : Prop) :
  sid p → sid' p r :=  λ⟨a,ha⟩ h, ⟨a,ha∘h⟩

def sid'' {α : Sort u} [nonempty α] (r : Prop) (p : r → α → Prop) :=
  (∀h:r, ∃a, p h a) → ∃a, ∀h:r, p h a
-- proof parameterized version of sid'

example {α : Sort u} [nonempty α] (r : Prop) (p : r → α → Prop) :
  sid (λa, ∃h:r, p h a) → sid'' r p :=
λ⟨a,ha⟩ he, ⟨a, λh, let ⟨b,hb⟩ := he h in (ha ⟨b,h,hb⟩).snd⟩
-- proof uses proof irrelevance; no axioms

-- Next we introduce an apparently novel (not mentioned in the above references) "function extension principle" which says that any function from a subtype of α to a nonempty type β can be extended to α.
def extendable {α : Sort u} {β : Sort v} [nonempty β] (p : α → Prop)
  (f : {a // p a} → β) := ∃g:α→β, ∀a, f a = g a

lemma ex_choice {α : Sort u} {p : α → Prop} {r : Prop} :
  (r → ∃a, p a) → ∃f:r→α, ∀h:r, p (f h) :=  λhi, cond_choice (λ_ a, p a) hi
-- can't really avoid choice even with subsingleton domain

example {α : Sort u} [nonempty α] (p : α → Prop) (r : Prop):
  (∀f:{a:unit//r}→α, extendable (λ_, r) f) → sid' p r :=
λhe hi, let ⟨f,hf⟩ := ex_choice hi, ⟨g,hg⟩ := he (λa, f a.2)
         in ⟨g (), λh, (hg ⟨_,h⟩).subst (hf h)⟩
-- must use proof irrelevance if succeed in not using choice
-- cf. Bell's Intuitionistic Set Theory http://publish.uwo.ca/~jbell/INTBOOK(Repaired).pdf p.16 : power set of 1, frame of truth values, subset classifier Ω


example {α : Sort u} {β : Sort v} [nonempty β] (p : α → Prop) (f : {a // p a} →
β) :
  (∀r (q:r→β→Prop), sid'' r q) → extendable p f :=
λs, let ⟨g,hg⟩ := cond_choice (λa b, ∀h:p a, f⟨a,h⟩ = b)
  (λa, by {apply s, exact λh, ⟨f⟨a,h⟩,rfl⟩}) in  ⟨g, λ⟨a,h⟩, hg a h⟩

def linv_of_inj {α : Sort u} [nonempty α] {β : Sort v} (f : α → β)
  (hi : function.injective f) := ∃g:β→α, ∀a, g (f a) = a
-- function extension principle implies that any injective function has a left inverse
example {α : Sort u} [nonempty α] {β : Sort v} (f : α → β)
  (hi : function.injective f) :
  (∀(p:β→Prop) (f:{b//p b}→α), extendable p f) → linv_of_inj f hi :=
λhe, let ⟨g',hg'⟩ := cond_choice (λ(b:{b//∃a,f a=b}) a, f a = b) (λ⟨b,h⟩,h),
         ⟨g, hg⟩  := he _ g' in
         ⟨g, λa, hi ((hg ⟨f a,a,rfl⟩).subst (hg' ⟨f a,a,rfl⟩))⟩
-- axiom : nonempty_pi

theorem em_of_extendable {p : Prop} :
  @extendable unit {u:bool//p∨u=tt} ⟨⟨tt,or.inr rfl⟩⟩
    (λ_,p) (λ⟨u,h⟩,⟨ff,or.inl h⟩)  →  em p :=
λ⟨f,hf⟩, (f()).2.imp id
  (λh hp, by {specialize hf ⟨(),hp⟩, dsimp at hf, rw ← hf at h, triv})

theorem em_of_linv_inj {p : Prop} :
  @linv_of_inj {u:bool//p∨u=tt} ⟨⟨tt,or.inr rfl⟩⟩ _
    subtype.val subtype.val_injective  →  em p :=
λ⟨g,hg⟩, (g ff).2.imp id (λv h, by {rw hg ⟨ff,or.inl h⟩ at v, cases v})
#print axioms em_of_linv_inj -- no axioms, proof irrelevance for injectivity


-- outline: daco ⇒ dac ⇒ dac₂ ⇒ dis (⇔ hddl) ⇒ em

def dac {α : Sort u} {β : Sort v} {p : α → β → Prop} :=
  (∀f:α→β, ∃a, p a (f a)) → ∃a, ∀b, p a b
-- dual axiom of choice, non-omniscient/non-guarded, converse trivially holds

def daco {α : Sort u} {β : Sort v} [nonempty (α→β)] {p : α → β → Prop} :=
  ∃f:α→β, (∃a, p a (f a)) → ∃a, ∀b, p a b

example {α : Sort u} {β : Sort v} [nonempty (α→β)] {p : α → β → Prop} :
  @daco α β _ p → @dac α β p :=  λ⟨f,hf⟩ h, hf (h f)

example {α : Sort u} {β : Sort v} [nonempty (α→β)] {p : α → β → Prop} :
  @drinker (α→β) _ (λf, ∃a, p a (f a)) → @dac α β p → @daco α β _ p :=
  λ⟨f,hf⟩ d, ⟨f,d∘hf⟩

-- digression: outline: daco₁ = drinker ⇔ daco₂ (already showed drinker ⇒ em)
def daco₂ {β : Sort v} [nonempty β] {p₁ : β → Prop} {p₂ : β → Prop} :=
  ∃b₁ b₂, p₁ b₁ ∨ p₂ b₂ → (∀b, p₁ b) ∨ (∀b, p₂ b)

@[instance] def nonempty.funsp {α : Sort u} {β : Sort v} [h : nonempty β] :
  nonempty (α → β) := let ⟨n⟩ := h in ⟨λ_,n⟩

example {β : Sort v} [nonempty β] {p₁ : β → Prop} {p₂ : β → Prop} :
  @daco bool β _ (@bool.rec (λ_, β→Prop) p₁ p₂) → @daco₂ β _ p₁ p₂ :=
λ⟨f,h⟩, ⟨f ff, f tt, λo, o.elim
  (λh₁, let ⟨a,p⟩ := h ⟨ff,h₁⟩ in by {cases a, exacts [or.inl p, or.inr p]})
  (λh₂, let ⟨a,p⟩ := h ⟨tt,h₂⟩ in by {cases a, exacts [or.inl p, or.inr p]})⟩

-- `drinker` is simply daco₁:
example {β : Sort v} [nonempty β] {p : β → Prop} :
  @daco unit β _ (λ_,p) → drinker p :=
λ⟨f,h⟩, ⟨f (), λo, let ⟨_,r⟩ := h ⟨(),o⟩ in r⟩
-- similarly, aco₁ (not defined) ⇔ sid

example {β : Sort v} [nonempty β] {p : β → Prop} :
  @daco₂ β _ (λ_,false) p → drinker p :=
λ⟨_,b,h⟩, ⟨b, λe, (h (or.inr e)).elim (λf, (f b).rec _) id⟩

example {β : Sort v} [nonempty β] {p₁ : β → Prop} {p₂ : β → Prop} :
  drinker p₁ → drinker p₂ → @daco₂ β _ p₁ p₂ :=
λ⟨b₁,h₁⟩ ⟨b₂,h₂⟩, ⟨b₁,b₂,or.imp h₁ h₂⟩
-- to prove daco this way we'd need nonempty_pi
-- end of digression

def dac₂ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} :=
  (∀a b, p a ∨ q b) → (∀a, p a) ∨ (∀b, q b)
-- notice here p and q has different domain, as opposed to daco₂ above
-- however dac with fixed β can still imply dac₂ with variable domain, as shown below

def psum_prop {α : Sort u} {β : Sort v} (p : α → Prop) (q : β → Prop) :=
  @bool.rec (λ_,psum α β → Prop)
  (λe, ∀a, e = psum.inl a → p a) (λe, ∀b, e = psum.inr b → q b)

example {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} :
  @dac bool (psum α β) (psum_prop p q) → @dac₂ α β p q :=
λd h, by { have := d _, swap, intro f,
           suffices : psum_prop p q ff (f ff) ∨ psum_prop p q tt (f tt),
           { cases this, exacts [⟨ff,this⟩,⟨tt,this⟩] },
           { cases f tt with a b, right, intros b e, cases e,
             cases f ff with a b, cases h a b with hp hq,
             left, intros a' e, cases e, exact hp,
             right, intros b' e, cases e, exact hq,
             left, intros b e, cases e },
           cases this with x hx, cases x,
           left, exact λa, hx (psum.inl a) a rfl,
           right, exact λb, hx (psum.inr b) b rfl }

def dis {α : Sort u} {p : Prop} {q : α → Prop} :=
  (∀a, p ∨ q a) → p ∨ (∀a, q a)
-- ∀ distributes over ∨, converse trivially holds

def hddl {α : Sort u} {p : α → Prop} {q : α → Prop} :=
  (∀a, p a ∨ q a) → (∃a, p a) ∨ (∀a, q a)
-- converse invalid in general

example : (∀{α p} q, @dis α p q) ↔ ∀α β p q, @dac₂ α β p q :=
⟨λd α β p q h, d q (λb, or.comm.1 (d p (λa, or.comm.1 (h a b)))),
 λd α p q h, (d unit α (λ_,p) q (λ_,h)).imp (λh,h ()) id⟩

example {α} {p q : α→Prop} : @dis α (∃a, p a) q → @hddl α p q :=
  λd h, d (λa, (h a).imp (λha, ⟨a,ha⟩) id)

example {α} {p:Prop} {q:α→Prop} : @hddl α (λ_, p) q → @dis α p q :=
  λhd h, (hd h).imp (λ⟨_,h⟩,h) id

example {p : Prop} : @dis p p (λ_, false) → em p :=  λd, d (λh, or.inl h)
-- λd, d or.inl doesn't work

-- em clearly implies all these principles, but if we only know em but not decidability, would still require nonempty_pi for reification.


/- Appendix: classical and intermediate logics -/
-- logic LC
def lin (p q : Prop) := (p → q) ∨ (q → p)
def lin₁ (p q r : Prop) := (r → p ∨ q) → ((r → p) ∨ (r → q))
def lin₂ (p q : Prop) := ((p → q) → q) ∧ ((q → p) → p) → p ∨ q

example (p q) : p ∨ q → ((p → q) → q) ∧ ((q → p) → p) :=
  λd, d.elim (λh, ⟨λi,i h, λ_,h⟩) (λh, ⟨λ_,h, λi,i h⟩)
-- thus lin₂ allows us to define ∨ in terms of ∧ and → in the logic LC

example (p q r) : lin q p → lin₁ p q r :=
  λl h, l.imp (λi hr, (h hr).elim id i) (λi hr, (h hr).elim i id)

example (p q) : lin₁ q p (q ∨ p) → lin p q :=
  λl, (l id).imp (λh, h ∘ or.inr) (λh, h ∘ or.inl)

lemma limp {p q : Prop} : ((p → q) → (q → p)) → (q → p) := λi h, i (λ_,h) h

example (p q : Prop) : lin₂ (p → q) (q → p) → lin p q := λl, l ⟨limp,limp⟩

example (p q : Prop) : lin q p → lin₂ p q :=  λl ⟨h₁,h₂⟩, l.imp h₂ h₁


theorem nnem {p} : ¬¬em p := λn, n (or.inr (n ∘ or.inl))
-- what about ¬¬lem ?

example (p : Prop) : lin p ¬p → em ¬p :=  λl, l.imp (λi h, i h h) (λi h, h (i h))

def dne (p : Prop) := ¬¬p → p
-- double negation elimination / definition of regular element in Heyting algebra

-- triple negation elimination
theorem tne {p : Prop} : dne ¬p := mt (λh n, n h)

lemma reg_iff {p : Prop} : dne p ↔ (∃q, p ↔ ¬q) :=
⟨λd, ⟨¬p, ⟨λ h n,n h, d⟩⟩,  λ⟨q,⟨e₁,e₂⟩⟩, e₂ ∘ tne ∘ mt (mt e₁)⟩
-- ⟨λd, ⟨¬p, ⟨λ h n, n h, d⟩⟩, λ⟨q,⟨e₁,e₂⟩⟩ dp, e₂ (tne (λdq, dp (dq ∘ e₁)))⟩

/- de Morgan logic -/
-- cf. https://en.wikipedia.org/wiki/Heyting_algebra#The_De_Morgan_laws_in_a_Heyting_algebra

def dm₂ := ∀p q, ¬(p ∧ q) → ¬p ∨ ¬q
def dm₃ := ∀p q, dne p → dne q → ¬(p ∧ q) → ¬p ∨ ¬q
def dm₄ := ∀p q, ¬¬(p ∨ q) → ¬¬p ∨ ¬¬q
def dm₅ := ∀p q, dne p → dne q → ¬¬(p ∨ q) → p ∨ q
def dm₇ := ∀p, em ¬p

lemma dm {p q} : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  ⟨λn, ⟨n ∘ or.inl, n ∘ or.inr⟩, λ⟨c₁,c₂⟩ d, d.elim c₁ c₂⟩

example : dm₂ → dm₃ := λd p q _ _, d p q
example : dm₃ → dm₄ := λd p q n, d (¬p) (¬q) tne tne (n ∘ dm.2)
example : dm₄ → dm₅ := λd p q dp dq dn, (d p q dn).imp dp dq
example : dm₅ → dm₇ := λd p, d (¬p) (¬¬p) tne tne nnem
example : dm₇ → dm₂ := λd p q n, (d p).imp id (mt (λh₂ h₁, n ⟨h₁,h₂⟩))

def ipeirce (p q : Prop) := ((p → q) → p) → p

theorem dne_of_peirce (p) : ipeirce p false → dne p := λh d, h (false.elim ∘ d)
theorem peirce_of_dne (p q) : dne p → ipeirce p q :=
  λd i, d (λn, n (i (false.elim ∘ n)))

theorem dne_of_em (p) : em p → dne p := λe d, e.elim id (false.elim ∘ d)
theorem em_of_dne : (∀p, dne p) → lem := λd p, d _ nnem

theorem em_of_em_iff_em (p) : em (em p) ↔ em p :=
  ⟨λd, d.elim id (false.elim ∘ nnem), or.inl⟩
--or ⟨λd, d.elim id (λn, or.inr (n ∘ or.inl)), or.inl⟩


/- leanpkg.toml
[package]
name = "lftcm2020"
version = "0.1"
lean_version = "leanprover-community/lean:3.17.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4a6b7168e7fe47c7bb3991736de569f981ed93a8"}
-/

http://eprints.nottingham.ac.uk/28941/1/Nuo%20Li%27s_Thesis.pdf Theorem 3.3: propext implies quotient.exact