From 44a9f78bb082dbc5275f7d4ae07501dc7cba8a07 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 14 Jun 2016 15:21:35 -0400 Subject: Finished admits for canonicalization proofs. --- src/BaseSystemProofs.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/BaseSystemProofs.v') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index ab56cb711..a2ebb7b41 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -130,6 +130,18 @@ Section BaseSystemProofs. Qed. Hint Rewrite zeros_app0. + Lemma nth_default_zeros : forall n i, nth_default 0 (BaseSystem.zeros n) i = 0. + Proof. + induction n; intros; [ cbv [BaseSystem.zeros]; apply nth_default_nil | ]. + rewrite <-zeros_app0, nth_default_app. + rewrite length_zeros. + destruct (lt_dec i n); auto. + destruct (eq_nat_dec i n); subst. + + rewrite Nat.sub_diag; apply nth_default_cons. + + apply nth_default_out_of_bounds. + cbv [length]; omega. + Qed. + Lemma rev_zeros : forall n, rev (zeros n) = zeros n. Proof. induction n; boring. -- cgit v1.2.3