Unexpect grind failure

Stream: metaprogramming / tactics

[Ching-Tsun Chou]

I have the following goal:

Symbol : Type u_1
State : Type u_2
na : FinAcc State Symbol
xs : ωSequence Symbol
ss : ωSequence (State ⊕ Unit)
n : ℕ
h : na.totalize.Run xs ss
hl : (ss n).isLeft = true
s : State
left✝ : s ∈ na.start
right✝ : inl s = ss 0
t : State
h✝ : ss n = inl t
this : na.totalize.MTr (ss 0) (xs.extract 0 n) (ss n)
⊢ na.totalize.MTr (inl s) (xs.extract 0 n) (inl t)

I thought grind should solve it, but grind failed. In the end I had to use:

simp_all only
assumption

to finish the proof. Is this a bug in grind? Note that the consequent follows from the antecedents without needing additional theorems because lnl s = ss 0 and ss n = int t.

[Aaron Liu]

there might be some defeq abuse is the problem I'm guessing

[Aaron Liu]

Is ωSequence (State ⊕ Unit) a function type at reducible transparency

[Chris Henson]

I would guess the same. This is from CSLib: https://api.cslib.io/docs/Cslib/Foundations/Data/OmegaSequence/Defs.html#Cslib.%CF%89Sequence

[Chris Henson]

In general, I do not expect grind to always succeed in these situations, as my understanding is it will not be using isDefEq in the same way as the assumption tactic.

[Ching-Tsun Chou]

I don't know enough about grind to tell. But note that the only logical rules needed in the proof is that equal can be substituted for equal. That is, even if we don't know anything about what the symbols mean, we can still see that this is a valid proof.

[Ching-Tsun Chou]

In other words, congruence closure alone should be able to solve this goal. My understanding is that grind can do congruence closure.