Minimal relation satisfying `trans_gen`

Stream: Is there code for X?

[Patrick Johnson]

While working on improving and generalizing definitions in the formalization of the angel problem, I spent too much time wrestling with this lemma:

import logic.relation
import set_theory.cardinal
open relation
open_locale cardinal

example {α : Type*} {R : α → set α} {t : α} :
  ∃ (r : α → set α), ∀ x,
  (r x ⊆ R x) ∧
  (# (r x) = min (# (R x)) 1) ∧
  (trans_gen R x t → trans_gen r x t) :=
begin
  sorry
end

What is the easiest way to prove it? I tried several different approaches, but haven't finished any of them, because things start to get complicated.

Here is an informal proof (I just don't know what's the easiest way to translate it to Lean): We explicitly construct relation r. Given some (x : α). If R x is empty, then r x is empty too. Otherwise, if trans_gen R x t is false, then return the singleton containing some element of R x (using the axiom of choice). If trans_gen R x t is true, it must be constructed using trans_gen.tail, which takes some (y : α) and proofs of trans_gen R x y and R y t. Return the singleton containing that y (we can't obtain y directly, because of proof irrelevance, but it exists, so we can use the axiom of choice).

It turns out that the problem is t being fixed, so we can't easily prove that transitivity works for some other t.

My attempt

import tactic
import data.set
import set_theory.cardinal
import logic.relation

open set
open cardinal
open relation

noncomputable theory
open_locale classical
open_locale cardinal

variables {α : Type*}

lemma trans_gen_flip' {R : α → set α} {x t : α}
  (h : trans_gen R x t) :
  trans_gen (λ a b, R b a) t x :=
begin
  induction h with _ h y y₁ h₁ h₂ ih,
  {
    left,
    exact h,
  },
  {
    fapply trans_gen.trans,
    { exact y, },
    {
      left,
      exact h₂,
    },
    {
      exact ih,
    },
  },
end

lemma trans_gen_flip {R : α → set α} {x t : α} :
  trans_gen R x t = trans_gen (λ a b, R b a) t x :=
begin
  ext, split; exact trans_gen_flip',
end

def mk_r (R : α → set α) (t : α) (x : α) : set α :=
begin
  refine if h₁ : ∃ y, R x y then _ else ∅,
  refine if h₂ : trans_gen R x t then _ else {h₁.some},
  refine if h₃ : R x t then {t} else _,
  refine {(_ : ∃ y, R x y ∧ trans_gen R y t).some},
  revert h₃,
  apply trans_gen.trans_induction_on h₂; clear h₁ h₂ x t,
  { rintro x y h₁ h₂, contradiction, },
  { rintro x y z h₁ h₂ h₃ h₄ h₅, by_cases h₆ : R x y,
    { refine ⟨_, h₆, h₂⟩ },
    replace h₃ := h₃ h₆, clear h₆, cases h₃ with c₁ hc₁,
    refine ⟨_, hc₁.1, _⟩, transitivity y,
    { exact hc₁.2, },
    { exact h₂, }},
end

lemma R_of_r {R : α → set α} {x t : α}
  (h : trans_gen (mk_r R t) x t) :
  trans_gen R x t :=
begin
  rw trans_gen_flip at h ⊢,
  induction h with y h y y₁ h₁ h₂ ih,
  {
    rw mk_r at h,
    split_ifs at h with h₁ h₂ h₃,
    {
      left,
      exact h₃,
    },
    {
      revert h,
      generalize_proofs h₄,
      intro h,
      change t = _ at h,
      rw h at h₃,
      exact (h₃ h₄.some_spec.1).elim,
    },
    {
      change t = _ at h,
      subst h,
      left,
      exact h₁.some_spec,
    },
    {
      cases h,
    },
  },
  {
    transitivity y,
    { exact ih, },
    {
      rw mk_r at h₂,
      rw trans_gen_flip at h₁ ih ⊢,
      dsimp at h₁ ih ⊢,
      split_ifs at h₂ with h₃ h₄ h₅,
      {
        change y = t at h₂,
        subst h₂,
        left,
        exact h₅,
      },
      {
        revert h₂,
        generalize_proofs h₆,
        intro h₂,
        change y = _ at h₂,
        rw h₂,
        left,
        exact h₆.some_spec.1,
      },
      {
        change y = _ at h₂,
        rw h₂,
        left,
        exact h₃.some_spec,
      },
      {
        cases h₂,
      },
    },
  },
end

lemma r_single {R : α → set α} {x t : α}
  (h : R x t) :
  trans_gen (mk_r R t) x t :=
begin
  apply trans_gen.single,
  rw mk_r,
  split_ifs with h₁ h₂,
  {
    exact rfl,
  },
  {
    refine (h₂ (trans_gen.single _)).elim,
    exact h,
  },
  {
    push_neg at h₁,
    exact (h₁ _ h).elim,
  },
end

example {R : α → set α} {t : α} :
  ∃ (r : α → set α), ∀ x,
  (r x ⊆ R x) ∧
  (# (r x) = min (# (R x)) 1) ∧
  (trans_gen R x t → trans_gen r x t) :=
begin
  use mk_r R t,
  intro x,
  refine ⟨_, _, _⟩,
  {
    change ∀ y, mk_r R t x y → R x y,
    rintro y h,
    rw mk_r at h,
    split_ifs at h with h₁ h₂ h₃,
    {
      change y = t at h,
      subst h,
      exact h₃,
    },
    {
      change y = _ at h,
      subst y,
      generalize_proofs h₄,
      exact h₄.some_spec.1,
    },
    {
      change y = _ at h,
      subst h,
      exact h₁.some_spec,
    },
    {
      exact false.elim h,
    },
  },
  {
    by_cases h : R x = ∅,
    {
      simp [h],
      rw mk_emptyc_iff,
      rw mk_r,
      split_ifs with h₁ h₂ h₃,
      {
        rw h at h₃,
        exact false.elim h₃,
      },
      {
        rw h at h₁,
        exact false.elim h₁.some_spec,
      },
      {
        rw h at h₁,
        exact false.elim h₁.some_spec,
      },
      {
        refl,
      },
    },
    {
      have h₁ : 1 ≤ # (R x),
      {
        sorry
      },
      replace h₁ : min (# (R x)) 1 = 1,
      {
        simp [h₁],
      },
      simp [h₁], clear h₁,
      rw cardinal.eq_one_iff_unique,
      simp,
      rw mk_r,
      split_ifs with h₁ h₂ h₃,
      {
        simp,
      },
      {
        simp,
      },
      {
        simp,
      },
      {
        rw eq_empty_iff_forall_not_mem at h,
        push_neg at h h₁,
        exact (h₁ _ h.some_spec).elim,
      },
    },
  },
  {
    intro h,
    apply trans_gen.head_induction_on h; clear h x,
    {
      rintro x h,
      exact r_single h,
    },
    {
      sorry
    },
  },
end

[Eric Wieser]

You should either change r to α → α → Prop and replace r x with {y | r x y}, or replace trans_gen r with trans_gen (λ x y, y ∈ r x), else you'll end up with a nonsense goal along the way

[Patrick Johnson]

Sure, I'll polish the proof in the end. But I somehow managed to establish a mental model to literally see y ∈ r x as r x y, or {x} y as y = x, or ∅ x as false. :upside_down:

[David Wärn]

This is basically docs#quiver.geodesic_arborescence. It shows that in a directed graph where there is a path from r to any other vertex, there is a subgraph where there is a unique path from r to every other vertex. Of course there is a wrinkle in that your lemma doesn't assume that there are paths to t...

[David Wärn]

BTW I don't think your proof sketch will work. For example suppose α is with_top nat, R is <, and t is top. If you're unlucky, the axiom of choice will pick r n = {n+1}. Then trans_gen r n top is always false: if you follow the path from n in r you will just go n -> n+1 -> n+2 ... forever. This issue is basically the reason to use the 'geodesic' subgraph. I see that you use a different choice of r in the code above, which will work on this counterexample, but you can construct another counterexample where it doesn't work by adding one more top' which is related to top but not to n : nat.

[Patrick Johnson]

Thanks. I'll play with geodesic subgraph and see how it goes.

[Patrick Johnson]

As a side question, how to finish this subgoal?

example {α : Type*} {S : set α}
  (h : ¬S = ∅) :
  1 ≤ # S :=
begin
  sorry
end

[Patrick Johnson]

I have this proof, but it looks very ugly. I hope there is a better way:

example {α : Type*} {S : set α}
  (h : ¬S = ∅) :
  1 ≤ # S :=
begin
  rw set.eq_empty_iff_forall_not_mem at h,
  push_neg at h,
  cases h with x h,
  fsplit, fsplit,
  { intro u, exact ⟨x, h⟩ },
  { rintro a b h₁, cases h₁, simp, },
end

[Yaël Dillies]

Looks like you should switch over to finset and use docs#finset.one_le_card_iff

[Stuart Presnell]

Does docs#cardinal.one_le_iff_ne_zero help?

[Reid Barton]

and docs#cardinal.mk_ne_zero_iff

[Ruben Van de Velde]

import logic.relation
import set_theory.cardinal

open_locale cardinal

example {α : Type*} {S : set α}
  (h : ¬S = ∅) :
  1 ≤ # S :=
begin
  suffices : # S ≠ 0,
  { -- library_search
    refine cardinal.one_le_iff_ne_zero.mpr this },
  contrapose! h,
  -- library_search
  refine cardinal.mk_emptyc_iff.mp h,
end

[Stuart Presnell]

Or, condensing it further:

import logic.relation
import set_theory.cardinal

open_locale cardinal

example {α : Type*} {S : set α}
  (h : ¬S = ∅) :
  1 ≤ # S :=
cardinal.one_le_iff_ne_zero.mpr (mt cardinal.mk_emptyc_iff.mp h)

[Patrick Johnson]

It's interesting how the "side question" turns out to be so bikesheddy. But thanks, those proofs are definitely shorter than mine.