From 1bacc083da890d7289f1ee54a41996db7a787a92 Mon Sep 17 00:00:00 2001 From: jadep Date: Sat, 17 Sep 2016 14:44:20 -0400 Subject: Move side lemmas to appropriate files --- src/BaseSystemProofs.v | 15 ++ .../ModularBaseSystemListProofs.v | 29 ++++ src/ModularArithmetic/ModularBaseSystemProofs.v | 158 +-------------------- src/ModularArithmetic/Pow2BaseProofs.v | 61 +++++++- src/Util/ListUtil.v | 37 +++++ src/Util/Tuple.v | 23 +++ 6 files changed, 162 insertions(+), 161 deletions(-) (limited to 'src') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 6e5bbbaea..1c2fe0fbe 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -4,6 +4,7 @@ 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. +Import Morphisms. Local Open Scope Z. Local Infix ".+" := add. @@ -44,6 +45,7 @@ Section BaseSystemProofs. Proof. intros; rewrite decode'_truncate; auto. Qed. + Hint Rewrite decode_base_nil. Lemma mul_each_rep : forall bs u vs, @@ -194,6 +196,19 @@ Section BaseSystemProofs. Qed. Hint Rewrite zeros_rep peel_decode. + Lemma decode_Proper : Proper (Logic.eq ==> (Forall2 Logic.eq) ==> Logic.eq) decode'. + Proof. + repeat intro; subst. + revert y y0 H0; induction x0; intros. + + inversion H0. rewrite !decode_nil. + reflexivity. + + inversion H0; subst. + destruct y as [|y0 y]; [rewrite !decode_base_nil; reflexivity | ]. + specialize (IHx0 y _ H4). + rewrite !peel_decode. + f_equal; auto. + Qed. + Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs. Proof. induction xs; destruct bs; boring. diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 48c4f2402..b3eff4caa 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -144,3 +144,32 @@ Section LengthProofs. Qed. End LengthProofs. + +Section ConditionalSubtractModulusProofs. + Context `{prm :PseudoMersenneBaseParams}. + Local Notation base := (base_from_limb_widths limb_widths). + + Lemma ge_modulus_spec : forall u, length u = length limb_widths -> + (ge_modulus u = false <-> 0 <= BaseSystem.decode base u < modulus). + Proof. + Admitted. + + Lemma conditional_subtract_modulus_spec : forall u cond, + length u = length limb_widths -> + BaseSystem.decode base (conditional_subtract_modulus u cond) = + BaseSystem.decode base u - (if cond then 1 else 0) * modulus. + Proof. + Admitted. + + Lemma conditional_subtract_modulus_preserves_bounded : forall u, + bounded limb_widths u -> + bounded limb_widths (conditional_subtract_modulus u (ge_modulus u)). + Proof. + Admitted. + + Lemma conditional_subtract_lt_modulus : forall u, + bounded limb_widths u -> + ge_modulus (conditional_subtract_modulus u (ge_modulus u)) = false. + Proof. + Admitted. +End ConditionalSubtractModulusProofs. \ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index ae5db0fc2..a551adc2f 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -92,87 +92,12 @@ Section FieldOperationProofs. + eauto using base_upper_bound_compatible, limb_widths_nonneg. Qed. - (* TODO : move to Pow2Base *) - Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil. - Proof. - cbv [bounded]; intros. - rewrite nth_default_nil. - apply nth_default_preserves_properties; intros; split; zero_bounds. - Qed. - - (* TODO : move to Pow2Base *) - Lemma length_encode' : forall lw z i, length (encode' lw z i) = i. - Proof. - induction i; intros; simpl encode'; distr_length. - Qed. - Hint Rewrite length_encode' : distr_length. - - (* TODO : move to ListUtil *) - Lemma nth_default_firstn : forall {A} (d : A) l i n, - nth_default d (firstn n l) i = if le_dec n (length l) - then if lt_dec i n then nth_default d l i else d - else nth_default d l i. - Proof. - induction n; intros; break_if; autorewrite with push_nth_default; auto; try omega. - + rewrite (firstn_succ d) by omega. - autorewrite with push_nth_default; repeat (break_if; distr_length); - rewrite Min.min_l in * by omega; try omega. - - apply IHn; omega. - - replace i with n in * by omega. - rewrite Nat.sub_diag. - autorewrite with push_nth_default; auto. - - rewrite nth_default_out_of_bounds; distr_length; auto. - + rewrite firstn_all2 by omega. - auto. - Qed. - Hint Rewrite @nth_default_firstn : push_nth_default. - - (* TODO : move to Pow2Base *) - Lemma bounded_encode' : forall z i, (0 <= z) -> - bounded (firstn i limb_widths) (encode' limb_widths z i). - Proof. - intros; induction i; simpl encode'; - repeat match goal with - | |- _ => progress intros - | |- _ => progress autorewrite with push_nth_default in * - | |- _ => progress autorewrite with Ztestbit - | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in * - | |- _ => rewrite Z.testbit_pow2_mod by auto - | |- _ => rewrite Z.ones_spec by zero_bounds - | |- _ => rewrite sum_firstn_succ_default - | |- _ => rewrite nth_default_out_of_bounds by distr_length - | |- _ => break_if; distr_length - | |- _ => apply bounded_nil_r - | |- appcontext[nth_default _ (_ :: nil) ?i] => case_eq i; intros; autorewrite with push_nth_default - | |- Z.pow2_mod (?a >> ?b) _ = (?a >> ?b) => apply Z.bits_inj' - | IH : forall i, _ = nth_default 0 (encode' _ _ _) i - |- appcontext[nth_default 0 limb_widths ?i] => specialize (IH i) - | H : In _ (firstn _ _) |- _ => apply In_firstn in H - | H1 : ~ (?a < ?b)%nat, H2 : (?a < S ?b)%nat |- _ => - progress replace a with b in * by omega - | H : bounded _ _ |- bounded _ _ => - apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H - | |- _ => solve [auto] - | |- _ => contradiction - | |- _ => reflexivity - end. - Qed. - - (* TODO : move to Pow2Base *) - Lemma bounded_encodeZ : forall z, (0 <= z) -> - bounded limb_widths (encodeZ limb_widths z). - Proof. - cbv [encodeZ]; intros. - pose proof (bounded_encode' z (length limb_widths)) as Hencode'. - rewrite firstn_all in Hencode'; auto. - Qed. - Lemma bounded_encode : forall x, bounded limb_widths (to_list (encode x)). Proof. intros. cbv [encode]; rewrite to_list_from_list. cbv [ModularBaseSystemList.encode]. - apply bounded_encodeZ. + apply bounded_encodeZ; auto. apply F.to_Z_range. pose proof prime_modulus; prime_bound. Qed. @@ -873,55 +798,6 @@ Section CanonicalizationProofs. auto using length_carry_full, bound_after_second_loop. Qed. - Lemma ge_modulus_spec : forall u, length u = length limb_widths -> - (ge_modulus u = false <-> 0 <= BaseSystem.decode base u < modulus). - Proof. - Admitted. - - Lemma conditional_subtract_modulus_spec : forall u cond, - length u = length limb_widths -> - BaseSystem.decode base (conditional_subtract_modulus u cond) = - BaseSystem.decode base u - (if cond then 1 else 0) * modulus. - Proof. - Admitted. - - Lemma conditional_subtract_modulus_preserves_bounded : forall u, - bounded limb_widths u -> - bounded limb_widths (conditional_subtract_modulus u (ge_modulus u)). - Proof. - Admitted. - - Lemma conditional_subtract_lt_modulus : forall u, - bounded limb_widths u -> - ge_modulus (conditional_subtract_modulus u (ge_modulus u)) = false. - Proof. - Admitted. - - (* bounded canonical -> freeze bounded -> freeze canonical *) - - Import SetoidList. - (* TODO : move to Tuple *) - Lemma fieldwise_to_list_iff : forall {T n} R (s t : tuple T n), - (fieldwise R s t <-> Forall2 R (to_list _ s) (to_list _ t)). - Proof. - induction n; split; intros. - + constructor. - + cbv [fieldwise]. auto. - + destruct n; cbv [tuple to_list fieldwise] in *. - - cbv [to_list']; auto. - - simpl in *. destruct s,t; cbv [fst snd] in *. - constructor; intuition auto. - apply IHn; auto. - + destruct n; cbv [tuple to_list fieldwise] in *. - - cbv [fieldwise']; auto. - cbv [to_list'] in *; inversion H; auto. - - simpl in *. destruct s,t; cbv [fst snd] in *. - inversion H; subst. - split; try assumption. - apply IHn; auto. - Qed. - - Local Notation initial_bounds u := (forall n : nat, 0 <= to_list (length limb_widths) u [n] < @@ -931,38 +807,6 @@ Section CanonicalizationProofs. else (2 ^ B) >> (limb_widths [Init.Nat.pred n]))). Local Notation minimal_rep u := ((bounded limb_widths (to_list (length limb_widths) u)) /\ (ge_modulus (to_list _ u) = false)). - Import Morphisms. - (* TODO : move somewhere *) - Check Proper. - Lemma decode_Proper : Proper (Logic.eq ==> (Forall2 Logic.eq) ==> Logic.eq) decode'. - Proof. - repeat intro; subst. - revert y y0 H0; induction x0; intros. - + inversion H0. rewrite !decode_nil. - reflexivity. - + inversion H0; subst. - destruct y as [|y0 y]; [rewrite !decode_base_nil; reflexivity | ]. - specialize (IHx0 y _ H4). - rewrite !peel_decode. - f_equal; auto. - Qed. - - (* TODO : move to ListUtil *) - Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys -> - (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). - Proof. - split; intros. - + revert xs ys H H0 H1. - induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto. - eapply IHi; auto. omega. - + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor. - - specialize (H0 0%nat); specialize_by omega. - autorewrite with push_nth_default in *; auto. - - apply IHxs; try omega. - intros. - specialize (H0 (S i)); specialize_by omega. - autorewrite with push_nth_default in *; auto. - Qed. Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v -> (fieldwise Logic.eq u v <-> diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 7158dc22a..be2986ce6 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -555,6 +555,13 @@ Section Pow2BaseProofs. autorewrite with distr_length simpl_sum_firstn pull_Zpow. reflexivity. Qed. + + Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil. + Proof. + cbv [bounded]; intros. + rewrite nth_default_nil. + apply nth_default_preserves_properties; intros; split; zero_bounds. + Qed. Section make_base_vector. Local Notation k := (sum_firstn limb_widths (length limb_widths)). @@ -639,6 +646,8 @@ Section BitwiseDecodeEncode. sum_firstn limb_widths (i + j) <= sum_firstn limb_widths i + sum_firstn limb_widths j). Local Hint Resolve limb_widths_nonneg. + Local Hint Resolve nth_default_limb_widths_nonneg. + Local Hint Resolve sum_firstn_limb_widths_nonneg. Local Notation "w[ i ]" := (nth_default 0 limb_widths i). Local Notation base := (base_from_limb_widths limb_widths). Local Notation upper_bound := (upper_bound limb_widths). @@ -650,7 +659,7 @@ Section BitwiseDecodeEncode. + rewrite encode'_zero. reflexivity. + rewrite encode'_succ, <-IHi by omega. simpl; do 2 f_equal. - rewrite Z.land_ones, Z.shiftr_div_pow2 by auto using sum_firstn_limb_widths_nonneg. + rewrite Z.land_ones, Z.shiftr_div_pow2 by auto. match goal with H : (S _ <= length limb_widths)%nat |- _ => apply le_lt_or_eq in H; destruct H end. - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity. @@ -660,6 +669,50 @@ Section BitwiseDecodeEncode. congruence. Qed. + Lemma length_encode' : forall lw z i, length (encode' lw z i) = i. + Proof. + induction i; intros; simpl encode'; distr_length. + Qed. + Hint Rewrite length_encode' : distr_length. + + Lemma bounded_encode' : forall z i, (0 <= z) -> + bounded (firstn i limb_widths) (encode' limb_widths z i). + Proof. + intros; induction i; simpl encode'; + repeat match goal with + | |- _ => progress intros + | |- _ => progress autorewrite with push_nth_default in * + | |- _ => progress autorewrite with Ztestbit + | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in * + | |- _ => rewrite Z.testbit_pow2_mod by auto + | |- _ => rewrite Z.ones_spec by zero_bounds + | |- _ => rewrite sum_firstn_succ_default + | |- _ => rewrite nth_default_out_of_bounds by distr_length + | |- _ => break_if; distr_length + | |- _ => apply bounded_nil_r + | |- appcontext[nth_default _ (_ :: nil) ?i] => case_eq i; intros; autorewrite with push_nth_default + | |- Z.pow2_mod (?a >> ?b) _ = (?a >> ?b) => apply Z.bits_inj' + | IH : forall i, _ = nth_default 0 (encode' _ _ _) i + |- appcontext[nth_default 0 limb_widths ?i] => specialize (IH i) + | H : In _ (firstn _ _) |- _ => apply In_firstn in H + | H1 : ~ (?a < ?b)%nat, H2 : (?a < S ?b)%nat |- _ => + progress replace a with b in * by omega + | H : bounded _ _ |- bounded _ _ => + apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H + | |- _ => solve [auto] + | |- _ => contradiction + | |- _ => reflexivity + end. + Qed. + + Lemma bounded_encodeZ : forall z, (0 <= z) -> + bounded limb_widths (encodeZ limb_widths z). + Proof. + cbv [encodeZ]; intros. + pose proof (bounded_encode' z (length limb_widths)) as Hencode'. + rewrite firstn_all in Hencode'; auto. + Qed. + Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound. Proof. unfold base_max_succ_divide; intros i lt_Si_length. @@ -667,14 +720,14 @@ Section BitwiseDecodeEncode. rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; rewrite !nth_default_base by (omega || auto). + erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega). - rewrite Z.pow_add_r; eauto using sum_firstn_limb_widths_nonneg, nth_default_limb_widths_nonneg. + rewrite Z.pow_add_r; eauto. apply Z.divide_factor_r. + rewrite nth_default_out_of_bounds by (distr_length; omega). unfold Pow2Base.upper_bound. replace (length limb_widths) with (S (pred (length limb_widths))) by omega. replace i with (pred (length limb_widths)) by omega. erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega). - rewrite Z.pow_add_r; eauto using sum_firstn_limb_widths_nonneg, nth_default_limb_widths_nonneg. + rewrite Z.pow_add_r; eauto. apply Z.divide_factor_r. Qed. Hint Resolve base_upper_bound_compatible. @@ -686,7 +739,7 @@ Section BitwiseDecodeEncode. assert (length base = length limb_widths) by distr_length. unfold encodeZ; rewrite encode'_spec by omega. erewrite BaseSystemProofs.encode'_spec; unfold Pow2Base.upper_bound; - zero_bounds; intros; eauto using sum_firstn_limb_widths_nonneg, base_positive, b0_1. { + zero_bounds; intros; eauto using base_positive, b0_1. { rewrite nth_default_out_of_bounds by omega. reflexivity. } { diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 11c92c72c..4f544d2c8 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1541,6 +1541,43 @@ Proof. intuition (congruence || eauto). Qed. +Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys -> + (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). +Proof. + split; intros. + + revert xs ys H H0 H1. + induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto. + eapply IHi; auto. omega. + + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor. + - specialize (H0 0%nat). + autorewrite with push_nth_default in *; auto. + apply H0; omega. + - apply IHxs; try omega. + intros. + specialize (H0 (S i)). + autorewrite with push_nth_default in *; auto. + apply H0; omega. +Qed. + +Lemma nth_default_firstn : forall {A} (d : A) l i n, + nth_default d (firstn n l) i = if le_dec n (length l) + then if lt_dec i n then nth_default d l i else d + else nth_default d l i. +Proof. + induction n; intros; break_if; autorewrite with push_nth_default; auto; try omega. + + rewrite (firstn_succ d) by omega. + autorewrite with push_nth_default; repeat (break_if; distr_length); + rewrite Min.min_l in * by omega; try omega. + - apply IHn; omega. + - replace i with n in * by omega. + rewrite Nat.sub_diag. + autorewrite with push_nth_default; auto. + - rewrite nth_default_out_of_bounds; distr_length; auto. + + rewrite firstn_all2 by omega. + auto. +Qed. +Hint Rewrite @nth_default_firstn : push_nth_default. + Lemma nth_error_repeat {T} x n i v : nth_error (@repeat T x n) i = Some v -> v = x. Proof. revert n x v; induction i as [|i IHi]; destruct n; simpl in *; eauto; congruence. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 76064e7b4..dbd585cca 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -238,5 +238,28 @@ Definition apply {R T} (n:nat) : function R T n -> tuple T n -> R := | S n' => fun f x => apply' n' f x end. +Require Import Coq.Lists.SetoidList. + +Lemma fieldwise_to_list_iff : forall {T n} R (s t : tuple T n), + (fieldwise R s t <-> Forall2 R (to_list _ s) (to_list _ t)). +Proof. + induction n; split; intros. + + constructor. + + cbv [fieldwise]. auto. + + destruct n; cbv [tuple to_list fieldwise] in *. + - cbv [to_list']; auto. + - simpl in *. destruct s,t; cbv [fst snd] in *. + constructor; intuition auto. + apply IHn; auto. + + destruct n; cbv [tuple to_list fieldwise] in *. + - cbv [fieldwise']; auto. + cbv [to_list'] in *; inversion H; auto. + - simpl in *. destruct s,t; cbv [fst snd] in *. + inversion H; subst. + split; try assumption. + apply IHn; auto. +Qed. + + Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *) Hint Rewrite length_to_list' @length_to_list : distr_length. -- cgit v1.2.3