How to use structures?

Stream: new members

[Antoine Chambert-Loir]

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 :=
begin
  sorry, -- refl does not work
end

[Jakub Kądziołka]

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]

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]

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]

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]

@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]

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

[Damiano Testa]

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]

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]

The linter will complain that the lemma should be a definition

[Damiano Testa]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Kevin Buzzard]

The delta tactic will unfold irreducible definitions

[Damiano Testa]

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 :=
begin
  delta struc_mk,
  refl,
end

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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]

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]

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