Proof Over Inductive Prop

Stream: new members

[Marcus Rossel]

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'?

[Alex J. Best]

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

[Yakov Pechersky]

You need to generalize on your i i'

[Marcus Rossel]

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.

[Reid Barton]

just deleting this fake tactic block should help

[Reid Barton]

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

[Marcus Rossel]

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

[Reid Barton]

well, at least the nonworking proof is shorter now

[Marcus Rossel]

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

[Reid Barton]

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

[Reid Barton]

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

[Marcus Rossel]

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 !