Beginner questions (match expression)

Stream: lean4

[Tom]

Hi everyone,

Is there a syntax to match a structure field to a specific value? Seems it's possible with pairs but I've been looking through the Lean 4 manual (as well as GH) and can't find any documentation about the syntax (other than reading the compiler code itself, I guess; I realize I could match on the field itself if it's not supported)

E.g. using the Point example from the "Functional Programming in Lean" book, I'd like to do:

match point with
   | { x := 0, y := a } => /- Do something with points on this vertical line -/

Second, is there a way to bind a (sub)match to a name, e.g. like

match xs with
 | y1 :: (y2 :: ys) /- as sublist -/ => /- use sublist -]

Thanks very much!

[Mario Carneiro]

That syntax should be legal already

[Mario Carneiro]

you will need to provide another match arm for the case where x is not zero of course

[Mario Carneiro]

the syntax in the second case is

match xs with
 | y1 :: sublist@(y2 :: ys) => /- use sublist -/

[Mario Carneiro]

assuming you wanted to bind y2 :: ys to a variable sublist

[Mario Carneiro]

(you already have a name for y1 :: (y2 :: ys), that's xs)

[Tom]

Great, thanks! The naming syntax works but when I try the following:

def test: Point -> Bool
  | { x := 0.0, y := a } => true
  | _ => false

I see the following error:

dependent elimination failed, type mismatch when solving alternative with type
  motive { x := Float.ofScientific 0 true 1, y := y✝ }
but expected
  motive { x := x✝, y := y✝ }

I can't quite understand what I'm being told.

[Sebastian Ullrich]

@Tom I think this is a specific problem with Floats

[Tom]

@Sebastian Ullrich Thank you for the response, I can confirm that when I change the fields to be Nats, the match works.
Is the Float behavior intentional or an omission?

[Henrik Böving]

Most likely an omission I think

[Kyle Miller]

Floats are fairly special compared to nats (see the definition of Float). It's an opaque type. The function Float.ofScientific isn't something you can pattern match on either.

[Kyle Miller]

The general wisdom with IEEE floating point is that you shouldn't do equality tests unless you know what you're doing -- do you need to check whether a field of Point is precisely zero?

[Reid Barton]

Do you also want to match negative zero?

[Reid Barton]

I imagine you don't really care, but this is one example of how this is subtle

[Tom]

@Kyle Miller Thanks for the feedback! I did wonder if this was a language design decision because of precision issues (hence my follow up question about it being a deliberate omission; I am fairly familiar with IEEE and floating point arithmetic).

@Reid Barton As for the negative zero question, it's a good one but I would expect that pattern match to be the same as equality, and hence (as per IEEE), 0.0 would match both a positive and a negative zero (even though I suppose I've never considered the design implications of that decision from the POV of a theorem prover!)

In any case, the question, in-and-of-itself, is not really about IEEE semantics. I am in the process of going through the Lean documentation and trying to learn the language and was surprised that a very early example I wrote didn't work. Sometimes as a learner it's hard to know why something is not working, so I'm trying to dig into it. I appreciate the discussion/feedback!

[Mac]

Tom said:

I am in the process of going through the Lean documentation and trying to learn the language and was surprised that a very early example I wrote didn't work.

This is very good piece of feedback for the book!

@David Thrane Christiansen, it might be better to use a constructive Scientific for the floating point examples, rather than deal with ugliness of IEEE. For example:

structure Scientific where
  mantissa : Nat
  sign : Bool
  exponent : Nat

instance : OfScientific Scientific := ⟨Scientific.mk⟩

structure SPoint where
  x : Scientific
  y : Scientific

def origin : SPoint := { x := 0.0, y := 0.0 }

-- Pattern matching now works as a beginner would expect
def test: SPoint -> Bool
  | { x := 0.0, y := a } => true
  | _ => false

To make learning easier, it would probably be best if such a constructive Scientific was in core with the usual features (arithmetic, rounding, etc.) so that people can easily follow along with the book. What do you think, @Leonardo de Moura ?

[David Thrane Christiansen]

As the language is right now, I'm not so sure that this would really make things easier at that stage of the book, because there's so much in what you've written here that would be beyond any readers. But language changes could make that make sense, for sure.

[Mac]

@David Thrane Christiansen , I agree that providing the Scientific up front would be confusing (except maybe if it was in a supplementary library that was meant to used along with the book). I was curious as to whether you thought, for pedagogical purposes, the existence and use of such a Scientific (e.g., in core) would be beneficial to readers (as opposed to the current use of Float).

[David Thrane Christiansen]

IEEE floats are actually tricky to get right in a dependent type system. If you take the definitional equality at type Float to be IEEE, then you can prove false by rewriting with predicate (fun x => if 1/x < 0 then True else False) along the reflexivity proof that -0.0 = +0.0. So the definitional equality needs to be bit-pattern equality of the underlying Float, which makes arithmetic funky.

[David Thrane Christiansen]

