How to prove Eq.ndrec

Stream: general

[Moritz R]

i have this Thing Eq.ndrec in my goal, and can't find out how to prove it :smiling_face_with_tear:
I have dumbed down the definition of Term a bit, but kept the spirit of my real problem otherwise.

import Mathlib.Data.Sym.Sym2



inductive Term (F : ℕ → Type*) (α : Type*) where
  | var : α → Term F α
export Term (var)

namespace Term

variable {α : Type*} {F : ℕ → Type*}

@[simp]
def varFinset [DecidableEq α] : Term F α → Finset α
  | .var a => {a}

/-- Restricts a term to use only a set of the given variables. -/
def restrictVar [DecidableEq α] : ∀ (t : Term F α) (_f : t.varFinset → β), Term F β
  | var a, f => var (f ⟨a, Finset.mem_singleton_self a⟩)

end Term

/-- An Atom is an unordered pair of Terms, representing an (unordered)
    equation of the form s1 ≈ s2. -/
abbrev Atom (F : ℕ → Type*) (α : Type*) := Sym2 (Term F α)

abbrev Prod.toAtom (ts : Term F α × Term F α) : Atom F α := Sym2.mk ts



section rec
/- just for easier reference a copy of the used recursion theorem (Quot.rec). The copy isn't used below, only the original. -/
variable {α : Sort u}
variable {r : α → α → Prop}
variable {motive : Quot r → Sort v}

@[elab_as_elim] abbrev rec22
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → (Eq.ndrec (f a) (Quot.sound p)) = f b)
    (q : Quot r) : motive q :=
  Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((Quot.lift (Quot.indep f) (Quot.indepCoherent f h) q).2)

end rec

section restrictAtom

namespace Atom

variable {α : Type*} {F : ℕ → Type*}

/-- The Finset of all variables that appear in a given atom. -/
def varFinset [DecidableEq α] : Atom F α → Finset α :=
  Quot.lift (fun ts ↦ ts.fst.varFinset ∪ ts.snd.varFinset) (by grind [Sym2.Rel])

@[simp, grind =]
lemma varFinset_eq [DecidableEq α] (t1 t2 : Term F α) :
    Atom.varFinset s(t1, t2) = Term.varFinset t1 ∪ Term.varFinset t2 := by
    rfl

def restrictVar {β : Type*} [DecidableEq α] : (a :Atom F α) → ((a.varFinset → β) → Atom F β) :=
    Quot.rec (fun ts transf =>
      s(ts.fst.restrictVar (transf ∘ Set.inclusion (by grind)), ts.snd.restrictVar (transf ∘ Set.inclusion (by grind))))
  (by
    intro a b hrel
    sorry

  )


end Atom

end restrictAtom

[Aaron Liu]

  (by
    intro a b hrel
    rw! [Quot.sound hrel]
    simp only
    -- the goal now has no `Eq.ndrec`
    sorry

  )

for the rw! tactic you will need to add an import Mathlib.Tactic.DepRewrite

[Aaron Liu]

you probably shouldn't be using the Quot.rec but rather the specialized docs#Sym2.rec since you're using Sym2

[Aaron Liu]

even though it's exactly the same the benefit is that you don't break api boundaries

[Moritz R]

It seems something has changed about rw! in the latest mathlib, on my version, it screams at me to use rw! (castMode := .all) [Quot.sound hrel] in stable mathlib (but it works then)

[Moritz R]

Why does rewriting with [a] = [b] eliminate this Eq.ndrec?

[Aaron Liu]

because the equality it's working on is rewritten from [a] = [b] to [b] = [b]

[Aaron Liu]

and [b] = [b] is definitionally equal to rfl

[Moritz R]

Let me phrase it in my own words: We have the goal
(Eq.ndrec (context [a]) ([a] = [b])) = context [b]).
rewriting it changes it to
(Eq.ndrec (context [b]) ([b] = [b])) = context [b])? i dont think that's the goal after the rw!.

