# Zulip Chat Archive

## Stream: maths

### Topic: Sets and boolean reflection

#### Tobias Grosser (Sep 19 2018 at 18:18):

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 (Sep 19 2018 at 18:33):

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 (Sep 19 2018 at 18:34):

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

#### Mario Carneiro (Sep 19 2018 at 18:34):

where the branches are usually some more complicated expressions

#### Tobias Grosser (Sep 19 2018 at 18:56):

Thank you. Playing with it.

#### Tobias Grosser (Sep 19 2018 at 20:02):

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 (Sep 19 2018 at 20:02):

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')`

Last updated: May 10 2021 at 08:14 UTC