Getting values from an existential with a "let"

Stream: lean4

[Mark Wilhelm]

Is this the right syntax for breaking out the sub-parts of the existential?

def fn (h: ∃ n: Nat, n + 1 = 2) : Nat :=
  let ⟨a, b⟩ := h
  123

it gives an error:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
motive : (∃ n, n + 1 = 2) → Sort ?u.1347
h_1 : (a : Nat) → a + 1 = 2 → motive (_ : ∃ n, n + 1 = 2)
h✝ : ∃ n, n + 1 = 2
⊢ motive h✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

[Ruben Van de Velde]

Not in a def

[Ruben Van de Velde]

That would allow you to extract a witness, which would cause trouble

[Mark Wilhelm]

hm ok, so you can only do that in tactics then or something?

[Ruben Van de Velde]

You could do it in a theorem

[Mark Wilhelm]

ah ok that is what i need here, theorem instead of function, thank you

[Kevin Buzzard]

You can use classical.some but then your definition would be noncomputable

[Eric Wieser]

Note that the error you get is recursor 'Exists.casesOn' can only eliminate into Prop; your syntax is totally fine, but the type theory says "you can't produce data (aka not Prop) by taking apart an Exists".

[Locria Cyber]

I think you want Subtype

[Jeremy Tan]

@Eric Wieser I'm getting the same error when trying to follow @Oliver Nash's suggestion of moving #6648 to GroupTheory.OrderOfElement. But in defining the inverse I really need the n from the ((isOfFinOrder_iff_pow_eq_one x).1 hx) : ∃ n, 0 < n ∧ x ^ n = 1. Is there a way I can preserve computability?

abbrev IsOfFinOrder.groupPowers (hx : IsOfFinOrder x) : Group (Submonoid.powers x) where
  inv z := by
    obtain ⟨n, _⟩ := ((isOfFinOrder_iff_pow_eq_one x).1 hx)
    exact z ^ (n - 1)
  ...

[Oliver Nash]

@Jeremy Tan don't worry about computability, we're doing classical maths. E.g., use Classical.choose if you need it.

[Jeremy Tan]

But then I'm getting another headache.

open Submonoid in
/-- The submonoid generated by an element is a group if that element has finite order. -/
noncomputable abbrev IsOfFinOrder.groupPowers (hx : IsOfFinOrder x) : Group (powers x) where
  inv z := z ^ (((isOfFinOrder_iff_pow_eq_one x).1 hx).choose - 1)
  mul_left_inv y := Subtype.ext <| by
    obtain ⟨_, k, rfl⟩ := y
    simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]
    -- here
    rw [← _root_.pow_succ', Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]

The goal state at the comment is

G: Type u_1
H: Type u_2
A: Type u_3
α: Type u_4
β: Type u_5
inst✝¹: Monoid G
inst✝: AddMonoid A
xy: G
ab: A
nm: ℕ
hx: IsOfFinOrder x
k: ℕ
⊢ (x ^ k) ^ (Exists.choose (_ : ∃ n, 0 < n ∧ x ^ n = 1) - 1) * x ^ k = 1

I want to ensure that the noncomputably-chosen n in the inv field is the same as the result of the Exists.choose in this goal. How would that go?

[Jeremy Tan]

@Oliver Nash I'm really feeling that even with classical logic porting the abbrev to GroupTheory.OrderOfElement is simply impossible

[Mario Carneiro]

Don't use obtain, just apply Exists.choose and Exists.choose_spec directly

[Mario Carneiro]

actually maybe it's fine, but you are missing ((isOfFinOrder_iff_pow_eq_one x).1 hx).choose_spec in the proof

[Mario Carneiro]

I want to ensure that the noncomputably-chosen n in the inv field is the same as the result of the Exists.choose in this goal. How would that go?

This sentence is a bit confusing to me because the noncomputably-chosen n in the inv field is the Exists.choose in that goal

[Mario Carneiro]

I would be inclined to revert this definition to the original version, with

abbrev groupOfPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (powers x) where

and then define

noncomputable abbrev IsOfFinOrder.groupPowers (hx : IsOfFinOrder x) : Group (powers x) where

by using choose to select the n and then call the other function

[Mario Carneiro]

because different witnesses yield different groups, at least as defined here

[Jeremy Tan]

@Mario Carneiro I managed to complete the move anyway

[Jeremy Tan]

It looks a bit uglier with all the choose_specs though

[Eric Wieser]

Oliver Nash said:

Jeremy Tan don't worry about computability, we're doing classical maths. E.g., use Classical.choose if you need it.

I don't agree with this. Since it costs almost nothing, I think we should split this into two definitions:

• A computable one that takes n explicitly
• A non-computable one that takes IsOfFinOrder x

[Eric Wieser]

The former is pretty much just a subexpression of the latter

[Oliver Nash]

I have no objection to making this split, though of course I stand by my original remark :-)

[Eric Wieser]

Oh, I now see Mario made exactly the same comment as me

[Jeremy Tan]

@Eric Wieser I responded to your comment about the abstruseness of the computable abbrev