Can you dumb it down a bit more please?

[Aaron Liu]

what's the goal after rw!?

[Aaron Liu]

rw! went through some fixes over the past month so what I see might not be the same as what you see

[Moritz R]

Lets use the Lean 4 Web on latest mathlib with this code:

import Mathlib.Data.Sym.Sym2
import Mathlib.Tactic.DepRewrite


inductive Term (F : ℕ → Type*) (α : Type*) where
  | var : α → Term F α
export Term (var)

namespace Term

variable {α : Type*} {F : ℕ → Type*}

@[simp]
def varFinset [DecidableEq α] : Term F α → Finset α
  | .var a => {a}

/-- Restricts a term to use only a set of the given variables. -/
def restrictVar [DecidableEq α] : ∀ (t : Term F α) (_f : t.varFinset → β), Term F β
  | var a, f => var (f ⟨a, Finset.mem_singleton_self a⟩)

end Term

/-- An Atom is an unordered pair of Terms, representing an (unordered)
    equation of the form s1 ≈ s2. -/
abbrev Atom (F : ℕ → Type*) (α : Type*) := Sym2 (Term F α)

abbrev Prod.toAtom (ts : Term F α × Term F α) : Atom F α := Sym2.mk ts



section rec
/- just for easier reference a copy of the used recursion theorem: -/
variable {α : Sort u}
variable {r : α → α → Prop}
variable {motive : Quot r → Sort v}

@[elab_as_elim] abbrev rec22
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → (Eq.ndrec (f a) (Quot.sound p)) = f b)
    (q : Quot r) : motive q :=
  Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((Quot.lift (Quot.indep f) (Quot.indepCoherent f h) q).2)

end rec

section restrictAtom

namespace Atom

variable {α : Type*} {F : ℕ → Type*}

/-- The Finset of all variables that appear in a given atom. -/
def varFinset [DecidableEq α] : Atom F α → Finset α :=
  Quot.lift (fun ts ↦ ts.fst.varFinset ∪ ts.snd.varFinset) (by grind [Sym2.Rel])

@[simp, grind =]
lemma varFinset_eq [DecidableEq α] (t1 t2 : Term F α) :
    Atom.varFinset s(t1, t2) = Term.varFinset t1 ∪ Term.varFinset t2 := by
    rfl

def restrictVar {β : Type*} [DecidableEq α] : (a :Atom F α) → ((a.varFinset → β) → Atom F β) :=
    Quot.rec (fun ts transf =>
      s(ts.fst.restrictVar (transf ∘ Set.inclusion (by grind)), ts.snd.restrictVar (transf ∘ Set.inclusion (by grind))))
  (by
    intro a b hrel
    rw! [Quot.sound hrel]
    simp only

  )


end Atom

end restrictAtom

[Moritz R]

Before the rw! we have the goal:

Eq.ndrec (motive := fun x ↦ (↥(varFinset x) → β) → Atom F β)
    (fun transf ↦ s(a.1.restrictVar (transf ∘ Set.inclusion ⋯), a.2.restrictVar (transf ∘ Set.inclusion ⋯))) ⋯ =
  fun transf ↦ s(b.1.restrictVar (transf ∘ Set.inclusion ⋯), b.2.restrictVar (transf ∘ Set.inclusion ⋯))

[Moritz R]

