type checker does not use simp lemmas?

Stream: general

[deepest recursion]

hello, ive written code, and lean complains about type incompatibility, which wouldve not been the case if typechecker could see a simp lemma Ive defined. is there something that can be done?

[Robin Arnez]

The type checker uses definitional equality and not propositional equality so in particular no lemmas. Instead, it reduces the expression by unfolding and since they don't come out equal after that, they aren't considered definitionally equivalent and the type-checker complains. You can avoid this by using cast:

example {p : PathP K a1 a2} :
    Path _ (path_symm (path_symm p)) (cast (by congr; simp) p) := by
  sorry

But that might get you in dependent type theory hell (casts are not very easy to work with).

[Robin Arnez]

Also, I'm not entirely sure why you do the whole Squash Bool thing, is this intentional?

example (x : PathP K a1 a2) : a1 ≍ a2 := by
  obtain ⟨a, h⟩ := x
  rw [← h.1, ← h.2]
  congr
  apply Subsingleton.allEq

[deepest recursion]

I thought that I should not interact with data. Not sure if it's relevant tho