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-12-15 15:38:08 +01:00
parent 5af9d44f02
commit 2786ad33bd
1 changed files with 46 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
thue-morse.v
View File

@ -35,7 +35,7 @@ Qed.
Lemma negb_double_map : forall (l : list bool),
map negb (map negb l) = l.
Proof.
intros l.
intro l.
induction l.
- reflexivity.
- simpl. rewrite IHl. replace (negb (negb a)) with (a).
@ -54,7 +54,7 @@ Qed.
Lemma tm_morphism_rev : forall (l : list bool),
rev (tm_morphism l) = tm_morphism (map negb (rev l)).
Proof.
intros l. induction l.
intro l. induction l.
- reflexivity.
- simpl. rewrite negb_map_explode.
rewrite IHl. rewrite tm_morphism_concat.
@ -62,10 +62,19 @@ Proof.
rewrite negb_involutive. reflexivity.
Qed.
Lemma tm_morphism_rev' : forall (l : list bool),
rev (tm_morphism l) = map negb (tm_morphism (rev l)).
Proof.
intro l. rewrite tm_morphism_rev. induction l.
- reflexivity.
- simpl. rewrite map_app. rewrite tm_morphism_concat. rewrite IHl.
rewrite tm_morphism_concat. rewrite map_app. reflexivity.
Qed.
Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
nth_error l k = nth_error (tm_morphism l) (2*k).
Proof.
intros l.
intro l.
induction l.
- intro k.
simpl. replace (nth_error [] k) with (None : option bool).
@ -82,7 +91,7 @@ Qed.
Lemma tm_build_negb : forall (l : list bool),
tm_morphism (map negb l) = map negb (tm_morphism l).
Proof.
intros l.
intro l.
induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
@ -92,13 +101,23 @@ Qed.
Lemma tm_step_lemma : forall n : nat,
tm_morphism (tm_step n) = tm_step (S n).
Proof.
intros n. reflexivity.
intro n. reflexivity.
Qed.
Theorem tm_step_negb : forall (n : nat),
map negb (tm_step (S n)) = rev (tm_morphism (rev (tm_step n))).
Proof.
intro n.
rewrite <- tm_step_lemma. symmetry.
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_involutive. rewrite tm_morphism_rev'. reflexivity.
rewrite rev_involutive. reflexivity.
Qed.
Theorem tm_build : forall (n : nat),
tm_step (S n) = tm_step n ++ map negb (tm_step n).
Proof.
intros n.
intro n.
induction n.
- reflexivity.
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
@ -109,7 +128,7 @@ Qed.
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
Proof.
intros n.
intro n.
induction n.
- reflexivity.
- rewrite tm_build. rewrite app_length. rewrite map_length.
@ -120,7 +139,7 @@ Qed.
Lemma tm_step_head_2 : forall (n : nat),
tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
Proof.
intros n.
intro n.
induction n.
- reflexivity.
- simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
@ -130,7 +149,7 @@ Qed.
Lemma tm_step_end_2 : forall (n : nat),
rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))).
Proof.
intros n. induction n.
intro n. induction n.
- reflexivity.
- simpl tm_step. rewrite tm_morphism_rev.
replace (tm_morphism (tm_step n)) with (tm_step (S n)).
@ -144,7 +163,8 @@ Qed.
Lemma tm_step_head_1 : forall (n : nat),
tm_step n = false :: tl (tm_step n).
Proof.
intros n. destruct n.
intro n.
destruct n.
- reflexivity.
- rewrite tm_step_head_2. reflexivity.
Qed.
@ -152,7 +172,7 @@ Qed.
Lemma tm_step_end_1 : forall (n : nat),
rev (tm_step n) = odd n :: tl (rev (tm_step n)).
Proof.
intros n.
intro n.
destruct n.
- reflexivity.
- rewrite tm_step_end_2. simpl.
@ -174,7 +194,7 @@ Qed.
Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
intros n.
intro n.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
replace (true) with (negb false). apply map_nth_error.
@ -182,39 +202,27 @@ Proof.
reflexivity. rewrite tm_size_power2. easy.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intros n.
intro 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.
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_nth. rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag.
rewrite tm_step_end_1. reflexivity.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
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.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
apply rev_involutive. 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.
intros l l1 l2 b. intros H. rewrite H.
intros l l1 l2 b. intro H. rewrite H.
rewrite app_length. simpl. apply Nat.lt_add_pos_r.
apply Nat.lt_0_succ.
Qed.
@ -223,7 +231,7 @@ Lemma tm_step_next_range :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
Proof.
intros n k b. intros H. assert (I := H).
intros n k b. intro H. assert (I := H).
apply nth_error_split in H. destruct H. destruct H. inversion H.
rewrite tm_build. rewrite nth_error_app1. apply I.
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
@ -232,7 +240,7 @@ Qed.
Lemma tm_step_add_range : forall (n m k : nat),
k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
Proof.
intros n m k. intros H.
intros n m k. intro H.
induction m.
- rewrite Nat.add_comm. reflexivity.
- rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
@ -269,7 +277,7 @@ Lemma tm_step_next_range2 :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Proof.
intros n k. intros H.
intros n k. intro H.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
@ -289,7 +297,7 @@ Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
nth_error (tm_step (S n)) (k + 2^n)
= nth_error (tm_step (S n)) (m + 2^n).
Proof.
intros n k m. intros H. intros I.
intros n k m. intro H. intro I.
(* Part 1: preamble *)
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).