(in particular, the Boolean equality ends up not matching the decidable equality, or else the Boolean equality doesn't match IEEE)

[David Thrane Christiansen]

I don't have a full enough picture of the ergonomics of that Scientific type to say for sure how it would work for new users. I would worry about issues with multiple representations of the same number (e.g. 0.0e10 vs 0.0e1, or 0.0 vs -0.0). Would there be a quotient on top of that? How painful would proofs be?

[Mac]

David Thrane Christiansen said:

(in particular, the Boolean equality ends up not matching the decidable equality, or else the Boolean equality doesn't match IEEE)

i Very true, which is why the Float code in core is mostly opaque definitions (and thus not very fun for beginners to read).

[Gabriel Ebner]

Arithmetic is always funky with floating pointing numbers, having 0 ≠ -0 doesn't make it any worse. Definitional equality should definitely be bit-pattern equality, and == as well. In my opinion IEEE equality is a historical accident and it's not worth giving up reflexivity and transitivity for it.

[Mac]

David Thrane Christiansen said:

I would worry about issues with multiple representations of the same number (e.g. 0.0e10 vs 0.0e1, or 0.0 vs -0.0). Would there be a quotient on top of that? How painful would proofs be?

Yeah, this is a concern. There may be a better, more properly constructive definition of Scientific that avoids these multiple representations. On the other hand, the multiple representations of my very basic Scientific could be a good opportunity to demonstrate that a pattern match of 0e1 is not equivalent to a pattern match of 0e4 and help motivate why more complex representations are needed (deeper in the the book for proofs and such).

[David Thrane Christiansen]

I think that this gets waaaaay too deep in the weeds for most beginners. A different kind of book aimed at intermediate users of dependent-type-based proof systems could very productively include a big exploration of these topics, and that would be useful. But the target audience of this book is programmers who have never studied formal proof nor functional programming, and I think that other things are more useful at this stage.

The book is trying to be honest about difficulties, e.g. by presenting confusing error messages in prominent positions and explaining how to work around them. The difficulties here should at least be reasonably familiar to those who have worked with IEEE floats in other languages, and most undergrad CS curricula have at least a little warning about exact equality comparisons. I think I'd rather explain the difficulties in terms of things they know, rather than define new things that are also difficult, and then move on.

[David Thrane Christiansen]

If I want to get into the weeds of number representations, which might make sense at some point, then Int is tricky enough :-)

[Kyle Miller]

I didn't realize Scheme takes a hard-line "0 is not equal to -0". Here's mit-scheme:

1 ]=> (eq? -0.0 0.0)

;Value: #f

1 ]=> (eqv? -0.0 0.0)

;Value: #f

1 ]=> (equal? -0.0 0.0)

;Value: #f

Scheme has multiple notions of equality, and these are in the order of increasing courseness. If equal? had returned #t I would have suggested that Lean include a special equality operator for "value equals" of floats rather than the Eq "representation equals" (i.e., use something like a setoid rather than a full quotient).

[Kyle Miller]

Ah, there it is, it does have an IEEE floating point equality:

1 ]=> (flo:= -0.0 0.0)

;Value: #t

[Mac]

Gabriel Ebner said:

In my opinion IEEE equality is a historical accident and it's not worth giving up reflexivity and transitivity for it.

As an aside, I personally love the oddities of IEEE equality because it provides a nice practical motivational example for non-reflexive equality in discussions on alternative logics. :laughter_tears: However, since you are much more of a mathematician than me, I can definitely see why you would not be of the same opinion.

[Tom]

Maybe we should implement Unum/Posits instead. They don't have the multiple zero problem:

https://en.wikipedia.org/wiki/Unum_(number_format)#:~:text=Unums%20(universal%20numbers)%20are%20a,Gustafson.

:smile:

[Mario Carneiro]

Unless you are doing a hardware implementation or proving properties of one, there is no point to formalize any kind of floating point, be it IEEE or posits. Rational numbers or dyadic rationals are infinitely better behaved. So while I can understand modeling IEEE because you have a chip that does it, posits are just a curiosity and seem like a waste of time unless you are trying to petition the powers that be with a proof, and I'm not even sure which powers that be would even care about that

[Tomas Skrivan]

If I understand match correctly, it matches only on constructors. It does not use equality at all. Thus it can work only for inductive or structure types. Float is an opaque type, therefore it does not have constructors and you can't match on it. (I just skimmed the thread, but failed to find this explanation)

[Locria Cyber]

IEEE floating point should not be used in proofs
See https://github.com/idris-lang/Idris2/issues/601

[Locria Cyber]

I think there are flags in C you can change to change the behavior of overflow/division/inexact

[Locria Cyber]

Rational numbers is probably enough

[Tom]

@Mario Carneiro My quip about the posits was said in jest, sorry for any confusion.

[Tom]

@Locria Cyber Please note that the original question was posted in the context of just writing a "regular function" which I was trying to make with the match expression.
If Lean is used as a better/general purpose FP language, I think this functionality may be surprising to people not involved in theorem proving. So while I 100% agree with your statement that "IEEE should not be used in proofs", I don't quite know if it'll be easy to accept by the more the general Software Eng community. :shrug:

[Locria Cyber]

match is not "switch statement"

[Locria Cyber]

you probably need something like cond in scheme?