{"action":"created","comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments/73560120","id":73560120,"diff_hunk":"@@ -68,680 +34,326 @@ Ltac demod :=\n            notFancy y; rewrite (Zmult_mod_idemp_r y)\n          | [ |- context[(?x mod _) mod _] ] =>\n            notFancy x; rewrite (Zmod_mod x)\n-         | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in *\n          end.\n \n-(* Remove exists under equals: we do this a lot *)\n-Ltac eq_remove_proofs := lazymatch goal with\n-| [ |- @eq (F _) ?a ?b ] =>\n-    assert (Q := F_eq a b);\n-    simpl in *; apply Q; clear Q\n-end.\n-\n-(** TODO FIXME(from jgross): This tactic is way too powerful for\n-    arcane reasons.  It should not be using so many databases with\n-    [intuition]. *)\n-Ltac Fdefn :=\n+Ltac unwrap_F :=\n   intros;\n   repeat match goal with [ x : F _ |- _ ] => destruct x end;\n-  try eq_remove_proofs;\n-  demod;\n-  rewrite ?Z.mul_1_l;\n-  intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ].\n-\n-Local Open Scope F_scope.\n-\n-Section FEquality.\n-  Context {m:Z}.\n-\n-  (** Equality **)\n-  Definition F_eqb (x y : F m) : bool :=  Z.eqb x y.\n-\n-  Lemma F_eqb_eq x y : F_eqb x y = true -> x = y.\n-  Proof.\n-    unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial.\n-  Qed.\n-\n-  Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true.\n-  Proof.\n-    intros; subst; apply Z.eqb_refl.\n-  Qed.\n-\n-  Lemma F_eqb_refl : forall x, F_eqb x x = true.\n-  Proof.\n-    intros; apply F_eqb_complete; trivial.\n-  Qed.\n-\n-  Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y.\n-  Proof.\n-    intuition; subst y.\n-    pose proof (F_eqb_refl x).\n-    congruence.\n-  Qed.\n-\n-  Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false.\n-  Proof.\n-    intros.\n-    case_eq (F_eqb x y); intros; trivial.\n-    pose proof (F_eqb_eq x y); intuition.\n-  Qed.\n-\n-  Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}.\n-  Proof.\n-    intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq.\n-  Qed.\n-\n-  Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b).\n-  Proof.\n-    intros; intuition; break_if.\n-    - rewrite F_eqb_complete; trivial.\n-    - rewrite F_eqb_neq_complete; trivial.\n-  Defined.\n-End FEquality.\n-\n-Section FandZ.\n-  Context {m:Z}.\n-\n-  Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m).\n-  Proof.\n-    intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith.\n-  Qed.\n-\n-  Require Crypto.Algebra.\n-  Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.\n-  Proof.\n-    repeat split; Fdefn; try apply F_eq_dec.\n-    { rewrite Z.add_0_r. auto. }\n-    { rewrite Z.mul_1_r. auto. }\n-  Qed.\n-\n-  Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma ZToField_0 : @ZToField m 0 = 0.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma mod_FieldToZ : forall x,  (@FieldToZ m x) mod m = FieldToZ x.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  (** ZToField distributes over operations **)\n-  Lemma ZToField_add : forall (x y : Z),\n-      @ZToField m (x + y) = ZToField x + ZToField y.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma FieldToZ_add : forall x y : F m,\n-      FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma FieldToZ_mul : forall x y : F m,\n-      FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma FieldToZ_pow_Zpow_mod : forall (x : F m) n,\n-    (FieldToZ x ^ Z.of_N n mod m = FieldToZ (x ^ n)%F)%Z.\n-  Proof.\n-    intros.\n-    induction n using N.peano_ind;\n-      destruct (F_pow_spec x) as [pow_0 pow_succ] . {\n-      rewrite pow_0.\n-      rewrite Z.pow_0_r; auto.\n-    } {\n-      rewrite N2Z.inj_succ.\n-      rewrite Z.pow_succ_r by apply N2Z.is_nonneg.\n-      rewrite <- N.add_1_l.\n-      rewrite pow_succ.\n-      rewrite <- Zmult_mod_idemp_r.\n-      rewrite IHn.\n-      apply FieldToZ_mul.\n-    }\n-  Qed.\n-\n-  Lemma FieldToZ_pow_efficient : forall (x : F m) n, FieldToZ (x^n) = powmod m (FieldToZ x) n.\n-  Proof.\n-    intros.\n-    rewrite powmod_Zpow_mod.\n-    rewrite <-FieldToZ_pow_Zpow_mod.\n-    reflexivity.\n-  Qed.\n-\n-  Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n.\n-  Proof.\n-    induction n using N.peano_ind;\n-      destruct (F_pow_spec x) as [pow_0 pow_succ];\n-      rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ;\n-      simpl; congruence.\n-  Qed.\n-\n-  Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->\n-                                     b mod m =  (- a)  mod m.\n-  Proof.\n-    rewrite <-Z.sub_0_l; intros.\n-    replace (0-a)%Z with (b-(a + b))%Z by omega.\n-    rewrite Zminus_mod.\n-    rewrite <- H.\n-    rewrite Zmod_0_l.\n-    replace (b mod m - 0)%Z with (b mod m) by omega.\n-    rewrite Zmod_mod.\n-    reflexivity.\n-  Qed.\n-\n-  Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m.\n-  Proof.\n-    intros.\n-    pose proof (FieldToZ_add x (opp x)) as H.\n-    rewrite F_opp_spec, FieldToZ_ZToField in H.\n-    auto using mod_plus_zero_subproof.\n-  Qed.\n-\n-  Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m.\n-  Proof.\n-    intros.\n-    pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial.\n-  Qed.\n-\n-  Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.\n-  Proof.\n-    intros.\n-    replace (x + (m - y))%Z with (m+(x-y))%Z by omega.\n-    rewrite Zplus_mod.\n-    rewrite Z_mod_same_full; simpl Z.add.\n-    rewrite Zmod_mod.\n-    reflexivity.\n-  Qed.\n-\n-  (* Compatibility between inject and subtraction *)\n-  Lemma ZToField_sub : forall (x y : Z),\n-      @ZToField m (x - y) = ZToField x - ZToField y.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  (* Compatibility between inject and multiplication *)\n-  Lemma ZToField_mul : forall (x y : Z),\n-      @ZToField m (x * y) = ZToField x * ZToField y.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  (* Compatibility between inject and GFtoZ *)\n-  Lemma ZToField_idempotent : forall (x : F m), ZToField x = x.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-  Definition ZToField_FieldToZ := ZToField_idempotent. (* alias *)\n-\n-  (* Compatibility between inject and mod *)\n-  Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m).\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  (* Compatibility between inject and pow *)\n-  Lemma ZToField_pow : forall x n,\n-    @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m).\n-  Proof.\n-    intros.\n-    induction n using N.peano_ind;\n-      destruct (F_pow_spec (@ZToField m x)) as [pow_0 pow_succ] . {\n-      rewrite pow_0.\n-      Fdefn.\n-    } {\n-      rewrite N2Z.inj_succ.\n-      rewrite Z.pow_succ_r by apply N2Z.is_nonneg.\n-      rewrite <- N.add_1_l.\n-      rewrite pow_succ.\n-      rewrite IHn.\n-      Fdefn.\n-    }\n-  Qed.\n-\n-  Lemma ZToField_eqmod : forall x y : Z, x mod m = y mod m -> ZToField x = @ZToField m y.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma FieldToZ_nonzero:\n-    forall x0 : F m, x0 <> 0 -> FieldToZ x0 <> 0%Z.\n-  Proof.\n-    intros x0 Hnz Hz.\n-    rewrite <- Hz, ZToField_FieldToZ in Hnz; auto.\n-  Qed.\n-\n-End FandZ.\n-\n-Section RingModuloPre.\n-  Context {m:Z}.\n-  Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.\n-  (* Substitution to prove all Compats *)\n-  Ltac compat := repeat intro; subst; trivial.\n-\n-  Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  Instance Fopp_compat : Proper (eq==>eq) (@opp m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  Instance Finv_compat : Proper (eq==>eq) (@inv m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m).\n-  Proof.\n-    compat.\n-  Qed.\n-\n-  (***** Ring Theory *****)\n-  Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq.\n-  Proof.\n-    constructor; Fdefn.\n-  Qed.\n-\n-  Lemma F_mul_1_r:\n-    forall x : F m, x * 1 = x.\n-  Proof.\n-    Fdefn; rewrite Z.mul_1_r; auto.\n-  Qed.\n-\n-  Lemma F_mul_assoc:\n-    forall x y z : F m, x * (y * z) = x * y * z.\n-  Proof.\n-    Fdefn.\n-  Qed.\n-\n-  Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.\n-  Proof.\n-    destruct (F_pow_spec x) as [HO HS]; intros.\n-    destruct n; auto; unfold id.\n-    rewrite Pre.N_pos_1plus at 1.\n-    rewrite HS.\n-    simpl.\n-    induction p using Pos.peano_ind.\n-    - simpl. rewrite HO; apply F_mul_1_r.\n-    - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ F_mul_assoc x).\n-      rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS.\n-      f_equal.\n-  Qed.\n-\n-  (***** Power theory *****)\n-  Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m).\n-  Proof.\n-    constructor; apply F_pow_pow_N.\n-  Qed.\n-\n-  (***** Division Theory *****)\n-  Definition Fquotrem(a b: F m): F m * F m :=\n-    let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m).\n-  Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.\n-  Proof.\n-    constructor; intros; unfold Fquotrem, id.\n-\n-    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by\n-      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).\n-\n-    Fdefn; rewrite <-Z.quot_rem'; trivial.\n-  Qed.\n-\n-  Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z.\n-    intros.\n-    rewrite Zmult_mod, Z_mod_same_full.\n-    rewrite Z.mul_0_r, Zmod_0_l.\n-    reflexivity.\n-  Qed.\n-\n-  Lemma Z_mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->\n-                                       (-x) mod m =   y  mod m.\n-  Proof.\n-    intros.\n-    rewrite <-Z.sub_0_l.\n-    rewrite Zminus_mod. rewrite H.\n-    rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.\n-    destruct y; auto.\n-  Qed.\n-\n-  Lemma Z_opp_opp : forall x : Z, (-(-x)) = x.\n-    destruct x; auto.\n-  Qed.\n-\n-  Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.\n-    intros.\n-    apply Z_mod_opp_equiv.\n-    rewrite Z_opp_opp.\n-    demod; auto.\n-  Qed.\n-\n-  (* Define a \"ring morphism\" between GF and Z, i.e. an equivalence\n-   * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.\n-   *\n-   * Doing this allows us to do our coefficient manipulations in Z\n-   * rather than GF, because we know it's equivalent to inject the\n-   * result afterward.\n-   *)\n-  Lemma Fring_morph:\n-      ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq\n-                 0%Z 1%Z Z.add    Z.mul    Z.sub    Z.opp  Z.eqb\n-                 (@ZToField m).\n-  Proof.\n-    constructor; intros; try Fdefn; unfold id;\n-      try (apply gf_eq; simpl; intuition).\n-    - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity.\n-    - rewrite (proj1 (Z.eqb_eq x y)); trivial.\n-  Qed.\n-\n-  (* Redefine our division theory under the ring morphism *)\n-  Lemma Fmorph_div_theory:\n+  lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *;\n+  try apply eqsig_eq;\n+  demod.\n+\n+(* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *)\n+Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.\n+\n+Global Instance commutative_ring_modulo m\n+  : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul.\n+Proof.\n+  repeat (split || intro); unwrap_F;\n+    autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence].\n+Qed.\n+\n+\n+Module Zmod.\n+  Lemma pow_spec {m} a : pow a 0%N = 1%F :> F m /\\ forall x, pow a (1 + x)%N = mul a (pow a x).\n+  Proof. change (@pow m) with (proj1_sig (@pow_with_spec m)); destruct (@pow_with_spec m); eauto. Qed.\n+\n+  Section FandZ.\n+    Context {m:Z}.\n+    Local Open Scope F_scope.\n+\n+    Theorem eq_FieldToZ_iff (x y : F m) : x = y <-> FieldToZ x = FieldToZ y.\n+    Proof. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed.\n+\n+    Lemma eq_ZToField_iff : forall x y : Z, x mod m = y mod m <-> ZToField m x = ZToField m y.\n+    Proof. split; unwrap_F; congruence. Qed.\n+\n+    \n+    Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m.\n+    Proof. unwrap_F; trivial. Qed.\n+\n+    Lemma ZToField_FieldToZ x : ZToField m (FieldToZ x) = x :> F m.\n+    Proof. unwrap_F; congruence. Qed.\n+\n+    \n+    Lemma ZToField_mod : forall x, ZToField m x = ZToField m (x mod m).\n+    Proof. unwrap_F; trivial. Qed.\n+\n+    Lemma mod_FieldToZ : forall (x:F m),  FieldToZ x mod m = FieldToZ x.\n+    Proof. unwrap_F. congruence. Qed.\n+\n+    Lemma FieldToZ_0 : FieldToZ (0:F m) = 0%Z.\n+    Proof. unwrap_F. apply Zmod_0_l. Qed.\n+\n+    Lemma ZToField_small_nonzero z : (0 < z < m)%Z -> ZToField m z <> 0.\n+    Proof. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed.\n+\n+    Lemma FieldToZ_nonzero (x:F m) : x <> 0 -> FieldToZ x <> 0%Z.\n+    Proof. intros Hnz Hz. rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. Qed.\n+\n+    Lemma FieldToZ_range (x : F m) : 0 < m -> 0 <= x < m.\n+    Proof. intros. rewrite <- mod_FieldToZ. apply Z.mod_pos_bound. trivial. Qed.\n+\n+    Lemma FieldToZ_nonzero_range (x : F m) : (x <> 0) -> 0 < m -> (1 <= x < m)%Z.\n+    Proof.\n+      unfold not; intros Hnz Hlt.\n+      rewrite eq_FieldToZ_iff, FieldToZ_0 in Hnz; pose proof (FieldToZ_range x Hlt).\n+      omega.\n+    Qed.\n+\n+    Lemma ZToField_add : forall (x y : Z),\n+        ZToField m (x + y) = ZToField m x + ZToField m y.\n+    Proof. unwrap_F; trivial. Qed.\n+\n+    Lemma FieldToZ_add : forall x y : F m,\n+        FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z.\n+    Proof. unwrap_F; trivial. Qed.\n+\n+    Lemma ZToField_mul x y : ZToField m (x * y) = ZToField _ x * ZToField _ y :> F m.\n+    Proof. unwrap_F. trivial. Qed.\n+\n+    Lemma FieldToZ_mul : forall x y : F m,\n+        FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z.\n+    Proof. unwrap_F; trivial. Qed.\n+    \n+    Lemma ZToField_sub x y : ZToField _ (x - y) = ZToField _ x - ZToField _ y :> F m.\n+    Proof. unwrap_F. trivial. Qed.\n+\n+    Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m.\n+    Proof. unwrap_F; trivial. Qed.\n+\n+    Lemma ZToField_pow x n : ZToField _ x ^ n = ZToField _ (x ^ (Z.of_N n) mod m) :> F m.\n+    Proof.\n+      intros.\n+      induction n using N.peano_ind;\n+        destruct (pow_spec (@ZToField m x)) as [pow_0 pow_succ] . {\n+        rewrite pow_0.\n+        unwrap_F; trivial.\n+      } {\n+        rewrite N2Z.inj_succ.\n+        rewrite Z.pow_succ_r by apply N2Z.is_nonneg.\n+        rewrite <- N.add_1_l.\n+        rewrite pow_succ.\n+        rewrite IHn.\n+        unwrap_F; trivial.\n+      }\n+    Qed.\n+\n+    Lemma FieldToZ_pow : forall (x : F m) n,\n+        FieldToZ (x ^ n)%F = (FieldToZ x ^ Z.of_N n mod m)%Z.\n+    Proof.\n+      intros.\n+      symmetry.\n+      induction n using N.peano_ind;\n+        destruct (pow_spec x) as [pow_0 pow_succ] . {\n+        rewrite pow_0, Z.pow_0_r; auto.\n+      } {\n+        rewrite N2Z.inj_succ.\n+        rewrite Z.pow_succ_r by apply N2Z.is_nonneg.\n+        rewrite <- N.add_1_l.\n+        rewrite pow_succ.\n+        rewrite <- Zmult_mod_idemp_r.\n+        rewrite IHn.\n+        apply FieldToZ_mul.\n+      }\n+    Qed.\n+\n+    Lemma square_iff (x:F m) :\n+      (exists y : F m, y * y = x) <-> (exists y : Z, y * y mod m = x)%Z.\n+    Proof.\n+      setoid_rewrite eq_FieldToZ_iff; setoid_rewrite FieldToZ_mul; split; intro H; destruct H as [x' H].\n+      - eauto.\n+      - exists (ZToField _ x'); rewrite !FieldToZ_ZToField; demod; auto.\n+    Qed.\n+\n+    (* TODO: move to ZUtil *)","path":"src/ModularArithmetic/ModularArithmeticTheorems.v","position":585,"original_position":585,"commit_id":"5e8b12bf42b1925306ebd61be5c90d60059c1d51","original_commit_id":"5e8b12bf42b1925306ebd61be5c90d60059c1d51","user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"body":"This lemma was dead code, I deleted it.","created_at":"2016-08-04T16:53:10Z","updated_at":"2016-08-04T16:53:10Z","html_url":"https://github.com/mit-plv/fiat-crypto/pull/40#discussion_r73560120","pull_request_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40","_links":{"self":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments/73560120"},"html":{"href":"https://github.com/mit-plv/fiat-crypto/pull/40#discussion_r73560120"},"pull_request":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40"}}},"pull_request":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40","id":79281868,"html_url":"https://github.com/mit-plv/fiat-crypto/pull/40","diff_url":"https://github.com/mit-plv/fiat-crypto/pull/40.diff","patch_url":"https://github.com/mit-plv/fiat-crypto/pull/40.patch","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/40","number":40,"state":"open","locked":false,"title":"Refactor ModularArithmetic into Zmod, expand Decidable","user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars.githubusercontent.com/u/918403?v=3","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"body":"ModularArithmetic now uses Algebra lemmas in various places instead of\r\ncustom manual proofs. Similarly, Util.Decidable is used to state and\r\nprove the relevant decidability results.\r\n\r\nBackwards-incompatible changes:\r\n\r\nF_some_lemma -> Zmod.some_lemma\r\nArguments ZToField _%Z _%Z : clear implicits.\r\ninv_spec says inv x * x = 1, not x * inv x = 1","created_at":"2016-07-28T22:50:41Z","updated_at":"2016-08-04T16:53:10Z","closed_at":null,"merged_at":null,"merge_commit_sha":"8bac8bf5f9fd0ba34b1c6e977b7677d7a4bfcd1d","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40/commits","review_comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40/comments","review_comment_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments{/number}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/40/comments","statuses_url":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/5e8b12bf42b1925306ebd61be5c90d60059c1d51","head":{"label":"mit-plv:modular-arithmetic-refactor","ref":"modular-arithmetic-refactor","sha":"5e8b12bf42b1925306ebd61be5c90d60059c1d51","user":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars.githubusercontent.com/u/11860253?v=3","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"repo":{"id":42269036,"name":"fiat-crypto","full_name":"mit-plv/fiat-crypto","owner":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars.githubusercontent.com/u/11860253?v=3","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/mit-plv/fiat-crypto","description":"Cryptographic Primitive Code Generation in Fiat","fork":false,"url":"https://api.github.com/repos/mit-plv/fiat-crypto","forks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/forks","keys_url":"https://api.github.com/repos/mit-plv/fiat-crypto/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mit-plv/fiat-crypto/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mit-plv/fiat-crypto/teams","hooks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/hooks","issue_events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/events{/number}","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/events","assignees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/assignees{/user}","branches_url":"https://api.github.com/repos/mit-plv/fiat-crypto/branches{/branch}","tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/tags","blobs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/refs{/sha}","trees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/{sha}","languages_url":"https://api.github.com/repos/mit-plv/fiat-crypto/languages","stargazers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/stargazers","contributors_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contributors","subscribers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscribers","subscription_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscription","commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/commits{/sha}","git_commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/commits{/sha}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/comments{/number}","issue_comment_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments{/number}","contents_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contents/{+path}","compare_url":"https://api.github.com/repos/mit-plv/fiat-crypto/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mit-plv/fiat-crypto/merges","archive_url":"https://api.github.com/repos/mit-plv/fiat-crypto/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mit-plv/fiat-crypto/downloads","issues_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues{/number}","pulls_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls{/number}","milestones_url":"https://api.github.com/repos/mit-plv/fiat-crypto/milestones{/number}","notifications_url":"https://api.github.com/repos/mit-plv/fiat-crypto/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/labels{/name}","releases_url":"https://api.github.com/repos/mit-plv/fiat-crypto/releases{/id}","deployments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/deployments","created_at":"2015-09-10T20:29:16Z","updated_at":"2016-06-25T23:32:17Z","pushed_at":"2016-08-04T16:34:12Z","git_url":"git://github.com/mit-plv/fiat-crypto.git","ssh_url":"git@github.com:mit-plv/fiat-crypto.git","clone_url":"https://github.com/mit-plv/fiat-crypto.git","svn_url":"https://github.com/mit-plv/fiat-crypto","homepage":null,"size":2143,"stargazers_count":7,"watchers_count":7,"language":"Coq","has_issues":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":4,"mirror_url":null,"open_issues_count":11,"forks":4,"open_issues":11,"watchers":7,"default_branch":"master"}},"base":{"label":"mit-plv:master","ref":"master","sha":"09f49b6eb74caf65e552fcf70a23d11e6fa62133","user":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars.githubusercontent.com/u/11860253?v=3","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"repo":{"id":42269036,"name":"fiat-crypto","full_name":"mit-plv/fiat-crypto","owner":{"login":"mit-plv","id":11860253,"avatar_url":"https://avatars.githubusercontent.com/u/11860253?v=3","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/mit-plv/fiat-crypto","description":"Cryptographic Primitive Code Generation in Fiat","fork":false,"url":"https://api.github.com/repos/mit-plv/fiat-crypto","forks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/forks","keys_url":"https://api.github.com/repos/mit-plv/fiat-crypto/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mit-plv/fiat-crypto/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mit-plv/fiat-crypto/teams","hooks_url":"https://api.github.com/repos/mit-plv/fiat-crypto/hooks","issue_events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/events{/number}","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/events","assignees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/assignees{/user}","branches_url":"https://api.github.com/repos/mit-plv/fiat-crypto/branches{/branch}","tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/tags","blobs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/refs{/sha}","trees_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/{sha}","languages_url":"https://api.github.com/repos/mit-plv/fiat-crypto/languages","stargazers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/stargazers","contributors_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contributors","subscribers_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscribers","subscription_url":"https://api.github.com/repos/mit-plv/fiat-crypto/subscription","commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/commits{/sha}","git_commits_url":"https://api.github.com/repos/mit-plv/fiat-crypto/git/commits{/sha}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/comments{/number}","issue_comment_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments{/number}","contents_url":"https://api.github.com/repos/mit-plv/fiat-crypto/contents/{+path}","compare_url":"https://api.github.com/repos/mit-plv/fiat-crypto/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mit-plv/fiat-crypto/merges","archive_url":"https://api.github.com/repos/mit-plv/fiat-crypto/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mit-plv/fiat-crypto/downloads","issues_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues{/number}","pulls_url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls{/number}","milestones_url":"https://api.github.com/repos/mit-plv/fiat-crypto/milestones{/number}","notifications_url":"https://api.github.com/repos/mit-plv/fiat-crypto/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/labels{/name}","releases_url":"https://api.github.com/repos/mit-plv/fiat-crypto/releases{/id}","deployments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/deployments","created_at":"2015-09-10T20:29:16Z","updated_at":"2016-06-25T23:32:17Z","pushed_at":"2016-08-04T16:34:12Z","git_url":"git://github.com/mit-plv/fiat-crypto.git","ssh_url":"git@github.com:mit-plv/fiat-crypto.git","clone_url":"https://github.com/mit-plv/fiat-crypto.git","svn_url":"https://github.com/mit-plv/fiat-crypto","homepage":null,"size":2143,"stargazers_count":7,"watchers_count":7,"language":"Coq","has_issues":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":4,"mirror_url":null,"open_issues_count":11,"forks":4,"open_issues":11,"watchers":7,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40"},"html":{"href":"https://github.com/mit-plv/fiat-crypto/pull/40"},"issue":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/40"},"comments":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/40/comments"},"review_comments":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40/comments"},"review_comment":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/40/commits"},"statuses":{"href":"https://api.github.com/repos/mit-plv/fiat-crypto/statuses/5e8b12bf42b1925306ebd61be5c90d60059c1d51"}}}}
{"actor":{"display_login":"andres-erbsen"}}