Eq.rec with a constant does nothing: h ▸ c = c

Stream: Is there code for X?

[Snir Broshi]

docs#eq_rec_constant solves the simple case:

import Mathlib
theorem eq_rec_constant' {α β : Sort*} {x y : α} (h : x = y) (c : β) : h.rec c = c :=
  eq_rec_constant c h

The motive (fun _ _ ↦ β) takes a value of type α, a proof that x is equal to it, and returns a some constant type β that doesn't depend on those two values.

[Snir Broshi]

But what about cases where the motive is more complicated?

theorem eq_rec_constant₂ {α β : Sort*} {P : α → Sort*} {x y : α} (p : P y) (h : x = y) (c : β) :
    h.rec (fun _ ↦ c) p = c := by
  cases h
  rfl

Here the motive has another argument p for a term of type P _ (I'm not sure what the motive is exactly, but something like that).

[Snir Broshi]

theorem eq_rec_constant₃ {α β : Sort*} {P : α → Sort*} {Q : (a : α) → P a → Sort*} {x y : α}
    (p : P y) (q : Q y p) (h : x = y) (c : β) : h.rec (fun _ _ ↦ c) p q = c := by
  cases h
  rfl

Now there's a q that depends on the values before it, including p. And we can keep going like this.
I think we can even add a term whose type depends on the equality h and not just y, which further complicates matters.

[Snir Broshi]

Is there an easy way to solve this, perhaps with a tactic? Or should we add the versions with more params to Mathlib?
This came up when working with Sym2 (and Sym2.rec which uses Eq.rec), but I'm not able to inline the proof for eq_rec_constant₂ in this:

theorem Sym2.eq_rec_constant₂ {α : Type*} {β : Sort*} {P : Sym2 α → Sort*} {a b : α} (p : P s(b, a))
    (c : β) : (Sym2.sound (Sym2.Rel.swap a b)).rec (fun _ ↦ c) p = c := by
  cases Sym2.sound (Sym2.Rel.swap a b) -- error
  rfl

Also I was surprised that just rfl doesn't work here (without cases)

[Aaron Liu]

import Mathlib

theorem Sym2.eq_rec_constant₂ {α : Type*} {β : Sort*} {P : Sym2 α → Sort*} {a b : α} (p : P s(b, a))
    (c : β) : (Sym2.sound (Sym2.Rel.swap a b)).rec (fun _ ↦ c) p = c := by
  rw! [Sym2.sound (Sym2.Rel.swap a b)]
  rfl

[Snir Broshi]

Thanks! and thank you for creating rw! :)
Is there a way without it though? why doesn't simp [Sym2.sound (Sym2.Rel.swap a b)] work here?

[Aaron Liu]

that's because it's in a dependent position

[Snir Broshi]

yeah but simp usually magically works
I'm just a bit worried about how being one of the first users of a tactic might affect my PR getting approved

[Violeta Hernández]

Wait, what's this new rw!?

[Robin Arnez]

A dependent rewrite tactic, i.e. rw but it inserts casts to avoid "motive is not type-correct". See #metaprogramming / tactics > dependent rewrite tactic @ 💬 for the original discussion and docs#Mathlib.Tactic.DepRewrite.evalDepRewriteSeq for implementation and documentation.

[Kyle Miller]

Here's how you can do it by hand:

import Mathlib

theorem Sym2.eq_rec_constant₂ {α : Type*} {β : Sort*} {P : Sym2 α → Sort*} {a b : α} (p : P s(b, a))
    (c : β) : (Sym2.sound (Sym2.Rel.swap a b)).rec (fun _ ↦ c) p = c := by
  generalize_proofs h
  revert p h
  generalize s(b, a) = s1, s(a, b) = s2  -- note: can delete second clause
  intro _ rfl
  rfl

The idea is to generalize everything in sight until you get an equality between variables, then you can use intro rfl (alias for subst) to reduce the equality proof to something that's defeq to rfl.

I strongly recommend taking a moment to reflect on how you've gotten into this situation — very often there's a different design to avoid the morass of low-level casting!

(For what it's worth, I think it's better to do the above sort of proof by hand when necessary rather than introduce more specialized lemmas like eq_rec_constant.)

[Kyle Miller]

Something I've been planning on doing is getting congr! to see through Eq.rec casts. In principle it's straightforward to do, at least for most cases. The idea is to have it apply lemmas like rec_heq_of_heq. Possibly it could even have a flag to enable some smarts around recursors like Nat.rec, to transform over-applications of recursors into something simpler.

[Snir Broshi]

Kyle Miller said:

The idea is to generalize everything in sight until you get an equality between variables, then you can use intro rfl (alias for subst) to reduce the equality proof to something that's defeq to rfl.

Thanks! I didn't know about generalize_proofs and generalize and they look useful even beyond this situation (when "motive is not type correct")

Kyle Miller said:

