Induction on eqv_gen

Stream: new members

[Levi Poon]

Has the following induction principle been implemented? I can't find it but I may just be searching the wrong terms.

example : {α : Type*} {r p : α → α → Prop} (hre : ∀ a, p a a)
(htl : ∀ a b c, p a b → r c b → p a c) (htr : ∀ a b c, p a b → r b c → p a c)
(a b : α) (hab : eqv_gen r a b) : p a b := sorry

The non-Lean proof for this is that the equivalence relation generated by r just relates things that can be connected by a finite sequence of intermediate things with consecutive terms related by r in either direction. I'm not sure if going through this alternate description is the only way to do it in Lean.

[Junyan Xu]

It's a bit tricky but here is a full proof:

inductive eqv_gen' {α} (r : α → α → Prop) : α → α → Prop
| refl (a) : eqv_gen' a a
| transl {a b c} : eqv_gen' a b → r c b → eqv_gen' a c
| transr {a b c} : eqv_gen' a b → r b c → eqv_gen' a c

lemma imp_imp_iff {a b : Prop} : (a → a → b) ↔ (a → b) := ⟨λ h ha, h ha ha, λ h ha _, h ha⟩

lemma eqv_gen'_self {α} {a b : α} {r : α → α → Prop} (h : r a b) : eqv_gen' r a b :=
(eqv_gen'.refl a).transr h

lemma eqv_gen'_symm {α} {a b : α} {r : α → α → Prop} (h : r a b) : eqv_gen' r b a :=
(eqv_gen'.refl b).transl h

lemma eqv_gen'.trans' {α} {a b c : α} {r : α → α → Prop} (h : eqv_gen' r b c) :
  eqv_gen' r a b → eqv_gen' r a c :=
begin
  induction h with d d e f hde hfe ih d e f hde hef ih,
  exacts [id,  λ h, (ih h).transl hfe,  λ h, (ih h).transr hef],
end

lemma eqv_gen'.symm {α} {a b : α} {r : α → α → Prop} : eqv_gen' r a b → eqv_gen' r b a :=
begin
  rw ← imp_imp_iff, intro h,
  induction h with c c d e hcd hed ih c d e hcd hde ih,
  { exact id },
  { exact λ hce, (ih $ hce.transr hed).trans' (eqv_gen'_self hed) },
  { exact λ _, (ih hcd).trans' (eqv_gen'_symm hde) },
end

lemma eqv_gen_eq_eqv_gen' {α} {r : α → α → Prop} : eqv_gen r = eqv_gen' r :=
begin
  funext a b, apply propext, split; intro h,
  { induction h with c d hcd c c d hcd ih c d e hcd hde ihcd ihde,
    exacts [eqv_gen'_self hcd, eqv_gen'.refl c, ih.symm, ihde.trans' ihcd] },
  { induction h with c c d e hcd hed ih c d e hcd hde ih,
    { exact eqv_gen.refl c },
    { exact ih.trans c d e ((eqv_gen.rel e d hed).symm e d) },
    { exact ih.trans c d e (eqv_gen.rel d e hde) } },
end

example {α : Type*} {r p : α → α → Prop} (hre : ∀ {a}, p a a)
  (htl : ∀ {a b c}, p a b → r c b → p a c) (htr : ∀ {a b c}, p a b → r b c → p a c)
  (a b : α) (hab : eqv_gen r a b) : p a b :=
begin
  rw eqv_gen_eq_eqv_gen' at hab,
  induction hab with c c d e hcd hed ih c d e hcd hde ih,
  exacts [hre, htl ih hed, htr ih hde],
end

[Levi Poon]

This does seem like a good way to proceed, thanks!