diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/BaseSystem.v | 25 | ||||
| -rw-r--r-- | src/BaseSystemProofs.v | 26 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 53 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pre.v | 9 | ||||
| -rw-r--r-- | src/Testbit.v | 3 | ||||
| -rw-r--r-- | src/Util/CaseUtil.v | 6 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 4 | ||||
| -rw-r--r-- | src/Util/NatUtil.v | 2 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 8 |
10 files changed, 72 insertions, 66 deletions
@@ -28,7 +28,7 @@ coqprime-8.5: $(MAKE) -C coqprime-8.5 Makefile.coq: Makefile _CoqProject - coq_makefile -f _CoqProject -o Makefile.coq + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq clean: Makefile.coq $(MAKE) -f Makefile.coq clean diff --git a/src/BaseSystem.v b/src/BaseSystem.v index e6ad55f18..c07aad759 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -1,7 +1,8 @@ Require Import Coq.Lists.List. -Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Import Nat. Local Open Scope Z. @@ -39,7 +40,7 @@ Section BaseSystem. Proof. unfold decode'; intros; f_equal; apply combine_truncate_l. Qed. - + Fixpoint add (us vs:digits) : digits := match us,vs with | u::us', v::vs' => u+v :: add us' vs' @@ -58,26 +59,26 @@ Section BaseSystem. | nil, v::vs' => (0-v)::sub nil vs' end. - Definition crosscoef i j : Z := + Definition crosscoef i j : Z := let b := nth_default 0 base in (b(i) * b(j)) / b(i+j)%nat. Hint Unfold crosscoef. Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end. - + (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) - Fixpoint mul_bi' (i:nat) (vsr:digits) := + Fixpoint mul_bi' (i:nat) (vsr:digits) := match vsr with | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr' | nil => nil end. Definition mul_bi (i:nat) (vs:digits) : digits := zeros i ++ rev (mul_bi' i (rev vs)). - + (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) Fixpoint mul' (usr vs:digits) : digits := match usr with - | u::usr' => + | u::usr' => mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs | _ => nil end. @@ -87,7 +88,7 @@ End BaseSystem. (* Example : polynomial base system *) Section PolynomialBaseCoefs. - Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true). + Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : ltb 0 baseLength = true). (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *) Definition bi i := (Zpos b1)^(Z.of_nat i). Definition poly_base := map bi (seq 0 baseLength). @@ -96,7 +97,7 @@ Section PolynomialBaseCoefs. unfold poly_base, bi, nth_default. case_eq baseLength; intros. { assert ((0 < baseLength)%nat) by - (rewrite <-NPeano.ltb_lt; apply baseLengthNonzero). + (rewrite <-ltb_lt; apply baseLengthNonzero). subst; omega. } auto. @@ -119,7 +120,7 @@ Section PolynomialBaseCoefs. Qed. Lemma poly_base_succ : - forall i, ((S i) < length poly_base)%nat -> + forall i, ((S i) < length poly_base)%nat -> let b := nth_default 0 poly_base in let r := (b (S i) / b i) in b (S i) = r * b i. @@ -127,7 +128,7 @@ Section PolynomialBaseCoefs. intros; subst b; subst r. repeat rewrite poly_base_defn in * by omega. unfold bi. - replace (Z.pos b1 ^ Z.of_nat (S i)) + replace (Z.pos b1 ^ Z.of_nat (S i)) with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition). replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i) @@ -166,7 +167,7 @@ Import ListNotations. Section BaseSystemExample. Definition baseLength := 32%nat. - Lemma baseLengthNonzero : NPeano.ltb 0 baseLength = true. + Lemma baseLengthNonzero : ltb 0 baseLength = true. compute; reflexivity. Qed. Definition base2 := poly_base 2 baseLength. diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index ab56cb711..f786714d7 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -18,7 +18,7 @@ Section BaseSystemProofs. Qed. Lemma decode'_splice : forall xs ys bs, - decode' bs (xs ++ ys) = + decode' bs (xs ++ ys) = decode' (firstn (length xs) bs) xs + decode' (skipn (length xs) bs) ys. Proof. unfold decode'. @@ -83,7 +83,7 @@ Section BaseSystemProofs. unfold decode, encode; destruct z; boring. Qed. - Lemma mul_each_base : forall us bs c, + Lemma mul_each_base : forall us bs c, decode' bs (mul_each c us) = decode' (mul_each c bs) us. Proof. induction us; destruct bs; boring; ring. @@ -99,8 +99,8 @@ Section BaseSystemProofs. induction us; destruct low; boring. Qed. - Lemma base_mul_app : forall low c us, - decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + + Lemma base_mul_app : forall low c us, + decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + c * decode' low (skipn (length low) us). Proof. intros. @@ -118,7 +118,7 @@ Section BaseSystemProofs. Qed. Hint Rewrite length_zeros. - Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m). + Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m)%nat. Proof. induction n; boring. Qed. @@ -225,7 +225,7 @@ Section BaseSystemProofs. Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n. induction n; auto. - simpl; f_equal; auto. + simpl; f_equal; auto. Qed. Lemma mul_bi'_n_nil : forall n, mul_bi' base n nil = nil. @@ -243,13 +243,13 @@ Section BaseSystemProofs. induction us; auto. Qed. Hint Rewrite add_nil_r. - + Lemma add_first_terms : forall us vs a b, (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs). auto. Qed. Hint Rewrite add_first_terms. - + Lemma mul_bi'_cons : forall n x us, mul_bi' base n (x :: us) = x * crosscoef base n (length us) :: mul_bi' base n us. Proof. @@ -266,7 +266,7 @@ Section BaseSystemProofs. Hint Rewrite app_nil_l. Hint Rewrite app_nil_r. - Lemma add_snoc_same_length : forall l us vs a b, + Lemma add_snoc_same_length : forall l us vs a b, (length us = l) -> (length vs = l) -> (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil. Proof. @@ -276,7 +276,7 @@ Section BaseSystemProofs. Lemma mul_bi'_add : forall us n vs l (Hlus: length us = l) (Hlvs: length vs = l), - mul_bi' base n (rev (us .+ vs)) = + mul_bi' base n (rev (us .+ vs)) = mul_bi' base n (rev us) .+ mul_bi' base n (rev vs). Proof. (* TODO(adamc): please help prettify this *) @@ -310,7 +310,7 @@ Section BaseSystemProofs. Proof. induction n; boring. Qed. - + Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) -> (rev us) .+ (rev vs) = rev (us .+ vs). Proof. @@ -352,7 +352,7 @@ Section BaseSystemProofs. Hint Rewrite minus_diag. Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat -> - us .+ vs = us .+ (vs ++ (zeros (length us - length vs))). + us .+ vs = us .+ (vs ++ (zeros (length us - length vs)%nat)). Proof. induction us, vs; boring; f_equal; boring. Qed. @@ -450,7 +450,7 @@ Section BaseSystemProofs. (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) Fixpoint mul' (usr vs:digits) : digits := match usr with - | u::usr' => + | u::usr' => mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs | _ => nil end. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index dabfcf883..8566177a1 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -1,3 +1,4 @@ +Require Import Coq.omega.Omega. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.Pre. @@ -19,20 +20,20 @@ Section ModularArithmeticPreliminaries. f_equal. eapply UIP_dec, Z.eq_dec. Qed. - + Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. intros a. pose (@opp_with_spec m) as H. - change (@opp m) with (proj1_sig H). + change (@opp m) with (proj1_sig H). destruct H; eauto. Qed. - + Lemma F_pow_spec : forall (a:F m), pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). Proof. intros a. pose (@pow_with_spec m) as H. - change (@pow m) with (proj1_sig H). + change (@pow m) with (proj1_sig H). destruct H; eauto. Qed. End ModularArithmeticPreliminaries. @@ -81,7 +82,7 @@ Ltac eq_remove_proofs := lazymatch goal with assert (Q := F_eq a b); simpl in *; apply Q; clear Q end. - + Ltac Fdefn := intros; rewrite ?F_opp_spec; @@ -217,7 +218,7 @@ Section FandZ. rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ; simpl; congruence. Qed. - + Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> b mod m = (- a) mod m. Proof. @@ -244,7 +245,7 @@ Section FandZ. intros. pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial. Qed. - + Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z. Proof. intros. @@ -282,7 +283,7 @@ Section FandZ. Proof. Fdefn. Qed. - + (* Compatibility between inject and pow *) Lemma ZToField_pow : forall x n, @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m). @@ -317,7 +318,7 @@ End FandZ. Section RingModuloPre. Context {m:Z}. - Local Coercion ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. + Local Coercion ZToFm' := ZToField : Z -> F m. Hint Unfold ZToFm'. (* Substitution to prove all Compats *) Ltac compat := repeat intro; subst; trivial. @@ -362,12 +363,12 @@ Section RingModuloPre. Proof. Fdefn; rewrite Z.mul_1_r; auto. Qed. - + Lemma F_mul_assoc: forall x y z : F m, x * (y * z) = x * y * z. Proof. Fdefn. - Qed. + Qed. Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. Proof. @@ -390,7 +391,7 @@ Section RingModuloPre. Qed. (***** Division Theory *****) - Definition Fquotrem(a b: F m): F m * F m := + Definition Fquotrem(a b: F m): F m * F m := let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m). Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem. Proof. @@ -434,7 +435,7 @@ Section RingModuloPre. Qed. (* Redefine our division theory under the ring morphism *) - Lemma Fmorph_div_theory: + Lemma Fmorph_div_theory: div_theory eq Zplus Zmult (@ZToField m) Z.quotrem. Proof. constructor; intros; intuition. @@ -451,7 +452,7 @@ Section RingModuloPre. Fdefn. Qed. End RingModuloPre. - + Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end. Ltac Fexp_tac t := Ncst t. Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. @@ -470,49 +471,49 @@ Module RingModulo (Export M : Modulus). Definition ring_morph_modulo := @Fring_morph modulus. Definition morph_div_theory_modulo := @Fmorph_div_theory modulus. Definition power_theory_modulo := @Fpower_theory modulus. - + Add Ring GFring_Z : ring_theory_modulo (morphism ring_morph_modulo, constants [Fconstant], div morph_div_theory_modulo, - power_tac power_theory_modulo [Fexp_tac]). + power_tac power_theory_modulo [Fexp_tac]). End RingModulo. Section VariousModulo. Context {m:Z}. - + Add Ring GFring_Z : (@Fring_theory m) (morphism (@Fring_morph m), constants [Fconstant], div (@Fmorph_div_theory m), - power_tac (@Fpower_theory m) [Fexp_tac]). + power_tac (@Fpower_theory m) [Fexp_tac]). Lemma F_mul_0_l : forall x : F m, 0 * x = 0. Proof. intros; ring. Qed. - + Lemma F_mul_0_r : forall x : F m, x * 0 = 0. Proof. intros; ring. Qed. - + Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. intros; intuition; subst. assert (0 * b = 0) by ring; intuition. Qed. - + Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. intros; intuition; subst. assert (a * 0 = 0) by ring; intuition. Qed. - + Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N -> (x ^ z) * (y ^ z) = (x * y) ^ z. Proof. intros. replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id. - apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | + apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto]. intros z' z'_nonneg IHz'. rewrite Z2N.inj_succ by auto. @@ -521,7 +522,7 @@ Section VariousModulo. rewrite <- IHz'. ring. Qed. - + Lemma F_opp_0 : opp (0 : F m) = 0%F. Proof. intros; ring. @@ -563,7 +564,7 @@ Section VariousModulo. Proof. intros; ring. Qed. - + Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z. Proof. intros ? ? ? A. @@ -653,7 +654,7 @@ Section VariousModulo. Proof. split; intro A; [ replace w with (w - x + x) by ring - | replace w with (w + z - z) by ring ]; rewrite A; ring. + | replace w with (w + z - z) by ring ]; rewrite A; ring. Qed. Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 2978fdd42..fca5576b7 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArit Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.omega.Omega. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. @@ -46,7 +47,7 @@ Defined. Definition mulmod m := fun a b => a * b mod m. Definition powmod_pos m := Pos.iter_op (mulmod m). Definition powmod m a x := match x with N0 => 1 mod m | Npos p => powmod_pos m p (a mod m) end. - + Lemma mulmod_assoc: forall m x y z : Z, mulmod m x (mulmod m y z) = mulmod m (mulmod m x y) z. Proof. @@ -144,7 +145,7 @@ Definition mod_inv_eucl (a m:Z) : Z. (match d with Z.pos _ => u | _ => -u end) end) mod m). Defined. - + Lemma reduced_nonzero_pos: forall a m : Z, m > 0 -> a <> 0 -> a = a mod m -> 0 < a. Proof. @@ -209,7 +210,7 @@ Proof. unfold mod_inv_eucl; simpl. lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end. auto. - - + - destruct a. cbv [proj1_sig mod_inv_eucl_sig]. rewrite Z.mul_comm. @@ -217,4 +218,4 @@ Proof. rewrite mod_inv_eucl_correct; eauto. intro; destruct H0. eapply exist_reduced_eq. congruence. -Qed.
\ No newline at end of file +Qed. diff --git a/src/Testbit.v b/src/Testbit.v index 264069587..2bfcc3df6 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.BaseSystem Crypto.BaseSystemProofs. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. +Import Nat. Local Open Scope Z. @@ -209,4 +210,4 @@ Lemma testbit_spec : forall n us base limb_width, (0 < limb_width)%nat -> Proof. intros. erewrite unfold_bits_testbit, unfold_bits_decode; eauto; omega. -Qed.
\ No newline at end of file +Qed. diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v index cf3ebf29c..2d1ab6c58 100644 --- a/src/Util/CaseUtil.v +++ b/src/Util/CaseUtil.v @@ -1,12 +1,12 @@ -Require Import Coq.Arith.Arith. +Require Import Coq.Arith.Arith Coq.Arith.Max. Ltac case_max := match goal with [ |- context[max ?x ?y] ] => destruct (le_dec x y); match goal with - | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by + | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by (exact H) - | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_l by + | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_l by (exact (le_Sn_le _ _ (not_le _ _ H))) end end. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 6116312e1..82d22046d 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,5 +1,7 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. +Require Import Coq.Numbers.Natural.Peano.NPeano. + Local Open Scope equiv_scope. Generalizable All Variables. @@ -147,7 +149,7 @@ Section IterAssocOp. destruct (funexp (test_and_op n a) (x, acc) y) as [i acc']. simpl in IHy. unfold test_and_op. - destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. + destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. Qed. Lemma iter_op_termination : forall sc a bound, diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 1f69b04d2..f86ecee2e 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Import Nat. Local Open Scope nat_scope. @@ -66,4 +67,3 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. - diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1b7cfafdc..3ffc69fc5 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Coq.Lists.List. +Import Nat. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -208,7 +209,7 @@ Proof. rewrite (le_plus_minus n m) at 1 by assumption. rewrite Nat2Z.inj_add. rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. - rewrite <- Z.div_div by first + rewrite <- Z.div_div by first [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega | apply Z.pow_pos_nonneg; omega ]. rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). @@ -345,7 +346,7 @@ Qed. + unfold Z.ones. rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. omega. - + intros. + + intros. destruct (Z_lt_le_dec x n); try omega. intuition. left. @@ -360,7 +361,7 @@ Qed. Z.shiftr a i <= Z.ones (n - i) . Proof. intros a n i G G0 G1. - destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. destruct (Z_eq_dec a 0). @@ -415,4 +416,3 @@ Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. zero_bounds. apply Z.pow_nonneg; omega. Qed. - |