From 9e1ddef671220e78bbbf3d1a2c54b799cce84602 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 25 Jan 2016 15:25:16 -0500 Subject: ModualrBaseSystem: proved lingering admit in subtraction proof. --- src/Galois/BaseSystem.v | 12 ++++++++++++ src/Galois/ModularBaseSystem.v | 6 ++---- 2 files changed, 14 insertions(+), 4 deletions(-) (limited to 'src/Galois') 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. -- cgit v1.2.3