# Zulip Chat Archive

## Stream: new members

### Topic: from inclusion to belonging

#### Arthur Paulino (Oct 27 2021 at 15:49):

If I have `e: ↥(G.incidence_set ↑v)`

and `h': ∀ (v : V), G.incidence_set v ⊆ G.edge_set`

, how do I use `h'`

to prove that `e`

belongs to `G.edge_set`

?

#### Johan Commelin (Oct 27 2021 at 15:54):

Just apply it (-;

#### Johan Commelin (Oct 27 2021 at 15:54):

`h _ e`

#### Kevin Buzzard (Oct 27 2021 at 15:55):

The *definition* of `A ⊆ B`

is `∀ x, x ∈ A → x ∈ B`

, so tactics like `apply`

(which work up to definitional equality) will work.

#### Kevin Buzzard (Oct 27 2021 at 15:56):

`h' _ e`

or similar

#### Arthur Paulino (Oct 27 2021 at 16:03):

```
type mismatch at application
h' ?m_1 e
term
e
has type
↥(G.incidence_set ↑v) : Type u
but is expected to have type
?m_1 ∈ G.incidence_set ?m_2 : Prop
```

Something I've been intending to ask for a while: what are those arrows pointing up (`↥`

and `↑`

)?

#### Bryan Gin-ge Chen (Oct 27 2021 at 16:05):

These are coercion arrows. They are also covered in chapter 10 of TPiL: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes

#### Kevin Buzzard (Oct 27 2021 at 16:07):

Perhaps now is the time to explain this, because that error is a bit more complicated to debug.

#### Kevin Buzzard (Oct 27 2021 at 16:09):

It seems to me that ` G.incidence_set v`

and `G.edge_set`

are probably sets, because of (a) their name and (b) the fact that `G.incidence_set v ⊆ G.edge_set`

typechecks. But Lean uses type theory, not set theory. Everything in Lean is either a universe, a type, or a term -- it exists at one of those three levels. Sets exist at the term level -- they are not types. But you have `e: ↥(G.incidence_set ↑v)`

, so `e`

is a term and its type is `↥(G.incidence_set ↑v)`

, which is the type corresponding to the set `G.incidence_set ↑v`

.

#### Kevin Buzzard (Oct 27 2021 at 16:11):

So strictly speaking your original question does not even make sense: `e`

is a term of the type `↥(G.incidence_set ↑v)`

, and in particular it is not a term of type `sym2 V`

(the set of unordered pairs of elements of V), so `e`

cannot belong to `G.edge_set`

.

#### Kevin Buzzard (Oct 27 2021 at 16:12):

What is going on is that if `X`

is a type (e.g. `sym2 V`

) and if `S : set X`

is a subset of `X`

then there is an associated type `↥S`

, and a term of this type is a *pair* consisting of `x : X`

and a proof `hx : x ∈ S`

.

#### Kevin Buzzard (Oct 27 2021 at 16:13):

So `e`

in your code is this pair; the element itself is called `e.1`

and the proof that it's in the set is called `e.2`

. The error indicates that where you put `e`

Lean was expecting a proof, so I would replace `e`

with `e.2`

.

#### Arthur Paulino (Oct 27 2021 at 16:17):

So that's why I can use `e.val`

and `e.property`

? `.val`

being the same as `.1`

and `.property`

the same as `.2`

?

#### Kevin Buzzard (Oct 27 2021 at 16:17):

yeah, those are the same thing

#### Kevin Buzzard (Oct 27 2021 at 16:18):

e.val is the value (the term of type `sym2 V`

) and `e.property`

is the proof that it's in the set which you're coercing to a type

#### Kevin Buzzard (Oct 27 2021 at 16:20):

The various flavours of arrows indicate when you want to conflate things which Lean thinks are different and which you might want to treat as the same; for example

```
example (a : ℤ) (b : ℕ) : a = b :=
begin
-- ⊢ a = ↑b
sorry
end
```

