Diaconescu’s Theorem

Stream: general

[Sabrina Jewson]

I’m really struggling to understand Diaconescu’s Theorem in Lean. I’ve gotten this far:

universe u
parameter p : Prop
private def U (x : Prop) : Prop := x = true ∨ p
private def V (x : Prop) : Prop := x = false ∨ p
private def exU : ∃ x, U x := ⟨true, or.inl rfl⟩
private def exV : ∃ x, V x := ⟨false, or.inl rfl⟩
private def u : Prop := classical.some exU
private def v : Prop := classical.some exV
private lemma u_def : U u := classical.some_spec exU
private lemma v_def : V v := classical.some_spec exV
private lemma not_uv_or_p : u ≠ v ∨ p := sorry
private lemma hpred (hp : p) : U = V := sorry
private lemma h₀ (hp : p) : ∀ exU exV, @classical.some _ U exU = @classical.some _ V exV :=
  hpred hp ▸ λ exU exV, refl (@classical.some _ U exU)

This works. The problem is the last line however — I cannot seem to get it to compile using anything but exactly that syntax. The weird thing is using eq.subst instead of ▸ compiles, but even just switching to @ makes it fail:

@eq.subst _ _ _ _ (hpred hp) (λ exU exV, refl (@classical.some _ U exU))

  hpred hp ▸ λ (exU : ∃ (x : Prop), U x) (exV : ?m_2[exU]), refl (classical.some exU)
term
  λ (exU : ∃ (x : Prop), U x) (exV : ?m_1[exU]), refl (classical.some exU)
has type
  Π (exU : ∃ (x : Prop), U x) (exV : ?m_1[exU]), ?m_2[exU, exV] (classical.some exU) (classical.some exU)
but is expected to have type
  ?m_1 U

I tried filling in those parameters in several different permutations, I tried with eq.rec_on, eq.rec, @eq.rec, rw, simp…nothing succeeded. Is it actually possible to make it compile, or is eq.subst the only way?

and if so, that’s really weird, because it makes it seems like the actual axiom is not the Axiom of Choice but rather some magic special code in the compiler that makes this one case work (in fact, I can “prove” LEM constructively if I use subtype instead of ∃ and replace h₀ with sorry).

[Reid Barton]

If you use @, you will need to fill in the motive for eq.subst correctly.

[Reid Barton]

You should be able to use set pp.all true and then #print h₀ to see the whole proof term.

[Patrick Johnson]

This also works:

begin
  rw hpred _ hp,
  exact λ _ _, rfl,
end

The difference is that in term mode the parameter p of hpred is implicit, while inside begin...end it becomes explicit. I guess it is intentional design.

[Sabrina Jewson]

Reid Barton said:

You should be able to use set pp.all true and then #print h₀ to see the whole proof term.

Thanks, I didn’t know about that option, it appeared to work:

Output from set pp.all true

theorem h₀ : ∀ (p : Prop),
  p →
  ∀ (exU : @Exists.{1} Prop (λ (x : Prop), U p x)) (exV : @Exists.{1} Prop (λ (x : Prop), V p x)),
    @eq.{1} Prop (@classical.some.{1} Prop (U p) exU) (@classical.some.{1} Prop (V p) exV) :=
λ (p : Prop) (hp : p),
  @eq.subst.{1} (Prop → Prop → Prop)
    (λ (_x : Prop → Prop → Prop),
       ∀ (exU : @Exists.{1} Prop (λ (x : Prop), U p x)) (exV : @Exists.{1} Prop (λ (x : Prop), _x p x)),
         @eq.{1} Prop (@classical.some.{1} Prop (U p) exU) (@classical.some.{1} Prop (_x p) exV))
    U
    V
    (hpred p hp)
    (λ (exU exV : @Exists.{1} Prop (λ (x : Prop), U p x)),
       @refl.{0} Prop (@eq.{1} Prop)
         (@is_preorder.to_is_refl.{0} Prop (@eq.{1} Prop)
            (@is_equiv.to_is_preorder.{0} Prop (@eq.{1} Prop) (eq_is_equiv.{0} Prop)))
         (@classical.some.{1} Prop (U p) exU))

Patrick Johnson said:

This also works:

begin
  rw hpred _ hp,
  exact λ _ _, rfl,
end

The difference is that in term mode the parameter p of hpred is implicit, while inside begin...end it becomes explicit. I guess it is intentional design.

parameters continue to make my life hard :upside_down:. That simpler solution is really helpful as well though :)

[Patrick Johnson]

The difference is that in term mode the parameter p of hpred is implicit, while inside begin...end it becomes explicit. I guess it is intentional design.

Hm.. I'm not sure about it actually. Testing with simpler examples doesn't support this statement. Maybe I was wrong.

[Patrick Johnson]

Oh, I see. It's because of private lemmas. Here is a simplified example:

import tactic
section

parameter (n : ℕ)
def f : ℕ := n - 1

private lemma aux (h : 0 < n) : f + 1 = n :=
begin
  cases n,
  { cases h },
  { refl },
end

-- `n` is implicit in `aux`
example (h : 0 < n) : (f + 1) * 2 = n + n :=
aux h ▸ mul_two _

-- `n` is explicit in `aux`
example (h : 0 < n) : (f + 1) * 2 = n + n :=
begin
  rw aux _ h,
  exact mul_two _,
end

end

[Sabrina Jewson]

ah, that private lemmas thing is helpful, what a weird quirk

---

after staring at some errors some more I think I finally get it: the fundamental crux of theorem, the reason why it works for ∃ but not //, is that proof irrelevance means all values of type ∃ are equal. This then enables us to show that for two different existentials, their “left hand side” (i.e. what is returned by classical.some) will always be equal and that somehow leads into LEM.

[Kevin Buzzard]

Parameters are discouraged, there are always other ways to do things. Mathlib never uses parameters I believe

[Yaël Dillies]

It's still used in old files, file#computability/partrec for example.

[Martin Dvořák]

I was told that parameter was buggy, but I don't know what exactly is wrong with it.

[Junyan Xu]

See here for an example where parameter makes induction' fail.