After the rw! with [a] = [b]` we have the goal

((fun {α} a motive refl ↦ refl) (Quot.mk (Sym2.Rel (Term F α)) b)
    (fun x x_1 ↦ (fun x ↦ (↥(varFinset x) → β) → Atom F β) x) fun transf ↦
    s(a.1.restrictVar (transf ∘ Set.inclusion ⋯), a.2.restrictVar (transf ∘ Set.inclusion ⋯))) =
  fun transf ↦ s(b.1.restrictVar (transf ∘ Set.inclusion ⋯), b.2.restrictVar (transf ∘ Set.inclusion ⋯))

[Moritz R]

And further after the simp only we have the for me solvable goal

(fun transf ↦ s(a.1.restrictVar (transf ∘ Set.inclusion ⋯), a.2.restrictVar (transf ∘ Set.inclusion ⋯))) = fun transf ↦
  s(b.1.restrictVar (transf ∘ Set.inclusion ⋯), b.2.restrictVar (transf ∘ Set.inclusion ⋯))

[Aaron Liu]

seems like your version of mathlib doesn't have #32306 yet

[Aaron Liu]

the goal might be more understandable if you rewrite! instead?

[Aaron Liu]

and then simp only

[Moritz R]

So before the rw! we have a goal along the lines of

(Eq.ndrec (context [a]) ([a] = [b])) = context [b])

[Aaron Liu]

yes

[Moritz R]

aha, after rewrite! (not rw!) the goal is "exactly the same" but some of the proofs ⋯ have been changed.

[Moritz R]

and after the this suddenly it simps to the nice goal

context [a] = context [b]

[Moritz R]

E.g. it changes a proof of

↑(Term.varFinset a.1) ⊆ ↑(Atom.varFinset [a])

to a proof of

↑(Term.varFinset a.1) ⊆ ↑(Atom.varFinset [b])

(i have simplified notation a bit)

[Moritz R]

But why is the Eq.ndrec now vanishing after the simp only?

[Moritz R]

i.e. why is (now with the invisible proofs hidden in context changed)

(Eq.ndrec (context [a]) ([a] = [b])) = context [a]

[Aaron Liu]

it's not just the proofs that change

[Aaron Liu]

the implicit arguments change too

[Moritz R]

ah yes, there is a bunch of [a]s which change to [b]s.

[Moritz R]

But still i dont get it. I dont really know what Eq.ndrec is trying to say

[Kevin Buzzard]

I think it's worth stressing the point that you probably shouldn't be dealing with Eq.ndrec in the first place and a better question is "how did I end up with this in my goal and what should I have done instead".

[Kevin Buzzard]

Aaron Liu said:

you probably shouldn't be using the Quot.rec but rather the specialized docs#Sym2.rec since you're using Sym2

Is this the issue?

[Moritz R]

Sym2.rec is basically just a renaming of Quot.rec, (instantiated for the quotient Sym 2 of course)

[Moritz R]

I don't know how to the restrictvar definition without one of the .recs, since I don't think it's possible using only Quot.lift

[Ruben Van de Velde]

Looks like you introduced it yourself in rec22

[Ruben Van de Velde]

Why?

[Aaron Liu]

Kevin Buzzard said:

I think it's worth stressing the point that you probably shouldn't be dealing with Eq.ndrec in the first place and a better question is "how did I end up with this in my goal and what should I have done instead".

in this case it's pretty unavoidable though?

[Aaron Liu]

you would have to change the definition of Atom or something

[Moritz R]

Ruben Van de Velde schrieb:

Looks like you introduced it yourself in rec22

sorry for the confusion, that is just a copy of Quot.rec so i had it viewable in the same file. It isnt even used, its just for helping me with the arguments

[Aaron Liu]

well you can avoid it if you prefer HEq instead

[Aaron Liu]

I would consider HEq to be worse though

[Moritz R]

Oh wait, i can use Quot.map (or better Sym2.map) since my function only works on each element of the unordered pair by it's own!

[Moritz R]

Then i don't need a lifting proof at all

[Moritz R]

oh wait no that doesn't work

[Moritz R]

maybe i can use some dependant version of map

[Moritz R]

Yes! Sym2.pmap works out for me

[Moritz R]

def restrictVar {β : Type*} [DecidableEq α] (a : Atom F α) (f : (a.varFinset → β)) : Atom F β :=
    Sym2.pmap (P := fun t ↦ t ∈ a) (fun (t: Term F α) (h_t_in_a) ↦ (t.restrictVar (f ∘ Set.inclusion (by sorry))) a (by simp)

The sorry that is left, is provable for my actual definition of Term (i used a simplified one for the example)