diff options
author | jadep <jade.philipoom@gmail.com> | 2016-07-19 15:35:35 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-07-19 15:35:35 -0400 |
commit | b4875d9ca86b5626512178c0bf48e324a6391b7b (patch) | |
tree | d0e2081c5ca29724c7f80a0bc9a0b035cf01d702 | |
parent | 6bc05eaded36d4c2e31e8d9979ee8660ad179080 (diff) | |
parent | 51602bd1ccf7493e53f78afa958238cad14571f2 (diff) |
merge
m--------- | etc/coq-scripts | 0 | ||||
-rw-r--r-- | src/BaseSystemProofs.v | 92 | ||||
-rw-r--r-- | src/Experiments/GenericFieldPow.v | 2 | ||||
-rw-r--r-- | src/Experiments/SpecEd25519.v | 4 | ||||
-rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 36 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 11 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 126 | ||||
-rw-r--r-- | src/ModularArithmetic/Pow2Base.v | 19 | ||||
-rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 188 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 64 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 76 |
11 files changed, 393 insertions, 225 deletions
diff --git a/etc/coq-scripts b/etc/coq-scripts -Subproject d858db1f3a64ea683e46204d0d8f775c5dbff97 +Subproject 3bdb920cb46ceeaaa93fce83e00ecaeb4276298 diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index eb7f31ba6..8de0fdd0a 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. @@ -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. @@ -532,26 +526,54 @@ 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'. + unfold BaseSystem.mul'; fold mul'. unfold mul_each. rewrite add_length_exact, map_length, mul_bi_length, length_cons. destruct us. + 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 BaseSystem.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. 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. @@ -559,7 +581,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 +628,32 @@ 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. + +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/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 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 + }. diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index d4df6040f..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,6 +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 7c7004dce..696f10438 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 *. @@ -374,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. @@ -403,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. @@ -475,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 58f44e8e9..7d4f0107c 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1,7 +1,7 @@ -Require Import Zpower ZArith. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import List. -Require Import VerdiTactics. +Require Import Coq.Lists.List. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. Require Import Crypto.BaseSystemProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. @@ -19,6 +19,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}. @@ -30,6 +31,7 @@ Section PseudoMersenneProofs. Local Notation "u ~= x" := (rep u x). Local Notation digits := (tuple Z (length limb_widths)). 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). @@ -85,27 +87,29 @@ Section PseudoMersenneProofs. f_equal; assumption. 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. + rewrite ext_base_alt; 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. @@ -137,7 +141,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. @@ -463,8 +467,8 @@ Section CanonicalizationProofs. Opaque Z.pow2_mod max_value. (* 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'. @@ -499,11 +503,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. @@ -515,11 +516,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. @@ -533,10 +531,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)-> @@ -548,12 +544,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) -> @@ -562,21 +554,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_value 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_value_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 -> @@ -590,15 +588,17 @@ Section CanonicalizationProofs. split; [ apply Hcarry_done; auto | ]. apply shiftr_eq_0_max_value. 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_value). assumption. - - rewrite shiftr_0_i by omega. - rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_value). - 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, @@ -712,8 +712,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. @@ -790,8 +792,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. @@ -849,8 +852,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 | ]. @@ -875,7 +879,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. @@ -923,8 +929,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. @@ -962,10 +967,11 @@ Section CanonicalizationProofs. split; [ auto using carry_full_2_bounds_lower | ]. destruct i; rewrite <-max_value_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_value 0 + c) - (1 + max_value 0)); try omega. replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring. @@ -1882,7 +1888,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..acc96ad73 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -48,31 +48,20 @@ 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)). - 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 a7d7da800..db910ba93 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. @@ -575,7 +587,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 = @@ -615,12 +627,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 +644,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 +676,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 +698,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 +726,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 +750,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, - (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. - - - Lemma nth_default_carry_gen - : 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. -*) + 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. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9225ee065..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 @@ -72,6 +73,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 +849,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 (@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 (@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 (@nth_error_None A 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} (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. + 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. @@ -1061,6 +1098,20 @@ 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_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. @@ -1074,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)) @@ -1168,4 +1230,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. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 6d4efd9f4..3eef976b2 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -207,3 +207,79 @@ 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). + destruct IHm as [? IHm]; [ omega | ]. + 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. + +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 le_dec_right_val n m (pf0 : ~n <= m) : { pf | le_dec n m = right pf }. +Proof. + 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. + +Lemma not_lt_n_pred_n n : ~n < pred n. +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. +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; [ | 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. 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; [ | destruct n; simpl in *; omega ]. + apply f_equal, le_unique. +Qed. +Hint Rewrite le_dec_pred_plus_same : natsimplify. |