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-23 21:44:45 +01:00
parent 99a4a193b6
commit e4870cb63e
1 changed files with 55 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
thue-morse.v
View File

@ -976,33 +976,75 @@ Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
= eqb
(nth (k + 2^(n+m)) (tm_step (S n+m)) false) (nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
Proof.
intros n m k. intros H. induction m.
intros n m k. intros H.
induction m.
- rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply tm_step_next_range2_neighbor.
apply H.
- rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
(*
assert (I: S k < 2^(S n + m)).
assert (2^n < 2^(S n + m)).
assert (n < S n + m). rewrite Nat.add_succ_comm.
assert (I : eqb (nth k (tm_step (S n + m)) false)
(nth (S k) (tm_step (S n + m)) false)
= eqb (nth (k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)
(nth (S k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)).
apply tm_step_next_range2_neighbor. induction m.
+ rewrite Nat.add_0_r. simpl. generalize H. apply Nat.lt_lt_add_r.
+ assert (2^n < 2^(S n + S m)).
assert (n < S n + S m). rewrite Nat.add_succ_comm.
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
apply Nat.pow_lt_mono_r. generalize H0. generalize H.
apply Nat.lt_trans.
generalize I.
+ rewrite <- I. rewrite <- IHm.
apply tm_step_next_range2_neighbor. induction m.
assert (U: S k < 2^(S n+m)).
assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
assert (L: 2^n < 2^(S n + m)).
assert (M: n < S n + m). rewrite Nat.add_succ_comm.
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
generalize L. generalize H. apply Nat.lt_trans.
assert (K := U). apply Nat.lt_succ_l in K.
assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)).
generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
(* assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false). *)
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
generalize K. generalize J. apply tm_step_stable.
rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
rewrite H4.
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 + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
generalize U. generalize H. apply tm_step_stable.
rewrite H3 in H6. rewrite H5 in H6.
inversion H6. rewrite H8.
reflexivity.
Qed.
Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
S k < 2^n ->
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
= eqb
(nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
*)
(nth (k + 2^(n+m)) (tm_step (S n+m)) false) (nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
Proof.
intros n m k. intros H. induction m.
- rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply tm_step_next_range2_neighbor.
apply H.
- rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
assert (I : eqb (nth k (tm_step (S n + m)) false)
(nth (S k) (tm_step (S n + m)) false)
@ -1042,7 +1084,6 @@ Proof.
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
assert (2^n < 2^(S n + m)).
assert (n < S n + m). rewrite Nat.add_succ_comm.
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
@ -1068,7 +1109,6 @@ Proof.
generalize H7. generalize H. apply tm_step_stable.
rewrite H3 in H6. rewrite H5 in H6.
inversion H6. rewrite H8.
reflexivity.
Qed.