[WIP] Poly rewrites (#104)

* Fix FHE to work with new framework + new mathlib

* Add a few statements for rewrites in FHE

* Add FHE to Projects

* Update `Poly` ops to reflect changes in HEIR repo

* prove some additional properties, sorried characterizations of fromTensor and toTensor

* add additional rewrite

* rewrite `fromTensor` without `do` and `ForIn`, some helper lemmas

* progress on toTensor <-> fromTensor

* more helper lemmas

* Apply suggestions from code review

Co-authored-by: Alex Keizer <[email protected]>

* add Poly namespace

* from_poly -> fromPoly

* fill two sorrys

* add fromTensor' to display fromTensor as a Z/qZ[X] element

* wip: add super useful lemma I don't know how mathlib yet

* add proof of previous fact

* add missing type signature

* prove rep_length bound

* switch to using ZMod.cast to coe to Int/Fin

* Add toTensor' with the 0-padding as in the representation

* clear three sorrys by following the prior proof script

* WIP: make progress on coeff_fromTensor

The key idea is to use as much mathlib as possible, so we
use the mathlib API to convert a List into a Finsupp into a Polynomial,
so we get lots of nice inbuilt theorems.

I'm now stuck in a purely ring-theoretic problem, which is trivial
on paper but I don't know the mathlib API.

The problem feels far more tractable than the gnarly induction I was stuck
with before.

* try to make more progress, now stuck at coercion hell

* chore: whitespace nits

* feat: finish toTensor_fromTensor

* show that representative is an additive hom

* add fromTensor_snoc

* add proof script I tried for coeff_fromTensor

* chore: fix whitespace

* feat: show that representative interacts well with multiplication

* feat: add another version of  in terms of finsupp

* Apply suggestions from code review

Co-authored-by: Chris Hughes <[email protected]>

* Address rest of comments from review

* Apply suggestions from code review

Co-authored-by: Chris Hughes <[email protected]>

* Fix naming

* missing renames

* forgot a few rep_lengths

---------

Co-authored-by: Alex Keizer <[email protected]>
Co-authored-by: Siddharth Bhat <[email protected]>
Co-authored-by: Chris Hughes <[email protected]>
Co-authored-by: Andrés Goens <Andrés Goens>

SSA.lean

@@ -8,6 +8,7 @@ import SSA.Core.Framework
 
 -- Eventually, all projects must be imported.
 import SSA.Projects.InstCombine.Alive
+import SSA.Projects.FullyHomomorphicEncryption
 import SSA.Projects.Tensor1D.Tensor1D
 import SSA.Projects.Tensor2D.Tensor2D
 import SSA.Projects.Holor.Holor

SSA/Projects/FullyHomomorphicEncryption.lean

@@ -0,0 +1,2 @@
+import SSA.Projects.FullyHomomorphicEncryption.Basic
+import SSA.Projects.FullyHomomorphicEncryption.Statements