Eta reduction for structures

Stream: Is there code for X?

[Jeremy Salwen]

MWE:

import Std.Data.Array.Init.Lemmas

theorem bar: ∀ (t : Nat) {a b c : Fin t}, { val := a.1, isLt := a.2 }= b * c  := by
  simp

I believe that "eta reduction for structures' should simplify the goal to a = b*c. However, simp doesn't seem to do this. is there another way I can get "eta reduction for structures" to simplify this expression?

[Yaël Dillies]

docs4#Fin.eta

[Mario Carneiro]

there is no "eta reduction" rule, there is an eta defeq rule

[Jeremy Salwen]

I would like to do this simplification in general, i.e. MyType.mk x.1 x.2 x.3 = x. Is there a way to do so?

[Yaël Dillies]

I would guess simp (cfg:={eta:=true}), which is the (quite more verbose) Lean 4 version of simp {eta:=tt}.

[Jeremy Salwen]

simp (config:={eta:=true}) doesn't simplify anything. (I think it is also enabled by default.)

[Jeremy Salwen]

(for completeness, simp (config:={eta:=true, etaStruct := .all}) does nothing either, but I believe that's the default option as well)

[Scott Morrison]

Could you #xy? It seems unlikely one would need this frequently.

[Jeremy Salwen]

@Scott Morrison I am writing a tactic that takes a theorem like:

lemma foo t a b (h₁: a<t) (h₂:b<t): Fin.mk a h₁ = Fin.mk b h₂ := sorry

And rewrites it to

∀ (t : ℕ) (x x_1 : Fin t), x = x_1

I have gotten it to the point where it generates this theorem:

∀ (t : ℕ) (x x_1 : Fin t), { val := x.1, isLt := (_ : x.1 < t) } = { val := x_1.1, isLt := (_ : x_1.1 < t) }

I don't think this is such an odd request, to simplify structures in this way in the context of a tactic.

[Scott Morrison]

Aren't those statement definitionally equal? You wouldn't actually need to simplify, you can just assign.

[Jeremy Salwen]

Hmm, ok, I could try to write a tactic that uses change where it finds this pattern.

[Jeremy Salwen]

Ok, I got it working!

import Lean
import Mathlib.Tactic.Find
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def isEtaStruct (e: Expr): MetaM (Option Expr) := do
  let (declName, declArgs) := e.getAppFnArgs
  match (← getEnv).find? declName with
  | ConstantInfo.ctorInfo ctorInfo =>
    match (← getEnv).find? ctorInfo.induct with
    | ConstantInfo.inductInfo indInfo =>
      if indInfo.ctors.length == 1
        && ctorInfo.numFields > 0
        && declArgs.size == ctorInfo.numParams + ctorInfo.numFields then
        match declArgs.get? ctorInfo.numParams with
        | some (Expr.proj _ _ arg) =>
          logInfo "hello"
          if ←  isDefEq e arg then
            pure (some arg)
          else
            pure none
        | some a =>
          match (a).getAppArgs'.back? with
          | some arg =>
              if ←  isDefEq e arg then
                pure (some arg)
              else
                pure none
          | none => pure none
        | _ => pure none
      else
        pure none
    | _ => pure none
  | _ =>
    pure none


partial def etastruct (e: Expr): MetaM Expr := do
  Meta.transform e (post:= fun n => do
    match (← isEtaStruct n) with
    | some t => pure (TransformStep.done t)
    | none => pure TransformStep.continue
  )

syntax "etastruct" (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| etastruct $[$loc?]?) =>
  withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
    (atLocal := fun h => liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← h.getType)
      mvarId.changeLocalDecl' h (← etastruct ty))
    (atTarget := liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      mvarId.change (← etastruct ty))
    (failed := fun _ => throwError "etastruct failed")

theorem bar (t : Nat) {a b c : Fin t} (d:{ val := a.1, isLt := a.2 }= b * c ): { val := a.1, isLt := a.2 }= b * c  := by
  etastruct at d
  etastruct
  ```

[Scott Morrison]

Jeremy Salwen said:

I am writing a tactic that takes a theorem like:

lemma foo t a b (h₁: a<t) (h₂:b<t): Fin.mk a h₁ = Fin.mk b h₂ := sorry

And rewrites it to

∀ (t : ℕ) (x x_1 : Fin t), x = x_1

I'm still curious about when you would use this tactic.

[Jeremy Salwen]

@Scott Morrison

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

Which I then use in my simp set. It is important to simplify the LHS, because if I just leave the LHS like this:

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]

Simp will not match it properly.

[Kyle Miller]

(a little previous discussion)