Zulip Chat Archive

Stream: new members

Topic: Proof Over Inductive Prop


view this post on Zulip Marcus Rossel (Jan 14 2021 at 17:04):

I can't figure out how to handle the following inductive proposition in a proof.
Sorry for not having a MWE - I hope the code is understandable anyway:

inductive has_path_from_to (g : digraph ι) : ι  ι  Prop
  | direct {i i' : ι} : (g.has_edge_from_to i i')  has_path_from_to i i'
  | composite {i i' : ι} (iₘ : ι) : has_path_from_to i iₘ  has_path_from_to iₘ i'  has_path_from_to i i'

I'm trying to prove:

lemma edges_inv_path_inv {g g' : digraph ι} {i i' : ι} (h : g.edges = g'.edges) :
  (g.has_path_from_to i i')  (g'.has_path_from_to i i')
  | (has_path_from_to.direct p) := begin
      rw [has_edge_from_to, h] at p,
      exact has_path_from_to.direct p
    end
  | (has_path_from_to.composite iₘ p_α p_ω) := begin
      sorry -- ?
    end

The goal state at the sorry is:

ι: Type u_1
_inst_1: decidable_eq ι
g g': digraph ι
i i': ι
h: g.edges = g'.edges
edges_inv_path_inv: g.has_path_from_to i i'  g'.has_path_from_to i i'
iₘ: ι
p_α: g.has_path_from_to i iₘ
p_ω: g.has_path_from_to iₘ i'
 g'.has_path_from_to i i'

I thought it would be possible to inductively use edges_inv_path_inv on p_α and p_ω, since they are "smaller" than g.has_path_from_to i i'. But If I try to use edges_inv_path_inv p_α , Lean complains that p_α doesn't have the required type g.has_path_from_to i i', which makes sense from how edges_inv_path_inv is defined in the goal state.
What I don't get is, of what use the recursive edges_inv_path_inv is, if it can only be used on g.has_path_from_to i i'?

view this post on Zulip Alex J. Best (Jan 14 2021 at 17:07):

Try moving i i'right of the colon, recursion can only happens on those arguments in lean.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 17:07):

You need to generalize on your i i'

view this post on Zulip Marcus Rossel (Jan 14 2021 at 17:38):

Awesome that worked! Now I have:

lemma edges_inv_path_inv {g g' : digraph ι} (h : g.edges = g'.edges) :
   {i i' : ι}, (g.has_path_from_to i i')  (g'.has_path_from_to i i')
  | i i' (has_path_from_to.direct p) := -- doesn't matter
  | i i' (has_path_from_to.composite iₘ p_α p_ω) := begin
      have p_α', from edges_inv_path_inv p_α,
      have p_ω', from edges_inv_path_inv p_ω,
      exact has_path_from_to.composite iₘ p_α' p_ω'
    end

The problem I have now though is that I get ...

failed to prove recursive application is decreasing

... for both invocations of edges_inv_path_inv.
How can I prove that p_α and p_ω are "smaller" than has_path_from_to.composite iₘ p_α p_ω? I thought this inductive approach would automatically imply that.

view this post on Zulip Reid Barton (Jan 14 2021 at 17:45):

just deleting this fake tactic block should help

view this post on Zulip Reid Barton (Jan 14 2021 at 17:46):

... := has_path_from_to.composite iₘ (edges_inv_path_inv p_α) (edges_inv_path_inv p_ω)

view this post on Zulip Marcus Rossel (Jan 14 2021 at 17:48):

Reid Barton said:

just deleting this fake tactic block should help

Nope, that didn't work :oh_no: I'll try to get a MWE going...

view this post on Zulip Reid Barton (Jan 14 2021 at 17:48):

well, at least the nonworking proof is shorter now

view this post on Zulip Marcus Rossel (Jan 14 2021 at 18:03):

Ok, this produces the error:

structure digraph (ι : Type*) := (edges : ι)

namespace digraph

  variable {ι : Type*}

  def has_edge_from_to (g : digraph ι) (i i' : ι) : Prop := sorry

  inductive has_path_from_to (g : digraph ι) : ι  ι  Prop
    | direct {i i' : ι} : (g.has_edge_from_to i i')  has_path_from_to i i'
    | composite {i i' : ι} (iₘ : ι) : has_path_from_to i iₘ  has_path_from_to iₘ i'  has_path_from_to i i'

  lemma edges_inv_path_inv {g g' : digraph ι} (h : g.edges = g'.edges) :
     {i i' : ι}, (g.has_path_from_to i i')  (g'.has_path_from_to i i')
    | i i' (has_path_from_to.direct p) := sorry
    | i i' (has_path_from_to.composite iₘ p_α p_ω) := begin
        have p_α', from edges_inv_path_inv p_α,
        have p_ω', from edges_inv_path_inv p_ω,
        exact has_path_from_to.composite iₘ p_α' p_ω'
      end

end digraph

view this post on Zulip Reid Barton (Jan 14 2021 at 18:09):

The equation compiler seems not to understand that structural recursion should be happening here

view this post on Zulip Reid Barton (Jan 14 2021 at 18:09):

You can start like this

lemma edges_inv_path_inv {g g' : digraph ι} (h : g.edges = g'.edges) :
     {i i' : ι}, (g.has_path_from_to i i')  (g'.has_path_from_to i i') :=
begin
   intros i₀ i'₀ h,
   induction h with i i' h' i i' iₘ h₁ h₂ IH₁ IH₂,
 end

view this post on Zulip Marcus Rossel (Jan 14 2021 at 18:12):

Reid Barton said:

You can start like this

lemma edges_inv_path_inv {g g' : digraph ι} (h : g.edges = g'.edges) :
     {i i' : ι}, (g.has_path_from_to i i')  (g'.has_path_from_to i i') :=
begin
   intros i₀ i'₀ h,
   induction h with i i' h' i i' iₘ h₁ h₂ IH₁ IH₂,
 end

Awesome, I was able to prove it from there. Thanks @Reid Barton !


Last updated: May 16 2021 at 05:21 UTC