Automating generic rewrites

Stream: general

[nrs]

The following piece of code defines a simple interpreter, by defining a signature AttrsSig to interpret, and an interpretation at interp. The interpretation is produced by the fold cata that takes an interpretation and something to interpret. At interp, a rewrite must be done in order for the typechecker to take the correct Fin, but these rewrites are super trivial (they follow from applying AttrsSig.arity to fst). Would there be a way to apply them generically, or test for them automatically?

structure Signature where
  symbol : Type
  arity : symbol -> Nat

inductive AttrsSymb | nil | nat | bool | attrs

def AttrsSig : Signature := .mk AttrsSymb fun
| .nil => 0
| .nat => 1
| .bool => 1
| .attrs => 2

inductive Ext (σ : Signature) (α : Type _)
| mk : (s : σ.symbol) -> (Fin (σ.arity s) -> α) -> Ext σ α

inductive μ (σ : Signature)
| sup : Ext σ (μ σ) -> μ σ

def Alg (σ : Signature) (α : Type _) := Ext σ α -> α

def cata (alg : Alg σ α) : μ σ -> α := fun ⟨fst, snd⟩ => alg ⟨fst, fun x => cata alg (snd x)⟩

def interp : Alg AttrsSig Type := fun
| ⟨fst, snd⟩ => match fst with
  | .nil => Unit
  | .nat => Nat × (snd ⟨0, by reduce; simp only [Nat.le_eq, le_refl]⟩)
  | .bool => Bool × (snd (by reduce; exact 0)) -- same proof as above but using coercion
  | .attrs => (snd (by reduce; exact 0)) × (snd (by reduce; exact 1))

def simpleAttrs : μ AttrsSig := .sup <| .mk .nat fun _ => .sup <| .mk .bool fun _ => .sup <| .mk .nil (nomatch ·)

#reduce (types := true) cata interp simpleAttrs -- Nat × Bool × Unit