diff options
author | Jade Philipoom <jadep@mit.edu> | 2016-01-25 15:25:16 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:38:54 -0400 |
commit | 9e1ddef671220e78bbbf3d1a2c54b799cce84602 (patch) | |
tree | d255ce7c82c37ce453ad0fd0727a83a0f1bb2d78 /src/Galois | |
parent | 00e16db76b2cc395857c43c28b885240d02c5df9 (diff) |
ModualrBaseSystem: proved lingering admit in subtraction proof.
Diffstat (limited to 'src/Galois')
-rw-r--r-- | src/Galois/BaseSystem.v | 12 | ||||
-rw-r--r-- | src/Galois/ModularBaseSystem.v | 6 |
2 files changed, 14 insertions, 4 deletions
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 28ae37233..f0e0db077 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -407,6 +407,18 @@ Module BaseSystem (Import B:BaseCoefs). (apply length_add_ge; omega) . Qed. + Lemma sub_nil_length: forall us : digits, length (sub nil us) = length us. + Proof. + induction us; boring. + Qed. + + Lemma sub_length_le_max : forall us vs, + (length (sub us vs) <= max (length us) (length vs))%nat. + Proof. + induction us, vs; boring. + rewrite sub_nil_length; auto. + Qed. + Lemma mul_bi_length : forall us n, length (mul_bi n us) = (length us + n)%nat. Proof. pose proof mul_bi'_length; unfold mul_bi. diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index 138eabd3f..b0b8e1495 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -258,10 +258,8 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara Lemma sub_rep : forall u v x y, u ~= x -> v ~= y -> sub u v ~= (x-y)%GF. Proof. autounfold; intuition. { - (*unfold add. - rewrite B.add_length_le_max. - B.case_max; try rewrite Max.max_r; omega.*) - admit. + rewrite B.sub_length_le_max. + case_max; try rewrite Max.max_r; omega. } unfold toGF in *; unfold B.decode in *. rewrite B.sub_rep. |