diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-12 16:04:15 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-12 16:20:48 -0700 |
| commit | bfccc241c5bbbdd479d06c1db05834b1e719e8f6 (patch) | |
| tree | 27e0c2f5abab1c3a563afbc951d8e546888adf7c /src/Util/Tuple.v | |
| parent | 61bbfdbb458b2a4d6421218fdb1b04e1c98f3112 (diff) | |
Add length lemmas
After | File Name | Before || Change
------------------------------------------------------------------------------------
2m21.44s | Total | 2m18.90s || +0m02.54s
------------------------------------------------------------------------------------
0m35.19s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.60s || +0m00.58s
0m17.20s | ModularArithmetic/ModularBaseSystemProofs | 0m16.72s || +0m00.48s
0m15.34s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.21s || +0m00.12s
0m14.89s | Specific/GF25519 | 0m14.38s || +0m00.50s
0m14.03s | Experiments/SpecEd25519 | 0m13.67s || +0m00.35s
0m08.57s | ModularArithmetic/Pow2BaseProofs | 0m08.67s || -0m00.09s
0m04.32s | Testbit | 0m04.28s || +0m00.04s
0m03.73s | BaseSystemProofs | 0m03.75s || -0m00.02s
0m03.30s | Experiments/SpecificCurve25519 | 0m03.24s || +0m00.05s
0m02.92s | Util/ListUtil | 0m02.98s || -0m00.06s
0m02.15s | Specific/GF1305 | 0m02.11s || +0m00.04s
0m02.11s | ModularArithmetic/ModularBaseSystemOpt | 0m02.16s || -0m00.05s
0m01.77s | Experiments/EdDSARefinement | 0m01.76s || +0m00.01s
0m01.67s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.64s || +0m00.03s
0m01.54s | Encoding/PointEncodingPre | 0m01.50s || +0m00.04s
0m01.52s | Util/Tuple | 0m01.31s || +0m00.20s
0m01.20s | BaseSystem | 0m01.19s || +0m00.01s
0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || +0m00.02s
0m00.97s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || +0m00.06s
0m00.93s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.88s || +0m00.05s
0m00.84s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.87s || -0m00.03s
0m00.82s | ModularArithmetic/Montgomery/ZBounded | 0m00.83s || -0m00.01s
0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || +0m00.04s
0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.61s || +0m00.06s
0m00.64s | Util/AdditionChainExponentiation | 0m00.68s || -0m00.04s
0m00.64s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.07s
0m00.62s | Spec/EdDSA | 0m00.58s || +0m00.04s
0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || -0m00.01s
0m00.56s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.57s || -0m00.00s
0m00.43s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.01s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.01s
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 15a248afe..968eb99ad 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -62,11 +62,12 @@ Proof. induction xs; simpl in *; intros; congruence. Qed. +Lemma length_to_list' T n t : length (@to_list' T n t) = S n. +Proof. induction n; simpl in *; trivial; destruct t; simpl; congruence. Qed. + Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n. Proof. - destruct n; auto; intros; simpl in *. - induction n; auto; intros; simpl in *. - destruct xs; simpl in *; eauto. + destruct n; [ reflexivity | apply length_to_list' ]. Qed. Lemma from_list'_to_list' : forall T n (xs:tuple' T n), @@ -196,3 +197,6 @@ Definition apply {R T} (n:nat) : function R T n -> tuple T n -> R := | O => fun r _ => r | S n' => fun f x => apply' n' f x end. + +Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *) +Hint Rewrite length_to_list' @length_to_list : distr_length. |