term extraction

Stream: new members

[Arthur Paulino]

How do I turn

h: ∀ (w w' : V), M.adj v w ∧ M.adj v w' → w = w'

into

w: V
w': V
h: M.adj v w ∧ M.adj v w' → w = w'

?

[Kyle Miller]

You can't unless you happen to have two vertices w and w' on hand. If you do have them, you could do specialize h w w'.

[Alex J. Best]

If h is a hypothesis you can't do this, for instance if V was false you'd be able to turn false -> true into a proof of false.

[Arthur Paulino]

Can I use hu: rel.dom M.adj = set.univ to make this possible?

[Ruben Van de Velde]

Can you share a #mwe ?

[Arthur Paulino]

Sure

import combinatorics.simple_graph.subgraph


open finset
universe u

namespace simple_graph
variables {V : Type u} {G : simple_graph V} (M : subgraph G)

def is_matching : Prop := ∀ (v w w': V), M.adj v w ∧ M.adj v w' → w = w'

def is_perfect : Prop := is_matching M ∧ M.support = set.univ

lemma is_perfect_iff :
  is_perfect M ↔ ∀ (v : V), ∃! (w : V), M.adj v w :=
begin
  simp only [is_matching, is_perfect, subgraph.support, exists_unique],
  split,
  { intros h v,
    cases h with h hu,
    specialize h v,
    sorry,},
  { intro h,
    split,
    { intros v w w' hv,
      specialize h v,
      cases hv with hw hw',
      cases h with x h,
      cases h with _ hy,
      have hxw := hy w hw,
      have hxw' := hy w' hw',
      simp [hxw, hxw'], },
    { sorry, }, },
end

end simple_graph

I'm trying to clear that first sorry

[Arthur Paulino]

Both h and hu that I mentioned will be available after the line specialize h v, (right before sorry)

[Kyle Miller]

Did you define subgraph.support?

[Kyle Miller]

I'm guessing it's this (for M : G.subgraph):

def subgraph.support : set V := rel.dom M.adj

lemma subgraph.mem_support {v : V} : v ∈ M.support ↔ ∃ w, M.adj v w := iff.rfl

In that case, here's the first sorry:

lemma is_perfect_iff :
  is_perfect M ↔ ∀ (v : V), ∃! (w : V), M.adj v w :=
begin
  simp only [is_matching, is_perfect, exists_unique],
  split,
  { intros h v,
    cases h with h hu,
    have hu' := set.mem_univ v,
    rw [←hu, subgraph.mem_support] at hu',
    cases hu' with w hw,
    use [w, hw],
    intros u hu,
    exact h _ _ _ ⟨hu, hw⟩, },
  { sorry },
end

[Kyle Miller]

and I would suggest this for is_matching:

def is_matching : Prop := ∀ {v w w': V}, M.adj v w → M.adj v w' → w = w'