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-26 12:33:15 +01:00
parent a93c2a6607
commit 272abb67cf
1 changed files with 71 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

78
thue-morse.v
View File

@ -942,6 +942,76 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l. rewrite tm_size_power2. apply Nat.le_add_l.
Qed. Qed.
Require Import Ltac2.Option.
Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
k < 2^n -> m < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) m
<->
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.
(* Part 1: preamble *)
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
generalize H. apply tm_step_next_range2.
assert (nth_error (tm_step n) m <> nth_error (tm_step (S n)) (m + 2^n)).
generalize I. apply tm_step_next_range2.
assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize H. apply Nat.add_lt_mono_r.
assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize I. apply Nat.add_lt_mono_r.
(* Part 2 *)
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step n) m = Some (nth m (tm_step n) false)).
generalize I. 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 K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
apply nth_error_nth'.
assert (nth_error (tm_step (S n)) (m + 2 ^ n) =
Some (nth (m + 2^n) (tm_step (S n)) false)).
generalize J. 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 m (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
destruct (nth (m + 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 (m + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth m (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
easy.
destruct (nth (m + 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 (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
Qed.
Lemma tm_step_next_range2_neighbor : forall (n k : nat), Lemma tm_step_next_range2_neighbor : forall (n k : nat),
S k < 2^n -> S k < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) (S k) nth_error (tm_step n) k = nth_error (tm_step n) (S k)
@ -1101,19 +1171,13 @@ Proof.
apply Nat.lt_succ_diag_r. apply Nat.lt_succ_diag_r.
generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1. generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
rewrite tm_step_repunit_index. destruct (odd n). easy. easy. rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
rewrite <- J. rewrite I.
(* (*
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I. assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
apply tm_step_repunit. apply tm_step_repunit.
*) *)
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.
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.