## Stream: new members

### Topic: Proof Over Inductive Prop

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

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

#### Yakov Pechersky (Jan 14 2021 at 17:07):

You need to generalize on your i i'

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

#### Reid Barton (Jan 14 2021 at 17:45):

just deleting this fake tactic block should help

#### Reid Barton (Jan 14 2021 at 17:46):

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

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

#### Reid Barton (Jan 14 2021 at 17:48):

well, at least the nonworking proof is shorter now

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


#### Reid Barton (Jan 14 2021 at 18:09):

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

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


#### 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: Dec 20 2023 at 11:08 UTC