nsatz: reimplement, integrate, demonstrate

3 files changed, 197 insertions, 61 deletions

diff --git a/_CoqProject b/_CoqProject
index 4ad320808..2fc5b1b90 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,10 +1,10 @@
 -R src Crypto
+src/Algebra.v
 src/BaseSystem.v
 src/BaseSystemProofs.v
 src/EdDSAProofs.v
 src/Field.v
 src/Rep.v
-src/SaneField.v
 src/Testbit.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/DoubleAndAdd.v
diff --git a/src/SaneField.v b/src/Algebra.v
index 4149e2fd1..85602e64a 100644
--- a/src/SaneField.v
+++ b/src/Algebra.v
@@ -307,42 +307,46 @@ Module Field.
   End Field.
 End Field.
 
-Module _NsatzExportGuarantine.
-  Require Import Coq.nsatz.Nsatz.
-  Ltac sane_nsatz :=
-    let Hops := fresh "HRingOps" in
-    let carrierType := lazymatch goal with |- ?R ?x _ => type of x end in
-    let inst := constr:(_:Ncring.Ring (T:=carrierType)) in
-    lazymatch type of inst with
-    | @Ncring.Ring _ _ _ _ _ _ _ _ ?ops =>
-      lazymatch type of ops with
-        @Ncring.Ring_ops ?F ?zero ?one ?add ?mul ?sub ?opp ?eq
-        =>
-        pose ops as Hops;
-        (* (* apparently [nsatz] matches the goal to look for equalitites, so [eq] will need to become
-              [Algebra_syntax.equality]. However, reification is done using typeclasses so definitional
-              equality is enough (and faster) *)
-        change zero with (@Algebra_syntax.zero F (@Ncring.zero_notation F zero one add mul sub opp eq ops)) in *;
-        change one with (@Algebra_syntax.one F (@Ncring.one_notation F zero one add mul sub opp eq ops)) in *;
-        change add with (@Algebra_syntax.addition F (@Ncring.add_notation F zero one add mul sub opp eq ops)) in *;
-        change mul with (@Algebra_syntax.multiplication F F (@Ncring.mul_notation F zero one add mul sub opp eq ops)) in *;
-        change opp with (@Algebra_syntax.opposite F (@Ncring.opp_notation F zero one add mul sub opp eq ops)) in *;
-        change eq with (@Algebra_syntax.equality F (@Ncring.eq_notation F zero one add mul sub opp eq ops)) in *;
-        *)
-        move Hops at top (* [nsatz] requires equalities to be continuously at the bottom of the hypothesis list *)
-      end
-    end;
-    nsatz;
-    clear Hops.
-End _NsatzExportGuarantine.
-Import _NsatzExportGuarantine.
-Ltac nsatz_without_field := sane_nsatz.
+
+(*** Tactics for manipulating field equations *)
+Require Import Coq.setoid_ring.Field_tac.
+
+Ltac guess_field := 
+  match goal with
+  | |- ?eq _ _ =>  constr:(_:field (eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:field (eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:field (eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:field (eq:=eq))
+  end.
+
+Ltac common_denominator :=
+  let fld := guess_field in
+  lazymatch type of fld with
+    field (div:=?div) =>
+    lazymatch goal with
+    | |- appcontext[div] => field_simplify_eq
+    | |- _ => idtac
+    end
+  end.
+
+Ltac common_denominator_in H :=
+  let fld := guess_field in
+  lazymatch type of fld with
+    field (div:=?div) =>
+    lazymatch type of H with
+    | appcontext[div] => field_simplify_eq in H
+    | _ => idtac
+    end
+  end.
+
+Ltac common_denominator_all := 
+  common_denominator;
+  repeat match goal with [H: _ |- _ _ _ ] => common_denominator_in H end.
 
 Inductive field_simplify_done {T} : T -> Type :=
   Field_simplify_done : forall H, field_simplify_done H.
 
-Require Import Coq.setoid_ring.Field_tac.
-Ltac field_simplify_eq_all :=
+Ltac field_simplify_eq_hyps :=
   repeat match goal with
            [ H: _ |- _ ] =>
            match goal with
@@ -354,17 +358,154 @@ Ltac field_simplify_eq_all :=
          end;
   repeat match goal with [ H: field_simplify_done _ |- _] => clear H end.
 
-Ltac nsatz :=
-  field_simplify_eq_all;
-  try field_simplify_eq;
-  try nsatz_without_field.
+Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
+
+
+(*** Tactics for manipulating polynomial equations *)
+Require Nsatz.
+Require Import List.
+Open Scope core_scope.
+
+Generalizable All Variables.
+Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
+  : forall x y, eq (sub x y) zero <-> eq x y.
+Proof.
+  split;intros Hx.
+  { eapply Nsatz.psos_r1b. eapply Hx. }
+  { eapply Nsatz.psos_r1. eapply Hx. }
+Qed.
+
+Ltac get_goal := lazymatch goal with |- ?g => g end.
+
+Ltac nsatz_equation_implications_to_list eq zero g :=
+  lazymatch g with
+  | eq ?p zero => constr:(p::nil)
+  | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
+  end.
+
+Ltac nsatz_reify_equations eq zero :=
+  let g := get_goal in
+  let lb := nsatz_equation_implications_to_list eq zero g in
+  lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
+    (?variables, ?le) =>
+    lazymatch (eval compute in (List.rev le)) with
+    | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal)
+    end
+  end.
+
+Ltac nsatz_get_free_variables reified_package :=
+  lazymatch reified_package with (?fv, _, _) => fv end.
+
+Ltac nsatz_get_reified_givens reified_package :=
+  lazymatch reified_package with (_, ?givens, _) => givens end.
+
+Ltac nsatz_get_reified_goal reified_package :=
+  lazymatch reified_package with (_, _, ?goal) => goal end.
+
+Require Import Coq.setoid_ring.Ring_polynom.
+Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
+  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
+
+Ltac nsatz_compute_get_leading_coefficient :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
+  end.
+
+Ltac nsatz_compute_get_certificate :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b)
+  end.
+
+Ltac nsatz_rewrite_and_revert domain :=
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    lazymatch goal with
+    | |- eq _ zero => idtac
+    | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
+    end;
+    repeat match goal with
+           | [H : eq _ zero |- _ ] => revert H
+           | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
+           end
+  end.
+  
+Ltac nsatz_nonzero := 
+  try solve [apply Integral_domain.integral_domain_one_zero
+            |apply Integral_domain.integral_domain_minus_one_zero
+            |trivial].
+
+Ltac nsatz_domain_sugar_power domain sugar power := 
+  let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    nsatz_rewrite_and_revert domain;
+    let reified_package := nsatz_reify_equations eq zero in
+    let fv := nsatz_get_free_variables reified_package in
+    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
+    let reified_givens := nsatz_get_reified_givens reified_package in
+    let reified_goal := nsatz_get_reified_goal reified_package in
+    nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
+    let a := nsatz_compute_get_leading_coefficient in
+    let crt := nsatz_compute_get_certificate in
+    intros _ (* discard [nsatz_compute] output *); intros;
+    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
+    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
+    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
+    | solve [repeat (split; [assumption|]); exact I] ]
+  end.
+
+Ltac nsatz_guess_domain :=
+  match goal with
+  | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  end.
+
+Ltac nsatz_sugar_power sugar power :=
+  let domain := nsatz_guess_domain in
+  nsatz_domain_sugar_power domain sugar power.
+
+Tactic Notation "nsatz" constr(n) :=
+  let nn := (eval compute in (BinNat.N.of_nat n)) in
+  nsatz_sugar_power BinInt.Z0 nn.
+
+Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
+
+Ltac nsatz_contradict :=
+  intros;
+  let domain := nsatz_guess_domain in
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    assert (eq one zero) as Hbad;
+    [nsatz; nsatz_nonzero
+    |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
+  end.
+
+(*** Polynomial equations over fields *)
+
+Ltac field_algebra :=
+  intros;
+  common_denominator_all;
+  try (nsatz; dropRingSyntax);
+  repeat (apply conj);
+  try solve
+      [unfold not; intro; nsatz_contradict
+      |nsatz_nonzero].
 
 Section Example.
-  Context {F zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
+  Local Notation "0" := zero. Local Notation "1" := one.
 
   Add Field _ExampleField : (Field.field_theory_for_stdlib_tactic (T:=F)).
 
-  Example _example_field_nsatz x y z : y <> zero -> x/y = z -> z*y + y = x + y.
-  Proof. intros. nsatz. assumption. Qed.
+  Example _example_nsatz x y : 1+1 <> 0 -> x + y = 0 -> x - y = 0 -> x = 0.
+  Proof. field_algebra. Qed.
+
+  Example _example_field_nsatz x y z : y <> 0 -> x/y = z -> z*y + y = x + y.
+  Proof. field_algebra. Qed.
+
+  Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0).
+  Proof. intros. intro. nsatz_contradict. Qed.
 End Example.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 7cb05158d..e63aad34d 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,6 +1,5 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
-Close Scope nat_scope. Close Scope type_scope. Close Scope core_scope.
-Require Import Crypto.SaneField.
+Require Import Crypto.Algebra.
 
 Generalizable All Variables.
 Section Pre.
@@ -15,7 +14,7 @@ Section Pre.
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
 
   Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}.
