Unfolding relation.refl_trans_gen

Stream: new members

[Martin Dvořák]

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]

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

[Martin Dvořák]

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

[Kyle Miller]

Have you tried cases h?

[Martin Dvořák]

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]

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]

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]

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]

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

[Martin Dvořák]

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]

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]

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