Prove function using choose has properties it has

Stream: Is there code for X?

[Mark Andrew Gerads]

How do I prove that a function that uses choose to output a value from an existence proof has the properties claimed by the existence proof?

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable
def ChooseUnique9 : ℕ := by
  choose k h9exists h9unique using ExistsUnique9
  have h9 : k = 9 := by
    exact h9exists
  exact k

theorem ChooseUnique9_eq_9 : ChooseUnique9 = 9 := by
  rw [ChooseUnique9]
  simp only [Nat.reduceMul, forall_eq]
  -- not sure how to proceed
  sorry

[Mark Andrew Gerads]

Classical.choose_spec looks promising, but I have not figured out how to use it.

[Kim Morrison]

grind [Classical.choose_spec]

[Kim Morrison]

(possibly we should add @[grind] to Classical.choose_spec, I'll have to investigate)

[Kim Morrison]

Hopefully someone will also show you the old-fashioned way. It's sort of annoying to apply by hand!

[Mark Andrew Gerads]

Thanks.

[Robin Arnez]

You can use generalize_proofs:

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable
def ChooseUnique9 : ℕ := by
  choose k h9exists h9unique using ExistsUnique9
  have h9 : k = 9 := by
    exact h9exists
  exact k

theorem ChooseUnique9_eq_9 : ChooseUnique9 = 9 := by
  rw [ChooseUnique9]
  simp only [Nat.reduceMul, forall_eq]
  generalize_proofs hex
  exact hex.choose_spec.1

[Kenny Lau]

@Mark Andrew Gerads the "old-fashioned way" is "you shouldn't have used tactics in def to begin with":

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable
def ChooseUnique9 : ℕ :=
  ExistsUnique9.choose

theorem ChooseUnique9_eq_9 : ChooseUnique9 = 9 :=
  ExistsUnique9.choose_spec.left

[Kenny Lau]

@Robin Arnez is there a way to use h9 in the proof state here?

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable
def ChooseUnique9 : ℕ := by
  choose k h9exists h9unique using ExistsUnique9
  have h9 : k = 9 := by
    exact h9exists
  exact k

theorem ChooseUnique9_eq_9 : ChooseUnique9 = 9 := by
  unfold ChooseUnique9
/-
(fun k x =>
      have h9 := ⋯;
      k)
    (Classical.choose ExistsUnique9) ChooseUnique9._proof_2 =
  9
-/

[Kenny Lau]

I know that intro works on let in a different situation but intro didn't work here

[Kenny Lau]

@Mark Andrew Gerads but another way is to also carry around the proof in a subtype (so what you did with h9):

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable
def ChooseUnique9 : { k : ℕ // k = 9 } := by
  choose k h9exists h9unique using ExistsUnique9
  have h9 : k = 9 := by
    exact h9exists
  exact ⟨k, h9⟩

theorem ChooseUnique9_eq_9 : ChooseUnique9.val = 9 := by
  cases' ChooseUnique9 with k h9
  exact h9

[Robin Arnez]

Kenny Lau schrieb:

is there a way to use h9 in the proof state here?

Yes:

import Mathlib

theorem ExistsUnique9 : ∃! (k : ℕ), k = 3 * 3 := by
  use 9
  simp only [Nat.reduceMul, imp_self, implies_true, and_self]

noncomputable def ChooseUnique9 : ℕ := by
  choose k h9exists h9unique using ExistsUnique9
  have h9 : k = 9 := by
    exact h9exists
  exact k

theorem ChooseUnique9_eq_9 : ChooseUnique9 = 9 := by
  unfold ChooseUnique9
  dsimp -zetaUnused -zeta
  extract_lets h9
  exact h9

[Kenny Lau]

nice

[Kenny Lau]

I think this is the "correct" answer in the sense of intended