Using cases outside of Prop

Stream: new members

[André Hernández-Espiet (Rutgers)]

I was trying to provide a function. I then tried to use cases inside the proof, and it would not allow me. I feel like I am missing something very obvious. How does one extract k from junk?

example : ℕ → ℕ := by
  have junk : ∃ (k : ℕ), k = k := by use 1
  cases junk

[Henrik Böving]

You cannot do this. Proofs are irrelevant in Lean (to be more precise: Lean allows you to prove that any two proofs of the same proposition are the same and thus the actual value of the proof is irrelevant) the Lean compiler makes use of this by erasing all proof values at compile time so once you are outside of Prop and operate in run time relevant univeses (i.e. everything except Prop) you cannot do case distinctions etc. on a Prop.

That said you can use the Type variant of exists, docs#Subtype (or also docs#PSigma) to achieve basically what you want to do.

[Alex J. Best]

Or you can use choice, if you do not need the result to be computable, and do not want the exact same k back.

import Mathlib
noncomputable example : ℕ → ℕ := by
  have junk : ∃ (k : ℕ), k = k := by use 1
  choose n h using junk
  intro a
  use a * n

[André Hernández-Espiet (Rutgers)]

Very interesting! The choice alternative works fine. However, I am curious about how to implement these with Subtype, as I don´t think I have done this before.

[Kyle Miller]

@Henrik Böving There are exceptions -- you can do cases on an Eq for example; this is known as "large subsingleton elimination".

A logical reason why you can't do cases on Exists, rather than a compiler engineering explanation, also starts with proof irrelevance; what it implies is that if Exists.intro x p and Exists.intro y q are proofs of the same existential, if you could do cases you'd be able to prove that x = y, but that can quickly lead to a contradiction. For example, both Exists.mk 0 rfl and Exists.mk 1 rfl are proofs of ∃ (k : ℕ), k = k.

In particular, it would let you define the following two axioms and prove False.

axiom Exists.extract {α : Sort _} {p : α → Prop} : (∃ x, p x) → α

axiom Exists.extract_mk {α : Sort _} {p : α → Prop} {x : α} (h : p x) :
    Exists.extract (Exists.intro x h) = x

set_option pp.proofs true

example : False := by
  have : 0 = 1 :=
    calc
      0 = Exists.extract (Exists.intro 0 rfl : ∃ x, x = x) := (Exists.extract_mk (by rfl)).symm
      _ = Exists.extract (Exists.intro 1 rfl : ∃ x, x = x) := rfl
      _ = 1 := Exists.extract_mk (by rfl)
  simp at this

[Kyle Miller]

Here are those axioms implemented using the "bad casesOn". The error you get from the cases tactic is reporting that it's not able to use casesOn due to the universe limitation in the motive argument.

-- Bad casesOn. Does large elimination (the motive is `Sort _` valued instead of `Prop valued)
@[elab_as_elim]
axiom Exists.casesOn' {α : Sort _} {p : α → Prop} {motive : Exists p → Sort _} (t : Exists p)
    (intro : ∀ (w : α) (h : p w), motive (Exists.intro w h)) : motive t

-- Computation rule for casesOn. This comes with the normal casesOn as a defeq.
axiom Exists.casesOn'_intro {α : Sort _} {p : α → Prop} {motive : Exists p → Sort _}
    (intro : ∀ (w : α) (h : p w), motive (Exists.intro w h))
    (w : α) (h : p w) :
    Exists.casesOn' (Exists.intro w h) intro = intro w h

noncomputable
def Exists.extract {α : Sort _} {p : α → Prop} (h : ∃ x, p x) : α :=
  Exists.casesOn' h fun x _ => x

theorem Exists.extract_mk {α : Sort _} {p : α → Prop} {x : α} (h : p x) :
    Exists.extract (Exists.intro x h) = x := by
  rw [Exists.extract, Exists.casesOn'_intro]
  exact h