Zulip Chat Archive

Stream: new members

Topic: How to use structures?

Antoine Chambert-Loir (Mar 06 2022 at 00:01):

This is in relation with PR #12459 where I define a finpartition from setoid.is_partition.
For future work, I need to access the parts field of the created finpartition. But I can't even manage to have Lean prove that it equals its value.

Here is a MWE that shows my inability to understand these stuff:

import tactic

structure struc : Type :=
(fst : )
(snd : )
(le : fst  snd )

lemma struc_mk (a b : ) (hab : a  b) : struc :=
{ fst := a,
  snd := b,
  le := hab }

lemma test_fst (a b : ) (hab : a  b): (struc_mk a b hab).fst = a :=
  sorry, -- refl does not work

Jakub Kądziołka (Mar 06 2022 at 00:06):

This is because you used lemma to define struc_mk, which means the actual contents gets hidden, and only its type is available. I think this is for efficiency reasons. refl works if you use def struc_mk instead.

Damiano Testa (Mar 06 2022 at 07:10):

To expand on what Jakub says, proof-irrelevance implies that struct_mk does not remember how you defined the structure. It just knows that you can construct a struct from the given data.

In your structure, struct carries information (called often data) in its first two fields, and a prop in the le field. You should always keep an eye out for making sure that the data fields are not "swallowed up'" inside a proof.

As a mathematician, I had no explicit distinction in my head between data and props before using Lean.

Damiano Testa (Mar 06 2022 at 08:28):

To maybe drive better the point across, you could also prove struct_mk as follows (untested)

lemma struc_mk (a b : ) (hab : a  b) : struc :=
{ fst := 0,
  snd := 0,
  le := rfl.le }

Both proofs are equivalent and you should therefore not be able to get what you want out of them!

Antoine Chambert-Loir (Mar 06 2022 at 10:20):

Thank you! I understand better now. (As a mathematician, I have been taught to write maths so as never using something that is explained within a '\begin{proof}… \end{proof}', which is Bourbaki's proof irrelevance. While this is a good writing principle, which forces the writer to write down explicitly what they mean, and helps the reader tracking down what happened, usual mathematical practice has slightly stepped aside from this.)

Eric Wieser (Mar 06 2022 at 14:14):

@Damiano Testa, proof irrelevance does not imply what is happening here: lemma works the way it does because it assumes you're going to use it with Prop (as proof irrelevance makes it safe to do so), but it is not the mechanism of proof irrelevance itself

Eric Wieser (Mar 06 2022 at 14:15):

Also worth noting that #lint will detect this mistake for you

Damiano Testa (Mar 06 2022 at 14:32):

I wonder whether I misspoke or I am misunderstanding something. What I meant is that, once the proof is complete, Lean "forgets" the actual details of the constructed struct in the lemma and only lets you use the information that having an a and a b in with a ≤ b is sufficient to construct some struct.

Is this correct?

Damiano Testa (Mar 06 2022 at 14:33):

As for linting, you could produce a struct with fst := a+1 and snd := b+1 and a correct proof of le and the linter would be happy.

Kevin Buzzard (Mar 06 2022 at 14:45):

The linter will complain that the lemma should be a definition

Damiano Testa (Mar 06 2022 at 14:52):

I was worried about the unused arguments and forgot about the lemma/def linter!

Mario Carneiro (Mar 06 2022 at 15:06):

@Damiano Testa No, it is not true that lean "forgets" the contents of a lemma

Mario Carneiro (Mar 06 2022 at 15:07):

and the data being proof relevant is a function only of the type, not whether it is marked as lemma or def

Mario Carneiro (Mar 06 2022 at 15:08):

lemma is just a variation on @[irreducible] def which discourages unfolding from all but the most persistent tactics

Damiano Testa (Mar 06 2022 at 15:15):

Ok, thanks for the corrections! I did not know that you could "recover" data from a lemma, at least in some cases.

Kevin Buzzard (Mar 06 2022 at 15:19):

The delta tactic will unfold irreducible definitions

Damiano Testa (Mar 06 2022 at 15:21):

This is very interesting, thanks!

Indeed, what is below works!

lemma test_fst (a b : ) (hab : a  b): (struc_mk a b hab).fst = a :=
  delta struc_mk,

Damiano Testa (Mar 06 2022 at 15:27):

I had a mistaken idea of that proof-irrelevance means.

Damiano Testa (Mar 06 2022 at 15:31):

Just to repeat something that has been said before: in this case, you can recover the data, since the lemma is constructing a term in Type, not a term in Prop, right? This is how the lemma/def linter knows to complain, also.

Mario Carneiro (Mar 06 2022 at 15:32):

the lemma/def linter is just looking at the type, not the value. But yes, you can unfold the definition and prove that your definition of struc_mk is not equal to antoine's, for example. From the kernel's perspective there is no difference between def and lemma

Mario Carneiro (Mar 06 2022 at 15:34):

If you instead used

structure struc : Prop :=
(fst : )
(snd : )
(le : fst  snd )

then the two definitions would be equal; but lean won't allow this definition because it will not be able to construct the struc.fst projection function as required by the structure specification

Mario Carneiro (Mar 06 2022 at 15:36):

You can make this type without the projections, as

inductive struc : Prop
| mk (fst : ) (snd : ) (le : fst  snd) : struc

and in this case you can't extract fst and snd (as you would expect) and the two struc_mk definitions are equal (independent of whether they use def or lemma).

Damiano Testa (Mar 06 2022 at 17:04):

Ok, thanks! This discussion has been very enlightening and cleared up some doubts that I did not even know that I had!

Last updated: Dec 20 2023 at 11:08 UTC