Set notation with propositions

Stream: new members

[Gareth Ma]

Is there a better to write the commented line? I want to construct all Things such that $x \leq 3$.

inductive Thing
  | cons (x : ℕ) (h : x ≤ 5)

def S : Set Thing := { Thing.cons x.val (x.prop.trans $ by norm_num) | x : { y // y ≤ 3 } }
/- { Thing.cons x h | x : ℕ s.t. h : x ≤ 3 } -/

[Kyle Miller]

I can't parse your question, but is this the answer?

def S : Set Thing := { Thing.cons x (h.trans $ by norm_num) | (x : ℕ) (h : x ≤ 3) }

[Gareth Ma]

Yes perfect! Sorry for the unclear question :tear:

[Notification Bot]

Gareth Ma has marked this topic as resolved.

[Notification Bot]

Gareth Ma has marked this topic as unresolved.

[Gareth Ma]

Hope you don't mind me overloading this thread, since I don't want to spam with too many threads. Can you give some hint on how to construct this equivalence?

inductive Point
  | none
  | some {x y : ℚ} (h : y ^ 2 - x = 0)

def liftX (x₀ : ℚ) : Set Point :=
    { Point.some h | (y : ℚ) (h : y ^ 2 - x₀ = 0) }

theorem aux1 (x₀ : ℚ) :
    liftX x₀ ≃ { y | y ^ 2 - x₀ = 0 } := sorry

The annoying thing is that the Point inductive has none (which I don't care) and some, and I can't "extract" the y easily

[Yaël Dillies]

def aux1 (x₀ : ℚ) : liftX x₀ ≃ { y | y ^ 2 - x₀ = 0 } where
  toFun z := match z with
    | ⟨.none, hz⟩ => by simp [liftX] at hz
    | ⟨.some h, hz⟩ => by
      simp [liftX] at hz
      obtain rfl := hz.1
      exact ⟨_, hz.2⟩
  invFun y := ⟨.some y.2, _, _, rfl⟩
  left_inv z := match z with
    | ⟨.none, hz⟩ => by simp [liftX] at hz
    | ⟨.some h, hz⟩ => by
      simp [liftX] at hz
      obtain rfl := hz.1
      simp
  right_inv y := by simp

[Gareth Ma]

Thank you so much!

[Gareth Ma]

So this proof uses Classical.choice (from #print axioms aux1). Why is noncomputable not required?

[Yaël Dillies]

Are you sure it's not just using choice to prove LEM or something like that?

[Gareth Ma]

No I'm not sure. Would that mean noncomputable is not required?

[Yaël Dillies]

The data is not constructed using choice, so it is computable

[Yaël Dillies]

Try replacing the proof fields by sorry and I'm sure the definition won't use choice anymore

[Gareth Ma]

For proof fields you mean right_inv and left_inv?

[Yaël Dillies]

Yes, but possibly also the proofs fed to Point.some

[Gareth Ma]

Okay now I'm just confused. I extracted the toFun into a separate definition:

def func (x₀ : ℚ) : liftX x₀ → { y | y ^ 2 - x₀ = 0 } :=
  sorry
/- 'func' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx] -/
#print axioms func

[Gareth Ma]

So just the type definition requires choice?

[Gareth Ma]

Oh hmm the definition of Point also requires it

[Yaël Dillies]

Okay, that is quite strange

[Gareth Ma]

Screenshot-2024-03-04-at-04.22.09.png

[Gareth Ma]

Am I doing something stupid lol

[Yaël Dillies]

Maybe the y ^ 2 is the one requiring choice

[Gareth Ma]

Yes

[Yaël Dillies]

Check instances of the form docs#Rat.monoid

[Gareth Ma]

It seems the split here is the source of most choice usage in Rat. Interesting

[Eric Wieser]

Obligatory link to lean4#2414 which would fix that but is controversial

[Eric Wieser]

I think a PR to Std to remove that use of split would probably be accepted by @Mario Carneiro

[Mario Carneiro]

I would still prefer that split be fixed, because otherwise working around the tactic will produce much worse results overall

[Eric Wieser]

Is this a place where split_ifs would work instead?

[Mario Carneiro]

no, because split_ifs isn't in std

[Eric Wieser]

Are there plans to upstream it? (Edit: std4#243)

[Eric Wieser]

Or is the idea to eliminate it? (Edit: #7891)

[Mario Carneiro]

The obvious counterargument is that it overlaps with split

[Eric Wieser]

Eric Wieser said:

I think a PR to Std to remove that use of split would probably be accepted by Mario Carneiro

I guess I take back this comment with the knowledge about where split_ifs is

[Gareth Ma]

Is there any chance that lean4#2414 will ever be accepted :smiling_face_with_tear: it seems to be stalled since August

[Mario Carneiro]

I am worried that it fell into a bit of a gap in our processes, there isn't any recourse after something like this

[Gareth Ma]

Just to be clear, this is obviously not a thing that affects me practically in any way. I just get confused and slightly annoyed, and I imagine others (say beginners at Lean) might have the same confusion ^_^ hope one day the RFC will be reviewed, even if it’s low priority. I particularly agree with

Just because it's a low priority doesn't mean it should just be closed, that's what you do to things that are unwanted not low priority.

(Applied to the RFC, not the PR)