From fb6fd35b9cfc454b622c8bfa1364efdbf048e0df Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 24 Aug 2016 17:07:43 -0400 Subject: Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6 --- src/ModularArithmetic/ModularBaseSystemOpt.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index fd144a474..000f2599c 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -636,7 +636,8 @@ Global Instance Proper_fold_chain {T} {Teq} {Teq_Equivalence : Equivalence Teq} ==> Teq) fold_chain. Proof. do 9 intro. - subst; induction y1; repeat intro; rewrite !fold_chain_equation. + subst; induction y1; repeat intro; + unfold fold_chain; fold @fold_chain. + inversion H; assumption || reflexivity. + destruct a. apply IHy1. -- cgit v1.2.3 From 5de065df4799cb43aba9195bcd88a5f0479884ff Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 24 Aug 2016 17:09:28 -0400 Subject: Moved a tactic to Util/Tactics.v --- src/ModularArithmetic/Pow2BaseProofs.v | 1 - src/Util/Tactics.v | 2 ++ 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 0ce214bbd..7158dc22a 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -1230,7 +1230,6 @@ Section Conversion. /\ Z.of_nat i <= bitsIn limb_widthsA /\ forall n, Z.testbit (decodeB out) n = if Z_lt_dec n (Z.of_nat i) then Z.testbit (decodeA inp) n else false. - Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. Ltac subst_lia := subst_let; subst; lia. Lemma convert'_bounded_step : forall inp i out, diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index be777512c..cee2fc2a1 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -61,6 +61,8 @@ Ltac subst_evars := | [ e := ?E |- _ ] => is_evar E; subst e end. +Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. + (** destruct discriminees of [match]es in the goal *) (* Prioritize breaking apart things in the context, then things which don't need equations, then simple matches (which can be displayed -- cgit v1.2.3 From 589faec943ccd6e55c28fddd701fd38bc0f32507 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 24 Aug 2016 17:09:57 -0400 Subject: Added rewrite hints for two ListUtil lemmas --- src/Util/ListUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 1c39f22cb..2fd9befa0 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1340,6 +1340,7 @@ Proof. induction n; destruct l; boring. apply nth_error_nil_error. Qed. +Hint Rewrite @nth_error_skipn : push_nth_error. Lemma nth_default_skipn : forall {A} (l : list A) d n m, nth_default d (skipn n l) m = nth_default d l (n + m). Proof. @@ -1347,6 +1348,7 @@ cbv [nth_default]; intros. rewrite nth_error_skipn. reflexivity. Qed. +Hint Rewrite @nth_default_skipn : push_nth_default. Lemma sum_firstn_skipn : forall l n m, sum_firstn l (n + m) = (sum_firstn l n + sum_firstn (skipn n l) m)%Z. Proof. -- cgit v1.2.3 From 5e624a3289b2d4ffa3579dd74a4ca4e1c564afa4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Aug 2016 16:17:05 -0700 Subject: Fewer side-conditions on zsimplify After | File Name | Before || Change ---------------------------------------------------------------------------------- 3m23.91s | Total | 3m03.61s || +0m20.30s ---------------------------------------------------------------------------------- 0m52.44s | ModularArithmetic/Pow2BaseProofs | 0m38.87s || +0m13.57s 0m18.83s | ModularArithmetic/ModularBaseSystemProofs | 0m27.00s || -0m08.17s 0m13.77s | ModularArithmetic/Montgomery/ZProofs | 0m09.31s || +0m04.45s 0m16.91s | Experiments/SpecEd25519 | 0m14.02s || +0m02.89s 0m05.95s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.94s || +0m02.01s 0m15.10s | Specific/GF25519 | 0m16.29s || -0m01.18s 0m09.03s | Specific/GF1305 | 0m10.27s || -0m01.24s 0m05.09s | ModularArithmetic/Tutorial | 0m03.68s || +0m01.40s 0m03.78s | ModularArithmetic/ModularArithmeticTheorems | 0m02.61s || +0m01.16s 0m12.20s | Util/ZUtil | 0m11.39s || +0m00.80s 0m10.50s | Testbit | 0m10.45s || +0m00.05s 0m04.99s | BaseSystemProofs | 0m04.22s || +0m00.77s 0m04.01s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.05s || +0m00.96s 0m03.42s | Experiments/SpecificCurve25519 | 0m03.52s || -0m00.10s 0m02.87s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.38s || +0m00.49s 0m02.55s | ModularArithmetic/ModularBaseSystemOpt | 0m03.43s || -0m00.88s 0m02.14s | ModularArithmetic/BarrettReduction/Z | 0m01.55s || +0m00.59s 0m01.77s | Encoding/PointEncodingPre | 0m01.57s || +0m00.19s 0m01.68s | BaseSystem | 0m01.65s || +0m00.03s 0m01.51s | ModularArithmetic/PrimeFieldTheorems | 0m01.09s || +0m00.41s 0m01.37s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.86s || +0m00.51s 0m01.31s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || +0m00.14s 0m01.16s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.30s || -0m00.14s 0m01.15s | Util/NumTheoryUtil | 0m01.33s || -0m00.18s 0m01.07s | Encoding/ModularWordEncodingTheorems | 0m01.02s || +0m00.05s 0m00.98s | Encoding/ModularWordEncodingPre | 0m00.92s || +0m00.05s 0m00.97s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || +0m00.32s 0m00.85s | ModularArithmetic/Montgomery/ZBounded | 0m00.97s || -0m00.12s 0m00.79s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.69s || +0m00.10s 0m00.76s | ModularArithmetic/Pre | 0m00.48s || +0m00.28s 0m00.73s | ModularArithmetic/ModularBaseSystemList | 0m00.66s || +0m00.06s 0m00.71s | Spec/ModularWordEncoding | 0m00.58s || +0m00.13s 0m00.68s | ModularArithmetic/Pow2Base | 0m00.41s || +0m00.27s 0m00.67s | ModularArithmetic/ZBounded | 0m00.48s || +0m00.19s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.43s || +0m00.23s 0m00.66s | ModularArithmetic/ModularBaseSystem | 0m00.62s || +0m00.04s 0m00.45s | ModularArithmetic/Montgomery/Z | 0m00.40s || +0m00.04s 0m00.41s | Spec/ModularArithmetic | 0m00.36s || +0m00.04s --- src/Util/ZUtil.v | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d06477d3c..35aa20dc4 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -324,15 +324,27 @@ Module Z. Hint Resolve elim_mod : zarith. + Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c. + Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_full : zsimplify. + + Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b. + Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_l_full : zsimplify. + + Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b. + Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a. + Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify. + Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. - Hint Rewrite mod_add_l using zutil_arith : zsimplify. Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. - Hint Rewrite mod_add' mod_add_l' using zutil_arith : zsimplify. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. -- cgit v1.2.3 From c3767efd8c036477ba6ecdd1c5cca98dbf165e7a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Aug 2016 16:44:09 -0700 Subject: Add more reserved notations --- src/Util/Notations.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 5daa2d4a9..686443829 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -25,6 +25,8 @@ Reserved Infix "&" (at level 50). (* N.B. This conflicts with [{ a : T & P}] for Reserved Infix "∣" (at level 50). Reserved Infix "~=" (at level 70). Reserved Infix "==" (at level 70, no associativity). +Reserved Infix "=~>" (at level 70, no associativity). +Reserved Infix "<~=" (at level 70, no associativity). Reserved Infix "≡" (at level 70, no associativity). Reserved Infix "≢" (at level 70, no associativity). Reserved Infix "≡_n" (at level 70, no associativity). -- cgit v1.2.3 From 3e980c7a7cd6c6084bf763bd9b748c20fc37f649 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Aug 2016 19:34:19 -0700 Subject: More zarith After | File Name | Before || Change ---------------------------------------------------------------------------------- 2m59.90s | Total | 2m45.43s || +0m14.46s ---------------------------------------------------------------------------------- 0m47.27s | ModularArithmetic/Pow2BaseProofs | 0m37.78s || +0m09.49s 0m11.27s | ModularArithmetic/Montgomery/ZProofs | 0m09.44s || +0m01.83s 0m17.72s | ModularArithmetic/ModularBaseSystemProofs | 0m17.72s || +0m00.00s 0m13.74s | Experiments/SpecEd25519 | 0m13.85s || -0m00.10s 0m12.31s | Specific/GF25519 | 0m12.16s || +0m00.15s 0m11.55s | Util/ZUtil | 0m11.60s || -0m00.04s 0m09.67s | Testbit | 0m08.91s || +0m00.75s 0m07.47s | Specific/GF1305 | 0m07.60s || -0m00.12s 0m05.37s | BaseSystemProofs | 0m04.60s || +0m00.77s 0m04.17s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.98s || +0m00.18s 0m03.70s | ModularArithmetic/Tutorial | 0m03.70s || +0m00.00s 0m03.48s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m04.13s || -0m00.64s 0m03.32s | Experiments/SpecificCurve25519 | 0m03.34s || -0m00.02s 0m03.12s | ModularArithmetic/ModularArithmeticTheorems | 0m03.00s || +0m00.12s 0m02.55s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.37s || +0m00.17s 0m02.41s | ModularArithmetic/ModularBaseSystemOpt | 0m02.36s || +0m00.05s 0m02.08s | ModularArithmetic/BarrettReduction/Z | 0m02.06s || +0m00.02s 0m01.97s | Encoding/PointEncodingPre | 0m01.68s || +0m00.29s 0m01.66s | BaseSystem | 0m01.26s || +0m00.39s 0m01.55s | ModularArithmetic/PrimeFieldTheorems | 0m01.17s || +0m00.38s 0m01.40s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.25s || +0m00.14s 0m01.28s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.83s || +0m00.45s 0m01.21s | ModularArithmetic/ExtendedBaseVector | 0m01.15s || +0m00.06s 0m01.00s | Util/NumTheoryUtil | 0m00.88s || +0m00.12s 0m00.98s | ModularArithmetic/Montgomery/ZBounded | 0m00.97s || +0m00.01s 0m00.75s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.71s || +0m00.04s 0m00.70s | Encoding/ModularWordEncodingPre | 0m00.65s || +0m00.04s 0m00.69s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.78s || -0m00.09s 0m00.68s | Encoding/ModularWordEncodingTheorems | 0m01.00s || -0m00.31s 0m00.66s | ModularArithmetic/ModularBaseSystemList | 0m00.67s || -0m00.01s 0m00.64s | ModularArithmetic/ModularBaseSystem | 0m00.61s || +0m00.03s 0m00.63s | ModularArithmetic/ZBounded | 0m00.44s || +0m00.19s 0m00.60s | ModularArithmetic/Montgomery/Z | 0m00.50s || +0m00.09s 0m00.57s | Spec/ModularWordEncoding | 0m00.57s || +0m00.00s 0m00.50s | ModularArithmetic/Pre | 0m00.52s || -0m00.02s 0m00.46s | ModularArithmetic/Pow2Base | 0m00.43s || +0m00.03s 0m00.40s | Spec/ModularArithmetic | 0m00.36s || +0m00.04s 0m00.38s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.41s || -0m00.02s --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 35aa20dc4..1758f1496 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -19,7 +19,7 @@ Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos : zarith. Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith. Ltac zutil_arith := solve [ omega | lia | auto with nocore ]. -- cgit v1.2.3