Defining functions with choose and accessing hypotheses

Stream: new members

[VayusElytra]

Hello,

Let me start with an MWE:

structure DummyStructure

instance : CompleteLattice (DummyStructure) := by
  sorry

lemma ExistsDummyLemma : ∀ A : DummyStructure, ∃ B : Set (DummyStructure), A = sSup B := by
  sorry

-- DummyFunction maps the A in DummyLemma to B.
def DummyFunction : DummyStructure → Set (DummyStructure) := by
  intro A
  have h := ExistsDummyLemma A
  choose B h_B using h
  exact B

def sSupDummyLemma : ∀ A : DummyStructure, sSup (DummyFunction A) = A := by
  sorry

I often find myself in this situation, where I have a lemma containing an exists like ExistsDummyLemma guaranteeing the existence of some object with some property, which I wish to turn into a function for other purposes (for instance to be used with iSup).

How can I make sure that my function definition keeps the information that A = sSup B from ExistsDummyLemma? In this case I was thinking of writing this sSupDummyLemma lemma, but I'm unsure how to actually prove it, and even if I was this seems like a very stupid solution that can be done much more easily.

[Aaron Liu]

import Mathlib

structure DummyStructure

instance : CompleteLattice (DummyStructure) := by
  sorry

lemma ExistsDummyLemma : ∀ A : DummyStructure, ∃ B : Set (DummyStructure), A = sSup B := by
  sorry

-- DummyFunction maps the A in DummyLemma to B.
def DummyFunction : DummyStructure → Set (DummyStructure) :=
  fun A => (ExistsDummyLemma A).choose

def sSupDummyLemma : ∀ A : DummyStructure, sSup (DummyFunction A) = A :=
  fun A => (ExistsDummyLemma A).choose_spec

[VayusElytra]

Thank you, this is indeed a lot simpler :) am I safe to assume this is the most proper, Lean-ish way to do this?

[Kenny Lau]

VayusElytra said:

Thank you, this is indeed a lot simpler :) am I safe to assume this is the most proper, Lean-ish way to do this?

Yes, you're recommended to use term mode instead of tactic mode for definition (which might make things harder for you but easier in the long run)

[Kenny Lau]

and .choose and .choose_spec is the idiomatic way to do it

[Kenny Lau]

@VayusElytra i've made the answer above more mathlib compliant:

import Mathlib

def DummyStructure : Type := sorry
def DummyStructure₂ : Type := sorry
def dummyRel : DummyStructure → DummyStructure₂ → Prop := sorry
lemma exists_dummy : ∀ A : DummyStructure, ∃ B : DummyStructure₂, dummyRel A B := sorry

-- DummyFunction maps the A in DummyLemma to B.
noncomputable def dummyFunction (A : DummyStructure) : DummyStructure₂ :=
  (exists_dummy A).choose

lemma dummyR_dummyFunction (A : DummyStructure) : dummyRel A (dummyFunction A) :=
  (exists_dummy A).choose_spec

[VayusElytra]

Thank you very much, that is very useful.