## Stream: new members

### Topic: Unfolding relation.refl_trans_gen

#### Martin Dvořák (Feb 16 2022 at 09:28):

I have a vague question. When I have a hypothesis of the form

h : relation.refl_trans_gen my_relation a z


what can I unfold or extract from that and how? For example, I would like to have

h₀ : my_relation a b
h₁ : relation.refl_trans_gen my_relation b z


under the assumption that a ≠ z.

If it isn't possible in Lean, tell me just anything I can learn from h.

#### Kevin Buzzard (Feb 16 2022 at 09:30):

Can you make a #mwe with a goal you'd like to know how to solve?

#### Martin Dvořák (Feb 16 2022 at 09:30):

I tried destruct h but it gave me some scary things. Is the command destruct worth using in practice at all?

#### Kyle Miller (Feb 16 2022 at 09:31):

Have you tried cases h?

#### Martin Dvořák (Feb 16 2022 at 09:31):

Kevin Buzzard said:

Can you make a #mwe with a goal you'd like to know how to solve?

I can make a MWE but I first wanted to ask vaguely what kind of information get be obtained from that. I don't have a specific goal yet.

#### Martin Dvořák (Feb 16 2022 at 09:32):

Kyle Miller said:

Have you tried cases h?

Yes but that didn't work. I got a message:

cases tactic failed, unsupported equality between type and constructor indices


At this point, I should create a MWE because it is starting to get too specific.

#### Martin Dvořák (Feb 16 2022 at 09:42):

OK, here is a silly example:

import logic.relation

def r : ℕ → ℕ → Prop :=
λ a, λ b, (a + 10 = b) ∨ (a + 7 = b)

def rr : ℕ → ℕ → Prop :=
relation.refl_trans_gen r

example : rr 3 30 :=
begin
fconstructor,
exact 20,
fconstructor,
exact 10,
fconstructor,
exact 3,
refl,
repeat { unfold r, finish },
end

example {x z : ℕ} (nontriv : x ≠ z) (h : rr x z) :
∃ y : ℕ, r x y ∧ rr y z :=
begin
sorry,
end


#### Martin Dvořák (Feb 16 2022 at 09:43):

I will also be happy for any suggestions how the proof of relation.refl_trans_gen r 3 33 could be written easier.

#### Martin Dvořák (Feb 16 2022 at 09:48):

PS: I had to modify my example a bit so that it cannot be proved without using the hypothesis.

#### Martin Dvořák (Feb 16 2022 at 09:56):

Or, if you prefer a abstract MWE (less specific), you can prove this example for me:

import logic.relation

example {r : ℕ → ℕ → Prop} {x z : ℕ} (nontriv : x ≠ z) (h : relation.refl_trans_gen r x z) :
∃ y : ℕ, (r x y) ∧ (relation.refl_trans_gen r y z) :=
begin
sorry,
end


#### Martin Dvořák (Feb 16 2022 at 10:01):

Or, as a reusable lemma:

import logic.relation

lemma unpack_transitive_closure {α : Type} {r : α → α → Prop} {x z : α}
(h : relation.refl_trans_gen r x z) (nontriv : x ≠ z) :
∃ y : α, (r x y) ∧ (relation.refl_trans_gen r y z) :=
begin
sorry,
end


#### Kyle Miller (Feb 16 2022 at 10:11):

Martin Dvořák said:

Or, if you prefer a abstract MWE (less specific), you can prove this example for me:

import logic.relation

example {r : ℕ → ℕ → Prop} {x z : ℕ} (nontriv : x ≠ z) (h : relation.refl_trans_gen r x z) :
∃ y : ℕ, (r x y) ∧ (relation.refl_trans_gen r y z) :=
begin
sorry,
end


I found an induction lemma that helps:

example {r : ℕ → ℕ → Prop} {x z : ℕ} (nontriv : x ≠ z) (h : relation.refl_trans_gen r x z) :
∃ y : ℕ, (r x y) ∧ (relation.refl_trans_gen r y z) :=
begin
induction h using relation.refl_trans_gen.head_induction_on with a b c d ih,