Merge new base system (#112)

* Added sketch of new low-level base system code

* Implemented and proved addition

* Implemented carrying, which requires defining over Z rather than arbitrary ring

* Proved carry and proved ring-ness of base system ops

* Implemented split operation

* Started implementing modular reduction

* NewBaseSystem: prettify some proofs

* andres base

* improve andresbase

* new base

* first draft of goldilocks karatsuba

* Factored out goldilocks karatsuba

* Implement and prove karatsuba

* goldilocks cleanup

remodularize

* merge karatsuba and goldilocs karatsuba parameter blocks

* carry impl and proofs (not yet synthesis-ready)

* newbasesystem: use rewrite databases

* carry index range fix (TODO: allow for carry-then-reduce)

* simpler carry implementation

* Added compact operation for saturated base systems (this handles carries after multiplying or adding)

* debugging reduction for compact_rows

* rewrote compact

* Converted saturated section to CPS

* some progress on cps conversion for non-saturated stuff

* Converted associational non-saturated code to CPS, temporarily commented out examples

* pushed cps conversion through Positional

* moved list/tuple stuff to top of file

* proved lingering lemma

* worked on generic-style goal for simplified operations

* finished proving the generic-form example goal, revising a couple earlier lemmas

* revised previous lemmas

* finished revising previous lemmas

* removed commented-out code

* fixed non-terminating string in comment

* fix for 8.5

* removed old file

* better automation part 1

* better automation part 2 (goodbye proofs)

* better automation part 3/3

* some work on freeze

* remove saturated code and clean up exported-operations code

* Move helper lemmas for list/tuple CPS stuff to new CPSUtil file

* qualified imports

* fix runtime notations and module-level Let as per comments

* moved push_id to CPSUtil and cancel_pair lemmas to Prod

* fixed typo

* correctly generalized and moved lift_tuple2 (now called lift2_sig) and converted chained_carries into a fold

* moved karatsuba section to new file

* rename lemmas and definitions (now cps definitions are consistently <name>_cps and non-cps equivalents have no suffix)

* updated timing on mulT

* renamed push_eval to push_basesystem_eval

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
index 57c82df68..7a1d0cacb 100644
--- a/src/Util/Sigma.v
+++ b/src/Util/Sigma.v
@@ -16,6 +16,15 @@ Local Arguments f_equal {_ _} _ {_ _} _.
 
 (** ** Equality for [sigT] *)
 Section sigT.
+  (* Lift foralls out of sigT proofs and leave a sig goal *)
+  Definition lift2_sig {R S T} f (g:R->S)
+             (X : forall a b, {prod | g prod = f a b}) :
+    { op : T -> T -> R & forall a b, g (op a b) = f a b }.
+  Proof.
+    exists (fun a b => proj1_sig (X a b)).
+    exact (fun a b => proj2_sig (X a b)).
+  Defined.
+  
   (** *** Projecting an equality of a pair to equality of the first components *)
   Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
   : projT1 u = projT1 v