Merge branch 'field-experiment'

includes broken files to be removed in next commit

2 files changed, 712 insertions, 0 deletions

diff --git a/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v b/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v
new file mode 100644
index 000000000..146059ca4
--- /dev/null
+++ b/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v
@@ -0,0 +1,376 @@
+Require Import Bedrock.Word.
+Require Import Crypto.Spec.EdDSA.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic.
+Require Import ModularArithmetic.ModularArithmeticTheorems.
+Require Import ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Spec.CompleteEdwardsCurve.
+Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding.
+Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep.
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
+Require Import Zdiv.
+Require Import Crypto.Util.Tuple.
+Local Open Scope equiv_scope.
+
+Generalizable All Variables.
+
+
+Local Ltac set_evars :=
+  repeat match goal with
+         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
+         end.
+
+Local Ltac subst_evars :=
+  repeat match goal with
+         | [ e := ?E |- _ ] => is_evar E; subst e
+         end.
+
+Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)}
+           {HP:Proper (RA==>Basics.impl) P}
+           (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py))
+           (x : @sig A P) (y0:A) (pf : RA (proj1_sig x) y0)
+: Rsig x (exist _ y0 (HP _ _ pf (proj2_sig x))).
+Proof. destruct x. eapply H. assumption. Defined.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+Global Instance Let_In_Proper_changebody {A P R} {Reflexive_R:@Reflexive P R}
+  : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)).
+Proof.
+  lazy; intros; try congruence.
+  subst; auto.
+Qed.
+
+Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f}
+  : Proper (RA ==> RB) (fun x => Let_In x f).
+Proof. intuition. Qed.
+
+Ltac fold_identity_lambdas := 
+  repeat match goal with
+           | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in *
+           | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in *
+         end.
+
+Local Ltac replace_let_in_with_Let_In :=
+  match goal with
+  | [ |- context G[let x := ?y in @?z x] ]
+    => let G' := context G[Let_In y z] in change G'
+  end.
+
+Local Ltac Let_In_app fn :=
+  match goal with
+  | [ |- appcontext G[Let_In (fn ?x) ?f] ]
+    => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn y))); cbv beta
+  end.
+
+Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y).
+Proof.
+  destruct b; trivial.
+Qed.
+
+Lemma pull_Let_In {B C} (f : B -> C) A (v : A) (b : A -> B)
+  : Let_In v (fun v' => f (b v')) = f (Let_In v b).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) :
+    @Let_In _ (fun _ => T) (g x) f =
+    @Let_In _ (fun _ => T) x (fun p => f (g x)).
+Proof. reflexivity. Qed.
+
+Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R}
+                      (g : A -> B) (f : B -> T) (x : A)
+    f' (f'_ok: forall z, f' z === f (g z)),
+    Let_In (g x) f === Let_In x f'.
+Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed.
+Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl.
+
+Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) :
+    @Let_In _ (fun _ => T) (g1 x, g2 y) f =
+    @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))).
+Proof. reflexivity. Qed.
+
+Lemma funexp_proj {T T'} `{@Equivalence T' RT'}
+      (proj : T -> T')
+      (f : T -> T)
+      (f' : T' -> T') {Proper_f':Proper (RT'==>RT') f'}
+      (f_proj : forall a, proj (f a) === f' (proj a))
+      x n
+  : proj (funexp f x n) === funexp f' (proj x) n.
+Proof.
+  revert x; induction n as [|n IHn]; simpl; intros.
+  - reflexivity.
+  - rewrite f_proj. rewrite IHn. reflexivity.
+Qed.
+
+Global Instance pair_Equivalence {A B} `{@Equivalence A RA} `{@Equivalence B RB} : @Equivalence (A*B) (fun x y => fst x = fst y /\ snd x === snd y).
+Proof.
+  constructor; repeat intro; intuition; try congruence.
+  match goal with [H : _ |- _ ] => solve [rewrite H; auto] end.
+Qed.
+
+Global Instance Proper_test_and_op {T scalar} `{Requiv:@Equivalence T RT}
+      {op:T->T->T} {Proper_op:Proper (RT==>RT==>RT) op}
+      {testbit:scalar->nat->bool} {s:scalar} {zero:T} :
+  let R := fun x y => fst x = fst y /\ snd x === snd y in
+  Proper (R==>R) (test_and_op op testbit s zero).
+Proof.
+  unfold test_and_op; simpl; repeat intro; intuition;
+  repeat match goal with
+         | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:?; simpl in *; subst; try discriminate; auto
+         | [ H: _ |- _ ] => setoid_rewrite H; reflexivity
+         end.
+Qed.
+
+Lemma iter_op_proj {T T' S} `{T'Equiv:@Equivalence T' RT'}
+      (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') {Proper_op':Proper (RT' ==> RT' ==> RT') op'} x y z
+      (testbit : S -> nat -> bool) (bound : nat)
+      (op_proj : forall a b, proj (op a b) === op' (proj a) (proj b))
+  : proj (iter_op op x testbit y z bound) === iter_op op' (proj x) testbit y (proj z) bound.
+Proof.
+  unfold iter_op.
+  lazymatch goal with
+  | [ |- ?proj (snd (funexp ?f ?x ?n)) === snd (funexp ?f' _ ?n) ]
+    => pose proof (fun pf x0 x1 => @funexp_proj _ _ _ _ (fun x => (fst x, proj (snd x))) f f' (Proper_test_and_op (Requiv:=T'Equiv)) pf (x0, x1)) as H';
+      lazymatch type of H' with
+      | ?H'' -> _ => assert (H'') as pf; [clear H'|edestruct (H' pf); simpl in *; solve [eauto]]
+      end
+  end.
+
+  intros [??]; simpl.
+  repeat match goal with
+         | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:?
+         | _ => progress (unfold equiv; simpl)
+         | _ => progress (subst; intuition)
+         | _ => reflexivity
+         | _ => rewrite op_proj
+         end.
+Qed.
+
+Global Instance option_rect_Proper_nd {A T}
+  : Proper ((pointwise_relation _ eq) ==> eq  ==> eq ==> eq) (@option_rect A (fun _ => T)).
+Proof.
+  intros ?? H ??? [|]??; subst; simpl; congruence.
+Qed.
+
+Global Instance option_rect_Proper_nd' {A T}
+  : Proper ((pointwise_relation _ eq) ==> eq  ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
+Proof.
+  intros ?? H ??? [|]; subst; simpl; congruence.
+Qed.
+
+Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
+
+Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,
+    option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
+Proof.
+  destruct v; reflexivity.
+Qed.
+
+Lemma option_rect_function {A B C S' N' v} f
+  : f (option_rect (fun _ : option A => option B) S' N' v)
+    = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
+Proof. destruct v; reflexivity. Qed.
+Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
+  idtac;
+  lazymatch goal with
+  | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
+    => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
+    cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
+    [ set_evars;
+      let H := fresh in
+      intro H;
+      rewrite H;
+      clear;
+      abstract (cbv [Let_In]; reflexivity)
+    | ]
+  end.
+
+(** TODO: possibly move me, remove local *)
+Local Ltac replace_option_match_with_option_rect :=
+  idtac;
+  lazymatch goal with
+  | [ |- _ = ?RHS :> ?T ]
+    => lazymatch RHS with
+       | match ?a with None => ?N | Some x => @?S x end
+         => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
+       end
+  end.
+Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
+  repeat match goal with
+         | [ |- context[option_rect ?P ?S ?N None] ]
+           => change (option_rect P S N None) with N
+         | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
+           => change (option_rect P S N (Some x)) with (S x); cbv beta
+         end.
+
+Definition COMPILETIME {T} (x:T) : T := x.
+
+Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat.
+Proof.
+  intros.
+  pose proof (Nomega.Nlt_out a (N.succ b)).
+  rewrite N2Nat.inj_succ, N.lt_succ_r, <-NPeano.Nat.lt_succ_r in *; auto.
+Qed.
+Lemma N_size_nat_le_mono : forall a b, (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat.
+Proof.
+  intros.
+  destruct (N.eq_dec a 0), (N.eq_dec b 0); try abstract (subst;rewrite ?N.le_0_r in *;subst;simpl;omega).
+  rewrite !Nsize_nat_equiv, !N.size_log2 by assumption.
+  edestruct N.succ_le_mono; eauto using N_to_nat_le_mono, N.log2_le_mono.
+Qed.
+
+Lemma Z_to_N_Z_of_nat : forall n, Z.to_N (Z.of_nat n) = N.of_nat n.
+Proof. induction n; auto. Qed.
+
+Lemma Z_of_nat_nonzero : forall m, m <> 0 -> (0 < Z.of_nat m)%Z.
+Proof. intros. destruct m; [congruence|reflexivity]. Qed.
+
+Local Infix "mod" := NPeano.modulo : nat_scope.
+Lemma N_of_nat_modulo : forall n m, m <> 0 -> N.of_nat (n mod m)%nat = (N.of_nat n mod N.of_nat m)%N.
+Proof.
+  intros.
+  apply Znat.N2Z.inj_iff.
+  rewrite !Znat.nat_N_Z.
+  rewrite Zdiv.mod_Zmod by auto.
+  apply Znat.Z2N.inj_iff.
+  { apply Z.mod_pos_bound. apply Z_of_nat_nonzero. assumption. }
+  { apply Znat.N2Z.is_nonneg. }
+  rewrite Znat.Z2N.inj_mod by (auto using Znat.Nat2Z.is_nonneg, Z_of_nat_nonzero).
+  rewrite !Z_to_N_Z_of_nat, !Znat.N2Z.id; reflexivity.
+Qed.
+
+Lemma encoding_canonical' {T} {B} {encoding:canonical encoding of T as B} :
+  forall a b, enc a = enc b -> a = b.
+Proof.
+  intros.
+  pose proof (f_equal dec H).
+  pose proof encoding_valid.
+  pose proof encoding_canonical.
+  congruence.
+Qed.
+
+Lemma compare_encodings {T} {B} {encoding:canonical encoding of T as B}
+           (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b)
+           : forall a b : T, (a = b) <-> (B_eqb (enc a) (enc b) = true).
+Proof.
+  intros.
+  split; intro H.
+  { rewrite B_eqb_iff; congruence. }
+  { apply B_eqb_iff in H; eauto using encoding_canonical'. }
+Qed.
+
+Lemma eqb_eq_dec' {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) :
+    forall a b, if eqb a b then a = b else a <> b.
+Proof.
+  intros.
+  case_eq (eqb a b); intros.
+  { eapply eqb_iff; trivial. }
+  { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition. }
+Qed.
+
+Definition eqb_eq_dec {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) :
+  forall a b : T, {a=b}+{a<>b}.
+Proof.
+  intros.
+  pose proof (eqb_eq_dec' eqb eqb_iff a b).
+  destruct (eqb a b); eauto.
+Qed.
+
+Definition eqb_eq_dec_and_output {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) :
+  forall a b : T, {a = b /\ eqb a b = true}+{a<>b /\ eqb a b = false}.
+Proof.
+  intros.
+  pose proof (eqb_eq_dec' eqb eqb_iff a b).
+  destruct (eqb a b); eauto.
+Qed. 
+
+Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B}
+           (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b)
+           (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b)
+           : forall a b : T, T_eqb a b = B_eqb (enc a) (enc b).
+Proof.
+  intros;
+    destruct (eqb_eq_dec_and_output T_eqb T_eqb_iff a b);
+    destruct (eqb_eq_dec_and_output B_eqb B_eqb_iff (enc a) (enc b));
+    intuition;
+    try find_copy_apply_lem_hyp B_eqb_iff;
+    try find_copy_apply_lem_hyp T_eqb_iff;
+    try congruence.
+    apply (compare_encodings B_eqb B_eqb_iff) in H2; congruence.
+Qed.
+
+Lemma decode_failed_neq_encoding {T B} (encoding_T_B:canonical encoding of T as B) (X:B)
+  (dec_failed:dec X = None) (a:T) : X <> enc a.
+Proof. pose proof encoding_valid. congruence. Qed.
+Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B)
+      (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b)
+      (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b)
+      (P_:B) (Q:T) : 
+  option_rect (fun _ : option T => bool)
+                 (fun P : T => T_eqb P Q)
+                 false
+              (dec P_)
+    = B_eqb P_ (enc Q).
+Proof.
+  destruct (dec P_) eqn:Hdec; simpl option_rect.
+  { apply encoding_canonical in Hdec; subst; auto using eqb_compare_encodings. }
+  { pose proof encoding_canonical.
+    pose proof encoding_valid.
+    pose proof eqb_compare_encodings.
+    eapply decode_failed_neq_encoding in Hdec.
+    destruct (B_eqb P_ (enc Q)) eqn:Heq; [rewrite B_eqb_iff in Heq; eauto | trivial]. }
+Qed.
+
+Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed.
+
+Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x).
+Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed.
+
+Definition natToField {m} x : F m := ZToField (Z.of_nat x).
+Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x).
+Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x).
+  unfold natToField, FieldToNat; intros.
+  rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial.
+Qed.
+
+Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
+Proof.
+  split; eauto using F_eqb_eq, F_eqb_complete.
+Qed.
+
+Section FSRepOperations.
+  Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}.
+  Context {l:Z} {two_lt_l:(2 < l)%Z}.
+  Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}.
+  Context `(rcF:RepConversions (F q) FRep) (rcFOK:RepConversionsOK rcF).
+  Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul).
+  Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul).
+  Axiom SRep_testbit : SRep -> nat -> bool.
+  Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i.
+
+  Definition FSRepPow width x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x width.
+  Lemma FSRepPow_correct : forall width x n, (N.size_nat (FieldToN (unRep n)) <= width)%nat -> (unRep x ^ FieldToN (unRep n))%F = unRep (FSRepPow width x n).
+  Proof. (* this proof derives the required formula, which I copy-pasted above to be able to reference it without the length precondition *)
+    unfold FSRepPow; intros.
+    erewrite <-pow_nat_iter_op_correct by auto.
+    erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ _ SRep_testbit_correct n x width) by auto.
+    rewrite <-(rcFOK 1%F) at 1.
+    erewrite <-iter_op_proj;
+      [apply eq_refl
+      |eauto with typeclass_instances
+      |symmetry; eapply FRepMul_correct].
+  Qed.
+
+  Context (q_minus_2_lt_l:(q - 2 < l)%Z).
+  Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (ZToField (q - 2)))).
+  Lemma FRepInv_correct : forall x, inv (unRep x)%F = unRep (FRepInv x).
+    unfold FRepInv, COMPILETIME; intros.
+    rewrite <-FSRepPow_correct; rewrite FieldToN_correct, rcSOK, FieldToZ_ZToField, Zmod_small by omega; trivial.
+    pose proof @Fq_inv_fermat_correct as Hf; unfold inv_fermat in Hf; rewrite Hf by
+        auto using prime_q, two_lt_q.
+    reflexivity.
+  Qed.
+End FSRepOperations.
\ No newline at end of file
diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v
new file mode 100644
index 000000000..884a9fe5c
--- /dev/null
+++ b/src/Experiments/GenericFieldPow.v
@@ -0,0 +1,336 @@
+Require Import Coq.setoid_ring.Cring.
+Generalizable All Variables.
+
+
+(*TODO: move *)
+Lemma Z_pos_pred_0 p : Z.pos p - 1 = 0 -> p=1%positive.
+Proof. destruct p; simpl in *; try discriminate; auto. Qed.
+
+Lemma Z_neg_succ_neg : forall a b, (Z.neg a + 1)%Z = Z.neg b -> a = Pos.succ b.
+Admitted.
+
+Lemma Z_pos_pred_pos : forall a b, (Z.pos a - 1)%Z = Z.pos b -> a = Pos.succ b.
+Admitted.
+
+Lemma Z_pred_neg p : (Z.neg p - 1)%Z = Z.neg (Pos.succ p).
+Admitted.
+
+(* teach nsatz to deal with the definition of power we are use *)
+Instance  reify_pow_pos (R:Type) `{Ring R}
+e1 lvar t1 n
+`{Ring (T:=R)}
+{_:reify e1 lvar t1}
+: reify (PEpow e1 (N.pos n)) lvar (pow_pos t1 n)|1.
+
+Class Field_ops (F:Type)
+      `{Ring_ops F}
+      {inv:F->F} := {}.
+
+Class Division (A B C:Type) := division : A -> B -> C.
+
+Local Notation "_/_" := division.
+Local Notation "n / d" := (division n d).
+
+Module F.
+
+  Definition div `{Field_ops F} n d := n * (inv d).
+  Global Instance div_notation `{Field_ops F} : @Division F F F := div.
+
+  Class Field {F inv} `{FieldCring:Cring (R:=F)} {Fo:Field_ops F (inv:=inv)} :=
+    {
+      field_inv_comp : Proper (_==_ ==> _==_) inv;
+      field_inv_def : forall x, (x == 0 -> False) -> inv x * x == 1;
+      field_one_neq_zero : not (1 == 0)
+    }.
+  Global Existing Instance field_inv_comp.
+
+  Definition powZ `{Field_ops F} (x:F) (n:Z) :=
+    match n with
+    | Z0 => 1
+    | Zpos p => pow_pos x p
+    | Zneg p => inv (pow_pos x p)
+    end.
+  Global Instance power_field `{Field_ops F} : Power | 5 := { power := powZ }.
+
+  Section FieldProofs.
+    Context `{Field F}.
+    
+    Definition unfold_div (x y:F) : x/y = x * inv y := eq_refl.
+
+    Global Instance Proper_div :
+      Proper (_==_ ==> _==_ ==> _==_) div.
+    Proof.
+      unfold div; repeat intro.
+      repeat match goal with
+             | [H: _ == _ |- _ ] => rewrite H; clear H
+             end; reflexivity.
+    Qed.
+
+    Global Instance Proper_pow_pos : Proper (_==_==>eq==>_==_) pow_pos.
+    Proof.
+      cut (forall n (y x : F), x == y -> pow_pos x n == pow_pos y n);
+        [repeat intro; subst; eauto|].
+      induction n; simpl; intros; trivial;
+        repeat eapply ring_mult_comp; eauto.
+    Qed.
+    
+    Global Instance Propper_powZ : Proper (_==_==>eq==>_==_) powZ.
+    Proof.
+      repeat intro; subst; unfold powZ.
+      match goal with |- context[match ?x with _ => _ end] => destruct x end;
+        repeat (eapply Proper_pow_pos || f_equiv; trivial).
+    Qed.
+
+    Require Import Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
+    Lemma field_theory_for_tactic : field_theory 0 1 _+_ _*_ _-_ -_ _/_ inv _==_.
+    Proof.
+      split; repeat constructor; repeat intro; gen_rewrite; try cring;
+        eauto using field_one_neq_zero, field_inv_def. Qed.
+
+    Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.NArithRing.
+    Lemma power_theory_for_tactic : power_theory 1 _*_ _==_ NtoZ power.
+    Proof. constructor; destruct n; reflexivity. Qed.
+
+    Create HintDb field_nonzero discriminated.
+    Hint Resolve field_one_neq_zero : field_nonzero.
+    Ltac field_nonzero := repeat split; auto 3 with field_nonzero.
+    Ltac field_power_isconst t := Ncst t.
+    Add Field FieldProofsAddField : field_theory_for_tactic
+                                      (postprocess [field_nonzero],
+                                       power_tac power_theory_for_tactic [field_power_isconst]).
+
+    Lemma div_mul_idemp_l : forall a b, (a==0 -> False) -> a*b/a == b.
+    Proof. intros. field. Qed.
+
+    Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}.
+    Lemma mul_zero_why : forall a b, a*b == 0 -> a == 0 \/ b == 0.
+      intros; destruct (eq_dec a 0); intuition.
+      assert (a * b / a == 0) by
+          (match goal with [H: _ == _ |- _ ] => rewrite H; field end).
+      rewrite div_mul_idemp_l in *; auto.
+    Qed.
+
+    Require Import Coq.nsatz.Nsatz.
+    Global Instance Integral_domain_Field : Integral_domain (R:=F).
+    Proof.
+      constructor; intros; eauto using mul_zero_why, field_one_neq_zero.
+    Qed.
+
+    Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
+      let t := type of H in
+      generalize H;
+      field_lookup (PackField FIELD_SIMPL_EQ) [] t;
+      try (exact I);
+      try (idtac; []; clear H;intro H).
+
+    Require Import Util.Tactics.
+    Inductive field_simplify_done {x y:F} : (x==y) -> Type :=
+      Field_simplify_done : forall (H:x==y), field_simplify_done H.
+    Ltac field_nsatz :=
+      repeat match goal with
+               [ H: (_:F) == _ |- _ ] =>
+               match goal with
+               | [ Ha : field_simplify_done H |- _ ] => fail
+               | _ => idtac
+               end;
+               field_simplify_eq in H;
+               unique pose proof (Field_simplify_done H)
+             end;
+      repeat match goal with [ H: field_simplify_done _ |- _] => clear H end;
+      try field_simplify_eq;
+      try nsatz.
+    
+    Create HintDb field discriminated.
+    Hint Extern 5 (_ == _) => field_nsatz : field.
+    Hint Extern 5 (_ <-> _) => split.
+
+    Lemma mul_inv_l : forall x, not (x == 0) -> inv x * x == 1. Proof. auto with field. Qed.
+
+    Lemma mul_inv_r : forall x, not (x == 0) -> x * inv x == 1. Proof. auto with field. Qed.
+
+    Lemma mul_cancel_r' (x y z:F) : not (z == 0) -> x * z == y * z -> x == y.
+    Proof.
+      intros.
+      assert (x * z * inv z == y * z * inv z) by
+          (match goal with [H: _ == _ |- _ ] => rewrite H; auto with field end).
+      assert (x * z * inv z == x * (z * inv z)) by auto with field.
+      assert (y * z * inv z == y * (z * inv z)) by auto with field.
+      rewrite mul_inv_r, @ring_mul_1_r in *; auto with field.
+    Qed.
+
+    Lemma mul_cancel_r (x y z:F) : not (z == 0) -> (x * z == y * z <-> x == y).
+    Proof. intros;split;intros Heq; try eapply mul_cancel_r' in Heq; eauto with field. Qed.
+
+    Lemma mul_cancel_l (x y z:F) : not (z == 0) -> (z * x == z * y <-> x == y).
+    Proof. intros;split;intros; try eapply mul_cancel_r; eauto with field. Qed.
+
+    Lemma mul_cancel_r_eq : forall x z:F, not(z==0) -> (x*z == z <-> x == 1).
+    Proof.
+      intros;split;intros Heq; [|nsatz].
+      pose proof ring_mul_1_l z as Hz; rewrite <- Hz in Heq at 2; rewrite  mul_cancel_r in Heq; eauto.
+    Qed.
+
+    Lemma mul_cancel_l_eq : forall x z:F, not(z==0) -> (z*x == z <-> x == 1).
+    Proof. intros;split;intros Heq; try eapply mul_cancel_r_eq; eauto with field. Qed.
+
+    Lemma inv_unique (a:F) : forall x y, x * a == 1 -> y * a == 1 -> x == y. Proof. auto with field. Qed.
+    
+    Lemma mul_nonzero_nonzero (a b:F) : not (a == 0) -> not (b == 0) -> not (a*b == 0).
+    Proof. intros; intro Hab. destruct (mul_zero_why _ _ Hab); auto. Qed.
+    Hint Resolve mul_nonzero_nonzero : field_nonzero.
+
+    Lemma inv_nonzero (x:F) : not(x == 0) -> not(inv x==0).
+    Proof.
+      intros Hx Hi.
+      assert (Hc:not (inv x*x==0)) by (rewrite field_inv_def; auto with field_nonzero); contradict Hc.
+      ring [Hi].
+    Qed.
+    Hint Resolve inv_nonzero : field_nonzero.
+
+    Lemma div_nonzero (x y:F) : not(x==0) -> not(y==0) -> not(x/y==0).
+    Proof.
+      unfold division, div_notation, div; auto with field_nonzero.
+    Qed.
+    Hint Resolve div_nonzero : field_nonzero.
+
+    Lemma pow_pos_nonzero (x:F) p : not(x==0) -> not(Ncring.pow_pos x p == 0).
+    Proof.
+      intros; induction p using Pos.peano_ind; try assumption; [].
+      rewrite Ncring.pow_pos_succ; eauto using mul_nonzero_nonzero.
+    Qed.
+    Hint Resolve pow_pos_nonzero : field_nonzero.
+
+    Lemma sub_diag_iff (x y:F) : x - y == 0 <-> x == y. Proof. auto with field. Qed.
+
+    Lemma mul_same (x:F) : x*x == x^2%Z. Proof. auto with field. Qed.
+
+    Lemma inv_mul (x y:F) : not(x==0) -> not (y==0) -> inv (x*y) == inv x * inv y.
+    Proof. intros;field;intuition. Qed.
+
+    Lemma pow_0_r (x:F) : x^0 == 1. Proof. auto with field. Qed.
+    Lemma pow_1_r : forall x:F, x^1%Z == x. Proof. auto with field. Qed.
+    Lemma pow_2_r : forall x:F, x^2%Z == x*x. Proof. auto with field. Qed.
+    Lemma pow_3_r : forall x:F, x^3%Z == x*x*x. Proof. auto with field. Qed.
+
+    Lemma pow_succ_r (x:F) (n:Z) : not (x==0)\/(n>=0)%Z -> x^(n+1) == x * x^n.
+    Proof.
+      intros Hnz; unfold power, powZ, power_field, powZ; destruct n eqn:HSn.
+      - simpl; ring. 
+      - setoid_rewrite <-Pos2Z.inj_succ; rewrite Ncring.pow_pos_succ; ring.
+      - destruct (Z.succ (Z.neg p)) eqn:Hn.
+        + assert (p=1%positive) by (destruct p; simpl in *; try discriminate; auto).
+          subst; simpl in *; field. destruct Hnz; auto with field_nonzero.
+        + destruct p, p0; discriminate.
+        + setoid_rewrite Hn.
+          apply Z_neg_succ_neg in Hn; subst.
+          rewrite Ncring.pow_pos_succ; field;
+            destruct Hnz; auto with field_nonzero.
+    Qed.
+
+    Lemma pow_pred_r (x:F) (n:Z) : not (x==0) -> x^(n-1) == x^n/x.
+    Proof.
+      intros; unfold power, powZ, power_field, powZ; destruct n eqn:HSn.
+      - simpl. rewrite unfold_div; field.
+      - destruct (Z.pos p - 1) eqn:Hn.
+        + apply Z_pos_pred_0 in Hn; subst; simpl; field.
+        + apply Z_pos_pred_pos in Hn; subst.
+          rewrite Ncring.pow_pos_succ; field; auto with field_nonzero.
+        + destruct p; discriminate.
+      - rewrite Z_pred_neg, Ncring.pow_pos_succ; field; auto with field_nonzero.
+    Qed.
+    
+    Local Ltac pow_peano :=
+      repeat (setoid_rewrite pow_0_r 
+              || setoid_rewrite pow_succ_r
+              || setoid_rewrite pow_pred_r).
+    
+    Lemma pow_mul (x y:F) : forall (n:Z), not(x==0)/\not(y==0)\/(n>=0)%Z -> (x * y)^n == x^n * y^n.
+    Proof.
+      match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end.
+      { repeat intro. subst. reflexivity. }
+      - intros; cbv [power power_field powZ]; ring.
+      - intros n Hn IH Hxy.
+        repeat setoid_rewrite pow_succ_r; try rewrite IH; try ring; (right; omega).
+      - intros n Hn IH Hxy. destruct Hxy as [[]|?]; try omega; [].
+        repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; auto with field_nonzero.
+    Qed.
+
+    Lemma pow_nonzero (x:F) : forall (n:Z), not(x==0) -> not(x^n==0).
+      match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; pow_peano;
+        auto with field_nonzero.
+      { repeat intro. subst. reflexivity. }
+    Qed.
+    Hint Resolve pow_nonzero : field_nonzero.
+    
+    Lemma pow_inv (x:F) : forall (n:Z), not(x==0) -> inv x^n == inv (x^n).
+      match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end.
+      { repeat intro. subst. reflexivity. }
+      - intros; cbv [power power_field powZ]. field.
+      - intros n Hn IH Hx.
+        repeat setoid_rewrite pow_succ_r; try rewrite IH; try field; auto with field_nonzero.
+      - intros n Hn IH Hx. 
+        repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; auto 3 with field_nonzero.
+    Qed.
+
+    Lemma pow_0_l : forall n, (n>0)%Z -> (0:F)^n==0.
+      match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; try omega.
+      { repeat intro. subst. reflexivity. }
+      setoid_rewrite pow_succ_r; [auto with field|right;omega].
+    Qed.
+
+    Lemma pow_div (x y:F) (n:Z) : not (y==0) -> not(x==0)\/(n >= 0)%Z -> (x/y)^n == x^n/y^n.
+    Proof.
+      intros Hy Hxn. unfold division, div_notation, div.
+      rewrite pow_mul, pow_inv; try field; destruct Hxn; auto with field_nonzero.
+    Qed.
+
+    Hint Extern 3 (_ >= _)%Z => omega : field_nonzero.
+    Lemma issquare_mul (x y z:F) : not (y == 0) -> x^2%Z == z * y^2%Z -> (x/y)^2%Z == z.
+    Proof. intros. rewrite pow_div by (auto with field_nonzero); auto with field. Qed.
+
+    Lemma issquare_mul_sub (x y z:F) : 0 == z*y^2%Z - x^2%Z -> (x/y)^2%Z == z \/ x == 0.
+    Proof. destruct (eq_dec y 0); [right|left]; auto using issquare_mul with field. Qed.
+
+    Lemma div_mul : forall x y z : F, not(y==0) -> (z == (x / y) <-> z * y == x).
+    Proof. auto with field. Qed.
+
+    Lemma div_1_r : forall x : F, x/1 == x.
+    Proof. auto with field. Qed.
+
+    Lemma div_1_l : forall x : F, not(x==0) -> 1/x == inv x.
+    Proof. auto with field. Qed.
+
+    Lemma div_opp_l : forall x y, not (y==0) -> (-_ x) / y == -_ (x / y).
+    Proof. auto with field. Qed.
+
+    Lemma div_opp_r : forall x y, not (y==0) -> x / (-_ y) == -_ (x / y).
+    Proof. auto with field. Qed.
+    
+    Lemma eq_opp_zero : forall x : F, (~ 1 + 1 == (0:F)) -> (x == -_ x <-> x == 0).
+    Proof. auto with field. Qed.
+
+    Lemma add_cancel_l : forall x y z:F, z+x == z+y <-> x == y.
+    Proof. auto with field. Qed.
+
+    Lemma add_cancel_r : forall x y z:F, x+z == y+z <-> x == y.
+    Proof. auto with field. Qed.
+
+    Lemma add_cancel_r_eq : forall x z:F, x+z == z <-> x == 0.
+    Proof. auto with field. Qed.
+
+    Lemma add_cancel_l_eq : forall x z:F, z+x == z <-> x == 0.
+    Proof. auto with field. Qed.
+
+    Lemma sqrt_solutions : forall x y:F, y ^ 2%Z == x ^ 2%Z -> y == x \/ y == -_ x.
+    Proof.
+      intros ? ? squares_eq.
+      remember (y - x) as z eqn:Heqz.
+      assert (y == x + z) as Heqy by (subst; ring); rewrite Heqy in *; clear Heqy Heqz.
+      assert (Hw:(x + z)^2%Z == z * (x + (x + z)) + x^2%Z)
+        by (auto with field); rewrite Hw in squares_eq; clear Hw.
+      rewrite add_cancel_r_eq in squares_eq.
+      apply mul_zero_why in squares_eq; destruct squares_eq;  auto with field.
+    Qed.
+
+  End FieldProofs.
+End F.
\ No newline at end of file