diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/ModularArithmetic/FField.v | 62 |
2 files changed, 63 insertions, 1 deletions
@@ -7,7 +7,7 @@ SRC_DIR := src SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' update-_CoqProject:: - (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files "src/*.v" | $(SORT_COQPROJECT))) > _CoqProject + (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(SORT_COQPROJECT))) > _CoqProject coq: coqprime Makefile.coq $(MAKE) -f Makefile.coq diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v new file mode 100644 index 000000000..cd293056f --- /dev/null +++ b/src/ModularArithmetic/FField.v @@ -0,0 +1,62 @@ +Require Export Crypto.Spec.ModularArithmetic. +Require Export Field. + +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. + +Local Open Scope F_scope. + +Definition OpaqueF := F. +Definition OpaqueZmodulo := BinInt.Z.modulo. +Definition Opaqueadd {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @add p. +Definition Opaquemul {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @mul p. +Definition Opaquesub {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @sub p. +Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p. +Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p. +Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p. +Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p. +Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField. + +Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p. + +Ltac FIELD_SIMPL_idtac FLD lH rl := + let Simpl := idtac (* (protect_fv "field") *) in + let lemma := get_SimplifyEqLemma FLD in + get_FldPre FLD (); + Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH; + get_FldPost FLD (). +Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G. + +Ltac F_to_Opaque := + change F with OpaqueF in *; + change BinInt.Z.modulo with OpaqueZmodulo in *; + change @add with @Opaqueadd in *; + change @mul with @Opaquemul in *; + change @sub with @Opaquesub in *; + change @div with @Opaquediv in *; + change @opp with @Opaqueopp in *; + change @inv with @Opaqueinv in *; + change @ZToField with @OpaqueZToField in *. + +Ltac F_from_Opaque p := + change OpaqueF with F in *; + change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *; + change OpaqueZmodulo with BinInt.Z.modulo in *; + change @Opaqueadd with @add in *; + change @Opaquemul with @mul in *; + change @Opaquesub with @sub in *; + change @Opaquediv with @div in *; + change @Opaqueopp with @opp in *; + change @Opaqueinv with @inv in *; + change @OpaqueZToField with @ZToField in *. + +Ltac F_field_simplify_eq := + lazymatch goal with |- @eq (F ?p) _ _ => + F_to_Opaque; + field_simplify_eq_idtac; + compute; + F_from_Opaque p + end. + +Ltac F_field := F_field_simplify_eq; [ring|..]. + +Ltac notConstant t := constr:NotConstant.
\ No newline at end of file |