ReflTransGen iff finitely may steps

Stream: mathlib4

[Malvin Gattinger]

The description here about docs#Relation.ReflTransGen explains the reflexive transitive closure with the common equivalence ReflTransGen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b but as far as I see Mathlib does not contain a result saying this or something similar.

As part of a project we needed a way to go from ReflTransGen to these finite chains and back, so I proved the following. Now I would like to clean it up and upstream it to Mathlib, if that makes sense:

import Mathlib.Data.Vector.Basic
import Mathlib.Logic.Relation

/-- A version of `Relation.ReflTransGen.cases_tail` also giving (in)equalities. -/
theorem ReflTransGen.cases_tail_eq_neq {r : α → α → Prop} (h : Relation.ReflTransGen r x z) :
    x = z ∨ (x ≠ z ∧ ∃ y, x ≠ y ∧ r x y ∧ Relation.ReflTransGen r y z) := sorry

/-- `ReflTransGen r a b` is equivalent to `∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ = b` -/
theorem ReflTransGen.iff_finitelyManySteps (r : α → α → Prop) (x z : α) :
    Relation.ReflTransGen r x z ↔
      ∃ (n : ℕ) (ys : Vector α n.succ),
        x = ys.head ∧ z = ys.last ∧ ∀ i : Fin n, r (ys.get i.castSucc) (ys.get (i.succ)) := sorry

See https://github.com/m4lvin/lean4-pdl/blob/main/Pdl/Star.lean for the actual proofs.

To prepare a draft PR I started to edit Mathlib.Logic.Relation locally and ran into a problem:

• With import Mathlib.Data.Vector.Basic in Relation.lean I get into an import cycle :stuck_out_tongue_closed_eyes: I see two solutions: (i) a new file that imports both Relation and Data.Vector.Basic - what would be a good name and place for it? ReflTransGen.FiniteChains? or (maybe better?) (ii) avoid using Vector, and use a list instead? But that makes the theorem less useful, currently induction on the length n is a nice use case.

Also, I was wondering if having the equalities x = ys.head ∧ z = ys.last as part of the right hand side is problematic for anything - note that the documentation says r a x₀ where I now say a = x₀ but my version does then not need the ∨ a = b addition.

Thanks in advance for any comments and advice - I have not made any PRs with code for mathlib before!

[Floris van Doorn]

I think in Mathlib to talk about vectors of Length n we prefer to use Fin n -> A, see the definitions in the file Mathlib.Data.Fin.Tuple.Basic.

[Floris van Doorn]

But solution (i) is the correct way to avoid import cycles. You can call your new file Mathlib.Logic.Relation.Chain or something (and rename Mathlib.Logic.Relation to Mathlib.Logic.Relation.Basic).

[Malvin Gattinger]

Thanks! It seems Mathlib.Data.Fin.Tuple.Basic also transitively imports Mathlib.Logic.Relation, so even if I reformulate things in terms of Fin n -> A instead of Vector, a separate file is needed.

[Malvin Gattinger]

In general, if I rename Bla to Bla.Basic, do I have to replace import Bla with import Bla.Basic in all files throughout all of Mathlib?

[Ruben Van de Velde]

That's correct

[Malvin Gattinger]

Hmm. I think I replaced all and grep -nr "Mathlib.Logic.Relation" . | grep -v Basic finds nothing outside .git, but lake build still says:

error: 'Mathlib.Logic.Relation': no such file or directory (error code: 2)
 file: ./././Mathlib/Logic/Relation.lean

even after rm -rf .lake.

[Malvin Gattinger]

ah wait, my grep is bad. it missed ./Mathlib/Data/Set/Pairwise/Basic.lean:7:import Mathlib.Logic.Relation

[Floris van Doorn]

There are some results
image.png

[Malvin Gattinger]

I just found docs#List.Chain and think using that should be better / more systematic than using functions from Fin.

[Malvin Gattinger]

I also did not make a PR yet, but pushed the branch and the CI seems to have worked https://github.com/leanprover-community/mathlib4/blob/m4lvin_ReflTrans_Chain/Mathlib/Logic/Relation/Chain.lean

[Malvin Gattinger]

Aha! There already are docs#List.relationReflTransGen_of_exists_chain and docs#List.exists_chain_of_relationReflTransGen - bummer I did not find those some months ago :man_facepalming: