## 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