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-28 19:26:44 +01:00
parent ee3b1e364d
commit b51cd1781a
1 changed files with 0 additions and 118 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

118
thue-morse.v
View File

@ -762,124 +762,6 @@ Qed.
replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_shuffle0.
rewrite <- Nat.add_assoc.
rewrite Nat.sub_succ.
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add. rewrite <- Nat.add_assoc.
rewrite
replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1));
destruct (nth_error (tm_step (S n0)) (2 * (S (2 * k) * 2 ^ m) - 1)).
destruct (b); destruct (b0); destruct (b1).
split. reflexivity. reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity. simpl. split; reflexivity.
contradiction H. reflexivity. contradiction H. reflexivity.
simpl. split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity. contradiction H. reflexivity.
destruct (b); destruct (b0). destruct J. rewrite H0.
split. intro J. inversion J. destruct H0. reflexivity.
intro J. simpl in J. symmetry in J. apply diff_false_true in J.
contradiction J. reflexivity.
split. intro K. inversion K.
apply Nat.lt_0_2. apply Nat.mul_comm.
Lemma tm_step_repeating_patterns :
forall (n m i j : nat),
i < 2^m -> j < 2^m
-> forall k, k < 2^n -> nth_error (tm_step m) i
= nth_error (tm_step m) j
<-> nth_error (tm_step (m+n)) (k * 2^m + i)
= nth_error (tm_step (m+n)) (k * 2^m + j).
induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
intro H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index. intro H. split. intro I.
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
intro H.
- induction m.
+ rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index.
split.
intro I. symmetry in I.
apply tm_step_succ_double_index in I. contradiction I.
rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
+
split.
- induction m.
+ rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index. intro I. symmetry in I.
apply tm_step_succ_double_index in I. contradiction I.
rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
Theorem tm_step_succ_double_index : forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).