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

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

#### 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