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 11:02:01 +01:00
parent 1fb8dd5022
commit 89ffb25a40
1 changed files with 57 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
thue-morse.v
View File

@ -994,14 +994,65 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
nth_error (tm_step (S n)) (k + 2^n) nth_error (tm_step (S n)) (k + 2^n)
= nth_error (tm_step (S n)) (S k + 2^n). = nth_error (tm_step (S n)) (S k + 2^n).
Proof. Proof.
intros n k. intros H.
(* Part 1: preamble *)
assert (I := H). apply Nat.lt_succ_l in I.
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
generalize I. apply tm_step_next_range2''.
assert (nth_error (tm_step n) (S k) <> nth_error (tm_step (S n)) (S k + 2^n)).
generalize H. apply tm_step_next_range2''.
assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
(* Part 2 *)
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
Some (nth (k + 2^n) (tm_step (S n)) false)).
generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
apply nth_error_nth'.
assert (nth_error (tm_step (S n)) (S k + 2 ^ n) =
Some (nth (S k + 2^n) (tm_step (S n)) false)).
generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
apply nth_error_nth'.
rewrite H2. rewrite H3. rewrite H4. rewrite H5.
(* Part 3 *)
destruct (nth k (tm_step n) false).
destruct (nth (S k) (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
easy.
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth (S k) (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
easy.
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
Qed.
Lemma tm_step_add_range2_neighbor : forall (n m k : nat), Lemma tm_step_add_range2_neighbor : forall (n m k : nat),