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