Merge branch 'master' of github.mit.edu:plv/fiat-crypto

2 files changed, 185 insertions, 31 deletions

diff --git a/src/Scratch/fermat.v b/src/Scratch/fermat.v
new file mode 100644
index 000000000..7871db92f
--- /dev/null
+++ b/src/Scratch/fermat.v
@@ -0,0 +1,185 @@
+Require Import NPeano.
+Require Import List.
+Require Import Sorting.Permutation.
+Require Import BinInt.
+Require Import Util.ListUtil.
+Require Znumtheory.
+
+Lemma all_neq_NoDup : forall {T} (xs:list T),
+  (forall i j x y,
+  nth_error xs i = Some x ->
+  nth_error xs j = Some y ->
+  i <> j -> x <> y) <->  NoDup xs.
+Admitted.
+
+Definition F (q:nat) := { n : nat | n = n mod q}.
+ 
+Section Fq.
+  Context {q : nat}.
+  Axiom q_prime : Znumtheory.prime (Z.of_nat q).
+  Let Fq := F q.
+
+  Lemma q_is_succ : q = S (q-1). Admitted.
+
+  Definition natToField (n:nat) : Fq. exists (n mod q). abstract admit. Defined.
+  Definition fieldToNat (n:Fq) : nat := proj1_sig n.
+  Coercion fieldToNat : Fq >-> nat.
+
+  Definition zero : Fq. exists 0. abstract admit. Defined.
+  Definition one : Fq. exists 1. abstract admit. Defined.
+
+  Definition add (a b: Fq) : Fq.  exists (a+b mod q); abstract admit. Defined.
+  Infix "+" := add.
+  Definition mul (a b: Fq) : Fq.  exists (a*b mod q); abstract admit. Defined.
+  Infix "*" := mul.
+  Definition pow (a:Fq) (n:nat) : Fq. exists (pow a n mod q). abstract admit. Defined.
+  Infix "^" := pow.
+
+  Axiom opp : Fq -> Fq.
+  Axiom opp_spec : forall a, opp a + a = zero.
+  Definition sub a b := add a (opp b).
+  Infix "-" := sub.
+
+  Axiom inv : Fq -> Fq.
+  Axiom inv_spec : forall a, inv a * a = one.
+  Definition div a b := add a (inv b).
+  Infix "/" := div.
+
+  Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end.
+  Definition prod := fold_right mul one.
+
+  Lemma mul_one_l : forall a, one * a = a. Admitted.
+  Lemma mul_one_r : forall a, a * one = a. Admitted.
+
+  Lemma mul_cancel_l : forall a, a <> zero -> forall b c, a * b = a * c -> b = c. Admitted.
+  Lemma mul_cancel_r : forall a, a <> zero -> forall b c, b * a = c * c -> b = c. Admitted.
+  Lemma mul_cancel_l_1 : forall a, a <> zero -> forall b, a * b = a -> b = one. Admitted.
+  Lemma mul_cancel_r_1 : forall a, a <> zero -> forall b, b * a = a -> b = one. Admitted.
+  
+  Lemma mul_0_why : forall a b, a * b = zero -> a = zero \/ b = zero. Admitted.
+
+  Lemma mul_assoc : forall a b c, a * (b * c) = a * b * c. Admitted.
+  Lemma mul_assoc_pairs' : forall a b c d, (a * b) * (c * d) = a * (c * (b * d)). Admitted.
+
+  Lemma div_cancel : forall a, a <> zero -> forall b c, b / a = c / a -> b = c. Admitted.
+  Lemma div_cancel_neq : forall a, a <> zero -> forall b c, b / a <> c / a -> b <> c. Admitted.
+
+  Lemma div_mul : forall a, a <> zero -> forall b, (a * b) / a = b. Admitted.
+
+  Hint Resolve mul_assoc.
+  Hint Rewrite div_mul.
+
+  Lemma pow_zero : forall (n:nat), zero^n = zero. Admitted.
+
+  Lemma pow_S : forall a n, a ^ S n = a * a ^ n. Admitted.
+
+  Lemma prod_replicate : forall a n, a ^ n = prod (replicate n a). Admitted.
+
+  Lemma prod_perm : forall xs ys, Permutation xs ys -> prod xs = prod ys. Admitted.
+
+  Hint Resolve pow_zero mul_one_l mul_one_r prod_replicate.
+
+
+  Definition F_eq_dec : forall (a b:Fq), {a = b} + {a <> b}. Admitted.
+
+  Definition elements : list Fq := map natToField (seq 0 q).
+  Lemma elements_all : forall (a:Fq), In a elements. Admitted.
+  Lemma elements_unique : forall (a:Fq), NoDup elements. Admitted.
+  Lemma length_elements : length elements = q. Admitted.
+
+  Definition invertibles : list Fq := map natToField (seq 1 (q-1)%nat).
+  Lemma invertibles_all : forall (a:Fq), a <> zero -> In a invertibles. Admitted.
+  Lemma invertibles_unique : NoDup invertibles. Admitted.
+  Lemma prod_invertibles_nonzero : prod invertibles <> zero. Admitted.
+  Lemma length_invertibles : length invertibles = (q-1)%nat. Admitted.
+
+  Hint Resolve invertibles_unique.
+
+  Section FermatsLittleTheorem.
+    Variable a : Fq.
+    Axiom a_nonzero : a <> zero.
+    Hint Resolve a_nonzero.
+
+    Definition bag := map (mul a) invertibles.
+    Lemma bag_unique : NoDup bag.
+    Proof.
+      unfold bag; intros.
+      eapply all_neq_NoDup; intros.
+      eapply div_cancel_neq; eauto.
+      eapply all_neq_NoDup; eauto;
+      match goal with
+      | [H: nth_error (map _ _) ?i = Some _ |- _ ] =>
+        destruct (nth_error_map _ _ _ _ _ _ H) as [t [HtIn HtEq]]; rewrite <- HtEq; autorewrite with core; auto
+      end.
+    Qed.
+
+    Lemma bag_invertibles : forall b, b <> zero -> In b bag.
+    Proof.
+      unfold bag; intros.
+      assert (b/a <> zero) as Hdnz by admit.
+      replace b with (a * (b/a)) by admit.
+      destruct (In_nth_error_value _ _ (invertibles_all _ Hdnz)).
+      eauto using nth_error_value_In, map_nth_error.
+    Qed.
+
+    Lemma In_bag_equiv_In_invertibles : forall b, In b bag <-> In b invertibles.
+    Proof.
+      unfold bag; intros.
+      case (F_eq_dec b zero); intuition; subst;
+          eauto using invertibles_all, bag_invertibles;
+          repeat progress match goal with
+          | [ H : In _ (map _ _) |- _ ] => rewrite in_map_iff in H; destruct H;
+              pose proof a_nonzero; intuition
+          | [ H : ?a * ?b = zero |- _ ] => destruct (mul_0_why a b H); clear H;
+              intuition; try solve [subst; auto]
+          end.
+      assert (In zero invertibles -> In zero (map (mul a) invertibles)) by admit; auto.
+    Qed.
+
+    Lemma bag_perm_elements : Permutation bag invertibles.
+    Proof.
+      eauto using NoDup_Permutation, bag_unique, invertibles_unique, In_bag_equiv_In_invertibles.
+    Qed.
+
+    Hint Resolve prod_perm bag_perm_elements.
+    Lemma prod_bag_ref : prod bag = prod invertibles.
+    Proof.
+      auto.
+    Qed.
+
+    Lemma prod_bag_interspersed : prod (flat_map (fun b => a::b::nil) invertibles) = prod invertibles.
+    Proof.
+      intros.
+      rewrite <- prod_bag_ref.
+      unfold bag.
+      induction invertibles; auto; simpl.
+      rewrite IHl.
+      auto.
+    Qed.
+
+    Lemma prod_bag_sorted : prod (replicate (q-1)%nat a) * prod invertibles = prod invertibles.
+      rewrite <- length_invertibles.
+      rewrite <- prod_bag_interspersed at 2.
+      induction invertibles; auto; simpl.
+      rewrite mul_assoc_pairs'; repeat f_equal; auto.
+    Qed.
+      
+    Theorem fermat' : a <> zero -> a^(q-1) = one.
+    Proof.
+      rewrite prod_replicate; eauto using mul_cancel_r_1, prod_bag_sorted, prod_invertibles_nonzero.
+    Qed.
+  End FermatsLittleTheorem.
+
+  Theorem fermat (a:Fq) : a^q = a.
+  Proof.
+    case (F_eq_dec a zero); intros; subst; auto.
+    rewrite q_is_succ, pow_S, fermat'; auto.
+  Qed.
+End Fq.
+Arguments fermat' : default implicits.
+Arguments fermat : default implicits.
+Arguments elements : default implicits.
+Arguments invertibles : default implicits.
+
+Print Assumptions fermat.
+Check fermat.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index d30d1f7fe..235c34a9b 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -304,37 +304,6 @@ Section GF25519Base25Point5Formula.
     clear HmulRef Hh Hf Hg.
     existsFromEquations r.
     split; auto; congruence.
