Update

thue-morse.v

@@ -1,6 +1,7 @@
 (*
-https://oeis.org/A010060
-https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
+   Some proofs related to the Thue-Morse sequence.
+   See https://oeis.org/A010060
+       https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
 *)  
 
 Require Import Coq.Lists.List.
@@ -10,6 +11,12 @@ Require Import Bool.
 
 Import ListNotations.
 
+
+(*
+   This whole notebook contains proofs related to the following two functions.
+   Nothing else is defined afterwards.
+*)
+
 Fixpoint tm_morphism (l:list bool) : list bool :=
   match l with
   | nil => []
@@ -22,7 +29,12 @@ Fixpoint tm_step (n: nat) : list bool :=
   | S n' => tm_morphism (tm_step n')
   end.
 
-(* ad hoc more or less general lemmas *)
+
+(*
+   More or less "general" lemmas, which are not directly related to
+   the previous functions are proved below.
+*)
+
 Lemma lt_split_bits : forall n m k j,
   0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
 Proof.
@@ -84,6 +96,12 @@ Proof.
 Qed.
 
 
+(*
+   Some lemmas related to the first function (tm_morphism) are proved here.
+   They have a wider scope than the following ones since they don't focus on
+   the Thue-Morse sequence by itself.
+*)
+
 Lemma tm_morphism_concat : forall (l1 l2 : list bool),
   tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
 Proof.
@@ -262,7 +280,12 @@ Proof.
   rewrite app_inv_head_iff in L. assumption.
 Qed.
 
-(* Thue-Morse related lemmas and theorems *)
+
+(*
+   Lemmas and theorems below are related to the second function defined initially.
+   They focus on the Thue-Morse sequence.
+ *)
+
 Lemma tm_step_lemma : forall n : nat,
   tm_morphism (tm_step n) = tm_step (S n).
 Proof.
@@ -290,22 +313,12 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma tm_morphism_size : forall l : list bool,
-  length (tm_morphism l) = 2 * (length l).
-Proof.
-  intro l. induction l.
-  - reflexivity.
-  - simpl. rewrite Nat.add_0_r. rewrite IHl.
-    rewrite Nat.add_succ_r. replace (2) with (1+1). rewrite Nat.mul_add_distr_r.
-    rewrite Nat.mul_1_l. reflexivity. reflexivity.
-Qed.
-
 Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
 Proof.
   intro n.
   induction n.
   - reflexivity.
-  - rewrite <- tm_step_lemma. rewrite tm_morphism_size.
+  - rewrite <- tm_step_lemma. rewrite tm_morphism_length.
     rewrite Nat.pow_succ_r. rewrite Nat.mul_cancel_l.
     assumption. easy. apply Nat.le_0_l.
 Qed.
@@ -1269,7 +1282,7 @@ Proof.
 
    assert (length (b++b++b++tl2)
              = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
-   rewrite M. apply tm_morphism_size.
+   rewrite M. apply tm_morphism_length.
 
    assert (2 <= length (b++b++b++tl2)).
    rewrite app_length. rewrite <- Nat.add_0_r at 1.