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 14:18:39 +01:00
parent 9f6dc417be
commit 4b3495308e
1 changed files with 36 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
thue-morse.v
View File

@ -872,8 +872,6 @@ Proof.
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
Qed.
Lemma tm_step_next_range2 :
forall (n : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2
@ -905,6 +903,42 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Theorem tm_fullrange : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Proof.
intros n m k. rewrite <- tm_size_power2. intros.
induction n.
- destruct m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H.
replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
symmetry. apply tm_step_head_1.
- induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
symmetry. apply tm_step_head_1.
- induction m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H.
replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
symmetry. apply tm_step_head_1.
- induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
symmetry. apply tm_step_head_1.
replace (nth_error (tm_step m) k) with (nth_error (tm_step (S m)) k) in IHm.
apply IHm.
nth_error_nth':
forall [A : Type] (l : list A) [n : nat] (d : A),
n < length l -> nth_error l n = Some (nth n l d)
Lemma tm_step_consecutive_power2 :
forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),