I strongly recommend taking a moment to reflect on how you've gotten into this situation — very often there's a different design to avoid the morass of low-level casting!

By using Sym2.rec to define a function on Sym2s that has a dependent parameter so Sym2.lift won't work. I don't see how to avoid it, do you have suggestions?

import Mathlib
namespace SimpleGraph.ConnectedComponent

def mkFromEdge {V : Type*} {G : SimpleGraph V} {e : Sym2 V} (h : e ∈ G.edgeSet) : G.ConnectedComponent :=
  e.rec (fun p h ↦ G.connectedComponentMk p.fst) (by
    rintro _ _ (_ | _)
    · rfl
    ext1 h
    rw! [connectedComponentMk_eq_of_adj h, Sym2.sound <| Sym2.Rel.swap ..]
    rfl
  ) h

(I need h inside the recursion to prove that this function is indeed symmetric)

[Snir Broshi]

Edit: simplified the example

[Kyle Miller]

import Mathlib
namespace SimpleGraph.ConnectedComponent

/-!
# Solution 1

Already explored: use `Sym2.rec` directly. This version demonstrates `generalize`.
-/

def mkFromEdge {V : Type*} {G : SimpleGraph V} {e : Sym2 V} (h : e ∈ G.edgeSet) : G.ConnectedComponent :=
  e.rec (fun p h ↦ G.connectedComponentMk p.fst) (by
    rintro _ _ (_|_)
    · rfl
    · generalize_proofs h
      generalize s(_, _) = s1 at h
      subst h
      funext h
      apply connectedComponentMk_eq_of_adj
      apply G.adj_symm
      exact h) h

/-!
# Solution 2

Use `Sym2.recOnSubsingleton` to avoid dependence, by working with the subtype.
-/

def reachable_of_mem_edge {V : Type*} {G : SimpleGraph V} {e : Sym2 V} (h : e ∈ G.edgeSet)
    {v w : V} (hv : v ∈ e) (hw : w ∈ e) : G.Reachable v w := by
  cases e
  rw [Sym2.mem_iff] at hv hw
  obtain (rfl | rfl) := hv <;> obtain (rfl | rfl) := hw
  · rfl
  · exact h.reachable
  · exact h.reachable.symm
  · rfl

def subsingleton_of_mem_edgeSet {V : Type*} (G : SimpleGraph V) (p : V × V) :
    Subsingleton (Sym2.mk p ∈ G.edgeSet → { c : G.ConnectedComponent // ∃ v ∈ Sym2.mk p, v ∈ c.supp }) where
  allEq := by
    intro hv hw
    funext h
    obtain ⟨c, v, hv, hv'⟩ := hv h
    obtain ⟨d, w, hw, hw'⟩ := hw h
    cases c using ConnectedComponent.ind with | _ v'
    cases d using ConnectedComponent.ind with | _ w'
    rw [SimpleGraph.ConnectedComponent.mem_supp_iff, ConnectedComponent.eq] at hv' hw'
    rw [Subtype.mk.injEq, ConnectedComponent.eq]
    transitivity v
    · exact hv'.symm
    transitivity w
    · exact reachable_of_mem_edge h hv hw
    · exact hw'

def mkFromEdge' {V : Type*} {G : SimpleGraph V} {e : Sym2 V} (h : e ∈ G.edgeSet) : G.ConnectedComponent :=
  have := subsingleton_of_mem_edgeSet G
  let res : { c : G.ConnectedComponent // ∃ v ∈ e, v ∈ c.supp } :=
    e.recOnSubsingleton (fun p h ↦ ⟨G.connectedComponentMk p.fst, p.fst, by cases p; simp⟩) h
  res.1

/-!
# Solution 3

Define an `ndrec` that abstracts away `Sym2.rec`.
-/

def _root_.SimpleGraph.edgeSet_ndrec {C : Sort*} {V : Type*} (G : SimpleGraph V) (f : (v w : V) → G.Adj v w → C)
    (h : ∀ (v w : V) (hvw : G.Adj v w), f v w hvw = f w v hvw.symm) {e : Sym2 V} (he : e ∈ G.edgeSet) : C :=
  e.rec (fun p he ↦ f p.1 p.2 he) (by
    cases e
    rintro _ _ (_|_)
    · rfl
    next v w =>
      apply eq_of_heq
      rw [eqRec_heq_iff_heq]
      simp [h v w]
      congr! 1
      apply adj_comm) he

def mkFromEdge'' {V : Type*} {G : SimpleGraph V} {e : Sym2 V} (h : e ∈ G.edgeSet) : G.ConnectedComponent :=
  G.edgeSet_ndrec (fun v _ _ => G.connectedComponentMk v) (by
    intro v w hvw
    simp [hvw.reachable]) h

/-!
# Solution 4

Unexplored here. Use choice to simplify definition of `mkFromEdge`. Have `e ∈ G.edgeSet` hypothesis only appear in theorems.
Benefit: fewer DTT issues.
-/