from inclusion to belonging

Stream: new members

[Arthur Paulino]

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]

Just apply it (-;

[Johan Commelin]

h _ e

[Kevin Buzzard]

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]

h' _ e or similar

[Arthur Paulino]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

yeah, those are the same thing

[Kevin Buzzard]

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]

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]

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]

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]

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]

Showing the types of things will also help

[Arthur Paulino]

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]

Your goal isn't a Prop

[Kevin Buzzard]

So something odd is happening. You can specialize h' v probably, and then specialize h' e.2 after that

[Kevin Buzzard]

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

[Mario Carneiro]

exact \<_, h' _ e.2\> should work

[Mario Carneiro]

assuming that you want to prove that e.1 is the element in the set

[Arthur Paulino]

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]

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]

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]

errors in files have weird and unintended consequences

[Arthur Paulino]

branch updated. Kyle did what Mario proposed: exact ⟨_, e.property.1⟩
but I was trying to do it differently

[Arthur Paulino]

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]

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, ...