-
-    (* Here's the tactic code I added at this point at the end of the old version.
-     * Erase after reading, since it isn't needed anymore.
-
-    replace ([r0; r1; r2; r3; r4; r5; r6; r7; r8; r9]) with r; unfold rep; auto.
-
-    subst r.
-
-    Ltac rsubstBoth := repeat (match goal with [ |- ?a = ?b] => subst a; subst b; repeat progress f_equal || reflexivity end).
-    Ltac t := f_equal; abstract rsubstBoth || (try t).
-
-    Time t.
-    
-
-    (* But there's a nicer way! *)
-    Undo 2.
-
-    (* This tactic finds an [x := e] hypothesis and adds a matching [x = e] hypothesis. *)
-    Ltac letToEquality :=
-      match goal with
-      | [ x := ?e |- _ ] =>
-        match goal with
-        | [ _ : x = e |- _ ] => fail 1 (* To avoid infinite loop, make sure we didn't already do this one! *)
-        | _ => assert (x = e) by reflexivity
-        end
-      end.
-
-    (* Repeated introduction of those equalities enables [congruence] to solve the goal. *)
-    Ltac smarter_congruence := repeat letToEquality; congruence.
-
-    Time smarter_congruence.*)
   Defined.
 End GF25519Base25Point5Formula.