From 44a9f78bb082dbc5275f7d4ae07501dc7cba8a07 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 14 Jun 2016 15:21:35 -0400 Subject: Finished admits for canonicalization proofs. --- src/BaseSystemProofs.v | 12 + src/ModularArithmetic/ModularBaseSystemProofs.v | 729 ++++++++++++------------ src/Util/ListUtil.v | 9 + src/Util/ZUtil.v | 95 ++- 4 files changed, 467 insertions(+), 378 deletions(-) (limited to 'src') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index ab56cb711..a2ebb7b41 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -130,6 +130,18 @@ Section BaseSystemProofs. Qed. Hint Rewrite zeros_app0. + Lemma nth_default_zeros : forall n i, nth_default 0 (BaseSystem.zeros n) i = 0. + Proof. + induction n; intros; [ cbv [BaseSystem.zeros]; apply nth_default_nil | ]. + rewrite <-zeros_app0, nth_default_app. + rewrite length_zeros. + destruct (lt_dec i n); auto. + destruct (eq_nat_dec i n); subst. + + rewrite Nat.sub_diag; apply nth_default_cons. + + apply nth_default_out_of_bounds. + cbv [length]; omega. + Qed. + Lemma rev_zeros : forall n, rev (zeros n) = zeros n. Proof. induction n; boring. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index f7dbcc93a..bb6c68423 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -219,6 +219,21 @@ Section PseudoMersenneProofs. unfold add_to_nth; intros; rewrite set_nth_sum; try ring_simplify; auto. Qed. + Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat -> + nth_default 0 (add_to_nth n x l) i = + if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i. + Proof. + intros. + unfold add_to_nth. + rewrite set_nth_nth_default by assumption. + break_if; subst; reflexivity. + Qed. + + Lemma length_add_to_nth : forall n x l, length (add_to_nth n x l) = length l. + Proof. + unfold add_to_nth; intros; apply length_set_nth. + Qed. + Lemma nth_default_base_positive : forall i, (i < length base)%nat -> nth_default 0 base i > 0. Proof. @@ -240,6 +255,14 @@ Section PseudoMersenneProofs. apply base_succ; auto. Qed. + Lemma Fdecode_decode_mod : forall us x, (length us = length base) -> + decode us = x -> BaseSystem.decode base us mod modulus = x. + Proof. + unfold decode; intros ? ? ? decode_us. + rewrite <-decode_us. + apply FieldToZ_ZToField. + Qed. + End PseudoMersenneProofs. Section CarryProofs. @@ -405,43 +428,9 @@ Section CanonicalizationProofs. (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < max_bound 0 + 1) (* on the second reduce step, we add at most one bit of width to the first digit, and leave room to carry c one more time after the highest bit is carried *) - (c_reduce2 : c <= max_bound 0 - c). -(* TODO (c_reduce2: max_bound 0 + c < 2 ^ (log_cap 0 + 1)). c < max_bound 0 + 2*) - - (* TODO : move *) - Lemma set_nth_nth_default : forall {A} (d:A) n x l i, (0 <= i < length l)%nat -> - nth_default d (set_nth n x l) i = - if (eq_nat_dec i n) then x else nth_default d l i. - Proof. - induction n; (destruct l; [intros; simpl in *; omega | ]); simpl; - destruct i; break_if; try omega; intros; try apply nth_default_cons; - rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity. - Qed. - - (* TODO : move *) - Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat -> - nth_default 0 (add_to_nth n x l) i = - if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i. - Proof. - intros. - unfold add_to_nth. - rewrite set_nth_nth_default by assumption. - break_if; subst; reflexivity. - Qed. - - (* TODO : move *) - Lemma length_add_to_nth : forall n x l, length (add_to_nth n x l) = length l. - Proof. - unfold add_to_nth; intros; apply length_set_nth. - Qed. - - (* TODO : move *) - Lemma singleton_list : forall {A} (l : list A), length l = 1%nat -> exists x, l = x :: nil. - Proof. - intros; destruct l; simpl in *; try congruence. - eexists; f_equal. - apply length0_nil; omega. - Qed. + (c_reduce2 : c <= max_bound 0 - c) + (* this condition is probably implied by c_reduce2, but is more straighforward to compute than to prove *) + (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). (* BEGIN groundwork proofs *) @@ -459,7 +448,7 @@ Section CanonicalizationProofs. omega. Qed. - Hint Resolve log_cap_nonneg. + Local Hint Resolve log_cap_nonneg. Lemma pow2_mod_log_cap_range : forall a i, 0 <= pow2_mod a (log_cap i) <= max_bound i. Proof. intros. @@ -496,16 +485,6 @@ Section CanonicalizationProofs. omega. Qed. - (* TODO : move *) - Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. - Proof. - intros. - unfold Z.ones. - rewrite Z.shiftl_1_l. - apply Z.lt_succ_lt_pred. - apply Z.pow_gt_1; omega. - Qed. - Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i. Proof. unfold max_bound, log_cap; intros; apply Z_ones_pos_pos. @@ -529,15 +508,6 @@ Section CanonicalizationProofs. rewrite Z.land_ones; auto. Qed. - Lemma pow2_mod_upper_bound : forall a b, (0 <= a) -> (0 <= b) -> pow2_mod a b <= a. - Proof. - intros. - unfold pow2_mod. - rewrite Z.land_ones; auto. - apply Z.mod_le; auto. - apply Z.pow_pos_nonneg; omega. - Qed. - Lemma shiftr_eq_0_max_bound : forall i a, Z.shiftr a (log_cap i) = 0 -> a <= max_bound i. Proof. @@ -592,9 +562,9 @@ Section CanonicalizationProofs. 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'. - Ltac add_set_nth := rewrite ?add_to_nth_nth_default; try solve [carry_length_conditions]; - try break_if; try omega; rewrite ?set_nth_nth_default; try solve [carry_length_conditions]; - try break_if; try omega. + Ltac add_set_nth := + rewrite ?add_to_nth_nth_default by carry_length_conditions; break_if; try omega; + rewrite ?set_nth_nth_default by carry_length_conditions; break_if; try omega. (* BEGIN defs *) @@ -609,30 +579,10 @@ Section CanonicalizationProofs. specialize (PCB i). omega. Qed. - Hint Resolve pre_carry_bounds_nonzero. + Local Hint Resolve pre_carry_bounds_nonzero. - Definition carry_done us := forall i, (i < length base)%nat -> Z.shiftr (nth_default 0 us i) (log_cap i) = 0. - - Lemma carry_carry_done_done : forall i us, - (length us = length base)%nat -> - (i < length base)%nat -> - (forall i, 0 <= nth_default 0 us i) -> - carry_done us -> carry_done (carry i us). - Proof. - unfold carry_done; intros until 3. intros Hcarry_done ? ?. - unfold carry, carry_simple, carry_and_reduce; break_if; subst. - + rewrite Hcarry_done by omega. - rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). - destruct i0; add_set_nth; rewrite ?Z.mul_0_r, ?Z.add_0_l; auto. - match goal with H : S _ = pred (length base) |- _ => rewrite H; auto end. - + rewrite Hcarry_done by omega. - rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). - destruct i0; add_set_nth; subst; rewrite ?Z.add_0_l; auto. - Qed. - - Lemma carry_done_bounds : forall us, carry_done us <-> - (forall i, 0 <= nth_default 0 us i < 2 ^ log_cap i). - Admitted. + Definition carry_done us := forall i, (i < length base)%nat -> + 0 <= nth_default 0 us i /\ Z.shiftr (nth_default 0 us i) (log_cap i) = 0. (* END defs *) @@ -652,6 +602,7 @@ Section CanonicalizationProofs. apply pow2_mod_log_cap_bounds_upper. - rewrite nth_default_out_of_bounds by carry_length_conditions; auto. Qed. + Local Hint Resolve nth_default_carry_bound_upper. Lemma nth_default_carry_bound_lower : forall i us, (length us = length base) -> 0 <= nth_default 0 (carry i us) i. @@ -667,6 +618,7 @@ Section CanonicalizationProofs. apply pow2_mod_log_cap_bounds_lower. - rewrite nth_default_out_of_bounds by carry_length_conditions; omega. Qed. + Local Hint Resolve nth_default_carry_bound_lower. Lemma nth_default_carry_bound_succ_lower : forall i us, (forall i, 0 <= nth_default 0 us i) -> (length us = length base) -> @@ -677,13 +629,10 @@ Section CanonicalizationProofs. + subst. replace (S (pred (length base))) with (length base) by omega. rewrite nth_default_out_of_bounds; carry_length_conditions. unfold carry_and_reduce. - add_set_nth. + carry_length_conditions. + unfold carry_simple. destruct (lt_dec (S i) (length us)). - - add_set_nth. - apply Z.add_nonneg_nonneg; [ apply Z.shiftr_nonneg | ]; unfold pre_carry_bounds in PCB. - * specialize (PCB i). omega. - * specialize (PCB (S i)). omega. + - add_set_nth; zero_bounds. - rewrite nth_default_out_of_bounds by carry_length_conditions; omega. Qed. @@ -711,7 +660,7 @@ Section CanonicalizationProofs. destruct (lt_dec i (length us)); [ | rewrite !nth_default_out_of_bounds by carry_length_conditions; reflexivity]. unfold carry, carry_simple. - break_if; add_set_nth. + break_if; [omega | add_set_nth]. Qed. Lemma carry_nothing : forall i j us, (i < length base)%nat -> @@ -725,18 +674,60 @@ Section CanonicalizationProofs. | subst; apply pow2_mod_log_cap_small; assumption ]). Qed. + Lemma carry_done_bounds : forall us, (length us = length base) -> + (carry_done us <-> forall i, 0 <= nth_default 0 us i < 2 ^ log_cap i). + Proof. + intros ? ?; unfold carry_done; split; [ intros Hcarry_done i | intros Hbounds i i_lt ]. + + destruct (lt_dec i (length base)) as [i_lt | i_nlt]. + - specialize (Hcarry_done i i_lt). + split; [ intuition | ]. + rewrite <- max_bound_log_cap. + apply Z.lt_succ_r. + apply shiftr_eq_0_max_bound; intuition. + - rewrite nth_default_out_of_bounds; try split; try omega; auto. + + specialize (Hbounds i). + split; intuition. + apply max_bound_shiftr_eq_0; auto. + rewrite <-max_bound_log_cap in *; omega. + Qed. + + Lemma carry_carry_done_done : forall i us, + (length us = length base)%nat -> + (i < length base)%nat -> + carry_done us -> carry_done (carry i us). + Proof. + unfold carry_done; intros i ? ? i_bound Hcarry_done x x_bound. + destruct (Hcarry_done x x_bound) as [lower_bound_x shiftr_0_x]. + destruct (Hcarry_done i i_bound) as [lower_bound_i shiftr_0_i]. + split. + + rewrite carry_nothing; auto. + 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. + - 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. + Qed. + + Lemma carry_sequence_chain_step : forall i us, + carry_sequence (make_chain (S i)) us = carry i (carry_sequence (make_chain i) us). + Proof. + reflexivity. + Qed. + Lemma carry_bounds_0_upper : forall us j, (length us = length base) -> (0 < j < length base)%nat -> nth_default 0 (carry_sequence (make_chain j) us) 0 <= max_bound 0. Proof. - unfold carry_sequence; induction j; [simpl; intros; omega | ]. - intros. - simpl in *. - destruct (eq_nat_dec 0 j). - + subst. - apply nth_default_carry_bound_upper; fold (carry_sequence (make_chain 0) us); carry_length_conditions. - + rewrite carry_unaffected_low; try omega. - fold (carry_sequence (make_chain j) us); carry_length_conditions. + induction j as [ | [ | j ] IHj ]; [simpl; intros; omega | | ]; intros. + + subst; simpl; auto. + + rewrite carry_sequence_chain_step, carry_unaffected_low; carry_length_conditions. Qed. Lemma carry_bounds_upper : forall i us j, (0 < i < j)%nat -> (length us = length base) -> @@ -763,33 +754,41 @@ Section CanonicalizationProofs. apply IHj; omega. Qed. + (* makes omega run faster *) + Ltac clear_obvious := + match goal with + | [H : ?a <= ?a |- _] => clear H + | [H : ?a <= S ?a |- _] => clear H + | [H : ?a < S ?a |- _] => clear H + | [H : ?a = ?a |- _] => clear H + end. + Lemma carry_sequence_bounds_lower : forall j i us, (length us = length base) -> (forall i, 0 <= nth_default 0 us i) -> (j <= length base)%nat -> 0 <= nth_default 0 (carry_sequence (make_chain j) us) i. Proof. - induction j; intros. - + simpl. auto. - + simpl. - destruct (lt_dec (S j) i). - - rewrite carry_unaffected_high by carry_length_conditions. - apply IHj; auto; omega. - - assert ((i = S j) \/ (i = j) \/ (i < j))%nat as cases by omega. - destruct cases as [? | [? | ?]]. - * subst. apply nth_default_carry_bound_succ_lower; carry_length_conditions. - intros. - eapply IHj; auto; omega. - * subst. apply nth_default_carry_bound_lower; carry_length_conditions. - * destruct (eq_nat_dec j (pred (length base))); - [ | rewrite carry_unaffected_low by carry_length_conditions; apply IHj; auto; omega ]. - subst. - unfold carry, carry_and_reduce; break_if; try omega. - add_set_nth; [ | apply IHj; auto; omega ]. - apply Z.add_nonneg_nonneg; [ | apply IHj; auto; omega ]. - apply Z.mul_nonneg_nonneg; try omega. - apply Z.shiftr_nonneg. - apply IHj; auto; omega. + induction j; intros; simpl; auto. + destruct (lt_dec (S j) i). + + rewrite carry_unaffected_high by carry_length_conditions. + apply IHj; auto; omega. + + assert ((i = S j) \/ (i = j) \/ (i < j))%nat as cases by omega. + destruct cases as [? | [? | ?]]. + - subst. apply nth_default_carry_bound_succ_lower; carry_length_conditions. + intros; eapply IHj; auto; omega. + - subst. apply nth_default_carry_bound_lower; carry_length_conditions. + - destruct (eq_nat_dec j (pred (length base))); + [ | rewrite carry_unaffected_low by carry_length_conditions; apply IHj; auto; omega ]. + subst. + do 2 match goal with H : appcontext[S (pred (length base))] |- _ => + erewrite <-(S_pred (length base)) in H by eauto end. + unfold carry; break_if; [ unfold carry_and_reduce | omega ]. + clear_obvious. + add_set_nth; [ zero_bounds | ]; apply IHj; auto; omega. Qed. + Ltac carry_seq_lower_bound := + repeat (intros; eapply carry_sequence_bounds_lower; eauto; carry_length_conditions). + Lemma carry_bounds_lower : forall i us j, (0 < i <= j)%nat -> (length us = length base) -> (forall i, 0 <= nth_default 0 us i) -> (j <= length base)%nat -> 0 <= nth_default 0 (carry_sequence (make_chain j) us) i. @@ -801,13 +800,12 @@ Section CanonicalizationProofs. destruct (eq_nat_dec i (S j)). + subst. apply nth_default_carry_bound_succ_lower; auto; fold (carry_sequence (make_chain j) us); carry_length_conditions. - intros. - apply carry_sequence_bounds_lower; auto; omega. + carry_seq_lower_bound. + assert (i = j \/ i < j)%nat as cases by omega. destruct cases as [eq_j_i | lt_i_j]; subst; [apply nth_default_carry_bound_lower| rewrite carry_unaffected_low]; try omega; fold (carry_sequence (make_chain j) us); carry_length_conditions. - apply carry_sequence_bounds_lower; auto; omega. + carry_seq_lower_bound. Qed. Lemma carry_full_bounds : forall us i, (i <> 0)%nat -> (forall i, 0 <= nth_default 0 us i) -> @@ -831,15 +829,13 @@ Section CanonicalizationProofs. unfold carry, carry_simple; break_if; try omega. add_set_nth. replace (2 ^ B) with (2 ^ (B - log_cap i) + (2 ^ B - 2 ^ (B - log_cap i))) by omega. - split. - + apply Z.add_nonneg_nonneg; try omega. - apply Z.shiftr_nonneg; try omega. - + apply Z.add_lt_mono; try omega. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. - apply Z.div_lt_upper_bound; try apply pow_2_log_cap_pos. - rewrite <-Z.pow_add_r by (apply log_cap_nonneg || apply B_compat_log_cap). - replace (log_cap i + (B - log_cap i)) with B by ring. - omega. + split; [ zero_bounds | ]. + apply Z.add_lt_mono; try omega. + rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + apply Z.div_lt_upper_bound; try apply pow_2_log_cap_pos. + rewrite <-Z.pow_add_r by (apply log_cap_nonneg || apply B_compat_log_cap). + replace (log_cap i + (B - log_cap i)) with B by ring. + omega. Qed. Lemma carry_sequence_no_overflow : forall i us, pre_carry_bounds us -> @@ -853,16 +849,13 @@ Section CanonicalizationProofs. intuition. + simpl. destruct (lt_eq_lt_dec i (pred (length base))) as [[? | ? ] | ? ]. - - apply carry_simple_no_overflow; carry_length_conditions. - apply carry_sequence_bounds_lower; carry_length_conditions. - apply carry_sequence_bounds_lower; carry_length_conditions. - rewrite carry_sequence_unaffected; try omega. + - apply carry_simple_no_overflow; carry_length_conditions; carry_seq_lower_bound. + rewrite carry_sequence_unaffected; try omega. specialize (PCB (S i)); rewrite Nat.pred_succ in PCB. break_if; intuition. - unfold carry; break_if; try omega. rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ]. - subst. - unfold carry_and_reduce. + subst; unfold carry_and_reduce. carry_length_conditions. - rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ]. carry_length_conditions. @@ -877,22 +870,17 @@ Section CanonicalizationProofs. replace (length base) with (S (pred (length base))) at 1 2 by omega. simpl. unfold carry, carry_and_reduce; break_if; try omega. - add_set_nth. - split. - + apply Z.add_nonneg_nonneg. - - apply Z.mul_nonneg_nonneg; try omega. - apply Z.shiftr_nonneg. - apply carry_sequence_bounds_lower; auto; omega. - - apply carry_sequence_bounds_lower; auto; omega. - + rewrite Z.add_comm. - apply Z.add_le_mono. - - apply carry_bounds_0_upper; auto; omega. - - apply Z.mul_le_mono_pos_l; auto. - apply Z_shiftr_ones; auto; - [ | pose proof (B_compat_log_cap (pred (length base))); omega ]. - split. - * apply carry_bounds_lower; auto; try omega. - * apply carry_sequence_no_overflow; auto. + clear_obvious; add_set_nth. + split; [zero_bounds; carry_seq_lower_bound | ]. + rewrite Z.add_comm. + apply Z.add_le_mono. + + apply carry_bounds_0_upper; auto; omega. + + apply Z.mul_le_mono_pos_l; auto. + apply Z_shiftr_ones; auto; + [ | pose proof (B_compat_log_cap (pred (length base))); omega ]. + split. + - apply carry_bounds_lower; auto; omega. + - apply carry_sequence_no_overflow; auto. Qed. Lemma carry_full_bounds_lower : forall i us, pre_carry_bounds us -> @@ -919,12 +907,9 @@ Section CanonicalizationProofs. unfold carry, carry_simple; break_if; try omega. add_set_nth. split. - + apply Z.add_nonneg_nonneg. - - apply Z.shiftr_nonneg. - destruct (eq_nat_dec i 0); subst. - * simpl. - apply carry_full_bounds_0; auto. - * apply IHi; auto; omega. + + zero_bounds; [destruct (eq_nat_dec i 0); subst | ]. + - simpl; apply carry_full_bounds_0; auto. + - apply IHi; auto; omega. - rewrite carry_sequence_unaffected by carry_length_conditions. apply carry_full_bounds; auto; omega. + rewrite <-max_bound_log_cap, <-Z.add_1_l. @@ -953,15 +938,10 @@ Section CanonicalizationProofs. replace (length base) with (S (pred (length base))) by (pose proof base_length_nonzero; omega). simpl. unfold carry, carry_and_reduce; break_if; try omega. - add_set_nth. + clear_obvious; add_set_nth. split. - + apply Z.add_nonneg_nonneg. - apply Z.mul_nonneg_nonneg; try omega. - apply Z.shiftr_nonneg. + + zero_bounds; [ | carry_seq_lower_bound]. apply carry_sequence_carry_full_bounds_same; auto; omega. - eapply carry_sequence_bounds_lower; eauto; carry_length_conditions. - intros. - eapply carry_sequence_bounds_lower; eauto; carry_length_conditions. + rewrite Z.add_comm. apply Z.add_le_mono. - apply carry_bounds_0_upper; carry_length_conditions. @@ -986,17 +966,11 @@ Section CanonicalizationProofs. unfold carry_simple; intros ? ? PCB length_eq ? IH. add_set_nth. split. - + apply Z.add_nonneg_nonneg. - apply Z.shiftr_nonneg. - destruct i; + + zero_bounds. destruct i; [ simpl; pose proof (carry_full_2_bounds_0 us PCB length_eq); omega | ]. - - assert (0 < S i < length base)%nat as IHpre by omega. - specialize (IH IHpre). - omega. - rewrite carry_sequence_unaffected by carry_length_conditions. apply carry_full_bounds; carry_length_conditions. - intros. - apply carry_sequence_bounds_lower; eauto; carry_length_conditions. + carry_seq_lower_bound. + rewrite <-max_bound_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. apply Z.add_le_mono. @@ -1004,7 +978,7 @@ Section CanonicalizationProofs. ring_simplify. apply IH. omega. - rewrite carry_sequence_unaffected by carry_length_conditions. apply carry_full_bounds; carry_length_conditions. - intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions. + carry_seq_lower_bound. Qed. Lemma carry_full_2_bounds_same : forall us i, pre_carry_bounds us -> @@ -1017,11 +991,10 @@ Section CanonicalizationProofs. split; (destruct (eq_nat_dec i 0); subst; [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth | eapply carry_full_2_bounds_succ; eauto; omega]). - + apply Z.add_nonneg_nonneg. - apply Z.shiftr_nonneg. - eapply carry_full_2_bounds_0; eauto. - eapply carry_full_bounds; eauto; carry_length_conditions. - intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions. + + zero_bounds. + - eapply carry_full_2_bounds_0; eauto. + - eapply carry_full_bounds; eauto; carry_length_conditions. + carry_seq_lower_bound. + rewrite <-max_bound_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. apply Z.add_le_mono. @@ -1030,8 +1003,7 @@ Section CanonicalizationProofs. replace (Z.succ 1) with (2 ^ 1) by ring. rewrite <-max_bound_log_cap. ring_simplify. omega. - - apply carry_full_bounds; carry_length_conditions. - intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions. + - apply carry_full_bounds; carry_length_conditions; carry_seq_lower_bound. Qed. Lemma carry_full_2_bounds' : forall us i j, pre_carry_bounds us -> @@ -1085,6 +1057,13 @@ Section CanonicalizationProofs. - apply carry_full_bounds; carry_length_conditions. Qed. + Lemma carry_full_length : forall us, (length us = length base)%nat -> + length (carry_full us) = length us. + Proof. + intros; carry_length_conditions. + Qed. + Local Hint Resolve carry_full_length. + Lemma carry_carry_full_2_bounds_0_upper : forall us i, pre_carry_bounds us -> (length us = length base)%nat -> (0 < i < length base)%nat -> (nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0 <= max_bound 0 - c) @@ -1095,30 +1074,26 @@ Section CanonicalizationProofs. destruct i. + destruct (Z_le_dec (nth_default 0 (carry_full (carry_full us)) 0) (max_bound 0)). - right. - unfold carry_done. + apply carry_carry_done_done; try solve [carry_length_conditions]. + apply carry_done_bounds; try solve [carry_length_conditions]. intros. - apply max_bound_shiftr_eq_0; simpl; rewrite carry_nothing; try solve [carry_length_conditions]. - * apply carry_full_2_bounds_lower; auto. - * split; try apply carry_full_2_bounds_lower; auto. - * destruct i; auto. - apply carry_full_bounds; try solve [carry_length_conditions]. - auto using carry_full_bounds_lower. - * split; auto. - apply carry_full_2_bounds_lower; auto. - - unfold carry. + simpl. + 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. + rewrite carry_full_length; auto. + - left; unfold carry, carry_simple. break_if; [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ]. - simpl. - unfold carry_simple. - add_set_nth. left. + add_set_nth. 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. rewrite pow2_mod_spec by auto. + cbv [make_chain carry_sequence fold_right]. rewrite Z.mod_add by (pose proof (pow_2_log_cap_pos 0); omega). - rewrite <-max_bound_log_cap, <-Z.add_1_l, Z.mod_small. - apply Z.sub_le_mono_r. - subst; apply carry_full_2_bounds_0; auto. + rewrite <-max_bound_log_cap, <-Z.add_1_l, Z.mod_small; + [ apply Z.sub_le_mono_r; subst; apply carry_full_2_bounds_0; auto | ]. split; try omega. pose proof carry_full_2_bounds_0. apply Z.le_lt_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); @@ -1126,17 +1101,9 @@ Section CanonicalizationProofs. ring_simplify | ]; omega. + rewrite carry_unaffected_low by carry_length_conditions. assert (0 < S i < length base)%nat by omega. - intuition. - right. + intuition; right. apply carry_carry_done_done; try solve [carry_length_conditions]. - intro j. - destruct j. - - apply carry_carry_full_2_bounds_0_lower; auto. - - destruct (lt_eq_lt_dec j i) as [[? | ?] | ?]. - * apply carry_full_2_bounds; auto; omega. - * subst. apply carry_full_2_bounds_same; auto; omega. - * rewrite carry_sequence_unaffected; try solve [carry_length_conditions]. - apply carry_full_2_bounds_lower; auto; omega. + assumption. Qed. (* END proofs about second carry loop *) @@ -1149,7 +1116,7 @@ Section CanonicalizationProofs. Proof. intros. destruct i; [ | apply carry_full_bounds; carry_length_conditions; - do 2 (intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions) ]. + carry_seq_lower_bound ]. unfold carry_full at 1 4, full_carry_chain. case_eq limb_widths; [intros; pose proof limb_widths_nonnil; congruence | ]. simpl. @@ -1159,10 +1126,8 @@ Section CanonicalizationProofs. unfold carry, carry_and_reduce; break_if; try omega; intros. add_set_nth. split. - + apply Z.add_nonneg_nonneg. - - apply Z.mul_nonneg_nonneg; auto; try omega. - apply Z.shiftr_nonneg. - eapply carry_full_2_bounds_same; eauto; omega. + + zero_bounds. + - eapply carry_full_2_bounds_same; eauto; omega. - eapply carry_carry_full_2_bounds_0_lower; eauto; omega. + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))). assert (0 < pred (length base) < length base)%nat by omega. @@ -1175,9 +1140,15 @@ Section CanonicalizationProofs. apply Z.div_le_upper_bound; auto. ring_simplify. apply carry_full_2_bounds_same; auto. - - match goal with H : carry_done _ |- _ => unfold carry_done in H; rewrite H by omega end. + - match goal with H0 : (pred (length base) < length base)%nat, + H : carry_done _ |- _ => + destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end. ring_simplify. - apply shiftr_eq_0_max_bound; auto; omega. + apply shiftr_eq_0_max_bound; auto. + assert (0 < length base)%nat as zero_lt_length by omega. + match goal with H : carry_done _ |- _ => + destruct (H 0%nat zero_lt_length) end. + assumption. Qed. Lemma carry_full_3_done : forall us, pre_carry_bounds us -> @@ -1185,7 +1156,7 @@ Section CanonicalizationProofs. carry_done (carry_full (carry_full (carry_full us))). Proof. intros. - apply carry_done_bounds; intro i. + apply carry_done_bounds; [ carry_length_conditions | intros ]. destruct (lt_dec i (length base)). + rewrite <-max_bound_log_cap, Z.lt_succ_r. auto using carry_full_3_bounds. @@ -1194,12 +1165,6 @@ Section CanonicalizationProofs. (* END proofs about third carry loop *) - Lemma carry_full_length : forall us, (length us = length base)%nat -> - length (carry_full us) = length us. - Proof. - intros; carry_length_conditions. - Qed. - (* TODO : move? *) Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. Proof. @@ -1252,48 +1217,6 @@ Section CanonicalizationProofs. + eapply IHj; eauto. Qed. - (* TODO : move *) - Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. - Proof. - destruct p; cbv; congruence. - Qed. - - (* TODO : move *) - Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. - Proof. - induction a; destruct b; intros; try solve [cbv; congruence]; - simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; - try (apply N_le_1_l || apply N.le_0_l); intro land_eq; - rewrite land_eq in *; unfold N.le, N.compare in *; - rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; - try assumption. - destruct (p ?=a)%positive; cbv; congruence. - Qed. - - Lemma Zneg_nonneg_false : forall p, 0 <= Z.neg p -> False. - Admitted. - Hint Resolve Zneg_nonneg_false. - - (* TODO : move *) - Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= a. - Proof. - intros. - destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. - cbv [Z.land]. - rewrite <-N2Z.inj_pos, <-N2Z.inj_le. - auto using Pos_land_upper_bound_l. - Qed. - - (* TODO : move *) - Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= b. - Proof. - intros. - rewrite Z.land_comm. - auto using Z_land_upper_bound_l. - Qed. - Lemma max_ones_nonneg : 0 <= max_ones. Proof. unfold max_ones. @@ -1306,27 +1229,9 @@ Section CanonicalizationProofs. right. apply IHl; auto using in_cons. Qed. - Hint Resolve max_ones_nonneg. + (* + Local Hint Resolve max_ones_nonneg. *) - (* TODO : move *) - Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> - In x l -> x <= fold_right Z.max low l. - Proof. - induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. - simpl. - destruct (in_inv In_list); subst. - + apply Z.le_max_l. - + etransitivity. - - apply IHl; auto; intuition. - - apply Z.le_max_r. - Qed. - - (* TODO : move *) - Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. - Proof. - induction l; intros; try reflexivity. - etransitivity; [ apply IHl | apply Z.le_max_r ]. - Qed. Lemma land_max_ones_noop : forall x i, 0 <= x < 2 ^ log_cap i -> Z.land max_ones x = x. Proof. @@ -1348,14 +1253,6 @@ Section CanonicalizationProofs. apply Z_le_fold_right_max_initial. Qed. - Lemma land_max_ones_max_bound : forall i, Z.land max_ones (max_bound i) = max_bound i. - Proof. - intros. - apply land_max_ones_noop with (i := i). - rewrite <-max_bound_log_cap. - split; auto; omega. - Qed. - Lemma full_isFull'_true : forall j us, (length us = length base) -> ( max_bound 0 - c < nth_default 0 us 0 /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_bound i)) -> @@ -1406,11 +1303,57 @@ Section CanonicalizationProofs. if lt_dec i (min (length ls1) (length ls2)) then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) else d. - Admitted. + Proof. + induction ls1, ls2. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + simpl. + destruct i. + - intros. rewrite !nth_default_cons. + break_if; auto; omega. + - intros. rewrite !nth_default_cons_S. + rewrite IHls1 with (d1 := d1) (d2 := d2). + repeat break_if; auto; omega. + Qed. + + Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b, + map2 f (a :: ls1) (b :: ls2) = f a b :: map2 f ls1 ls2. + Proof. + reflexivity. + Qed. + + Lemma map2_nil_l : forall A B C (f : A -> B -> C) ls2, + map2 f nil ls2 = nil. + Proof. + reflexivity. + Qed. + + Lemma map2_nil_r : forall A B C (f : A -> B -> C) ls1, + map2 f ls1 nil = nil. + Proof. + destruct ls1; reflexivity. + Qed. + Hint Resolve map2_nil_r map2_nil_l. + + Opaque map2. Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, length (map2 f ls1 ls2) = min (length ls1) (length ls2). - Admitted. + Proof. + induction ls1, ls2; intros; try solve [cbv; auto]. + rewrite map2_cons, !length_cons, IHls1. + auto. + Qed. Lemma modulus_digits'_length : forall i, length (modulus_digits' i) = S i. Proof. @@ -1441,18 +1384,6 @@ Section CanonicalizationProofs. unfold freeze; intros; simpl_lengths. Qed. - Lemma map2_combine : forall {A B C} (f : A -> B -> C) ls1 ls2, - map2 f ls1 ls2 = map (fun xy => f (fst xy) (snd xy)) (combine ls1 ls2). - Admitted. - - Lemma map2_map_l : forall {A' A B C} (f : A -> B -> C) (g : A' -> A) ls1 ls2, - map2 f (map g ls1) ls2 = map2 (fun x y => f (g x) y) ls1 ls2. - Admitted. - - Lemma map2_map_r :forall {B' A B C} (f : A -> B -> C) (g : B' -> B) ls1 ls2, - map2 f ls1 (map g ls2) = map2 (fun x y => f x (g y)) ls1 ls2. - Admitted. - Lemma decode_firstn_succ : forall n us, (length us = length base) -> (n < length base)%nat -> BaseSystem.decode' (firstn (S n) base) (firstn (S n) us) = @@ -1476,7 +1407,11 @@ Section CanonicalizationProofs. (* TODO : move *) Lemma sum_firstn_all_succ : forall n l, (length l <= n)%nat -> sum_firstn l (S n) = sum_firstn l n. - Admitted. + Proof. + unfold sum_firstn; intros. + rewrite !firstn_all_strong by omega. + congruence. + Qed. Lemma decode_carry_done_upper_bound' : forall n us, carry_done us -> (length us = length base) -> @@ -1498,7 +1433,7 @@ Section CanonicalizationProofs. apply Z.mul_le_mono_nonneg_l; [ apply Z.pow_nonneg; omega | ]. replace 1 with (Z.succ 0) by reflexivity. rewrite Z.le_succ_l, Z.lt_0_sub. - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H; specialize (H n) end. + match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. replace x with (log_cap n); try intuition. rewrite log_cap_eq. apply nth_error_value_eq_nth_default; auto. @@ -1528,7 +1463,7 @@ Section CanonicalizationProofs. zero_bounds. - rewrite nth_default_base by assumption. apply Z.pow_nonneg; omega. - - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H; specialize (H n) end. + - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. intuition. + eapply Z.le_trans; [ apply IHn; eauto | ]. repeat rewrite firstn_all_strong by omega. @@ -1545,22 +1480,45 @@ Section CanonicalizationProofs. Qed. + Lemma nth_default_modulus_digits' : forall d j i, + nth_default d (modulus_digits' j) i = + if lt_dec i (S j) + then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i) + else d. + Proof. + induction j; intros; (break_if; [| apply nth_default_out_of_bounds; rewrite modulus_digits'_length; omega]). + + replace i with 0%nat by omega. + apply nth_default_cons. + + simpl. rewrite nth_default_app. + rewrite modulus_digits'_length. + break_if. + - rewrite IHj; break_if; try omega; reflexivity. + - replace i with (S j) by omega. + rewrite Nat.sub_diag, nth_default_cons. + reflexivity. + Qed. + Lemma nth_default_modulus_digits : forall d i, nth_default d modulus_digits i = if lt_dec i (length base) then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i) else d. - Admitted. + Proof. + unfold modulus_digits; intros. + rewrite nth_default_modulus_digits'. + replace (S (length base - 1)) with (length base) by omega. + reflexivity. + Qed. Lemma carry_done_modulus_digits : carry_done modulus_digits. Proof. - apply carry_done_bounds. + apply carry_done_bounds; [apply modulus_digits_length | ]. intros. rewrite nth_default_modulus_digits. break_if; [ | split; auto; omega]. break_if; subst; split; auto; try rewrite <- max_bound_log_cap; omega. Qed. - Hint Resolve carry_done_modulus_digits. + Local Hint Resolve carry_done_modulus_digits. (* TODO : move *) Lemma decode_mod : forall us vs x, (length us = length base) -> (length vs = length base) -> @@ -1574,11 +1532,40 @@ Section CanonicalizationProofs. assumption. Qed. + Ltac simpl_list_lengths := repeat match goal with + | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H + | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H + | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) + | |- appcontext[length (_ :: _)] => rewrite length_cons + end. + + Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2', + (length ls1 = length ls2) -> + map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. + Proof. + induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; + simpl_list_lengths; try omega. + rewrite <-!app_comm_cons, !map2_cons. + rewrite IHls1; auto. + Qed. + Lemma decode_map2_sub : forall us vs, - (length us = length base) -> (length vs = length base) -> - BaseSystem.decode base (map2 (fun x y => x - y) us vs) - = BaseSystem.decode base us - BaseSystem.decode base vs. - Admitted. + (length us = length vs) -> + BaseSystem.decode' base (map2 (fun x y => x - y) us vs) + = BaseSystem.decode' base us - BaseSystem.decode' base vs. + Proof. + induction us using rev_ind; induction vs using rev_ind; + intros; autorewrite with lengths in *; simpl_list_lengths; + rewrite ?decode_nil; try omega. + rewrite map2_app by omega. + rewrite map2_cons, map2_nil_l. + rewrite !set_higher. + autorewrite with lengths. + rewrite Min.min_l by omega. + rewrite IHus by omega. + replace (length vs) with (length us) by omega. + ring. + Qed. Lemma decode_modulus_digits' : forall i, (i <= length base)%nat -> BaseSystem.decode' base (modulus_digits' i) = 2 ^ (sum_firstn limb_widths (S i)) - c. @@ -1603,9 +1590,7 @@ Section CanonicalizationProofs. (rewrite log_cap_eq; apply nth_error_Some_nth_default; rewrite <-base_length; omega). rewrite Z.pow_add_r, <-max_bound_log_cap, set_higher by auto. - rewrite IHi by omega. - rewrite modulus_digits'_length. - rewrite nth_default_base by omega. + rewrite IHi, modulus_digits'_length, nth_default_base by omega. ring. - rewrite sum_firstn_all_succ by (rewrite <-base_length; omega). rewrite decode'_splice, modulus_digits'_length, firstn_all by auto. @@ -1614,7 +1599,7 @@ Section CanonicalizationProofs. omega. Qed. - Lemma decode_modulus_digits : BaseSystem.decode base modulus_digits = modulus. + Lemma decode_modulus_digits : BaseSystem.decode' base modulus_digits = modulus. Proof. unfold modulus_digits; rewrite decode_modulus_digits' by omega. replace (S (length base - 1)) with (length base) by omega. @@ -1649,7 +1634,9 @@ Section CanonicalizationProofs. Opaque modulus_digits. Lemma map_land_zero : forall ls, map (Z.land 0) ls = BaseSystem.zeros (length ls). - Admitted. + Proof. + induction ls; boring. + Qed. Lemma carry_full_preserves_Fdecode : forall us x, (length us = length base) -> decode us = x -> decode (carry_full us) = x. @@ -1659,14 +1646,6 @@ Section CanonicalizationProofs. unfold rep; auto. Qed. - Lemma Fdecode_decode_mod : forall us x, (length us = length base) -> - decode us = x -> BaseSystem.decode base us mod modulus = x. - Proof. - unfold decode; intros ? ? ? decode_us. - rewrite <-decode_us. - apply FieldToZ_ZToField. - Qed. - Lemma freeze_preserves_rep : forall us x, (length us = length base) -> rep us x -> rep (freeze us) x. Proof. @@ -1719,6 +1698,36 @@ Section CanonicalizationProofs. (in our context, this is the most significant end). *) Definition compare us vs := compare' us vs (length us). + Lemma compare'_Eq : forall us vs i, (length us = length vs) -> + compare' us vs i = Eq -> firstn i us = firstn i vs. + Proof. + induction i; intros; [ cbv; congruence | ]. + destruct (lt_dec i (length us)). + + repeat rewrite firstn_succ with (d := 0) by omega. + match goal with H : compare' _ _ (S _) = Eq |- _ => + inversion H end. + break_if; f_equal; auto. + - f_equal; auto. + - rewrite Z.compare_eq_iff in *. congruence. + - rewrite Z.compare_eq_iff in *. congruence. + + rewrite !firstn_all_strong in IHi by omega. + match goal with H : compare' _ _ (S _) = Eq |- _ => + inversion H end. + rewrite (nth_default_out_of_bounds i us) in * by omega. + rewrite (nth_default_out_of_bounds i vs) in * by omega. + break_if; try congruence. + f_equal; auto. + Qed. + + Lemma compare_Eq : forall us vs, (length us = length vs) -> + compare us vs = Eq -> us = vs. + Proof. + intros. + erewrite <-(firstn_all _ us); eauto. + erewrite <-(firstn_all _ vs); eauto. + apply compare'_Eq; auto. + Qed. + Lemma decode_lt_next_digit : forall us n, (length us = length base) -> (n < length base)%nat -> (n < length us)%nat -> carry_done us -> @@ -1740,7 +1749,7 @@ Section CanonicalizationProofs. * apply Z.gt_lt. apply nth_default_base_positive; omega. * rewrite Z.add_1_l. apply Z.le_succ_l. - rewrite carry_done_bounds in bounded. + rewrite carry_done_bounds in bounded by assumption. apply bounded. Qed. @@ -1870,7 +1879,6 @@ Section CanonicalizationProofs. reflexivity. Qed. - Lemma compare'_firstn_r_small_index : forall us j vs, (j <= length vs)%nat -> compare' us vs j = compare' us (firstn j vs) j. Proof. @@ -1957,8 +1965,7 @@ Section CanonicalizationProofs. rewrite nth_default_modulus_digits. repeat (break_if; try omega). rewrite <-Z.lt_succ_r with (m := max_bound i). - rewrite max_bound_log_cap; apply carry_done_bounds. - assumption. + rewrite max_bound_log_cap; apply carry_done_bounds; assumption. Qed. Lemma isFull_compare : forall us, (length us = length base) -> carry_done us -> @@ -2001,23 +2008,17 @@ Section CanonicalizationProofs. apply isFull_decode; auto. Qed. - Lemma land_ones_modulus_digits : map (Z.land max_ones) modulus_digits = modulus_digits. - Admitted. - - Lemma nth_default_map_land_zero : forall l i, nth_default 0 (map (Z.land 0) l) i = 0. - Admitted. - Lemma freeze_in_bounds : forall us, pre_carry_bounds us -> (length us = length base) -> carry_done (freeze us). Proof. unfold freeze; intros ? PCB lengths_eq. - rewrite carry_done_bounds; intro i. + rewrite carry_done_bounds by simpl_lengths; intro i. rewrite nth_default_map2 with (d1 := 0) (d2 := 0). simpl_lengths. break_if; [ | split; (omega || auto)]. break_if. - + rewrite land_ones_modulus_digits. + + rewrite map_land_max_ones_modulus_digits. apply isFull_true_iff in Heqb; [ | simpl_lengths]. destruct Heqb as [first_digit high_digits]. destruct (eq_nat_dec i 0). @@ -2026,7 +2027,7 @@ Section CanonicalizationProofs. rewrite nth_default_modulus_digits. repeat (break_if; try omega). pose proof (carry_full_3_done us PCB lengths_eq) as cf3_done. - rewrite carry_done_bounds in cf3_done. + rewrite carry_done_bounds in cf3_done by simpl_lengths. specialize (cf3_done 0%nat). omega. - assert ((0 < i <= length (carry_full (carry_full (carry_full us))) - 1)%nat) as i_range by @@ -2041,20 +2042,12 @@ Section CanonicalizationProofs. split; try omega. apply Z.lt_succ_r; auto. * rewrite Z.lt_succ_r, Z.sub_0_r. split; (omega || auto). - + rewrite nth_default_map_land_zero. + + rewrite map_land_zero, nth_default_zeros. rewrite Z.sub_0_r. - apply carry_done_bounds. + apply carry_done_bounds; [ simpl_lengths | ]. auto using carry_full_3_done. Qed. - Hint Resolve freeze_in_bounds. - - Lemma two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus. - Proof. - rewrite Z.sub_le_mono_r with (p := 2 ^ k). - rewrite Z.sub_diag. - replace (2 * modulus - 2 ^ k) with (2 ^ k - (2 * c)) by (unfold c; ring). - (* TODO : maybe just require this to be computed? seems doable but annoying to prove this way *) - Admitted. + Local Hint Resolve freeze_in_bounds. Local Hint Resolve carry_full_3_done. @@ -2065,12 +2058,12 @@ Section CanonicalizationProofs. intros. symmetry. apply Z.mod_small. split; break_if; rewrite decode_map2_sub; simpl_lengths. - + rewrite land_ones_modulus_digits, decode_modulus_digits. + + rewrite map_land_max_ones_modulus_digits, decode_modulus_digits. apply Z.le_0_sub. apply isFull_true_lower_bound; simpl_lengths. + rewrite map_land_zero, zeros_rep, Z.sub_0_r. apply decode_carry_done_lower_bound; simpl_lengths. - + rewrite land_ones_modulus_digits, decode_modulus_digits. + + rewrite map_land_max_ones_modulus_digits, decode_modulus_digits. rewrite Z.lt_sub_lt_add_r. apply Z.lt_le_trans with (m := 2 * modulus); try omega. eapply Z.lt_le_trans; [ | apply two_pow_k_le_2modulus ]. @@ -2078,21 +2071,39 @@ Section CanonicalizationProofs. + rewrite map_land_zero, zeros_rep, Z.sub_0_r. apply isFull_false_upper_bound; simpl_lengths. Qed. - Hint Resolve freeze_minimal_rep. + Local Hint Resolve freeze_minimal_rep. + + Lemma rep_decode_mod : forall us vs x, rep us x -> rep vs x -> + (BaseSystem.decode base us) mod modulus = (BaseSystem.decode base vs) mod modulus. + Proof. + unfold rep, decode; intros. + intuition. + repeat rewrite <-FieldToZ_ZToField. + congruence. + Qed. Lemma minimal_rep_unique : forall us vs x, - rep us x -> minimal_rep us -> carry_done us -> - rep vs x -> minimal_rep vs -> carry_done vs -> + length us = length base -> rep us x -> minimal_rep us -> carry_done us -> + length vs = length base -> rep vs x -> minimal_rep vs -> carry_done vs -> us = vs. Proof. - Admitted. + intros. + match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ => + pose proof (rep_decode_mod _ _ _ Hrep1 Hrep2) as eqmod end. + repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin; + rewrite <- Hmin in eqmod; clear Hmin end. + apply Z.compare_eq_iff in eqmod. + rewrite decode_compare in eqmod; auto. + apply compare_Eq; auto. + congruence. + Qed. Lemma freeze_canonical : forall us vs x, pre_carry_bounds us -> (length us = length base) -> rep us x -> pre_carry_bounds vs -> (length vs = length base) -> rep vs x -> freeze us = freeze vs. Proof. - intros; eapply minimal_rep_unique; eauto. + intros; eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. End CanonicalizationProofs. \ No newline at end of file diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index cbd7bd58c..9a9ce9a06 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -616,3 +616,12 @@ Proof. apply IHxs. omega. Qed. + +Lemma set_nth_nth_default : forall {A} (d:A) n x l i, (0 <= i < length l)%nat -> + nth_default d (set_nth n x l) i = + if (eq_nat_dec i n) then x else nth_default d l i. +Proof. + induction n; (destruct l; [intros; simpl in *; omega | ]); simpl; + destruct i; break_if; try omega; intros; try apply nth_default_cons; + rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity. +Qed. \ No newline at end of file diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1b7cfafdc..536566312 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -385,34 +385,91 @@ Qed. omega. Qed. -(* prove that known nonnegative numbers are nonnegative *) +(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) Ltac zero_bounds' := repeat match goal with | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg - | [ |- 0 <= _ - _] => apply Zle_minus_le_0 + | [ |- 0 <= _ - _] => apply Z.le_0_sub | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg | [ |- 0 <= _ / _] => apply Z.div_pos - | [ |- 0 < _ + _] => apply Z.add_pos_nonneg - (* TODO : this apply is not good: it can make a true goal false. Actually, - * we would want this tactic to explore two branches: - * - apply Z.add_pos_nonneg and continue - * - apply Z.add_nonneg_pos and continue - * Keep whichever one solves all subgoals. If neither does, don't apply. *) - - | [ |- 0 < _ - _] => apply Zlt_minus_lt_0 + | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg + | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg + | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; + try solve [apply Z.add_nonneg_pos; zero_bounds'] + | [ |- 0 < _ - _] => apply Z.lt_0_sub | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split | [ |- 0 < _ / _] => apply Z.div_str_pos + | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg end; try omega; try prime_bound; auto. Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. - Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. - Proof. - apply natlike_ind. - + unfold Z.ones. simpl; omega. - + intros. - rewrite Z_ones_succ by assumption. - zero_bounds. - apply Z.pow_nonneg; omega. - Qed. +Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. +Proof. + apply natlike_ind. + + unfold Z.ones. simpl; omega. + + intros. + rewrite Z_ones_succ by assumption. + zero_bounds. +Qed. + +Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. +Proof. + intros. + unfold Z.ones. + rewrite Z.shiftl_1_l. + apply Z.lt_succ_lt_pred. + apply Z.pow_gt_1; omega. +Qed. + +Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. +Proof. + destruct p; cbv; congruence. +Qed. + +Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. +Proof. + induction a; destruct b; intros; try solve [cbv; congruence]; + simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; + try (apply N_le_1_l || apply N.le_0_l); intro land_eq; + rewrite land_eq in *; unfold N.le, N.compare in *; + rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; + try assumption. + destruct (p ?=a)%positive; cbv; congruence. +Qed. +Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= a. +Proof. + intros. + destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. + cbv [Z.land]. + rewrite <-N2Z.inj_pos, <-N2Z.inj_le. + auto using Pos_land_upper_bound_l. +Qed. + +Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= b. +Proof. + intros. + rewrite Z.land_comm. + auto using Z_land_upper_bound_l. +Qed. + +Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> + In x l -> x <= fold_right Z.max low l. +Proof. + induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. + simpl. + destruct (in_inv In_list); subst. + + apply Z.le_max_l. + + etransitivity. + - apply IHl; auto; intuition. + - apply Z.le_max_r. +Qed. + +Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. +Proof. + induction l; intros; try reflexivity. + etransitivity; [ apply IHl | apply Z.le_max_r ]. +Qed. -- cgit v1.2.3