unconditional list sum lemma

Stream: lean4

[Joachim Breitner]

Not very deep, and certainly no surprise to most here, but still slightly amusing that this is a lemma for all lists:

import Mathlib
example (xs : List Nat) :
    xs.sum = xs.head! + xs.tail!.sum := by
  cases xs; rfl; simp

[Hanno Becker]

That's because Inhabited Nat picks 0 as the default and panic! uses that in head! []? Morally it feels wrong that this goes through -- should the value underlying panic!not be opaque to proofs? :thinking:

[Joachim Breitner]

It’s just like 0-1=0 – morally wrong, but too useful to not do it this way :-)

[Hanno Becker]

Hm, I'm not sure. I feel one shouldn't be able to prove anything specific about a panic'ing computation -- ideally it wouldn't even have a value, but that seems to be a formal necessity.

I think it would be more natural if panic! would wrap default in a way that can never be unfolded, or at least is not unfolded by standard tactics like the ones you use above?

[Mario Carneiro]

This was the original design (it was an opaque), but this causes problems of its own, for example you can't prove that (l : List A).head?.get! = l.head! and other things like that. (I was the one who lobbied to make it a regular definition.)

[Mario Carneiro]

And there are various cases where you want to panic and still return a well formed result (because you have to return some result and some are worse than others)

[Mario Carneiro]

For example a recent proof I needed to do was that Array.qsort doesn't change the length of the array, which is true even though it can panic in various places

[Mario Carneiro]

If panic! aborted the program, I think this would be slightly more reasonable, but in lean it doesn't, at least not under default settings, so programs have to prepare to handle what happens after a panic

[Hanno Becker]

Thank you for the perspectives, @Mario Carneiro, the example of (l : List A).head?.get! = l.head!is an interesting one. Would this not still be provable even if one used an opaque wrapper? Whatever one chooses, generic equations like x=x will still hold for the 'panic element' (for that reason, the equivalent of the lemma above is true in Isabelle, for example, even though Isabelle's undefined element is indeed opaque)

[Mario Carneiro]

The issue is that there isn't just one "panic element", it is a function which takes e.g. the panic message

[Mario Carneiro]

and the line/col of the occurrence of the panic! macro

[Mario Carneiro]

so one of them would reduce to panic "List.head! []" and the other would reduce to panic "none.get!" or similar

[Hanno Becker]

Got it. So I suppose there are more than two option here: On one extreme, panic itself could be opaque, in which case you can't prove anything about different invocations of panic, unless the arguments are exactly the same. One step more 'transparent' would be to transparently define panic via a one-per-type undefined element (as in Isabelle), but make _that_ element opaque -- then, your lemma would still hold, but e.g. @Joachim Breitner's list lemma wouldn't. And finally, what we have now, is completely transparent, where panic unfolds to default which is transparent for any specific type, so one can prove things about it.

[Mario Carneiro]

Even if you set things up to ignore that, the choice definitely has to depend on the inhabited instance

[Mario Carneiro]

By the way, regarding "tactics shouldn't automatically reduce it", I believe it is currently set to be semireducible, meaning that it won't be unfolded unless the user explicitly asks for it (and it's not like there is a simp lemma that unfolds panic invocations), but rfl counts as "asking for it" in this case

[Hanno Becker]

Ah! That's interesting.

[Mario Carneiro]

we could make it @[irreducible], which would still make it provable but only with more elaborate mechanisms

[Mario Carneiro]

but I'm not sure that would actually help very much, because it would just make the theorems that want to do this unfolding have to write that in a more obtuse way

[Hanno Becker]

Yes, though one could argue that's then by design? Lemmas like Joachim's are only true by accident. For example, xs.prod = xs.head! * xs.tail!.prod would not be true.

I guess it's a trade-off between conceptual clarity and convenience. I personally feel that having an opaque one-per-type 'undefined' element is a good middle-ground, as it means e.g. that equality of potentially-panicking functions means "Panic on the same inputs and are otherwise equal", but that's rather subjective.

[Mario Carneiro]

"by accident" is not quite the right word

[Mario Carneiro]

the choice of Inhabited values is done to maximize the number of such "accidental theorems"

[Mario Carneiro]

and in most cases it is documented to have a given value, sometimes called the "zero value" in other programming languages

[Hanno Becker]

Yes, though one would rather have a separate type class for that? (Zero or similar)

[Mario Carneiro]

All of the same properties you are describing hold if you replace head! and tail! with headI and tailI, or headD default and tailD default

[Mario Carneiro]

At least currently, this is what Inhabited means, it is a designated canonical element

[Mario Carneiro]

Nonempty is closer to being the class for "inhabited but no canonical element"

[Hanno Becker]

Ah, I wasn't aware of Nonempty.

Thanks Mario for your thoughts :pray:

[Mario Carneiro]

Zero already exists in mathlib for algebraic zero

[Mario Carneiro]

these types of course aren't always equipped with an algebraic structure such that default acts like a zero

[Hanno Becker]

One caveat of the current approach is that when code-extracting to a language which has a native panic, it would be nice if at least the presence/absence of panics [in the extracted code] would be preserved under function equality [before extraction]. But that's not the case, as e.g. Joachim's example shows. However, it is impossible to avoid this entirely without adding a separate language construct for panic! (e.g. how would one distinguish the identity function on the unit type from a panic! -- those will always be provably equal no matter whether panic is opaque or not); Isabelle suffers from this, too, though not 'as much' since undefined is opaque, so you wouldn't be able to prove e.g. Joachim's lemma.

[Joachim Breitner]

Isabelle also has 0 - 1 = 0, and not 0 - 1 = undefined. It's a trade off between “some lemmas are more convenient because they don't need extra preconditions” and “bad inputs should lead to unprovable goals as much as possible”. As long as nobody assumes that “verified lean code doesn't panic” or “verified lean code terminates” it doesn't matter much either way, I'd say.

[Mario Carneiro]

note that making panic opaque does not ensure the property "verified lean code doesn't panic" either. The best way to ensure that errors don't occur in lean code is to use Option or Expect so that the presence of the error is expressible in the type system

[Hanno Becker]

Agreed (and fwiw, I don't want 0-1=undefined :-) )