isolated some of the issues of dataflow rewriter

[goens]

and removed the mathlib dependency

[marcusrossel]

For the case:

example {val n} (isLt : val < n) (isLt' : (@LT.lt Nat instLTNat (↑(Fin.mk val isLt)) n)) : isLt = isLt'

we do find an explanation by egg [*]. It's just that proof reconstruction explicitly fails with:

egg received invalid explanation: step contains non-defeq type-level rewrite in proof or type class instance

We get this error because we are rewriting with the structure projection reduction ↑⟨?val, ?isLt⟩ = ?val in the type of isLt'. What is buggy is that the given structure projection theorem does hold definitionally. So there must be some place where the proof reconstruction doesn't correctly recognize this theorem as a defeq theorem.

[marcusrossel]

Same for the final example:

example {val T x1} (isLt : val < x1.length) :
  Eq (@Fin.val_lt_of_le (@List.length T x1) (@List.length T x1) (@Fin.mk (@List.length T x1) val isLt) (Nat.le_refl x1.length)) isLt

if we use egg [*, Fin.val_lt_of_le].

[marcusrossel]

This is kind of fixed in the latest commit now.