Rewriting a field in a struct goal using conv

Stream: general

[nrs]

My current goal is { symbols := myvar.toP.fieldA, arity := fun a => Fintype.card (myvar.toP.fieldB) }. I'd like to enter symbols to rewrite it, but if I try arg 1 I get 'arg' conv tactic failed. Any tips? (arg 2 does correctly get me into arity)

[Kyle Miller]

First, remember that we tend to expect a #mwe around here.

Second, if the second field depends on the first field, rewriting is going to be somewhat complicated, and you may need to rethink what you're trying to do.

[nrs]

Right, sorry, here's the context:

structure P where
  α : Type
  β : α -> Type

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

def Signature.toP : Signature -> P
| ⟨sy, ar⟩ => ⟨sy, (fun n : Nat => Fin2 n) ∘ ar⟩

def P.toSignature (F : P) [(a : F.α) -> Fintype (F.β a)] : Signature :=
 ⟨F.α, fun a => Fintype.card (F.β a)⟩

def inva {sig : Signature} [(a : sig.toP.α) → Fintype (sig.toP.β a)]: P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  conv =>
    lhs
    _

The second field does indeed depend on the first, thanks for pointing that out I'll see whether I can try rewriting by taking this into account

[Kyle Miller]

I'm not thinking hard about it, but here's potentially some progress:

def inva {sig : Signature} [(a : sig.toP.α) → Fintype (sig.toP.β a)]: P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  cases sig
  congr! with h a
  cases h
  -- ⊢ Fintype.card ({ symbols := symbols✝, arity := arity✝ }.toP.β a) = arity✝ a

[nrs]

Nice! thank you!