Sets and boolean reflection

Stream: maths

[Tobias Grosser]

ssreflect has a pattern [pick x in A | P] == Some x (See: http://ssr.msr-inria.inria.fr/doc/ssreflect-1.5/Ssreflect.fintype.html) which is used in a proof that I want to translate from COQ. @Johannes Hölzl already showed me how to model other parts of ssreflect in pure lean. I wonder if there is a canonical way to express this pattern in lean?

[Mario Carneiro]

There is classical.some, although I'm surprised to say there is no option-returning version of this. I guess it hasn't been necessary

[Mario Carneiro]

The usual way we write it is to do if h : \exists x, p x then classical.some h else default _

[Mario Carneiro]

where the branches are usually some more complicated expressions

[Tobias Grosser]

Thank you. Playing with it.

[Tobias Grosser]

This seems to not be as easy as I thought:

set_option class.instance_max_depth 200
def Gaussian_elimination [ordered_ring α] [decidable_eq α]:
   Π (m n), matrix (fin m) (fin n) α  → α
| (x+1) (y+1) A :=
  let S := { x | ¬ ((function.uncurry (A)) x = 0)} in
  if h: ∃ el, el ∈ S
  then
    let el2 := classical.some h in
    let i := el2.fst in
    let j := el2.snd in
    (A i j)
  else
  (A 0 0)
| _ _ A := (0 : α)

[Tobias Grosser]

This gives me an error maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')