diff options
author | 2016-01-25 15:25:16 -0500 | |
---|---|---|
committer | 2016-01-25 15:25:16 -0500 | |
commit | 95542cc2dc9b4fb93770dced7ef11d2179f93f96 (patch) | |
tree | 7d53b6193555ee4c5d64e2fd11e679938fba2be7 | |
parent | 75fd95e8948915328fc11033906b634768dd099e (diff) |
ModualrBaseSystem: proved lingering admit in subtraction proof.
-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. |