Zulip Chat Archive

Stream: maths

Topic: Sets and boolean reflection


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 _

view this post on Zulip Mario Carneiro (Sep 19 2018 at 18:34):

where the branches are usually some more complicated expressions

view this post on Zulip Tobias Grosser (Sep 19 2018 at 18:56):

Thank you. Playing with it.

view this post on Zulip 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 : α)

view this post on Zulip 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