# Zulip Chat Archive

## 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,
contradiction,
exact ⟨b, c, d⟩,
end
```

(The induction hypothesis isn't used though.)

Last updated: Dec 20 2023 at 11:08 UTC