diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Galois/BaseSystem.v | 2 | ||||
| -rw-r--r-- | src/Galois/ModularBaseSystem.v | 105 | ||||
| -rw-r--r-- | src/Util/CaseUtil.v | 12 | ||||
| -rw-r--r-- | src/Util/ListUtil.v | 141 |
5 files changed, 248 insertions, 13 deletions
diff --git a/_CoqProject b/_CoqProject index 0e56c1ee2..d92e7e640 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ -R fiat/src Fiat -R bedrock/Bedrock Bedrock src/Tactics/VerdiTactics.v +src/Util/CaseUtil.v src/Util/ListUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index e8c288de6..19fc90dba 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,5 +1,5 @@ Require Import List. -Require Import Util.ListUtil. +Require Import Util.ListUtil Util.CaseUtil. Require Import ZArith.ZArith ZArith.Zdiv. Require Import Omega NPeano Arith. diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index db9a8db2a..bd3f7dca0 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -2,6 +2,7 @@ Require Import Zpower ZArith. Require Import List. Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. Require Import Util.ListUtil. +Require Import VerdiTactics. Open Scope Z_scope. Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). @@ -241,7 +242,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara rewrite (combine_truncate_r us EC.base). f_equal; f_equal. unfold EC.base. - rewrite (firstn_app _ _ (map (Z.mul (2 ^ P.k)) BC.base)); auto. + rewrite firstn_app_inleft; auto; omega. Qed. Lemma extended_base_length: @@ -376,4 +377,106 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara auto. Qed. + Definition carry i us := + let di := nth_default 0 us i in + let bi := nth_default 0 BC.base i in + let di' := di mod bi in + let cr := di / bi in + let us' := set_nth i di' us in + if eq_nat_dec i (pred (length BC.base)) + then set_nth 0 (P.c * cr + nth_default 0 us 0 ) us' (* carry and reduce *) + else set_nth (S i) ( cr + nth_default 0 us (S i)) us'. (* simple carry *) + + Lemma carry_length : forall i us, + (length us <= length BC.base)%nat -> + (length (carry i us) <= length BC.base)%nat. + Proof. + unfold carry; intros; break_if; subst; repeat (rewrite length_set_nth); auto. + Qed. + + Lemma skipn_all : forall {T} n (xs:list T), + (n >= length xs)%nat -> + skipn n xs = nil. + Proof. + induction n, xs; boring; omega. + Qed. + + Lemma fold_right_cons : forall {A B} (f:B->A->A) a b bs, + fold_right f a (b::bs) = f b (fold_right f a bs). + Proof. + reflexivity. + Qed. + + Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs). + reflexivity. + Qed. + + Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. + Proof. + destruct a; omega. + Qed. + + Lemma firstn_combine : forall {A B} n (xs:list A) (ys:list B), + firstn n (combine xs ys) = combine (firstn n xs) (firstn n ys). + Proof. + induction n, xs, ys; boring. + Qed. + + Lemma combine_nil_r : forall {A B} (xs:list A), + combine xs (@nil B) = nil. + Proof. + induction xs; boring. + Qed. + + Lemma skipn_combine : forall {A B} n (xs:list A) (ys:list B), + skipn n (combine xs ys) = combine (skipn n xs) (skipn n ys). + Proof. + induction n, xs, ys; boring. + rewrite combine_nil_r; reflexivity. + Qed. + + Lemma carry_rep_reduce : forall us u9 us' u0 x + (Heq: us = u0::us'++u9::nil) + (Hl : length us = length BC.base), + us ~= x -> + carry (pred (length BC.base)) us ~= x. + Proof. + autounfold; intuition; subst. rewrite carry_length; auto; omega. + unfold toGF, B.decode, B.decode', carry; break_if; intuition. + pose proof EC.base_length_nonzero. + repeat (rewrite combine_set_nth). + nth_inbounds. + nth_inbounds. + nth_inbounds; [|rewrite length_set_nth, combine_length, Min.min_l by auto; omega]. + unfold nth_default. + nth_inbounds. + nth_inbounds. + nth_inbounds; [|rewrite combine_length, Min.min_l by auto; omega]. + unfold splice_nth. + + rewrite firstn0, app_nil_l. + assert (skipn (S (pred (length BC.base))) (combine (u0::us'++u9::nil) BC.base) = nil) + as Hnil; [|rewrite Hnil; clear Hnil]. { + rewrite skipn_all; auto. + rewrite combine_length, Min.min_l by auto; omega. + } + rewrite fold_right_cons. + rewrite B.base_eq_1cons at 1. + rewrite length_cons. + rewrite <- (pred_Sn (length (skipn 1 BC.base))). + rewrite skipn_length. + rewrite <- pred_of_minus. + rewrite firstn_combine. + rewrite skipn_app_inleft. + rewrite skipn_combine. + rewrite fold_right_app. + Abort. + + + Lemma carry_rep : forall i us x + (Hl : length us = length BC.base), + us ~= x -> + carry i us ~= x. + Proof. + Admitted. End GFPseudoMersenneBase. diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v new file mode 100644 index 000000000..35f207ffc --- /dev/null +++ b/src/Util/CaseUtil.v @@ -0,0 +1,12 @@ +Require Import Arith. + +Ltac case_max := + match goal with [ |- context[max ?x ?y] ] => + destruct (le_dec x y); + match goal with + | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by + (exact H) + | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_l by + (exact (le_Sn_le _ _ (not_le _ _ H))) + end + end. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 86e989731..c8ee7bd9d 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -126,17 +126,115 @@ Proof. destruct (eq_nat_dec n m), (eq_nat_dec (S n) (S m)); nth_tac. Qed. -Lemma set_nth_equiv_splice: forall {T} n x (xs:list T), +Lemma length_set_nth : forall {T} i (x:T) xs, length (set_nth i x xs) = length xs. + induction i, xs; boring. +Qed. + +Lemma nth_error_length_exists_value : forall {A} (i : nat) (xs : list A), + (i < length xs)%nat -> exists x, nth_error xs i = Some x. +Proof. + induction i, xs; boring; try omega. +Qed. + +Lemma nth_error_length_not_error : forall {A} (i : nat) (xs : list A), + nth_error xs i = None -> (i < length xs)%nat -> False. +Proof. + intros. + destruct (nth_error_length_exists_value i xs); intuition; congruence. +Qed. + +Lemma nth_error_value_eq_nth_default : forall {T} i xs (x d:T), + nth_error xs i = Some x -> forall d, nth_default d xs i = x. +Proof. + unfold nth_default; boring. +Qed. + +Lemma skipn0 : forall {T} (xs:list T), skipn 0 xs = xs. +Proof. + auto. +Qed. + +Lemma firstn0 : forall {T} (xs:list T), firstn 0 xs = nil. +Proof. + auto. +Qed. + +Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs. +Hint Unfold splice_nth. + +Lemma splice_nth_equiv_set_nth : forall {T} n x (xs:list T), + splice_nth n x xs = + if lt_dec n (length xs) + then set_nth n x xs + else xs ++ x::nil. +Proof. + induction n, xs; boring. + break_if; break_if; auto; omega. +Qed. + +Lemma splice_nth_equiv_set_nth_set : forall {T} n x (xs:list T), + n < length xs -> + splice_nth n x xs = set_nth n x xs. +Proof. + intros. + rewrite splice_nth_equiv_set_nth. + break_if; auto; omega. +Qed. + +Lemma splice_nth_equiv_set_nth_snoc : forall {T} n x (xs:list T), + n >= length xs -> + splice_nth n x xs = xs ++ x::nil. +Proof. + intros. + rewrite splice_nth_equiv_set_nth. + break_if; auto; omega. +Qed. + +Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), set_nth n x xs = if lt_dec n (length xs) - then firstn n xs ++ x :: skipn (S n) xs + then splice_nth n x xs else xs. Proof. induction n; destruct xs; intros; simpl in *; try (rewrite IHn; clear IHn); auto. - destruct (lt_dec n (length xs)), (lt_dec (S n) (S (length xs))); try omega; trivial. + break_if; break_if; auto; omega. Qed. +Ltac nth_error_inbounds := + match goal with + | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => + case_eq (nth_error xs i); + match goal with + | [ |- forall _, nth_error xs i = Some _ -> _ ] => + let x := fresh "x" in + let H := fresh "H" in + intros x H; + repeat progress erewrite H; + repeat progress erewrite (nth_error_value_eq_nth_default i xs x); auto + | [ |- nth_error xs i = None -> _ ] => + let H := fresh "H" in + intros H; + destruct (nth_error_length_not_error _ _ H); + try omega + end; + idtac + end. + +Ltac set_nth_inbounds := + match goal with + | [ |- context[set_nth ?i ?x ?xs] ] => + rewrite (set_nth_equiv_splice_nth i x xs); + destruct (lt_dec i (length xs)); + match goal with + | [ H : ~ (i < (length xs))%nat |- _ ] => destruct H + | [ H : (i < (length xs))%nat |- _ ] => try omega + end; + idtac + end. + +Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds. + Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B), combine (set_nth n x xs) ys = match nth_error ys n with @@ -207,21 +305,42 @@ Proof. destruct n; auto. Qed. -Lemma firstn_app : forall {A} n (xs ys : list A), (n <= length xs)%nat -> - firstn n xs = firstn n (xs ++ ys). +Lemma firstn_app : forall {A} n (xs ys : list A), + firstn n (xs ++ ys) = firstn n xs ++ firstn (n - length xs) ys. +Proof. + induction n, xs, ys; boring. +Qed. + +Lemma skipn_app : forall {A} n (xs ys : list A), + skipn n (xs ++ ys) = skipn n xs ++ skipn (n - length xs) ys. +Proof. + induction n, xs, ys; boring. +Qed. + +Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat -> + firstn n (xs ++ ys) = firstn n xs. +Proof. + induction n, xs, ys; boring; try omega. +Qed. + +Lemma skipn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat -> + skipn n (xs ++ ys) = skipn n xs ++ ys. Proof. - induction n; destruct xs; destruct ys; simpl_list; boring; try omega. - rewrite (IHn xs (a0 :: ys)) by omega; auto. + induction n, xs, ys; boring; try omega. Qed. -Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'. +Lemma firstn_app_sharp : forall A (l l': list A), firstn (length l) (l ++ l') = l. Proof. - intros. - induction l; simpl; auto. + induction l; boring. +Qed. + +Lemma skipn_app_sharp : forall A (l l': list A), skipn (length l) (l ++ l') = l'. +Proof. + induction l; boring. Qed. Lemma skipn_length : forall {A} n (xs : list A), length (skipn n xs) = (length xs - n)%nat. Proof. -induction n; destruct xs; boring. + induction n, xs; boring. Qed. |