search

lecopivo / scientific-computing-lean

work in progress book on Scientific Computing in Lean
https://lecopivo.github.io/scientific-computing-lean/
8 stars 1 forks source link

multiplicity `i : Fin n` by `n : Nat` #4

Open Seasawher opened 2 weeks ago

Seasawher commented 2 weeks ago

Beware! Fin n is endowed with modular arithmetic. Naively calling 2*i would multiply i by two and perform modulo by n/2. We do not want that; we have to get the underlying natural number i.1 and multiply then by two.

at https://lecopivo.github.io/scientific-computing-lean/working-with-arrays/tensor-operations.html#pooling-and-difficulties-with-dependent-types

But actually this holds:

#guard (2 : Nat) * (⟨3, by omega⟩ : Fin 4) = (6 : Nat)
lecopivo commented 2 weeks ago

But this also holds which I'm trying to warn about

#guard 2 * (3 : Fin 4) = 2

as here * is done on Fin 4

This does not hold

#guard (2 : Nat) * (3 : Fin 4) = 2

as here * is done on Nat.

This stuff is really confusing and will be a big footgun. Not sure what to do about it. Any tip on how to make this more clear?

Seasawher commented 2 weeks ago

Simply writing the code examples without omitting them will avoid confusion for readers of this book.

lecopivo commented 2 weeks ago

... without omitting then ...

Without omitting what? I'm not sure what are you trying to say. Can you phrase it differently?

Should I include the example 2 * (3 : Fin 4) = 2?

Seasawher commented 2 weeks ago

Sorry. My point was that it is the omission of code examples that makes it difficult to understand.

Should I include the example 2 * (3 : Fin 4) = 2?

Yes. Concrete code example is required.