From 58720d48d43d146751b9cfdb387d0c3b5b75ad72 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 10 Nov 2015 14:07:49 -0500 Subject: BaseSystem: implemented and proved subtraction. --- src/Galois/BaseSystem.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Galois/BaseSystem.v') diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 08c9653b1..4ec9853a1 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -89,6 +89,18 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Hint Rewrite decode'_cons. + Fixpoint sub (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => u-v :: sub us' vs' + | _, nil => us + | nil, v::vs' => (0-v)::sub nil vs' + end. + + Lemma sub_rep : forall bs us vs, decode' bs (sub us vs) = decode' bs us - decode' bs vs. + Proof. + induction bs; destruct us; destruct vs; boring. + Qed. + Lemma base_destruction: exists l, base = 1 :: l. Proof. assert (nth_default 0 base 0 = 1) by (apply b0_1). -- cgit v1.2.3