From fedeaa6d5f264df680b440e119591e4bfa8de54a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 10:54:43 -0700 Subject: Remove a nested proof Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated] --- src/Experiments/SpecEd25519.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 659a0ec66..30d8ce13d 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -32,7 +32,7 @@ Qed. Ltac q_bound := pose proof two_lt_q; omega. Lemma square_a : isSquare a. Proof. - Lemma q_1mod4 : (q mod 4 = 1)%Z. reflexivity. Qed. + assert (q_1mod4 : (q mod 4 = 1)%Z) by abstract reflexivity. intros. pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square. destruct minus1_square as [b b_id]. @@ -162,4 +162,4 @@ Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Een EdDSA_l_prime := prime_l; EdDSA_l_odd := l_odd; EdDSA_l_order_B := l_order_B - }. \ No newline at end of file + }. -- cgit v1.2.3 From 15623b0cede2694310fc41a5802444e3e86ee35f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 11:26:04 -0700 Subject: Add some lemmas about nth_default in bounds --- src/Util/ListUtil.v | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9225ee065..caeaefdb2 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -72,6 +72,7 @@ Ltac boring := simpl; intuition; repeat match goal with | [ H : _ |- _ ] => rewrite H; clear H + | [ |- appcontext[match ?pf with end] ] => solve [ case pf ] | _ => progress autounfold in * | _ => progress autorewrite with core | _ => progress simpl in * @@ -847,6 +848,41 @@ Ltac update_nth_inbounds := Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds || update_nth_inbounds. +Definition nth_dep {A} (ls : list A) (n : nat) (pf : n < length ls) : A. +Proof. + refine (match nth_error ls n as v return nth_error ls n = v -> A with + | Some v => fun _ => v + | None => fun bad => match _ : False with end + end eq_refl). + apply (proj1 (@List.nth_error_None _ _ _)) in bad; generalize dependent (length ls); clear. + abstract (intros; omega). +Defined. + +Lemma nth_error_nth_dep {A} ls n pf : nth_error ls n = Some (@nth_dep A ls n pf). +Proof. + unfold nth_dep. + generalize dependent (List.nth_error_None ls n). + edestruct nth_error; boring. +Qed. + +Lemma nth_default_nth_dep {A} d ls n pf : nth_default d ls n = @nth_dep A ls n pf. +Proof. + unfold nth_dep. + generalize dependent (List.nth_error_None ls n). + destruct (nth_error ls n) eqn:?; boring. + erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. +Qed. + +Lemma nth_default_in_bounds : forall {T} n us (d d' : T), (n < length us)%nat -> + nth_default d us n = nth_default d us n. +Proof. + intros; erewrite !nth_default_nth_dep; reflexivity. + Grab Existential Variables. + assumption. +Qed. + +Hint Resolve @nth_default_in_bounds : simpl_nth_default. + Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. Proof. intros; solve_by_inversion. @@ -1168,4 +1204,4 @@ Proof. do 5 intro; subst; induction 1. + repeat intro; rewrite !nth_default_nil; assumption. + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. -Qed. \ No newline at end of file +Qed. -- cgit v1.2.3 From 6be6e0a4b9828512fda0d3d81cf56fdff808af27 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 11:28:07 -0700 Subject: Fix some typos in the previous commit --- src/Util/ListUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index caeaefdb2..da02faa22 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -873,8 +873,8 @@ Proof. erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. -Lemma nth_default_in_bounds : forall {T} n us (d d' : T), (n < length us)%nat -> - nth_default d us n = nth_default d us n. +Lemma nth_default_in_bounds : forall {T} (d' d : T) n us, (n < length us)%nat -> + nth_default d us n = nth_default d' us n. Proof. intros; erewrite !nth_default_nth_dep; reflexivity. Grab Existential Variables. -- cgit v1.2.3 From 4611b121126c55bf32bf8fc89a9258cbb2337aa7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 11:55:38 -0700 Subject: Add natsimplify lemmas about eq_nat_dec --- src/Util/NatUtil.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'src') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 6d4efd9f4..4800ecb95 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -207,3 +207,31 @@ Proof. Qed. Hint Rewrite eq_nat_dec_refl : natsimplify. + +(** Helper to get around the lack of function extensionality *) +Definition eq_nat_dec_right_val n m (pf0 : n <> m) : { pf | eq_nat_dec n m = right pf }. +Proof. + revert dependent n; induction m; destruct n as [|n]; simpl; + intro pf0; + [ (exists pf0; exfalso; abstract congruence) + | eexists; reflexivity + | eexists; reflexivity + | ]. + { specialize (IHm n (fun e => pf0 (f_equal_nat nat S n m e))). + destruct IHm as [? IHm]. + eexists; rewrite IHm; reflexivity. } +Qed. + +Lemma eq_nat_dec_S_n n : eq_nat_dec (S n) n = right (proj1_sig (@eq_nat_dec_right_val _ _ (@neq_succ_diag_l n))). +Proof. + edestruct eq_nat_dec_right_val; assumption. +Qed. + +Hint Rewrite eq_nat_dec_S_n : natsimplify. + +Lemma eq_nat_dec_n_S n : eq_nat_dec n (S n) = right (proj1_sig (@eq_nat_dec_right_val _ _ (n_Sn n))). +Proof. + edestruct eq_nat_dec_right_val; assumption. +Qed. + +Hint Rewrite eq_nat_dec_n_S : natsimplify. -- cgit v1.2.3 From 662f07b23b0d03379fa0c0ee9cf377dbe6436e85 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:07:32 -0700 Subject: Add more NatUtil lemmas --- src/Util/NatUtil.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 4800ecb95..1a0cb67c7 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -235,3 +235,23 @@ Proof. Qed. Hint Rewrite eq_nat_dec_n_S : natsimplify. + +Hint Rewrite Max.max_0_l Max.max_0_r Max.max_idempotent Min.min_0_l Min.min_0_r Min.min_idempotent : natsimplify. + +(** Helper to get around the lack of function extensionality *) +Definition lt_dec_right_val n m (pf0 : ~n < m) : { pf | lt_dec n m = right pf }. +Proof. + destruct (lt_dec n m) eqn:Heq; [ | eexists; reflexivity ]. + exfalso; clear Heq; apply pf0; assumption. +Qed. + +Lemma lt_dec_irrefl n : lt_dec n n = right (proj1_sig (@lt_dec_right_val _ _ (lt_irrefl n))). +Proof. edestruct lt_dec_right_val; assumption. Qed. +Hint Rewrite lt_dec_irrefl : natsimplify. + +Lemma not_lt_n_pred_n n : ~n < pred n. +Proof. omega. Qed. + +Lemma lt_dec_n_pred_n n : lt_dec n (pred n) = right (proj1_sig (@lt_dec_right_val _ _ (not_lt_n_pred_n n))). +Proof. edestruct lt_dec_right_val; assumption. Qed. +Hint Rewrite lt_dec_n_pred_n : natsimplify. -- cgit v1.2.3 From 45474c87340288731ba0783325278406bec0c147 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:15:00 -0700 Subject: Add more natsimplify le_dec lemmas --- src/Util/NatUtil.v | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 1a0cb67c7..b957c39d1 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -239,12 +239,16 @@ Hint Rewrite eq_nat_dec_n_S : natsimplify. Hint Rewrite Max.max_0_l Max.max_0_r Max.max_idempotent Min.min_0_l Min.min_0_r Min.min_idempotent : natsimplify. (** Helper to get around the lack of function extensionality *) -Definition lt_dec_right_val n m (pf0 : ~n < m) : { pf | lt_dec n m = right pf }. +Definition le_dec_right_val n m (pf0 : ~n <= m) : { pf | le_dec n m = right pf }. Proof. - destruct (lt_dec n m) eqn:Heq; [ | eexists; reflexivity ]. + destruct (le_dec n m) eqn:Heq; [ | eexists; reflexivity ]. exfalso; clear Heq; apply pf0; assumption. Qed. +(** Helper to get around the lack of function extensionality *) +Definition lt_dec_right_val n m (pf0 : ~n < m) : { pf | lt_dec n m = right pf } + := @le_dec_right_val _ _ pf0. + Lemma lt_dec_irrefl n : lt_dec n n = right (proj1_sig (@lt_dec_right_val _ _ (lt_irrefl n))). Proof. edestruct lt_dec_right_val; assumption. Qed. Hint Rewrite lt_dec_irrefl : natsimplify. @@ -255,3 +259,27 @@ Proof. omega. Qed. Lemma lt_dec_n_pred_n n : lt_dec n (pred n) = right (proj1_sig (@lt_dec_right_val _ _ (not_lt_n_pred_n n))). Proof. edestruct lt_dec_right_val; assumption. Qed. Hint Rewrite lt_dec_n_pred_n : natsimplify. + +Lemma le_dec_refl n : le_dec n n = left (le_refl n). +Proof. + edestruct le_dec; try omega. + apply f_equal, le_unique. +Qed. +Hint Rewrite le_dec_refl : natsimplify. + +Lemma le_dec_pred_l n : le_dec (pred n) n = left (le_pred_l n). +Proof. + edestruct le_dec; try omega. + apply f_equal, le_unique. +Qed. +Hint Rewrite le_dec_pred_l : natsimplify. + +Lemma le_pred_plus_same n : n <= pred (n + n). +Proof. omega. Qed. + +Lemma le_dec_pred_plus_same n : le_dec n (pred (n + n)) = left (le_pred_plus_same n). +Proof. + edestruct le_dec; try omega. + apply f_equal, le_unique. +Qed. +Hint Rewrite le_dec_pred_plus_same : natsimplify. -- cgit v1.2.3 From 19dbf8eb3fd57262c6c66677f71e7a6617e0df9d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:32:06 -0700 Subject: Add more distr_length proofs in BaseSystemProofs --- src/BaseSystemProofs.v | 50 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 40 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index eb7f31ba6..8bd390635 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +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.BaseSystem. Require Import Crypto.Util.Notations. Local Open Scope Z. @@ -532,9 +532,13 @@ Section BaseSystemProofs. induction us; destruct vs; boring. Qed. - Lemma mul'_length_exact: forall us vs, - (length us <= length vs)%nat -> us <> nil -> - (length (mul' us vs) = pred (length us + length vs))%nat. + Hint Rewrite add_length_exact : distr_length. + + Lemma mul'_length_exact_full: forall us vs, + (length (mul' us vs) = match length us with + | 0 => 0%nat + | _ => pred (length us + length vs) + end)%nat. Proof. induction us; intros; try solve [boring]. unfold mul'; fold mul'. @@ -544,9 +548,33 @@ Section BaseSystemProofs. + rewrite Max.max_0_r. simpl; omega. + rewrite Max.max_l; [ omega | ]. rewrite IHus by ( congruence || simpl in *; omega). - omega. + simpl; omega. + Qed. + + Hint Rewrite mul'_length_exact_full : distr_length. + + (* TODO(@jadephilipoom, from jgross): one of these conditions isn't + needed. Should it be dropped, or was there a reason to keep it? *) + Lemma mul'_length_exact: forall us vs, + (length us <= length vs)%nat -> us <> nil -> + (length (mul' us vs) = pred (length us + length vs))%nat. + Proof. + intros; rewrite mul'_length_exact_full; destruct us; simpl; congruence. + Qed. + + Lemma mul_length_exact_full: forall us vs, + (length (mul us vs) = match length us with + | 0 => 0 + | _ => pred (length us + length vs) + end)%nat. + Proof. + intros; unfold mul; autorewrite with distr_length; reflexivity. Qed. + Hint Rewrite mul_length_exact_full : distr_length. + + (* TODO(@jadephilipoom, from jgross): one of these conditions isn't + needed. Should it be dropped, or was there a reason to keep it? *) Lemma mul_length_exact: forall us vs, (length us <= length vs)%nat -> us <> nil -> (length (mul us vs) = pred (length us + length vs))%nat. @@ -559,7 +587,7 @@ Section BaseSystemProofs. reflexivity. Qed. Definition encode'_zero z max : encode' base z max 0%nat = nil := eq_refl. - Definition encode'_succ z max i : encode' base z max (S i) = + Definition encode'_succ z max i : encode' base z max (S i) = encode' base z max i ++ ((z mod (nth_default max base (S i))) / (nth_default max base i)) :: nil := eq_refl. Opaque encode'. Hint Resolve encode'_zero encode'_succ. @@ -606,4 +634,6 @@ Section BaseSystemProofs. apply Z.mod_small; omega. Qed. -End BaseSystemProofs. \ No newline at end of file +End BaseSystemProofs. + +Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length. -- cgit v1.2.3 From dc585913d86991a12826e181a66f9c3a02afbd8f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:41:25 -0700 Subject: Fix for Coq 8.4 (omega used to be weaker) --- src/Util/NatUtil.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index b957c39d1..3eef976b2 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -217,8 +217,8 @@ Proof. | eexists; reflexivity | eexists; reflexivity | ]. - { specialize (IHm n (fun e => pf0 (f_equal_nat nat S n m e))). - destruct IHm as [? IHm]. + { specialize (IHm n). + destruct IHm as [? IHm]; [ omega | ]. eexists; rewrite IHm; reflexivity. } Qed. @@ -254,7 +254,7 @@ Proof. edestruct lt_dec_right_val; assumption. Qed. Hint Rewrite lt_dec_irrefl : natsimplify. Lemma not_lt_n_pred_n n : ~n < pred n. -Proof. omega. Qed. +Proof. destruct n; simpl; omega. Qed. Lemma lt_dec_n_pred_n n : lt_dec n (pred n) = right (proj1_sig (@lt_dec_right_val _ _ (not_lt_n_pred_n n))). Proof. edestruct lt_dec_right_val; assumption. Qed. @@ -269,17 +269,17 @@ Hint Rewrite le_dec_refl : natsimplify. Lemma le_dec_pred_l n : le_dec (pred n) n = left (le_pred_l n). Proof. - edestruct le_dec; try omega. + edestruct le_dec; [ | destruct n; simpl in *; omega ]. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_l : natsimplify. Lemma le_pred_plus_same n : n <= pred (n + n). -Proof. omega. Qed. +Proof. destruct n; simpl; omega. Qed. Lemma le_dec_pred_plus_same n : le_dec n (pred (n + n)) = left (le_pred_plus_same n). Proof. - edestruct le_dec; try omega. + edestruct le_dec; [ | destruct n; simpl in *; omega ]. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_plus_same : natsimplify. -- cgit v1.2.3 From ffc5e19d56b808e61fac1d94a9dfddc7b86cfa5d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:44:24 -0700 Subject: Fix for Coq 8.4 (missing lemmas) --- src/Util/ListUtil.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index da02faa22..3006dd799 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -854,21 +854,21 @@ Proof. | Some v => fun _ => v | None => fun bad => match _ : False with end end eq_refl). - apply (proj1 (@List.nth_error_None _ _ _)) in bad; generalize dependent (length ls); clear. + apply (proj1 (@nth_error_None _ _ _)) in bad; instantiate; generalize dependent (length ls); clear. abstract (intros; omega). Defined. Lemma nth_error_nth_dep {A} ls n pf : nth_error ls n = Some (@nth_dep A ls n pf). Proof. unfold nth_dep. - generalize dependent (List.nth_error_None ls n). + generalize dependent (@nth_error_None A ls n). edestruct nth_error; boring. Qed. Lemma nth_default_nth_dep {A} d ls n pf : nth_default d ls n = @nth_dep A ls n pf. Proof. unfold nth_dep. - generalize dependent (List.nth_error_None ls n). + generalize dependent (@nth_error_None A ls n). destruct (nth_error ls n) eqn:?; boring. erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. -- cgit v1.2.3 From d12f190a2ef6f129583f1fd69411638e237d731e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 14:31:18 -0700 Subject: Express carry_simple in terms of carry_gen Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity. --- src/ModularArithmetic/ModularBaseSystemOpt.v | 4 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 143 +++++++++++-------- src/ModularArithmetic/Pow2Base.v | 15 +- src/ModularArithmetic/Pow2BaseProofs.v | 174 ++++++++---------------- 4 files changed, 156 insertions(+), 180 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 7c7004dce..d7e6f1c65 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -3,6 +3,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil. @@ -118,9 +119,10 @@ Section Carries. cbv [carry]. rewrite <- pull_app_if_sumbool. cbv beta delta - [carry carry_and_reduce Pow2Base.carry_simple Pow2Base.add_to_nth + [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple Z.pow2_mod Z.ones Z.pred PseudoMersenneBaseParams.limb_widths]. + rewrite !add_to_nth_set_nth. change @Pow2Base.base_from_limb_widths with @base_from_limb_widths_opt. change @nth_default with @nth_default_opt in *. change @set_nth with @set_nth_opt in *. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index e5ae285de..daff60220 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1,8 +1,8 @@ -Require Import Zpower ZArith. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import List. +Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Require Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.Pow2Base. @@ -14,6 +14,7 @@ Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. +Local Opaque add_to_nth carry_simple. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. @@ -24,6 +25,7 @@ Section PseudoMersenneProofs. Local Notation "u .* x" := (ModularBaseSystem.mul u x). Local Hint Unfold rep. Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. + Local Hint Resolve log_cap_nonneg. Local Notation base := (base_from_limb_widths limb_widths). Local Notation log_cap i := (nth_default 0 limb_widths i). @@ -398,12 +400,17 @@ Section CarryProofs. Qed. Hint Resolve carry_rep. - Lemma carry_sequence_length: forall is us, - (length us = length base)%nat -> - (length (carry_sequence is us) = length base)%nat. + Lemma length_carry_sequence: forall is us, + (length (carry_sequence is us) = length us)%nat. Proof. induction is; boring. Qed. + Hint Rewrite length_carry_sequence : distr_length. + + Lemma carry_sequence_length: forall is us, + (length us = length base)%nat -> + (length (carry_sequence is us) = length base)%nat. + Proof. intros; autorewrite with distr_length; congruence. Qed. Hint Resolve carry_sequence_length. Lemma carry_sequence_rep : forall is us x, @@ -414,11 +421,16 @@ Section CarryProofs. induction is; boring. Qed. - Lemma carry_full_length : forall us, (length us = length base)%nat -> - length (carry_full us) = length base. + Lemma length_carry_full : forall us, + length (carry_full us) = length us. Proof. intros; cbv [carry_full]; auto using carry_sequence_length. Qed. + Hint Rewrite length_carry_full : distr_length. + + Lemma carry_full_length : forall us, (length us = length base)%nat -> + length (carry_full us) = length base. + Proof. intros; autorewrite with distr_length; congruence. Qed. Lemma carry_full_preserves_rep : forall us x, rep us x -> rep (carry_full us) x. @@ -438,17 +450,36 @@ Section CarryProofs. auto using mul_rep. Qed. + Local Arguments minus !_ !_. + + Lemma length_carry_mul : forall us vs, + length (carry_mul us vs) = (if eq_nat_dec (length us) 0 + then 0 + else if le_dec (length base) (pred (length us + length vs)) + then if lt_dec (length base + length base) (pred (length us + length vs)) + then pred (length us + length vs) - length base + else length base + else pred (length us + length vs))%nat. + Proof. + unfold carry_mul, ModularBaseSystem.mul, reduce; intros; autorewrite with distr_length natsimplify. + destruct us; simpl; autorewrite with natsimplify. + { reflexivity. } + { repeat break_if; omega *. } + Qed. + Lemma carry_mul_length : forall us vs, length us = length base -> length vs = length base -> length (carry_mul us vs) = length base. Proof. - intros; cbv [carry_mul]. - auto using carry_full_length, length_mul. + intros; rewrite length_carry_mul. + rewrite_hyp !* in *. + edestruct eq_nat_dec; [ congruence | ]. + autorewrite with natsimplify; reflexivity. Qed. End CarryProofs. -Hint Rewrite @length_carry_and_reduce @length_carry : distr_length. +Hint Rewrite @length_carry_and_reduce @length_carry @length_carry_sequence @length_carry_full @length_carry_mul : distr_length. Section CanonicalizationProofs. Context `{prm : PseudoMersenneBaseParams}. @@ -582,8 +613,8 @@ Section CanonicalizationProofs. Opaque Z.pow2_mod max_bound. (* automation *) - Ltac carry_length_conditions' := unfold carry_full, add_to_nth; - rewrite ?length_set_nth, ?length_carry, ?carry_sequence_length; + Ltac carry_length_conditions' := unfold carry_full; + rewrite ?length_set_nth, ?length_add_to_nth, ?length_carry, ?carry_sequence_length; try omega; try solve [pose proof base_length; pose proof base_length_nonzero; omega || auto ]. Ltac carry_length_conditions := try split; try omega; repeat carry_length_conditions'. @@ -618,11 +649,8 @@ Section CanonicalizationProofs. + unfold carry_and_reduce. add_set_nth. apply pow2_mod_log_cap_bounds_upper. - + unfold carry_simple. - destruct (lt_dec i (length us)). - - add_set_nth. - apply pow2_mod_log_cap_bounds_upper. - - rewrite nth_default_out_of_bounds by carry_length_conditions; auto. + + autorewrite with push_nth_default natsimplify. + destruct (lt_dec i (length us)); auto using pow2_mod_log_cap_bounds_upper. Qed. Local Hint Resolve nth_default_carry_bound_upper. @@ -634,11 +662,8 @@ Section CanonicalizationProofs. + unfold carry_and_reduce. add_set_nth. apply pow2_mod_log_cap_bounds_lower. - + unfold carry_simple. - destruct (lt_dec i (length us)). - - add_set_nth. - apply pow2_mod_log_cap_bounds_lower. - - rewrite nth_default_out_of_bounds by carry_length_conditions; omega. + + autorewrite with push_nth_default natsimplify. + break_if; auto using pow2_mod_log_cap_bounds_lower, Z.le_refl. Qed. Local Hint Resolve nth_default_carry_bound_lower. @@ -652,10 +677,8 @@ Section CanonicalizationProofs. rewrite nth_default_out_of_bounds; carry_length_conditions. unfold carry_and_reduce. carry_length_conditions. - + unfold carry_simple. - destruct (lt_dec (S i) (length us)). - - add_set_nth; zero_bounds. - - rewrite nth_default_out_of_bounds by carry_length_conditions; omega. + + autorewrite with push_nth_default natsimplify. + break_if; zero_bounds. Qed. Lemma carry_unaffected_low : forall i j us, ((0 < i < j)%nat \/ (i = 0 /\ j <> 0 /\ j <> pred (length base))%nat)-> @@ -667,12 +690,8 @@ Section CanonicalizationProofs. break_if. + unfold carry_and_reduce. add_set_nth. - + unfold carry_simple. - destruct (lt_dec i (length us)). - - add_set_nth. - - rewrite !nth_default_out_of_bounds by - (omega || rewrite length_add_to_nth; rewrite length_set_nth; pose proof base_length_nonzero; omega). - reflexivity. + + autorewrite with push_nth_default simpl_nth_default natsimplify. + repeat break_if; autorewrite with simpl_nth_default natsimplify; omega. Qed. Lemma carry_unaffected_high : forall i j us, (S j < i)%nat -> (length us = length base) -> @@ -681,21 +700,27 @@ Section CanonicalizationProofs. intros. destruct (lt_dec i (length us)); [ | rewrite !nth_default_out_of_bounds by carry_length_conditions; reflexivity]. - unfold carry, carry_simple. - break_if; [omega | add_set_nth]. + unfold carry. + break_if; [omega | autorewrite with push_nth_default natsimplify; repeat break_if; omega ]. Qed. + Hint Rewrite max_bound_shiftr_eq_0 using omega : core. + Hint Rewrite pow2_mod_log_cap_small using assumption : core. + Lemma carry_nothing : forall i j us, (i < length base)%nat -> (length us = length base)%nat -> 0 <= nth_default 0 us j <= max_bound j -> nth_default 0 (carry j us) i = nth_default 0 us i. Proof. - unfold carry, carry_simple, carry_and_reduce; intros. - break_if; (add_set_nth; - [ rewrite max_bound_shiftr_eq_0 by omega; ring - | subst; apply pow2_mod_log_cap_small; assumption ]). + unfold carry, carry_and_reduce; intros. + repeat (break_if + || subst + || (autorewrite with push_nth_default natsimplify core) + || omega). Qed. + Hint Rewrite pow2_mod_log_cap_small using (intuition; auto using shiftr_eq_0_max_bound) : core. + Lemma carry_carry_done_done : forall i us, (length us = length base)%nat -> (i < length base)%nat -> @@ -709,15 +734,17 @@ Section CanonicalizationProofs. split; [ apply Hcarry_done; auto | ]. apply shiftr_eq_0_max_bound. apply Hcarry_done; auto. - + unfold carry, carry_simple, carry_and_reduce; break_if; subst. + + unfold carry, carry_and_reduce; break_if; subst. - add_set_nth; subst. * rewrite shiftr_0_i, Z.mul_0_r, Z.add_0_l. assumption. * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). assumption. - - rewrite shiftr_0_i by omega. - rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). - add_set_nth; subst; rewrite ?Z.add_0_l; auto. + - repeat (carry_length_conditions + || (autorewrite with push_nth_default natsimplify core zsimplify) + || break_if + || subst + || rewrite shiftr_0_i by omega). Qed. Lemma carry_sequence_chain_step : forall i us, @@ -831,8 +858,10 @@ Section CanonicalizationProofs. 0 <= nth_default 0 (carry i us) (S i) < 2 ^ B. Proof. intros. - unfold carry, carry_simple; break_if; try omega. - add_set_nth. + unfold carry; break_if; try omega. + autorewrite with push_nth_default natsimplify. + break_if; try omega. + rewrite Z.add_comm. replace (2 ^ B) with (2 ^ (B - log_cap i) + (2 ^ B - 2 ^ (B - log_cap i))) by omega. split; [ zero_bounds | ]. apply Z.add_lt_mono; try omega. @@ -909,8 +938,9 @@ Section CanonicalizationProofs. Proof. induction i; intros; try omega. simpl. - unfold carry, carry_simple; break_if; try omega. - add_set_nth. + unfold carry; break_if; try omega. + autorewrite with push_nth_default natsimplify distr_length; break_if; [ | omega ]. + rewrite Z.add_comm. split. + zero_bounds; [destruct (eq_nat_dec i 0); subst | ]. - simpl; apply carry_full_bounds_0; auto. @@ -968,8 +998,9 @@ Section CanonicalizationProofs. 0 <= nth_default 0 (carry_simple limb_widths i (carry_sequence (make_chain i) (carry_full (carry_full us)))) (S i) <= 2 ^ log_cap (S i). Proof. - unfold carry_simple; intros ? ? PCB length_eq ? IH. - add_set_nth. + intros ? ? PCB length_eq ? IH. + autorewrite with push_nth_default natsimplify distr_length; break_if; [ | omega ]. + rewrite Z.add_comm. split. + zero_bounds. destruct i; [ simpl; pose proof (carry_full_2_bounds_0 us PCB length_eq); omega | ]. @@ -994,7 +1025,9 @@ Section CanonicalizationProofs. simpl; unfold carry. break_if; try omega. split; (destruct (eq_nat_dec i 0); subst; - [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth + [ cbv [make_chain carry_sequence fold_right]; + autorewrite with push_nth_default natsimplify distr_length; break_if; [ | omega ]; + rewrite Z.add_comm | eapply carry_full_2_bounds_succ; eauto; omega]). + zero_bounds. - eapply carry_full_2_bounds_0; eauto. @@ -1042,8 +1075,7 @@ Section CanonicalizationProofs. break_if; [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ]. simpl. - unfold carry_simple. - add_set_nth. + autorewrite with push_nth_default natsimplify. apply pow2_mod_log_cap_bounds_lower. + rewrite carry_unaffected_low by carry_length_conditions. assert (0 < S i < length base)%nat by omega. @@ -1081,10 +1113,11 @@ Section CanonicalizationProofs. split; [ auto using carry_full_2_bounds_lower | ]. destruct i; rewrite <-max_bound_log_cap, Z.lt_succ_r; auto. apply carry_full_bounds; auto using carry_full_bounds_lower. - - left; unfold carry, carry_simple. + - left; unfold carry. break_if; [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ]. - add_set_nth. simpl. + autorewrite with push_nth_default natsimplify. + simpl. remember ((nth_default 0 (carry_full (carry_full us)) 0)) as x. apply Z.le_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); try omega. replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring. @@ -2001,7 +2034,7 @@ Section CanonicalizationProofs. Lemma freeze_canonical : forall us vs x, pre_carry_bounds us -> rep us x -> pre_carry_bounds vs -> rep vs x -> - freeze us = freeze vs. + freeze us = freeze vs. Proof. intros. assert (length us = length base) by (unfold rep in *; intuition). diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index f434a0c9f..b842fa713 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -55,24 +55,19 @@ Section Pow2Base. (* Definition add_to_nth n (x:Z) xs := update_nth n (fun y => x + y) xs. - + *) Definition carry_and_reduce_single i := fun di => (Z.pow2_mod di (log_cap i), Z.shiftr di (log_cap i)). - Definition carry_gen f i := fun us => - let i := (i mod length us)%nat in + Definition carry_gen fc fi i := fun us => + let i := fi (length us) i in let di := nth_default 0 us i in let '(di', ci) := carry_and_reduce_single i di in let us' := set_nth i di' us in - add_to_nth ((S i) mod (length us)) (f ci) us'. + add_to_nth (fi (length us) (S i)) (fc ci) us'. - Definition carry_simple := carry_gen (fun ci => ci). - *) - Definition carry_simple i := fun us => - let di := nth_default 0 us i in - let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in - add_to_nth (S i) ( (Z.shiftr di (log_cap i))) us'. + Definition carry_simple := carry_gen (fun ci => ci) (fun _ i => i). Definition carry_simple_sequence is us := fold_right carry_simple us is. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index ed9b58ccc..819a5adb5 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -615,12 +615,10 @@ Section carrying. Local Notation log_cap i := (nth_default 0 limb_widths i). Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. - (* - Lemma length_carry_gen : forall f i us, length (carry_gen limb_widths f i us) = length us. + Lemma length_carry_gen : forall fc fi i us, length (carry_gen limb_widths fc fi i us) = length us. Proof. intros; unfold carry_gen, carry_and_reduce_single; distr_length; reflexivity. Qed. Hint Rewrite @length_carry_gen : distr_length. - *) Lemma length_carry_simple : forall i us, length (carry_simple limb_widths i us) = length us. Proof. intros; unfold carry_simple; distr_length; reflexivity. Qed. @@ -634,26 +632,29 @@ Section carrying. autorewrite with simpl_sum_firstn; reflexivity. Qed. - (* - Lemma carry_gen_decode_eq : forall f i' us (i := (i' mod length base)%nat), + Lemma carry_gen_decode_eq : forall fc fi i' us + (i := fi (length base) i') + (Si := fi (length base) (S i)), (length us = length base) -> - BaseSystem.decode base (carry_gen limb_widths f i' us) - = ((f (nth_default 0 us i / 2 ^ log_cap i)) - * (if eq_nat_dec (S i mod length base) 0 - then nth_default 0 base 0 - else (2 ^ log_cap i) * (nth_default 0 base i)) - - (nth_default 0 us i / 2 ^ log_cap i) * 2 ^ log_cap i * nth_default 0 base i - ) + BaseSystem.decode base (carry_gen limb_widths fc fi i' us) + = (fc (nth_default 0 us i / 2 ^ log_cap i) * + (if eq_nat_dec Si (S i) + then if lt_dec (S i) (length base) + then 2 ^ log_cap i * nth_default 0 base i + else 0 + else nth_default 0 base Si) + - 2 ^ log_cap i * (nth_default 0 us i / 2 ^ log_cap i) * nth_default 0 base i) + BaseSystem.decode base us. Proof. - intros f i' us i H; intros. + intros fc fi i' us i Si H; intros. destruct (eq_nat_dec 0 (length base)); [ destruct limb_widths, us, i; simpl in *; try congruence; + break_match; unfold carry_gen, carry_and_reduce_single, add_to_nth; autorewrite with zsimplify simpl_nth_default simpl_set_nth simpl_update_nth distr_length; reflexivity | ]. - assert (0 <= i < length base)%nat by (subst i; auto with arith). + (*assert (0 <= i < length base)%nat by (subst i; auto with arith).*) assert (0 <= log_cap i) by auto using log_cap_nonneg. assert (2 ^ log_cap i <> 0) by (apply Z.pow_nonzero; lia). unfold carry_gen, carry_and_reduce_single. @@ -663,17 +664,17 @@ Section carrying. unfold Z.pow2_mod. rewrite Z.land_ones by auto using log_cap_nonneg. rewrite Z.shiftr_div_pow2 by auto using log_cap_nonneg. - destruct (eq_nat_dec (S i mod length base) 0); - repeat first [ ring - | congruence - | match goal with H : _ = _ |- _ => rewrite !H in * end - | rewrite nth_default_base_succ by omega - | rewrite !(nth_default_out_of_bounds _ base) by omega - | rewrite !(nth_default_out_of_bounds _ us) by omega - | rewrite Z.mod_eq by assumption - | progress distr_length - | progress autorewrite with natsimplify zsimplify in * - | progress break_match ]. + change (fi (length base) i') with i. + subst Si. + repeat first [ ring + | match goal with H : _ = _ |- _ => rewrite !H in * end + | rewrite nth_default_base_succ by omega + | rewrite !(nth_default_out_of_bounds _ base) by omega + | rewrite !(nth_default_out_of_bounds _ us) by omega + | rewrite Z.mod_eq by assumption + | progress distr_length + | progress autorewrite with natsimplify zsimplify in * + | progress break_match ]. Qed. Lemma carry_simple_decode_eq : forall i us, @@ -685,26 +686,7 @@ Section carrying. autorewrite with natsimplify. break_match; lia. Qed. -*) - Lemma carry_simple_decode_eq : forall i us, - (length us = length base) -> - (i < (pred (length base)))%nat -> - BaseSystem.decode base (carry_simple limb_widths i us) = BaseSystem.decode base us. - Proof. - unfold carry_simple. intros. - rewrite add_to_nth_sum by (rewrite length_set_nth; omega). - rewrite set_nth_sum by omega. - unfold Z.pow2_mod. - rewrite Z.land_ones by eauto using log_cap_nonneg. - rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. - rewrite nth_default_base_succ by omega. - rewrite Z.mul_assoc. - rewrite (Z.mul_comm _ (2 ^ log_cap i)). - rewrite Z.mul_div_eq; try ring. - apply Z.gt_lt_iff. - apply Z.pow_pos_nonneg; omega || eauto using log_cap_nonneg. - Qed. Lemma length_carry_simple_sequence : forall is us, length (carry_simple_sequence limb_widths is us) = length us. Proof. @@ -732,32 +714,23 @@ Section carrying. Proof. induction x; simpl; intuition. Qed. -(* - Lemma nth_default_carry_gen_full : forall f d i n us, - nth_default d (carry_gen limb_widths f i us) n + + Lemma nth_default_carry_gen_full fc fi d i n us + : nth_default d (carry_gen limb_widths fc fi i us) n = if lt_dec n (length us) - then if eq_nat_dec n (i mod length us) - then (if eq_nat_dec (S n) (length us) - then (if eq_nat_dec n 0 - then f ((nth_default 0 us n) >> log_cap n) - else 0) - else 0) - + Z.pow2_mod (nth_default 0 us n) (log_cap n) - else (if eq_nat_dec n (if eq_nat_dec (S (i mod length us)) (length us) then 0%nat else S (i mod length us)) - then f (nth_default 0 us (i mod length us) >> log_cap (i mod length us)) - else 0) - + nth_default d us n + then (if eq_nat_dec n (fi (length us) i) + then Z.pow2_mod (nth_default 0 us n) (log_cap n) + else nth_default 0 us n) + + if eq_nat_dec n (fi (length us) (S (fi (length us) i))) + then fc (nth_default 0 us (fi (length us) i) >> log_cap (fi (length us) i)) + else 0 else d. Proof. unfold carry_gen, carry_and_reduce_single. intros; autorewrite with push_nth_default natsimplify distr_length. - edestruct lt_dec; [ | reflexivity ]. - change (S ?x) with (1 + x)%nat. - rewrite (Nat.add_mod_idemp_r 1 i (length us)) by omega. - autorewrite with natsimplify. - change (1 + ?x)%nat with (S x). - destruct (eq_nat_dec n (i mod length us)); - subst; repeat break_match; omega. + edestruct (lt_dec n (length us)) as [H|H]; [ | reflexivity ]. + rewrite !(@nth_default_in_bounds Z 0 d) by assumption. + repeat break_match; subst; try omega; try rewrite_hyp *; omega. Qed. Hint Rewrite @nth_default_carry_gen_full : push_nth_default. @@ -765,72 +738,45 @@ Section carrying. Lemma nth_default_carry_simple_full : forall d i n us, nth_default d (carry_simple limb_widths i us) n = if lt_dec n (length us) - then if eq_nat_dec n (i mod length us) - then (if eq_nat_dec (S n) (length us) - then (if eq_nat_dec n 0 - then (nth_default 0 us n >> log_cap n + Z.pow2_mod (nth_default 0 us n) (log_cap n)) - (* FIXME: The above is just [nth_default 0 us n], but do we really care about the case of [n = 0], [length us = 1]? *) - else Z.pow2_mod (nth_default 0 us n) (log_cap n)) - else Z.pow2_mod (nth_default 0 us n) (log_cap n)) - else (if eq_nat_dec n (if eq_nat_dec (S (i mod length us)) (length us) then 0%nat else S (i mod length us)) - then nth_default 0 us (i mod length us) >> log_cap (i mod length us) - else 0) - + nth_default d us n + then if eq_nat_dec n i + then Z.pow2_mod (nth_default 0 us n) (log_cap n) + else nth_default 0 us n + + if eq_nat_dec n (S i) then nth_default 0 us i >> log_cap i else 0 else d. Proof. - intros; unfold carry_simple; autorewrite with push_nth_default; - repeat break_match; reflexivity. + intros; unfold carry_simple; autorewrite with push_nth_default. + repeat break_match; try omega; try reflexivity. Qed. Hint Rewrite @nth_default_carry_simple_full : push_nth_default. Lemma nth_default_carry_gen - : forall f i us, + : forall fc fi i us, (0 <= i < length us)%nat - -> nth_default 0 (carry_gen limb_widths f i us) i - = (if PeanoNat.Nat.eq_dec i (if PeanoNat.Nat.eq_dec (S i) (length us) then 0%nat else S i) - then f (nth_default 0 us i >> log_cap i) + Z.pow2_mod (nth_default 0 us i) (log_cap i) - else Z.pow2_mod (nth_default 0 us i) (log_cap i)). + -> nth_default 0 (carry_gen limb_widths fc fi i us) i + = (if eq_nat_dec i (fi (length us) i) + then Z.pow2_mod (nth_default 0 us i) (log_cap i) + else nth_default 0 us i) + + if eq_nat_dec i (fi (length us) (S (fi (length us) i))) + then fc (nth_default 0 us (fi (length us) i) >> log_cap (fi (length us) i)) + else 0. Proof. - unfold carry_gen, carry_and_reduce_single. - intros; autorewrite with push_nth_default natsimplify; reflexivity. + intros; autorewrite with push_nth_default natsimplify; break_match; omega. Qed. Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. Lemma nth_default_carry_simple - : forall f i us, + : forall i us, (0 <= i < length us)%nat - -> nth_default 0 (carry_gen limb_widths f i us) i - = (if PeanoNat.Nat.eq_dec i (if PeanoNat.Nat.eq_dec (S i) (length us) then 0%nat else S i) - then f (nth_default 0 us i >> log_cap i) + Z.pow2_mod (nth_default 0 us i) (log_cap i) - else Z.pow2_mod (nth_default 0 us i) (log_cap i)). + -> nth_default 0 (carry_simple limb_widths i us) i + = Z.pow2_mod (nth_default 0 us i) (log_cap i). Proof. - unfold carry_gen, carry_and_reduce_single. - intros; autorewrite with push_nth_default natsimplify; reflexivity. + intros; autorewrite with push_nth_default natsimplify; break_match; omega. Qed. - Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. - - - Lemma nth_default_carry_gen - : forall f i us, - (0 <= i < length us)%nat - -> nth_default 0 (carry_gen limb_widths f i us) i - = (if PeanoNat.Nat.eq_dec i (if PeanoNat.Nat.eq_dec (S i) (length us) then 0%nat else S i) - then f (nth_default 0 us i >> log_cap i) + Z.pow2_mod (nth_default 0 us i) (log_cap i) - else Z.pow2_mod (nth_default 0 us i) (log_cap i)). - Proof. - unfold carry_gen, carry_and_reduce_single. - intros; autorewrite with push_nth_default natsimplify; reflexivity. - Qed. - Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. -*) + Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. End carrying. -(* Hint Rewrite @length_carry_gen : distr_length. -*) Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length. -(* -Hint Rewrite @nth_default_carry_gen_full : push_nth_default. -Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. -*) +Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default. +Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. -- cgit v1.2.3 From 90c6403a50addd0cd0775aa45510e78505304017 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 14:47:36 -0700 Subject: Silence a warning File "./src/Experiments/GenericFieldPow.v", line 130, characters 4-471: Warning: Casts are ignored in patterns [cast-in-pattern,automation] @andres-erbsen Did you intend for the cast at https://github.com/mit-plv/fiat-crypto/commit/6823b63275333ebb11c7f84068894f76cdb06068#diff-078114b2627a38e74938989c7ca2f6d1R131 to have semantic meaning for some reason, performance or otherwise? --- src/Experiments/GenericFieldPow.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v index 33d524567..b3d83dbe8 100644 --- a/src/Experiments/GenericFieldPow.v +++ b/src/Experiments/GenericFieldPow.v @@ -129,7 +129,7 @@ Module F. Field_simplify_done : forall (H:x==y), field_simplify_done H. Ltac field_nsatz := repeat match goal with - [ H: (_:F) == _ |- _ ] => + [ H: _ == _ |- _ ] => match goal with | [ Ha : field_simplify_done H |- _ ] => fail | _ => idtac -- cgit v1.2.3 From 29413b6c7d61993da6eaf9f5e6e9f227f4ec8709 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 14:51:51 -0700 Subject: Make Pow2BaseProofs independent of the def of add_to_nth --- src/ModularArithmetic/Pow2BaseProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 819a5adb5..6d6e3f530 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -575,7 +575,7 @@ Section carrying_helper. Lemma add_to_nth_sum : forall n x us, (n < length us \/ n >= length base)%nat -> BaseSystem.decode base (add_to_nth n x us) = x * nth_default 0 base n + BaseSystem.decode base us. - Proof. unfold add_to_nth; intros; rewrite set_nth_sum; try ring_simplify; auto. Qed. + Proof. intros; rewrite add_to_nth_set_nth, set_nth_sum; try ring_simplify; auto. Qed. Lemma add_to_nth_nth_default_full : forall n x l i d, nth_default d (add_to_nth n x l) i = -- cgit v1.2.3 From 526a60b8dcee4bcec55e50a7b6056b9c9090d73d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 15:49:42 -0700 Subject: Move more proofs earlier --- src/BaseSystemProofs.v | 44 ++++++++++++++++++------- src/ModularArithmetic/ExtendedBaseVector.v | 2 ++ src/ModularArithmetic/ModularBaseSystemProofs.v | 26 ++++++++------- 3 files changed, 48 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 8bd390635..8de0fdd0a 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -474,14 +474,8 @@ Section BaseSystemProofs. auto. Qed. - (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) - Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => - mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs - | _ => nil - end. - Definition mul us := mul' (rev us). + Local Notation mul' := (mul' base). + Local Notation mul := (mul base). Lemma mul'_rep : forall us vs, (length us + length vs <= length base)%nat -> @@ -521,7 +515,7 @@ Section BaseSystemProofs. Lemma mul_length: forall us vs, (length (mul us vs) <= length us + length vs)%nat. Proof. - intros; unfold mul. + intros; unfold BaseSystem.mul. rewrite mul'_length. rewrite rev_length; omega. Qed. @@ -541,7 +535,7 @@ Section BaseSystemProofs. end)%nat. Proof. induction us; intros; try solve [boring]. - unfold mul'; fold mul'. + unfold BaseSystem.mul'; fold mul'. unfold mul_each. rewrite add_length_exact, map_length, mul_bi_length, length_cons. destruct us. @@ -568,7 +562,7 @@ Section BaseSystemProofs. | _ => pred (length us + length vs) end)%nat. Proof. - intros; unfold mul; autorewrite with distr_length; reflexivity. + intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity. Qed. Hint Rewrite mul_length_exact_full : distr_length. @@ -579,7 +573,7 @@ Section BaseSystemProofs. (length us <= length vs)%nat -> us <> nil -> (length (mul us vs) = pred (length us + length vs))%nat. Proof. - intros; unfold mul. + intros; unfold BaseSystem.mul. rewrite mul'_length_exact; rewrite ?rev_length; try omega. intro rev_nil. match goal with H : us <> nil |- _ => apply H end. @@ -637,3 +631,29 @@ Section BaseSystemProofs. End BaseSystemProofs. Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length. + +Section MultiBaseSystemProofs. + Context base0 (base_vector0 : @BaseVector base0) base1 (base_vector1 : @BaseVector base1). + + Lemma decode_short_initial : forall (us : digits), + (firstn (length us) base0 = firstn (length us) base1) + -> decode base0 us = decode base1 us. + Proof. + intros us H. + unfold decode, decode'. + rewrite (combine_truncate_r us base0), (combine_truncate_r us base1), H. + reflexivity. + Qed. + + Lemma mul_rep_two_base : forall (us vs : digits), + (length us + length vs <= length base1)%nat + -> firstn (length us) base0 = firstn (length us) base1 + -> firstn (length vs) base0 = firstn (length vs) base1 + -> (decode base0 us) * (decode base0 vs) = decode base1 (mul base1 us vs). + Proof. + intros. + rewrite mul_rep by trivial. + apply f_equal2; apply decode_short_initial; assumption. + Qed. + +End MultiBaseSystemProofs. diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index d4df6040f..ddf787d21 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -160,3 +160,5 @@ Section ExtendedBaseVector. unfold ext_base; rewrite app_length; rewrite map_length; auto. Qed. End ExtendedBaseVector. + +Hint Rewrite @extended_base_length : distr_length. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index daff60220..227a3e77f 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -128,27 +128,29 @@ Section PseudoMersenneProofs. subst; auto. Qed. - Lemma decode_short : forall (us : BaseSystem.digits), - (length us <= length base)%nat -> - BaseSystem.decode base us = BaseSystem.decode ext_base us. + Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), + (length us <= length base)%nat + -> firstn (length us) base = firstn (length us) ext_base. Proof. - intros. - unfold BaseSystem.decode, BaseSystem.decode'. - rewrite combine_truncate_r. - rewrite (combine_truncate_r us ext_base). - f_equal; f_equal. - unfold ext_base. + unfold ext_base; intros. rewrite firstn_app_inleft; auto; omega. Qed. + Local Hint Immediate firstn_us_base_ext_base. + + Lemma decode_short : forall (us : BaseSystem.digits), + (length us <= length base)%nat -> + BaseSystem.decode base us = BaseSystem.decode ext_base us. + Proof. auto using decode_short_initial. Qed. + + Local Hint Immediate ExtBaseVector. Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), (length us <= length base)%nat -> (length vs <= length base)%nat -> (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs). Proof. - intros. - rewrite mul_rep by (apply ExtBaseVector || unfold ext_base; simpl_list; omega). - f_equal; rewrite decode_short; auto. + intros; apply mul_rep_two_base; auto; + autorewrite with distr_length; try omega. Qed. Lemma modulus_nonzero : modulus <> 0. -- cgit v1.2.3 From 3040eaa1c13725824fef2f8e7541fbf8540ee216 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:12:46 -0700 Subject: Add a ListUtil lemma --- src/Util/ListUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 3006dd799..49535da38 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1097,6 +1097,14 @@ Qed. Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn. +Lemma sum_firstn_succ_cons : forall x xs i, + sum_firstn (x :: xs) (S i) = (x + sum_firstn xs i)%Z. +Proof. + unfold sum_firstn; simpl; reflexivity. +Qed. + +Hint Rewrite @sum_firstn_succ_cons : simpl_sum_firstn. + Lemma sum_firstn_succ_default_rev : forall l i, sum_firstn l i = (sum_firstn l (S i) - nth_default 0 l i)%Z. Proof. -- cgit v1.2.3 From 6bcf94ac9f14950f140e00df78fd5cfd4bedb5bb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:33:14 -0700 Subject: Add a lemma about sum_firstn --- src/Util/ListUtil.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 49535da38..8b92ef4fa 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -23,6 +23,7 @@ Create HintDb pull_firstn discriminated. Create HintDb push_firstn discriminated. Create HintDb pull_update_nth discriminated. Create HintDb push_update_nth discriminated. +Create HintDb znonzero discriminated. Hint Rewrite @app_length @@ -1105,6 +1106,12 @@ Qed. Hint Rewrite @sum_firstn_succ_cons : simpl_sum_firstn. +Lemma sum_firstn_nil : forall i, + sum_firstn nil i = 0%Z. +Proof. destruct i; reflexivity. Qed. + +Hint Rewrite @sum_firstn_nil : simpl_sum_firstn. + Lemma sum_firstn_succ_default_rev : forall l i, sum_firstn l i = (sum_firstn l (S i) - nth_default 0 l i)%Z. Proof. @@ -1118,6 +1125,17 @@ Proof. intros; erewrite sum_firstn_succ by eassumption; omega. Qed. +Lemma sum_firstn_nonnegative : forall n l, (forall x, In x l -> 0 <= x)%Z + -> (0 <= sum_firstn l n)%Z. +Proof. + induction n as [|n IHn]; destruct l as [|? l]; autorewrite with simpl_sum_firstn; simpl; try omega. + { specialize (IHn l). + destruct n; simpl; autorewrite with simpl_sum_firstn simpl_nth_default in *; + intuition. } +Qed. + +Hint Resolve sum_firstn_nonnegative : znonzero. + Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, nth_default d (map2 f ls1 ls2) i = if lt_dec i (min (length ls1) (length ls2)) -- cgit v1.2.3 From 9b6a08343fd418296b069ead6fc4e879f8af0e7c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:35:51 -0700 Subject: Add a lemma about base_from_limb_widths and app --- src/ModularArithmetic/Pow2BaseProofs.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 6d6e3f530..6a8d4a8ff 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -150,6 +150,18 @@ Section Pow2BaseProofs. reflexivity. Qed. + Lemma base_from_limb_widths_app : forall l0 l + (l0_nonneg : forall x, In x l0 -> 0 <= x) + (l_nonneg : forall x, In x l -> 0 <= x), + base_from_limb_widths (l0 ++ l) + = base_from_limb_widths l0 ++ map (Z.mul (two_p (sum_firstn l0 (length l0)))) (base_from_limb_widths l). + Proof. + induction l0 as [|?? IHl0]. + { simpl; intros; rewrite <- map_id at 1; apply map_ext; intros; omega. } + { simpl; intros; rewrite !IHl0, !map_app, map_map, sum_firstn_succ_cons, two_p_is_exp by auto with znonzero. + do 2 f_equal; apply map_ext; intros; lia. } + Qed. + End Pow2BaseProofs. Section BitwiseDecodeEncode. -- cgit v1.2.3 From 2a14406a3d0ce41241471dbcb7cbd60fe2a66c59 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:44:57 -0700 Subject: ext_base: now defined in terms of ext_limb_widths --- src/ModularArithmetic/ExtendedBaseVector.v | 34 ++++++++++++++++++++----- src/ModularArithmetic/ModularBaseSystemOpt.v | 7 ++--- src/ModularArithmetic/ModularBaseSystemProofs.v | 4 +-- 3 files changed, 34 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index ddf787d21..0afd6b484 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -7,12 +7,13 @@ Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.BaseSystemProofs. Require Crypto.BaseSystem. Local Open Scope Z_scope. Section ExtendedBaseVector. Context `{prm : PseudoMersenneBaseParams}. - Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). (* This section defines a new BaseVector that has double the length of the BaseVector * used to construct [params]. The coefficients of the new vector are as follows: @@ -37,11 +38,19 @@ Section ExtendedBaseVector. * * This sum may be short enough to express using base; if not, we can reduce again. *) - Definition ext_base := base ++ (map (Z.mul (2^k)) base). + Definition ext_limb_widths := limb_widths ++ limb_widths. + Definition ext_base := base_from_limb_widths ext_limb_widths. + Lemma ext_base_alt : ext_base = base ++ (map (Z.mul (2^k)) base). + Proof. + unfold ext_base, ext_limb_widths. + rewrite base_from_limb_widths_app by auto using limb_widths_pos, Z.lt_le_incl. + rewrite two_p_equiv. + reflexivity. + Qed. Lemma ext_base_positive : forall b, In b ext_base -> b > 0. Proof. - unfold ext_base. intros b In_b_base. + rewrite ext_base_alt. intros b In_b_base. rewrite in_app_iff in In_b_base. destruct In_b_base as [In_b_base | In_b_extbase]. + eapply BaseSystem.base_positive. @@ -68,7 +77,7 @@ Section ExtendedBaseVector. Lemma b0_1 : forall x, nth_default x ext_base 0 = 1. Proof. - intros. unfold ext_base. + intros. rewrite ext_base_alt. rewrite nth_default_app. assert (0 < length base)%nat by (apply base_length_nonzero). destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega. @@ -120,7 +129,7 @@ Section ExtendedBaseVector. Proof. intros. subst b. subst r. - unfold ext_base in *. + rewrite ext_base_alt in *. rewrite app_length in H; rewrite map_length in H. repeat rewrite nth_default_app. repeat break_if; try omega. @@ -157,8 +166,21 @@ Section ExtendedBaseVector. Lemma extended_base_length: length ext_base = (length base + length base)%nat. Proof. - unfold ext_base; rewrite app_length; rewrite map_length; auto. + rewrite ext_base_alt, app_length, map_length; auto. + Qed. + + Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), + (length us <= length base)%nat + -> firstn (length us) base = firstn (length us) ext_base. + Proof. + rewrite ext_base_alt; intros. + rewrite firstn_app_inleft; auto; omega. Qed. + + Lemma decode_short : forall (us : BaseSystem.digits), + (length us <= length base)%nat -> + BaseSystem.decode base us = BaseSystem.decode ext_base us. + Proof. auto using decode_short_initial, firstn_us_base_ext_base. Qed. End ExtendedBaseVector. Hint Rewrite @extended_base_length : distr_length. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d7e6f1c65..696f10438 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -376,7 +376,7 @@ Section Multiplication. cbv [mul_bi'_step]. opt_step. { reflexivity. } - { cbv [crosscoef ext_base]. + { cbv [crosscoef]. change Z.div with Z_div_opt. change Z.mul with Z_mul_opt at 2. change @nth_default with @nth_default_opt. @@ -405,7 +405,7 @@ Section Multiplication. rewrite <- IHvsr; clear IHvsr. unfold mul_bi'_opt, mul_bi'_opt_step. apply f_equal2; [ | reflexivity ]. - cbv [crosscoef ext_base]. + cbv [crosscoef]. change Z.div with Z_div_opt. change Z.mul with Z_mul_opt at 2. change @nth_default with @nth_default_opt. @@ -477,7 +477,8 @@ Section Multiplication. Definition mul_opt_sig (us vs : digits) : { b : digits | b = mul us vs }. Proof. eexists. - cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. + cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros reduce]. + rewrite ext_base_alt. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. rewrite Z.map_shiftl by apply k_nonneg. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 227a3e77f..5d1becc00 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -132,7 +132,7 @@ Section PseudoMersenneProofs. (length us <= length base)%nat -> firstn (length us) base = firstn (length us) ext_base. Proof. - unfold ext_base; intros. + rewrite ext_base_alt; intros. rewrite firstn_app_inleft; auto; omega. Qed. Local Hint Immediate firstn_us_base_ext_base. @@ -184,7 +184,7 @@ Section PseudoMersenneProofs. Proof. intros. unfold BaseSystem.decode; rewrite <- mul_each_rep. - unfold ext_base. + rewrite ext_base_alt. replace (map (Z.mul (2 ^ k)) base) with (BaseSystem.mul_each (2 ^ k) base) by auto. rewrite base_mul_app. rewrite <- mul_each_rep; auto. -- cgit v1.2.3 From 51602bd1ccf7493e53f78afa958238cad14571f2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 18:25:20 +0200 Subject: Use update_nth in add_to_nth (#26) It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore. --- src/ModularArithmetic/Pow2Base.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index b842fa713..acc96ad73 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -48,14 +48,8 @@ Section Pow2Base. carrying. *) Notation log_cap i := (nth_default 0 limb_widths i). - - Definition add_to_nth n (x:Z) xs := - set_nth n (x + nth_default 0 xs n) xs. - (* TODO: Maybe we should use this instead? *) - (* Definition add_to_nth n (x:Z) xs := update_nth n (fun y => x + y) xs. - *) Definition carry_and_reduce_single i := fun di => (Z.pow2_mod di (log_cap i), Z.shiftr di (log_cap i)). -- cgit v1.2.3