baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-11-25 14:21:36 +01:00
parent 2649e789f0
commit 46829e78a1
1 changed files with 29 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
thue-morse.v
View File

@ -830,6 +830,35 @@ Proof.
reflexivity.
Qed.
Lemma tm_step_repunit : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intros n.
rewrite nth_error_nth' with (d := false).
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_nth. rewrite rev_length.
rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
rewrite Nat.sub_diag. rewrite tm_step_end_1.
simpl. reflexivity.
rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
simpl in IHn. rewrite Nat.mul_comm in IHn.
rewrite <- Nat.pow_succ_r in IHn. apply IHn.
apply Nat.le_0_l. apply Nat.lt_0_2.
rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
rewrite rev_involutive. reflexivity.
rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
Qed.
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
l = l1 ++ b :: l2 -> length l1 < length l.
Proof.
@ -1041,66 +1070,6 @@ Proof.
Qed.
Lemma tm_step_repunit : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intros n.
rewrite nth_error_nth' with (d := false).
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_nth. rewrite rev_length.
rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
rewrite Nat.sub_diag. rewrite tm_step_end_1.
simpl. reflexivity.
rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
simpl in IHn. rewrite Nat.mul_comm in IHn.
rewrite <- Nat.pow_succ_r in IHn. apply IHn.
apply Nat.le_0_l. apply Nat.lt_0_2.
rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
rewrite rev_involutive. reflexivity.
rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
Qed.
Nat.mul_lt_mono_neg_r: forall p n m : nat, p < 0 -> n < m <-> m * p < n * p
induction n. simpl. easy. simpl.
Nat.le_succ_l: forall n m : nat, S n <= m <-> n < m
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Nat.pow_nonzero: forall a b : nat, a <> 0 -> a ^ b <> 0
rev_nth:
forall [A : Type] (l : list A) (d : A) [n : nat],
n < length l -> nth n (rev l) d = nth (length l - S n) l d
nth_error_nth:
forall [A : Type] (l : list A) (n : nat) [x : A] (d : A),
nth_error l n = Some x -> nth n l d = x
nth_error_nth':
forall [A : Type] (l : list A) [n : nat] (d : A),
n < length l -> nth_error l n = Some (nth n l d)
Lemma tm_step_end_1 : forall (n : nat),
rev (tm_step n) = odd n :: tl (rev (tm_step n)).
last_length:
forall [A : Type] (l : list A) (a : A),
length (l ++ a :: nil) = S (length l)
Require Import BinPosDef.