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