# Zulip Chat Archive

## 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: May 16 2021 at 05:21 UTC