From 305253c724b263476e0aaf0359e5f9ec83211be6 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 13 Feb 2017 13:07:18 -0500 Subject: Moved N lemmas from Ed25519 and IterAssocOp into new NUtil file --- _CoqProject | 1 + src/Experiments/Ed25519.v | 32 +------------- src/Util/IterAssocOp.v | 81 ++--------------------------------- src/Util/NUtil.v | 106 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 113 insertions(+), 107 deletions(-) create mode 100644 src/Util/NUtil.v diff --git a/_CoqProject b/_CoqProject index ad5fd28b5..f13bf2b2c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -459,6 +459,7 @@ src/Util/Logic.v src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v +src/Util/NUtil.v src/Util/Option.v src/Util/PartiallyReifiedProp.v src/Util/PointedProp.v diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 825fe541e..123c72e2c 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -8,6 +8,7 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Option. +Require Import Crypto.Util.NUtil. Require Crypto.Specific.GF25519. Require Crypto.Specific.GF25519Bounded. Require Crypto.Specific.SC25519. @@ -248,35 +249,6 @@ Proof. assumption. Qed. -(* MOVE: I think this is all just generic N stuff? *) -Module N. - Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N. - Proof. - destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l. - { destruct a; auto. } - { rewrite !N.size_log2 by assumption. - rewrite <-N.succ_le_mono. - apply N.log2_le_mono. } - Qed. - - Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat. - Proof. - rewrite <-N.lt_succ_r. - rewrite <-Nat.lt_succ_r. - rewrite <-Nnat.N2Nat.inj_succ. - rewrite <-NatUtil.Nat2N_inj_lt. - rewrite !Nnat.N2Nat.id. - reflexivity. - Qed. - - Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. - Proof. - rewrite !IterAssocOp.Nsize_nat_equiv. - rewrite <-le_to_nat. - apply size_le. - Qed. -End N. - Section SRepERepMul. Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Import Coq.NArith.NArith Coq.PArith.BinPosDef. @@ -323,7 +295,7 @@ Section SRepERepMul. apply Z2N.inj_lt in Hu; try (eauto || vm_decide); []; apply Z2N.inj_le in Hl; try (eauto || vm_decide); []. clear Hl; generalize dependent (Z.to_N z); intro x; intros. - rewrite Nsize_nat_equiv. + rewrite N.size_nat_equiv. destruct (dec (x = 0%N)); subst; try vm_decide; []; rewrite N.size_log2 by assumption. rewrite N2Nat.inj_succ; assert (N.to_nat (N.log2 x) < ll); try omega. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index d630698e7..85868f33f 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,8 +1,8 @@ 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. -Require Import Crypto.Algebra. -Import Monoid. +Require Import Crypto.Algebra. Import Monoid. +Require Import Crypto.Util.NUtil. Local Open Scope equiv_scope. @@ -64,56 +64,6 @@ Section IterAssocOp. Definition test_and_op_inv a (s : nat * T) := snd s === nat_iter_op (N.to_nat (N.shiftr_nat x (fst s))) a. - Hint Rewrite - N.succ_double_spec - N.add_1_r - Nat2N.inj_succ - Nat2N.inj_mul - N2Nat.id: N_nat_conv - . - - Lemma Nsucc_double_to_nat : forall n, - N.succ_double n = N.of_nat (S (2 * N.to_nat n)). - Proof. - intros. - replace 2 with (N.to_nat 2) by auto. - autorewrite with N_nat_conv. - reflexivity. - Qed. - - Lemma Ndouble_to_nat : forall n, - N.double n = N.of_nat (2 * N.to_nat n). - Proof. - intros. - replace 2 with (N.to_nat 2) by auto. - autorewrite with N_nat_conv. - reflexivity. - Qed. - - Lemma Nshiftr_succ : forall n i, - N.to_nat (N.shiftr_nat n i) = - if N.testbit_nat n i - then S (2 * N.to_nat (N.shiftr_nat n (S i))) - else (2 * N.to_nat (N.shiftr_nat n (S i))). - Proof. - intros. - rewrite Nshiftr_nat_S. - case_eq (N.testbit_nat n i); intro testbit_i; - pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd; - rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd; - rewrite testbit_i in shiftr_n_odd. - + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift. - rewrite Nsucc_double_to_nat in Nsucc_double_shift. - apply Nat2N.inj. - rewrite Nsucc_double_shift. - apply N2Nat.id. - + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift. - rewrite Ndouble_to_nat in Nsucc_double_shift. - apply Nat2N.inj. - rewrite Nsucc_double_shift. - apply N2Nat.id. - Qed. - Lemma test_and_op_inv_step : forall a s, test_and_op_inv a s -> test_and_op_inv a (test_and_op a s). @@ -122,7 +72,7 @@ Section IterAssocOp. unfold test_and_op_inv, test_and_op; simpl; intro Hpre. destruct i; [ apply Hpre | ]. simpl. - rewrite Nshiftr_succ. + rewrite N.shiftr_succ. rewrite sel_correct. case_eq (testbit i); intro testbit_eq; simpl; rewrite testbit_correct in testbit_eq; rewrite testbit_eq; @@ -157,29 +107,6 @@ Section IterAssocOp. reflexivity. Qed. - Lemma Nsize_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n). - Proof. - destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. - Qed. - - Lemma Nshiftr_size : forall n bound, N.size_nat n <= bound -> - N.shiftr_nat n bound = 0%N. - Proof. - intros. - rewrite <- (Nat2N.id bound). - rewrite Nshiftr_nat_equiv. - destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|]. - apply N.shiftr_eq_0. - rewrite Nsize_nat_equiv in *. - rewrite N.size_log2 in * by auto. - apply N.le_succ_l. - rewrite <- N.compare_le_iff. - rewrite N2Nat.inj_compare. - rewrite <- Compare_dec.nat_compare_le. - rewrite Nat2N.id. - auto. - Qed. - Lemma iter_op_correct : forall a bound, N.size_nat x <= bound -> iter_op bound a === nat_iter_op (N.to_nat x) a. Proof. @@ -188,7 +115,7 @@ Section IterAssocOp. apply test_and_op_inv_holds. unfold test_and_op_inv. simpl. - rewrite Nshiftr_size by auto. + rewrite N.shiftr_size by auto. reflexivity. Qed. End IterAssocOp. diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v new file mode 100644 index 000000000..309272a90 --- /dev/null +++ b/src/Util/NUtil.v @@ -0,0 +1,106 @@ +Require Import Coq.NArith.NArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.Util.NatUtil Crypto.Util.Decidable. + +Module N. + Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N. + Proof. + destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l. + { destruct a; auto. } + { rewrite !N.size_log2 by assumption. + rewrite <-N.succ_le_mono. + apply N.log2_le_mono. } + Qed. + + Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat. + Proof. + rewrite <-N.lt_succ_r. + rewrite <-Nat.lt_succ_r. + rewrite <-Nnat.N2Nat.inj_succ. + rewrite <-NatUtil.Nat2N_inj_lt. + rewrite !Nnat.N2Nat.id. + reflexivity. + Qed. + + Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n). + Proof. + destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. + Qed. + + Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. + Proof. + rewrite !size_nat_equiv. + rewrite <-le_to_nat. + apply size_le. + Qed. + + Lemma shiftr_size : forall n bound, N.size_nat n <= bound -> + N.shiftr_nat n bound = 0%N. + Proof. + intros. + rewrite <- (Nat2N.id bound). + rewrite Nshiftr_nat_equiv. + destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|]. + apply N.shiftr_eq_0. + rewrite size_nat_equiv in *. + rewrite N.size_log2 in * by auto. + apply N.le_succ_l. + rewrite <- N.compare_le_iff. + rewrite N2Nat.inj_compare. + rewrite <- Compare_dec.nat_compare_le. + rewrite Nat2N.id. + auto. + Qed. + + Hint Rewrite + N.succ_double_spec + N.add_1_r + Nat2N.inj_succ + Nat2N.inj_mul + N2Nat.id: N_nat_conv + . + + Lemma succ_double_to_nat : forall n, + N.succ_double n = N.of_nat (S (2 * N.to_nat n)). + Proof. + intros. + replace 2 with (N.to_nat 2) by auto. + autorewrite with N_nat_conv. + reflexivity. + Qed. + + Lemma double_to_nat : forall n, + N.double n = N.of_nat (2 * N.to_nat n). + Proof. + intros. + replace 2 with (N.to_nat 2) by auto. + autorewrite with N_nat_conv. + reflexivity. + Qed. + + Lemma shiftr_succ : forall n i, + N.to_nat (N.shiftr_nat n i) = + if N.testbit_nat n i + then S (2 * N.to_nat (N.shiftr_nat n (S i))) + else (2 * N.to_nat (N.shiftr_nat n (S i))). + Proof. + intros. + rewrite Nshiftr_nat_S. + case_eq (N.testbit_nat n i); intro testbit_i; + pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd; + rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd; + rewrite testbit_i in shiftr_n_odd. + + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift. + rewrite succ_double_to_nat in Nsucc_double_shift. + apply Nat2N.inj. + rewrite Nsucc_double_shift. + apply N2Nat.id. + + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift. + rewrite double_to_nat in Nsucc_double_shift. + apply Nat2N.inj. + rewrite Nsucc_double_shift. + apply N2Nat.id. + Qed. + + +End N. -- cgit v1.2.3