Rewriting constructors under forall bindings

Stream: Is there code for X?

[Jeremy Salwen]

Is there a name for the transformation that converts one of these lemmas into the other? Is there existing code that will do this sort of transformation?

example a b (h₁: a<10) (h₂:b<10): Fin.mk a h₁  + Fin.mk b h₂ = Fin.ofNat 0 := sorry

example (a b: Fin 10): a + b = Fin.ofNat 0 := sorry

[Yury G. Kudryashov]

In Lean 4 these two statements are defeq.

[Kyle Miller]

To go to the first from the second you can do cases a and cases b

[Kyle Miller]

If you have foralls (so say you do revert a b in the second one), you can use docs4#Fin.forall_iff

[Jeremy Salwen]

Kyle Miller said:

If you have foralls (so say you do revert a b in the second one), you can use docs4#Fin.forall_iff

Hmm, but this seems like a type-specific lemma, but isn't there a more general principle that's true for all constructors? (That's what I'm actually interested in).

[Kevin Buzzard]

cases will deal with all constructors. What do you mean by "existing code" if cases is not the answer? cases applies the recursor for the inductive type in question.

[Jeremy Salwen]

Kevin Buzzard said:

cases will deal with all constructors. What do you mean by "existing code" if cases is not the answer? cases applies the recursor for the inductive type in question.

As far as I understand, cases does the transformation in one direction, but not the reverse?

[Kevin Buzzard]

Right: cases takes apart x : Fin 10 into a : Nat and ha : a < 10. And angle bracket notation (or the appropriate mk constructor) puts it back together again.

[Jeremy Salwen]

But there is not an "uncases", or something like that, which automates the reverse transformation in the way that cases does?

[Kevin Buzzard]

example  a (h : a < 10) : Fin 10 := Fin.mk a h
example  a (h : a < 10) : Fin 10 := ⟨a, h⟩

noncomputable -- I think they'll fix this one day
example (x : Fin 10) : Nat := Fin.rec (λ a h => a) x
example (x : Fin 10) : x.1 < 10 := Fin.rec (λ a h => h) x

example (x : Fin 10) : Nat := x.1
example (x : Fin 10) : x.1 < 10 := x.2

Does this help?

[Kyle Miller]

There's no "uncases" to my knowledge, but it seems like a reasonable extension to the generalize family

[Kyle Miller]

You can use generalize here:

example a b (h₁: a<10) (h₂:b<10): Fin.mk a h₁  + Fin.mk b h₂ = Fin.ofNat 0 := by
  generalize Fin.mk _ _ = a'
  generalize Fin.mk _ _ = b'
  clear a h₁ b h₂

If there's some more complicated dependence, you can use generalize ha : Fin.mk _ _ = a' for example to get an equation to help eliminate a and b from the goal before clearing.

[Kyle Miller]

I'm taking advantage of how generalize searches for the first thing that matches Fin.mk _ _, but of course you can be more explicit.

[Jeremy Salwen]

Kevin Buzzard said:

example  a (h : a < 10) : Fin 10 := Fin.mk a h
example  a (h : a < 10) : Fin 10 := ⟨a, h⟩

noncomputable -- I think they'll fix this one day
example (x : Fin 10) : Nat := Fin.rec (λ a h => a) x
example (x : Fin 10) : x.1 < 10 := Fin.rec (λ a h => h) x

example (x : Fin 10) : Nat := x.1
example (x : Fin 10) : x.1 < 10 := x.2

Does this help?

Trying my best to understand. I don't see how this directly applies to automating the reverse transformation. I see how you could use these primitives as part of a tool a tool that would traverse the expression and rewrite internally.

[Jeremy Salwen]

I think I could write an "uncases" tactic that would automatically find applications of constructors that could be simplified in this way, I just wasn't sure if there was an existing tool to do this.

[Kyle Miller]

@Jeremy Salwen Did you try the generalize code yet? I meant it as a way toward implementing this, or at least how to get the effect by hand without any specialized lemmas.

[Kevin Buzzard]

Jeremy Salwen said:

I think I could write an "uncases" tactic that would automatically find applications of constructors that could be simplified in this way, I just wasn't sure if there was an existing tool to do this.

I see -- you're looking for a tactic. I was just writing code :-)

[Jeremy Salwen]

Kyle Miller said:

Jeremy Salwen Did you try the generalize code yet? I meant it as a way toward implementing this, or at least how to get the effect by hand without any specialized lemmas.

I did try it out, it is very close to the automation I am looking for, but I am looking for an even higher degree of automation (i.e. detecting and picking out Fin.mk as eligible for simplification in this context). So I think I will need to write some automation myself.

For the full context of why I'm interested in this, I'm looking to rewrite this lemma for example

theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) :
a[i] = List.get a.data { val := i, isLt := h }

into

theorem Array.getElem_eq_data_get_reversed {α : Type u_1} (a : Array α) {i : Fin (Array.size a)} :
List.get a.data i = a[i.1]'i.2

[Kyle Miller]

Are there a lot of lemmas like this that you expect to need to rewrite? Usually lemmas are written in a way where you don't have constructors with variables for each argument, but this one is special since it has a bare i on the LHS. (And I mean this just for types with a single constructor, like Fin)

[Kyle Miller]

The transformation is a little tricky because of this stray i, but it's doable. Your tactic needs to look for a constructor with variable arguments, generalize it, then one-by-one construct equalities between variables and projections of x and subst them out

example {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) :
    a[i] = List.get a.data { val := i, isLt := h } := by
  generalize hx : Fin.mk i h = x
  have : i = x := congr_arg Fin.val hx
  subst i
  have : h = x.isLt := rfl
  subst h
  clear hx
  -- ⊢ a[↑x] = List.get a.data x

[Jeremy Salwen]

I expect that this will come up for other lemmas where I am reversing the lhs and rhs.

I guess I am assuming that lemmas like

theorem Array.getElem_eq_data_get_reversed {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) :
List.get a.data { val := i, isLt := h } = a[i]

would not apply properly without being simplified. But I should actually verify that...

[Jeremy Salwen]

Hmm, it looks like rw does not require simplifying the constructor on the lhs to work, but simp does.

[Yakov Pechersky]

wouldn't uncases be constructor?

[Jeremy Salwen]

Yakov Pechersky said:

wouldn't uncases be constructor?

Could you explain what you mean? Or just illustrate it with the example two theorems?