the arrow means "yeah b is a natural, but we want it to be an integer, so we apply the obvious function from naturals to integers"

#### Kevin Buzzard (Oct 27 2021 at 16:22):

That simple up-arrow is the most common, where terms get moved to terms. The one with the bottom edge is a more drastic one, where terms get moved to types. We see this in your setting because sets are terms because this is type theory not set theory. `set X`

is the type of subsets of `X`

, and `S : set X`

is a term of that type, i.e. a subset of `X`

, but it's not a type itself.

#### Arthur Paulino (Oct 27 2021 at 16:25):

And now, after `apply h' _ e.property,`

it says:

```
invalid apply tactic, failed to unify
↥(G.edge_set)
with
e.val ∈ G.edge_set
```

#### Kevin Buzzard (Oct 27 2021 at 16:25):

yup, I can't unify those either. Are you up to posting some Lean code which I can run at my end yet?

#### Mario Carneiro (Oct 27 2021 at 16:26):

Showing the types of things will also help

#### Arthur Paulino (Oct 27 2021 at 16:27):

This is the complete state description:

```
V: Type u
G: simple_graph V
_inst_1: decidable_eq V
_inst_2: fintype ↥(G.edge_set)
_inst_3: fintype V
_inst_4: nonempty V
h: G.is_tree
root: V
v: ↥{v : V | v ≠ root}
e: ↥(G.incidence_set ↑v) := next_edge ↑v root _ ↑(G.tree_path h ↑v root)
h': ∀ (v : V), G.incidence_set v ⊆ G.edge_set := G.incidence_set_subset
⊢ ↥(G.edge_set)
```

#### Kevin Buzzard (Oct 27 2021 at 16:28):

Your goal isn't a Prop

#### Kevin Buzzard (Oct 27 2021 at 16:30):

So something odd is happening. You can `specialize h' v`

probably, and then `specialize h' e.2`

after that

#### Kevin Buzzard (Oct 27 2021 at 16:30):

but it's much harder to help without having working code running in my own VS Code

#### Mario Carneiro (Oct 27 2021 at 16:30):

`exact \<_, h' _ e.2\>`

should work

#### Mario Carneiro (Oct 27 2021 at 16:31):

assuming that you want to prove that `e.1`

is the element in the set

#### Arthur Paulino (Oct 27 2021 at 16:32):

The code is from that branch I pointed earlier: `more_on_trees`

. I still find it hard to cut the exact pieces of the code and paste only essential things here

#### Kevin Buzzard (Oct 27 2021 at 16:32):

but even when I tried to use that branch I couldn't get it working -- there were errors on a file you were importing

#### Kevin Buzzard (Oct 27 2021 at 16:33):

if you can just push to the branch then I can pull and compile but the last time I tried that the first error was way before the part you were talking about, and I am reluctant to look at code beyond the first error in a file.

#### Kevin Buzzard (Oct 27 2021 at 16:34):

errors in files have weird and unintended consequences

#### Arthur Paulino (Oct 27 2021 at 16:37):

branch updated. Kyle did what Mario proposed: `exact ⟨_, e.property.1⟩`

but I was trying to do it differently

#### Arthur Paulino (Oct 27 2021 at 16:44):

This was my line of thought... please notice that I'm still figuring things out:

When Lean reads `let f : {v | v ≠ root} → G.edge_set`

, it requests that I express how to take an element of `{v | v ≠ root}`

to an element of `G.edge_set`

. And the goal `↥(G.edge_set)`

is how Lean demands it.

Is it what's happening?

#### Kevin Buzzard (Oct 27 2021 at 17:13):

Yes -- if you want to define a function in the middle of a tactic proof it's probably best to do it directly with `λ`

etc: `let f : {v | v ≠ root} → G.edge_set := λ w, ...`

Last updated: Dec 20 2023 at 11:08 UTC