diff options
author | 2015-10-27 17:26:30 -0400 | |
---|---|---|
committer | 2015-10-27 17:26:30 -0400 | |
commit | 612d7242648366fd9eb6a9c4c5444a48cd192d1a (patch) | |
tree | a1be3e4f0dfcceb700b685cf20c52075a72c5ddd /src/Galois/BaseSystem.v | |
parent | d0a8f3e1168466ae2e3d4948aed4ec829a0c8b01 (diff) |
Proved add_same_length lemma.
Diffstat (limited to 'src/Galois/BaseSystem.v')
-rw-r--r-- | src/Galois/BaseSystem.v | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index e399a93d4..3e1fd0f74 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -265,9 +265,36 @@ Module BaseSystem (Import B:BaseCoefs). unfold mul_bi'; auto. Qed. + Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs). + Proof. + auto. + Qed. + Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) -> length (us .+ vs) = l. - Admitted. + Proof. + induction us; intros. { + rewrite add_nil_l. + apply H0. + } { + destruct vs. { + rewrite add_nil_r; apply H. + } { + rewrite add_first_terms. + rewrite cons_length. + rewrite (IHus vs (pred l)). + apply NPeano.Nat.succ_pred_pos. + replace l with (length (a :: us)) by (apply H). + rewrite cons_length; simpl. + SearchAbout S. + apply gt_Sn_O. + replace l with (length (a :: us)) by (apply H). + rewrite cons_length; simpl; auto. + replace l with (length (z :: vs)) by (apply H). + rewrite cons_length; simpl; auto. + } + } + Qed. Lemma add_app_same_length : forall us vs a b l, (length (us ++ a :: nil) = l) -> (length (vs ++ a :: nil) = l) -> |