-  Context {d:F} {d_nonsquare : forall x, x^2 <> d}.
+  Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}.
   Context {char_gt_2 : 1+1 <> 0}.
   
   (* the canonical definitions are in Spec *)
@@ -25,23 +24,24 @@ Section Pre.
     let (x2, y2) := P2' in
     pair (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
 
-  Ltac admit_nonzero := abstract (repeat split; match goal with |- not (eq _ 0) => admit end).
+  Lemma opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0. Admitted.
+
+  Hint Extern 0 (not (eq _ 0)) => apply opp_nonzero_nonzero : field_algebra.
+
+  Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
 
   Lemma edwardsAddComplete' x1 y1 x2 y2 :
     onCurve (pair x1 y1) ->
     onCurve (pair x2 y2) ->
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
-    unfold onCurve, not; intros.
-    assert (d * x1 ^2 * y1 ^2 * (a * x2 ^2 + y2 ^2) = a * x1 ^2 + y1 ^2) as Heqt by nsatz.
-    destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
+    unfold onCurve, not; use_sqrt_a; intros.
     destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0);
       lazymatch goal with
       | [H: not (eq (?f (sqrt_a * x2)  y2) 0) |- _ ]
-        => eapply (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) / (x1 * y1 * (f (sqrt_a * x2)  y2))  ));
-             nsatz; admit_nonzero
-      | _ => apply a_nonzero; (do 2 nsatz) (* TODO: why does it not win on the first call? *)
-      end.
+        => apply d_nonsquare with (sqrt_d:=(f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) / (x1 * y1 * (f (sqrt_a * x2) y2)))
+      | _ => apply a_nonzero
+      end; field_algebra; auto using opp_nonzero_nonzero.
   Qed.
 
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
@@ -49,11 +49,7 @@ Section Pre.
     onCurve (x2, y2) ->
     (1 + d*x1*x2*y1*y2) <> 0.
   Proof.
-    intros Hc1 Hc2; simpl in Hc1, Hc2.
-    intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H].
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
-    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
-      intro Hz; rewrite Hz in H; intuition.
+    intros H1 H2 ?. apply (edwardsAddComplete' x1 y1 x2 y2 H1 H2); field_algebra.
   Qed.
   
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
@@ -61,16 +57,14 @@ Section Pre.
     onCurve (x2, y2) ->
     (1 - d*x1*x2*y1*y2) <> 0.
   Proof.
-    intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H].
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
-    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
-      intro Hz; rewrite Hz in H; apply H; field.
+    intros H1 H2 ?. apply (edwardsAddComplete' x1 y1 x2 y2 H1 H2); field_algebra.
   Qed.
   
   Definition zeroOnCurve : onCurve (0, 1).
-    simpl. field.
+    simpl. field_algebra.
   Qed.
   
+  (* TODO: port
   Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
     (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
     onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
@@ -119,4 +113,5 @@ Section Pre.
     remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
     eapply unifiedAdd'_onCurve'; eauto.
   Qed.
+  *)
 End Pre.
\ No newline at end of file