From ce10def144ca9a21c3b1ca4a262b1c94336513e5 Mon Sep 17 00:00:00 2001 From: jadephilipoom Date: Wed, 22 Feb 2017 18:44:33 -0500 Subject: 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 _cps and non-cps equivalents have no suffix) * updated timing on mulT * renamed push_eval to push_basesystem_eval --- src/Util/Prod.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/Prod.v') diff --git a/src/Util/Prod.v b/src/Util/Prod.v index bcd9404a6..6e6c7d3c4 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -16,6 +16,10 @@ Local Arguments f_equal {_ _} _ {_ _} _. Scheme Equality for prod. +Definition fst_pair {A B} (a:A) (b:B) : fst (a,b) = a := eq_refl. +Definition snd_pair {A B} (a:A) (b:B) : snd (a,b) = b := eq_refl. +Create HintDb cancel_pair discriminated. Hint Rewrite @fst_pair @snd_pair : cancel_pair. + (** ** Equality for [prod] *) Section prod. (** *** Projecting an equality of a pair to equality of the first components *) -- cgit v1.2.3