1692 lines
54 KiB
Coq
1692 lines
54 KiB
Coq
(*
|
|
https://oeis.org/A010060
|
|
https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
|
|
*)
|
|
|
|
Require Import Coq.Lists.List.
|
|
Require Import PeanoNat.
|
|
Require Import Nat.
|
|
Require Import Bool.
|
|
|
|
Import ListNotations.
|
|
|
|
Fixpoint tm_morphism (l:list bool) : list bool :=
|
|
match l with
|
|
| nil => []
|
|
| h :: t => h :: (negb h) :: (tm_morphism t)
|
|
end.
|
|
|
|
Fixpoint tm_step (n: nat) : list bool :=
|
|
match n with
|
|
| 0 => false :: nil
|
|
| S n' => tm_morphism (tm_step n')
|
|
end.
|
|
|
|
(* ad hoc more or less general lemmas *)
|
|
Lemma negb_map_explode : forall (l1 l2 : list bool),
|
|
map negb (l1 ++ l2) = map negb l1 ++ map negb l2.
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1.
|
|
- reflexivity.
|
|
- simpl. rewrite IHl1. reflexivity.
|
|
Qed.
|
|
|
|
Lemma negb_double_map : forall (l : list bool),
|
|
map negb (map negb l) = l.
|
|
Proof.
|
|
intro l.
|
|
induction l.
|
|
- reflexivity.
|
|
- simpl. rewrite IHl. replace (negb (negb a)) with (a).
|
|
reflexivity. rewrite negb_involutive. reflexivity.
|
|
Qed.
|
|
|
|
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.
|
|
intros n m k j. intros H I J.
|
|
|
|
assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
|
|
apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
|
|
|
|
assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
|
|
|
|
assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
|
|
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
|
|
apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
|
|
apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
|
|
replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
|
|
apply Nat.mul_le_mono_r with (p := 2^m) in H0.
|
|
rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
|
|
rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
|
|
|
|
rewrite Nat.add_le_mono_r with (p := j) in H0.
|
|
assert (2^n - 2^m + j < 2^n).
|
|
rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
|
|
rewrite Nat.add_lt_mono_r with (p := 2^m).
|
|
rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
|
|
rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
generalize H1. generalize H0. apply Nat.le_lt_trans.
|
|
apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
|
|
apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
|
|
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_concat : forall (l1 l2 : list bool),
|
|
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1.
|
|
- reflexivity.
|
|
- simpl. rewrite IHl1. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_rev : forall (l : list bool),
|
|
rev (tm_morphism l) = tm_morphism (map negb (rev l)).
|
|
Proof.
|
|
intro l. induction l.
|
|
- reflexivity.
|
|
- simpl. rewrite negb_map_explode.
|
|
rewrite IHl. rewrite tm_morphism_concat.
|
|
rewrite <- app_assoc. simpl.
|
|
rewrite negb_involutive. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_rev' : forall (l : list bool),
|
|
rev (tm_morphism l) = map negb (tm_morphism (rev l)).
|
|
Proof.
|
|
intro l. rewrite tm_morphism_rev. induction l.
|
|
- reflexivity.
|
|
- simpl. rewrite map_app. rewrite tm_morphism_concat. rewrite IHl.
|
|
rewrite tm_morphism_concat. rewrite map_app. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
|
|
nth_error l k = nth_error (tm_morphism l) (2*k).
|
|
Proof.
|
|
intro l.
|
|
induction l.
|
|
- intro k.
|
|
simpl. replace (nth_error [] k) with (None : option bool).
|
|
rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
|
|
reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
|
|
symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
|
|
- intro k. induction k.
|
|
+ rewrite Nat.mul_0_r. reflexivity.
|
|
+ simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
|
|
replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_build_negb : forall (l : list bool),
|
|
tm_morphism (map negb l) = map negb (tm_morphism l).
|
|
Proof.
|
|
intro l.
|
|
induction l.
|
|
- reflexivity.
|
|
- simpl. rewrite IHl. reflexivity.
|
|
Qed.
|
|
|
|
(* Thue-Morse related lemmas and theorems *)
|
|
Lemma tm_step_lemma : forall n : nat,
|
|
tm_morphism (tm_step n) = tm_step (S n).
|
|
Proof.
|
|
intro n. reflexivity.
|
|
Qed.
|
|
|
|
Theorem tm_step_negb : forall (n : nat),
|
|
map negb (tm_step (S n)) = rev (tm_morphism (rev (tm_step n))).
|
|
Proof.
|
|
intro n.
|
|
rewrite <- tm_step_lemma. symmetry.
|
|
replace (tm_step n) with (rev (rev (tm_step n))).
|
|
rewrite rev_involutive. rewrite tm_morphism_rev'. reflexivity.
|
|
rewrite rev_involutive. reflexivity.
|
|
Qed.
|
|
|
|
Theorem tm_build : forall (n : nat),
|
|
tm_step (S n) = tm_step n ++ map negb (tm_step n).
|
|
Proof.
|
|
intro n.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
|
|
simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
|
|
rewrite negb_map_explode. rewrite negb_double_map.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
|
|
Proof.
|
|
intro n.
|
|
induction n.
|
|
- reflexivity.
|
|
- rewrite tm_build. rewrite app_length. rewrite map_length.
|
|
replace (2^S n) with (2^n + 2^n). rewrite IHn. reflexivity.
|
|
simpl. rewrite <- plus_n_O. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_head_2 : forall (n : nat),
|
|
tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
|
|
Proof.
|
|
intro n.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
|
|
rewrite IHn. reflexivity. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_end_2 : forall (n : nat),
|
|
rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))).
|
|
Proof.
|
|
intro n. induction n.
|
|
- reflexivity.
|
|
- simpl tm_step. rewrite tm_morphism_rev.
|
|
replace (tm_morphism (tm_step n)) with (tm_step (S n)).
|
|
rewrite IHn. simpl tm_morphism. simpl tl.
|
|
rewrite Nat.even_succ.
|
|
rewrite Nat.odd_succ.
|
|
rewrite negb_involutive.
|
|
reflexivity. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_head_1 : forall (n : nat),
|
|
tm_step n = false :: tl (tm_step n).
|
|
Proof.
|
|
intro n.
|
|
destruct n.
|
|
- reflexivity.
|
|
- rewrite tm_step_head_2. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_end_1 : forall (n : nat),
|
|
rev (tm_step n) = odd n :: tl (rev (tm_step n)).
|
|
Proof.
|
|
intro n.
|
|
destruct n.
|
|
- reflexivity.
|
|
- rewrite tm_step_end_2. simpl.
|
|
rewrite Nat.odd_succ.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem tm_step_double_index : forall (n k : nat),
|
|
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
|
|
Proof.
|
|
intros n k.
|
|
destruct k.
|
|
- rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
|
|
rewrite tm_step_head_1. reflexivity.
|
|
- rewrite <- tm_step_lemma.
|
|
rewrite tm_morphism_double_index. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_single_bit_index : forall (n : nat),
|
|
nth_error (tm_step (S n)) (2^n) = Some true.
|
|
Proof.
|
|
intro n.
|
|
rewrite tm_build.
|
|
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
|
|
replace (true) with (negb false). apply map_nth_error.
|
|
rewrite tm_step_head_1. reflexivity.
|
|
reflexivity. rewrite tm_size_power2. easy.
|
|
Qed.
|
|
|
|
Lemma tm_step_repunit_index : forall (n : nat),
|
|
nth_error (tm_step n) (2^n - 1) = Some (odd n).
|
|
Proof.
|
|
intro n.
|
|
assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2.
|
|
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
|
|
|
|
rewrite nth_error_nth' with (d := false).
|
|
replace (tm_step n) with (rev (rev (tm_step n))).
|
|
rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2.
|
|
rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag.
|
|
rewrite tm_step_end_1. reflexivity.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
rewrite rev_length. assumption. apply rev_involutive. assumption.
|
|
Qed.
|
|
|
|
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
|
|
l = l1 ++ b :: l2 -> length l1 < length l.
|
|
Proof.
|
|
intros l l1 l2 b. intro H. rewrite H.
|
|
rewrite app_length. simpl. apply Nat.lt_add_pos_r.
|
|
apply Nat.lt_0_succ.
|
|
Qed.
|
|
|
|
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.
|
|
Proof.
|
|
intros n k b. intro H. assert (I := H).
|
|
apply nth_error_split in H. destruct H. destruct H. inversion H.
|
|
rewrite tm_build. rewrite nth_error_app1. apply I.
|
|
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
|
|
Qed.
|
|
|
|
Lemma tm_step_add_range : forall (n m k : nat),
|
|
k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
|
|
Proof.
|
|
intros n m k. intro H.
|
|
induction m.
|
|
- rewrite Nat.add_comm. reflexivity.
|
|
- rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
|
|
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
|
generalize H. apply nth_error_nth'.
|
|
rewrite H0 in IHm. symmetry in IHm.
|
|
rewrite H0. symmetry. generalize IHm.
|
|
apply tm_step_next_range.
|
|
Qed.
|
|
|
|
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.
|
|
Proof.
|
|
intros n m k. intros.
|
|
assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
|
|
apply Nat.max_spec. destruct I.
|
|
- destruct H1. replace (m) with (n + (m-n)). apply tm_step_add_range. apply H.
|
|
apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1.
|
|
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
|
|
assert (n <= n). apply le_n. symmetry.
|
|
replace (m) with (m + (n-n)) at 1. generalize H3.
|
|
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
|
|
reflexivity.
|
|
- destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
|
|
apply H0. replace (n) with (m + n - m) at 2. generalize H1.
|
|
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
|
|
assert (m <= m). apply le_n. symmetry.
|
|
replace (n) with (n + (m-m)) at 1. generalize H3.
|
|
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_step_next_range2 :
|
|
forall (n k : nat),
|
|
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
|
|
Proof.
|
|
intros n k. intro H.
|
|
rewrite tm_build.
|
|
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
|
|
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
|
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
|
|
rewrite H0.
|
|
assert (nth_error (map negb (tm_step n)) k
|
|
= Some (negb (nth k (tm_step n) false))).
|
|
generalize H0. apply map_nth_error. rewrite H1.
|
|
destruct (nth k (tm_step n) false). easy. easy.
|
|
rewrite tm_size_power2. apply Nat.le_add_l.
|
|
Qed.
|
|
|
|
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. intro H. intro 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: main proof *)
|
|
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: handling 16 different cases *)
|
|
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_add_range2_flip_two : forall (n m j k : 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+j)) (k + 2^(n+j))
|
|
= nth_error (tm_step (S n+j)) (m + 2^(n+j)).
|
|
Proof.
|
|
intros n m j k. intros H I.
|
|
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.
|
|
|
|
split.
|
|
- induction j.
|
|
+ intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
|
rewrite <- tm_step_next_range2_flip_two. apply L. apply H. apply I.
|
|
+ intros L.
|
|
|
|
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
|
|
|
|
assert (2^n < 2^(S n + j)).
|
|
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
|
|
generalize H0. apply Nat.lt_lt_add_r.
|
|
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
assert (k < 2^(S n + j)).
|
|
generalize H0. generalize H. apply Nat.lt_trans.
|
|
assert (m < 2^(S n + j)).
|
|
generalize H0. generalize I. apply Nat.lt_trans.
|
|
|
|
rewrite <- tm_step_next_range2_flip_two.
|
|
|
|
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
|
|
generalize H1. generalize H. apply tm_step_stable.
|
|
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
|
|
generalize H2. generalize I. apply tm_step_stable.
|
|
rewrite <- H3. rewrite <- H4. apply L.
|
|
|
|
apply H1. apply H2.
|
|
- induction j.
|
|
+ intro L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
|
|
apply tm_step_next_range2_flip_two. apply H. apply I. apply L.
|
|
+ intro L.
|
|
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
|
|
|
|
assert (2^n < 2^(S n + j)).
|
|
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
|
|
generalize H0. apply Nat.lt_lt_add_r.
|
|
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
assert (k < 2^(S n + j)).
|
|
generalize H0. generalize H. apply Nat.lt_trans.
|
|
assert (m < 2^(S n + j)).
|
|
generalize H0. generalize I. apply Nat.lt_trans.
|
|
|
|
rewrite <- tm_step_next_range2_flip_two in L.
|
|
|
|
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
|
|
generalize H1. generalize H. apply tm_step_stable.
|
|
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
|
|
generalize H2. generalize I. apply tm_step_stable.
|
|
rewrite <- H3 in L. rewrite <- H4 in L. apply L.
|
|
|
|
apply H1. apply H2.
|
|
Qed.
|
|
|
|
Lemma tm_step_repeating_patterns :
|
|
forall (n m i j : nat),
|
|
i < 2^m -> j < 2^m
|
|
-> forall k, k < 2^n -> nth_error (tm_step m) i
|
|
= nth_error (tm_step m) j
|
|
<-> nth_error (tm_step (m+n)) (k * 2^m + i)
|
|
= nth_error (tm_step (m+n)) (k * 2^m + j).
|
|
Proof.
|
|
intros n m i j. intros H I.
|
|
induction n.
|
|
- rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro.
|
|
rewrite H0. simpl. easy.
|
|
- rewrite Nat.add_succ_r. intro k. intro.
|
|
rewrite tm_build.
|
|
assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases.
|
|
destruct S.
|
|
|
|
assert (k*2^m < 2^(m+n)).
|
|
destruct k.
|
|
+ simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
+ rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
|
|
rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
|
|
assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
+ assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))).
|
|
intro l. intro M. rewrite tm_size_power2.
|
|
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
|
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
|
generalize H3. generalize M. apply Nat.lt_le_trans.
|
|
apply lt_split_bits. apply Nat.lt_0_succ. assumption.
|
|
assumption.
|
|
|
|
rewrite nth_error_app1. rewrite nth_error_app1.
|
|
generalize H1. apply IHn.
|
|
apply L. assumption. apply L. assumption.
|
|
|
|
+ assert (J: 2 ^ (m + n) <= k * 2 ^ m).
|
|
rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
|
|
apply Nat.mul_le_mono_r. assumption.
|
|
|
|
rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.
|
|
|
|
assert (forall a b, option_map negb a = option_map negb b <-> a = b).
|
|
intros a b. destruct a. destruct b. destruct b0; destruct b; simpl.
|
|
split; intro; reflexivity. split; intro; inversion H2.
|
|
split; intro; inversion H2. split; intro; reflexivity.
|
|
split; intro; inversion H2.
|
|
destruct b. split; intro; inversion H2. split; intro; reflexivity.
|
|
|
|
replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i).
|
|
replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).
|
|
rewrite nth_error_map. rewrite nth_error_map.
|
|
|
|
rewrite H2. apply IHn.
|
|
rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
|
|
rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0.
|
|
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
|
|
rewrite Nat.add_0_r in H0. assumption. reflexivity.
|
|
apply Nat.le_0_l. assumption.
|
|
|
|
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
|
|
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
|
|
rewrite Nat.add_comm. reflexivity. assumption.
|
|
|
|
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
|
|
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
|
|
rewrite Nat.add_comm. reflexivity. assumption.
|
|
|
|
rewrite tm_size_power2.
|
|
assert (k*2^m <= k*2^m + j). apply Nat.le_add_r.
|
|
generalize H2. generalize J. apply Nat.le_trans.
|
|
|
|
rewrite tm_size_power2.
|
|
assert (k*2^m <= k*2^m + i). apply Nat.le_add_r.
|
|
generalize H2. generalize J. apply Nat.le_trans.
|
|
Qed.
|
|
|
|
(* Note: a first version included the 0 < k hypothesis but in the very
|
|
unorthodox case where k=0 it happens to be true anyway, and the hypothesis
|
|
was removed in order to make the theorem more general *)
|
|
Theorem tm_step_flip_low_bit :
|
|
forall (n m k j : nat),
|
|
j < m -> k * 2^m < 2^n
|
|
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
|
|
Proof.
|
|
intros n m k j. intros H I.
|
|
|
|
assert (L: nth_error (tm_step m) 0 = Some false).
|
|
rewrite tm_step_head_1. reflexivity.
|
|
|
|
assert (M: 2^j < 2^m).
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
|
|
|
assert (N: nth_error (tm_step m) (2^j) = Some true).
|
|
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
|
rewrite tm_step_single_bit_index. reflexivity.
|
|
apply tm_step_stable.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
|
|
assumption.
|
|
|
|
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G as [G1|G2].
|
|
|
|
(* k = 0 *)
|
|
rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
|
|
rewrite tm_step_head_1 at 1.
|
|
assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
|
|
destruct S as [S1|S2]. rewrite Nat.lt_succ_r in S1.
|
|
apply Nat.pow_le_mono_r with (a := 2) in S1.
|
|
rewrite <- tm_size_power2 in S1. rewrite <- nth_error_None in S1.
|
|
rewrite S1. easy. easy.
|
|
rewrite Nat.le_succ_l in S2. apply Nat.pow_lt_mono_r with (a := 2) in S2.
|
|
rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
|
|
apply Nat.lt_1_2.
|
|
|
|
(* k < 0 *)
|
|
assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
|
|
assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
|
|
|
|
assert ( nth_error (tm_step m) 0
|
|
= nth_error (tm_step m) (2^j)
|
|
<-> nth_error (tm_step (m+n)) (k * 2^m + 0)
|
|
= nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ).
|
|
apply tm_step_repeating_patterns.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
|
|
|
assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg.
|
|
apply Nat.le_0_1. rewrite Nat.le_succ_l.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0.
|
|
rewrite Nat.mul_comm in H0.
|
|
generalize I. generalize H0. apply Nat.le_lt_trans.
|
|
rewrite Nat.add_0_r in H0.
|
|
|
|
replace (nth_error (tm_step (m + n)) (k * 2 ^ m))
|
|
with (nth_error (tm_step n) (k * 2 ^ m)) in H0.
|
|
replace (nth_error (tm_step (m + n)) (k * 2 ^ m + 2^j))
|
|
with (nth_error (tm_step n) (k * 2 ^ m + 2^j)) in H0.
|
|
rewrite L in H0. rewrite N in H0.
|
|
|
|
destruct (nth_error (tm_step n) (k * 2 ^ m)).
|
|
destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
|
|
destruct b; destruct b0; destruct H0.
|
|
assert (Some true = Some true). reflexivity.
|
|
apply H1 in H2. rewrite <- H2 at 1. easy. easy. easy.
|
|
assert (Some false = Some false). reflexivity.
|
|
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
|
rewrite nth_error_nth' with (d := false). easy.
|
|
rewrite tm_size_power2. assumption.
|
|
|
|
apply tm_step_stable. assumption.
|
|
generalize P. generalize O. apply Nat.lt_le_trans.
|
|
|
|
apply tm_step_stable. assumption.
|
|
generalize P. generalize I. apply Nat.lt_le_trans.
|
|
Qed.
|
|
|
|
Theorem tm_step_succ_double_index : forall (n k : nat),
|
|
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
|
|
Proof.
|
|
intros n k. intro H. rewrite tm_step_double_index.
|
|
rewrite Nat.mul_comm. replace (2) with (2^1).
|
|
replace (S (k*2^1)) with (k*2^1 + 2^0).
|
|
apply tm_step_flip_low_bit. apply Nat.lt_0_1.
|
|
simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k).
|
|
apply Nat.add_lt_mono; assumption.
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
simpl. rewrite Nat.add_1_r. reflexivity. reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_step_pred : forall (n k m : nat),
|
|
S (2*k) * 2^m < 2^n ->
|
|
nth_error (tm_step n) (S (2*k) * 2^m)
|
|
= nth_error (tm_step n) (S (2*k) * 2^m - 1)
|
|
<-> odd m = true.
|
|
Proof.
|
|
intros n k m.
|
|
|
|
generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
|
|
destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
|
|
intro H. apply Nat.neq_succ_0 in H. contradiction H.
|
|
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
|
|
rewrite <- tm_step_double_index. intro H. split. intro I.
|
|
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
|
|
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
|
|
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
|
|
intro I. apply diff_false_true in I. contradiction I.
|
|
|
|
intro n0. intro I.
|
|
destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
|
|
rewrite Nat.mul_eq_0 in I. destruct I.
|
|
apply Nat.neq_succ_0 in H. contradiction H.
|
|
apply Nat.pow_nonzero in H. contradiction H. easy.
|
|
rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc.
|
|
replace (S (2*k) * 2) with (2* (S (2*k))).
|
|
rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.
|
|
|
|
rewrite Nat.pow_succ_r' in I.
|
|
rewrite Nat.pow_succ_r' in I.
|
|
rewrite Nat.mul_assoc in I.
|
|
replace (S (2*k) * 2) with (2* (S (2*k))) in I.
|
|
rewrite <- Nat.mul_assoc in I.
|
|
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
|
assert (J := I). apply IHm in J.
|
|
|
|
assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
|
|
assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
|
|
replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
|
|
apply Nat.lt_succ_diag_r.
|
|
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn.
|
|
reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos.
|
|
apply Nat.lt_0_succ. assumption.
|
|
|
|
assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))).
|
|
rewrite tm_size_power2.
|
|
rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r.
|
|
rewrite Nat.sub_add. rewrite Nat.pow_succ_r'.
|
|
rewrite <- Nat.mul_le_mono_pos_l.
|
|
apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2.
|
|
apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
|
|
apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
|
|
assumption.
|
|
|
|
assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0).
|
|
generalize I. generalize L. apply Nat.lt_trans.
|
|
|
|
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
|
|
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
|
|
apply tm_step_succ_double_index. assumption.
|
|
|
|
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
|
|
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
|
|
|
|
split. intro K. rewrite <- K in H.
|
|
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
|
|
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
|
|
destruct J. replace (Some b) with (Some b0) in H. contradiction H.
|
|
reflexivity. symmetry. apply H1. reflexivity.
|
|
destruct J. replace (Some b) with (None : option bool) in H.
|
|
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
|
|
destruct J. replace (None : option bool) with (Some b) in H.
|
|
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
|
|
contradiction H. reflexivity.
|
|
|
|
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
|
|
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
|
|
intro K. simpl in K. apply diff_false_true in K. contradiction K.
|
|
intro K. simpl in K. apply diff_false_true in K. contradiction K.
|
|
intro K. simpl in K. apply diff_false_true in K. contradiction K.
|
|
intro K. simpl in K. apply diff_false_true in K. contradiction K.
|
|
|
|
rewrite nth_error_nth' with (d := false) in J.
|
|
rewrite nth_error_nth' with (d := false) in J.
|
|
rewrite nth_error_nth' with (d := false) in H.
|
|
rewrite nth_error_nth' with (d := false) in H.
|
|
rewrite nth_error_nth' with (d := false).
|
|
rewrite nth_error_nth' with (d := false).
|
|
destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false);
|
|
destruct (nth (S (2 * k) * 2 ^ m - 1) (tm_step n0) false);
|
|
destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (tm_step (S n0)) false).
|
|
simpl; split; reflexivity.
|
|
destruct J. rewrite H0 in H. contradiction H. reflexivity.
|
|
reflexivity.
|
|
simpl; split; reflexivity. contradiction H. reflexivity.
|
|
contradiction H. reflexivity.
|
|
simpl; split; reflexivity.
|
|
destruct J. rewrite H0 in H. contradiction H. reflexivity.
|
|
reflexivity.
|
|
simpl; split; reflexivity.
|
|
|
|
assumption. rewrite tm_size_power2. assumption. assumption.
|
|
rewrite tm_size_power2. assumption.
|
|
rewrite tm_size_power2. assumption.
|
|
rewrite tm_size_power2. assumption.
|
|
|
|
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
|
|
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity.
|
|
rewrite <- Nat.mul_1_r at 1.
|
|
apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2.
|
|
apply Nat.le_succ_l. apply Nat.mul_pos_pos.
|
|
apply Nat.lt_0_succ. assumption. apply Nat.lt_0_2.
|
|
|
|
apply Nat.mul_comm. apply Nat.mul_comm.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_morphism_count_occ : forall (l : list bool),
|
|
count_occ Bool.bool_dec (tm_morphism l) true
|
|
= count_occ Bool.bool_dec (tm_morphism l) false.
|
|
Proof.
|
|
intro l. induction l.
|
|
- reflexivity.
|
|
- destruct a.
|
|
+ simpl. apply eq_S. assumption.
|
|
+ simpl. apply eq_S. assumption.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_app : forall (l1 l2 : list bool),
|
|
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
|
Proof.
|
|
intros l1 l2.
|
|
induction l1.
|
|
- reflexivity.
|
|
- simpl. rewrite IHl1. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_eq : forall (l1 l2 : list bool),
|
|
l1 = l2 <-> tm_morphism l1 = tm_morphism l2.
|
|
Proof.
|
|
intros l1 l2. split.
|
|
- intro H. rewrite H. reflexivity.
|
|
- generalize l2. induction l1.
|
|
+ intro l. intro H. simpl in H.
|
|
induction l. reflexivity. simpl in H. inversion H.
|
|
+ simpl. intro l0. intro H.
|
|
induction l0. simpl in H. inversion H.
|
|
simpl in H. inversion H. apply IHl1 in H3. rewrite H3.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_length : forall (l : list bool),
|
|
length (tm_morphism l) = 2 * (length l).
|
|
Proof.
|
|
induction l.
|
|
- reflexivity.
|
|
- simpl. rewrite Nat.add_0_r. rewrite IHl.
|
|
rewrite Nat.add_succ_r.
|
|
simpl. rewrite Nat.add_0_r. reflexivity.
|
|
Qed.
|
|
|
|
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
|
tm_morphism l = hd ++ tl
|
|
-> even (length hd) = true
|
|
-> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
|
|
Proof.
|
|
intros l hd tl. intros H I.
|
|
assert (J : l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
|
|
symmetry. apply firstn_skipn.
|
|
rewrite tm_morphism_eq in J.
|
|
rewrite tm_morphism_app in J. rewrite H in J.
|
|
apply app_eq_app in J.
|
|
|
|
assert (H2: length (tm_morphism l) = length hd + length tl).
|
|
rewrite H. apply app_length.
|
|
|
|
assert (H3: length hd <= length (tm_morphism l)).
|
|
rewrite H2. apply Nat.le_add_r.
|
|
rewrite tm_morphism_length in H3.
|
|
|
|
assert (H4: Nat.div2 (length hd) <= length l).
|
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
|
rewrite <- Nat.add_0_r at 1.
|
|
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
|
|
rewrite <- Nat.div2_odd. assumption.
|
|
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
|
|
|
|
destruct J. destruct H0; destruct H0.
|
|
|
|
assert (L: length hd = length hd). reflexivity.
|
|
rewrite H0 in L at 2. rewrite app_length in L.
|
|
rewrite tm_morphism_length in L.
|
|
|
|
apply firstn_length_le in H4. rewrite H4 in L.
|
|
replace (2 * Nat.div2 (length hd))
|
|
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
|
rewrite <- Nat.div2_odd in L.
|
|
rewrite <- Nat.add_0_r in L at 1.
|
|
apply Nat.add_cancel_l in L. symmetry in L.
|
|
apply length_zero_iff_nil in L.
|
|
rewrite L in H0. rewrite <- app_nil_end in H0. assumption.
|
|
rewrite <- Nat.negb_even. rewrite I. simpl.
|
|
rewrite Nat.add_0_r. reflexivity.
|
|
|
|
assert (L: length (tm_morphism (firstn (Nat.div2 (length hd)) l))
|
|
= length (tm_morphism (firstn (Nat.div2 (length hd)) l))).
|
|
reflexivity. rewrite H0 in L at 2. rewrite app_length in L.
|
|
rewrite tm_morphism_length in L.
|
|
|
|
apply firstn_length_le in H4. rewrite H4 in L.
|
|
replace (2 * Nat.div2 (length hd))
|
|
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
|
|
rewrite <- Nat.div2_odd in L.
|
|
rewrite <- Nat.add_0_r in L at 1.
|
|
apply Nat.add_cancel_l in L. symmetry in L.
|
|
apply length_zero_iff_nil in L.
|
|
rewrite L in H0. rewrite <- app_nil_end in H0. symmetry. assumption.
|
|
rewrite <- Nat.negb_even. rewrite I. simpl.
|
|
rewrite Nat.add_0_r. reflexivity.
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
|
|
TODO Search "count_occ"
|
|
*)
|
|
Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
|
|
tm_step n = hd ++ tl -> even (length hd) = true
|
|
-> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
|
|
Proof.
|
|
intros hd tl n. intros H I.
|
|
destruct n.
|
|
- assert (J: hd = nil). destruct hd. reflexivity.
|
|
simpl in H. inversion H.
|
|
symmetry in H2. apply app_eq_nil in H2.
|
|
destruct H2. rewrite H0 in I. simpl in I. inversion I.
|
|
rewrite J. reflexivity.
|
|
- rewrite <- tm_step_lemma in H.
|
|
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
|
|
generalize I. generalize H. apply tm_morphism_app2.
|
|
rewrite J. apply tm_morphism_count_occ.
|
|
Qed.
|
|
|
|
|
|
Lemma count_occ_bool_list : forall (a: list bool),
|
|
length a = (count_occ bool_dec a true) + (count_occ bool_dec a false).
|
|
Proof.
|
|
intro a.
|
|
induction a.
|
|
- reflexivity.
|
|
- destruct a.
|
|
+ rewrite count_occ_cons_eq. rewrite count_occ_cons_neq.
|
|
simpl. rewrite IHa. reflexivity. easy. reflexivity.
|
|
+ rewrite count_occ_cons_neq. rewrite count_occ_cons_eq.
|
|
simpl. rewrite Nat.add_succ_r. rewrite IHa. reflexivity. reflexivity. easy.
|
|
Qed.
|
|
|
|
|
|
Lemma count_occ_bool_list2 : forall (a: list bool),
|
|
count_occ bool_dec a false = count_occ bool_dec a true -> even (length a) = true.
|
|
Proof.
|
|
intro a. intro H.
|
|
rewrite count_occ_bool_list. rewrite H.
|
|
replace (count_occ bool_dec a true) with (1 * (count_occ bool_dec a true)).
|
|
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
|
|
replace (2 * count_occ bool_dec a true) with (0 + 2 * count_occ bool_dec a true).
|
|
apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
|
|
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
|
|
Proof.
|
|
intros n a hd tl. intro H.
|
|
assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd.
|
|
assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd.
|
|
|
|
destruct H1.
|
|
- apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
|
|
- destruct H0.
|
|
assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
|
|
assert (Nat.even (length hd) = true).
|
|
apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
|
|
generalize H2. generalize H. apply tm_step_count_occ.
|
|
|
|
assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I.
|
|
assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false).
|
|
assert (even (length (hd++a++a)) = true).
|
|
rewrite app_length. rewrite Nat.even_add_even.
|
|
apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
|
|
|
|
rewrite app_length. replace (length a) with (1*(length a)).
|
|
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
|
|
rewrite <- Nat.add_0_l. apply Nat.EvenT_Even.
|
|
apply Nat.even_EvenT.
|
|
rewrite Nat.even_add_mul_2. reflexivity.
|
|
apply Nat.mul_1_l.
|
|
generalize H3. generalize I. apply tm_step_count_occ.
|
|
|
|
rewrite count_occ_app in H3. symmetry in H3.
|
|
rewrite count_occ_app in H3. rewrite H2 in H3.
|
|
rewrite Nat.add_cancel_l in H3.
|
|
|
|
rewrite count_occ_app in H3. rewrite count_occ_app in H3.
|
|
replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
|
|
replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
|
|
rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
|
|
rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
|
|
assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
|
|
rewrite app_assoc_reverse. reflexivity.
|
|
|
|
assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
|
|
assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
|
|
assert (even (length (hd++a)) = true).
|
|
rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
|
|
rewrite app_length. apply Nat.Odd_Odd_add; assumption.
|
|
generalize H2. generalize I. apply tm_step_count_occ.
|
|
|
|
assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J.
|
|
assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false).
|
|
assert (even (length (hd++a++a++a)) = true).
|
|
rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
|
|
rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length.
|
|
apply Nat.Even_Even_add.
|
|
rewrite app_length. apply Nat.Odd_Odd_add; assumption.
|
|
rewrite app_length. apply Nat.Odd_Odd_add; assumption.
|
|
generalize H3. generalize J. apply tm_step_count_occ.
|
|
|
|
replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3.
|
|
rewrite count_occ_app in H3. symmetry in H3.
|
|
rewrite count_occ_app in H3. rewrite H2 in H3.
|
|
rewrite Nat.add_cancel_l in H3.
|
|
|
|
rewrite count_occ_app in H3. rewrite count_occ_app in H3.
|
|
replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
|
|
replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
|
|
rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
|
|
rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
|
|
assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
|
|
rewrite app_assoc_reverse. reflexivity.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
|
|
rewrite app_assoc_reverse. reflexivity.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
|
|
tm_step n = hd ++ a ++ a ++ a ++ tl
|
|
-> 0 < length a
|
|
-> even (length hd) = even (length tl).
|
|
Proof.
|
|
intros n a hd tl. intros H J.
|
|
destruct n.
|
|
- assert (3 <= length (a ++ a ++ a)).
|
|
rewrite app_length. rewrite app_length.
|
|
rewrite <- Nat.le_succ_l in J.
|
|
assert (2 <= length a + length a).
|
|
generalize J. generalize J. apply Nat.add_le_mono.
|
|
generalize H0. generalize J. apply Nat.add_le_mono.
|
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
|
rewrite H in H1 at 2.
|
|
assert (0 <= length hd). apply Nat.le_0_l.
|
|
assert (0 + 3 <= length hd + length (a ++ a ++ a)).
|
|
generalize H0. generalize H2. apply Nat.add_le_mono.
|
|
simpl in H3. rewrite <- app_length in H3.
|
|
assert (0 <= length tl). apply Nat.le_0_l.
|
|
assert (3 + 0 <= length (hd ++ a ++ a ++ a) + length (tl)).
|
|
generalize H4. generalize H3. apply Nat.add_le_mono.
|
|
rewrite <- app_length in H5. rewrite Nat.add_0_r in H5.
|
|
replace ((hd++a++a++a)++tl) with (hd++a++a++a++tl) in H5.
|
|
rewrite <- H1 in H5. simpl in H5. apply le_S_n in H5.
|
|
apply Nat.nle_succ_0 in H5. contradiction H5.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
|
|
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
|
|
rewrite app_assoc_reverse. reflexivity.
|
|
- assert (Nat.Even (length (tm_step (S n)))).
|
|
rewrite tm_size_power2. rewrite Nat.pow_succ_r'.
|
|
apply Nat.Even_mul_l. apply Nat.EvenT_Even.
|
|
apply Nat.EvenT_2. apply Nat.EvenT_0.
|
|
rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
|
|
rewrite Nat.add_shuffle3 in H0.
|
|
assert (I := H). apply tm_step_cube1 in I.
|
|
apply Nat.even_EvenT in I. apply Nat.EvenT_Even in I.
|
|
assert (Nat.Even (length hd + length (a ++ a ++ tl))).
|
|
generalize I. generalize H0. apply Nat.Even_add_Even_inv_r.
|
|
rewrite app_length in H1. rewrite Nat.add_shuffle3 in H1.
|
|
assert (Nat.Even (length hd + length (a ++ tl))).
|
|
generalize I. generalize H1. apply Nat.Even_add_Even_inv_r.
|
|
rewrite app_length in H2. rewrite Nat.add_shuffle3 in H2.
|
|
assert (Nat.Even (length hd + length tl)).
|
|
generalize I. generalize H2. apply Nat.Even_add_Even_inv_r.
|
|
|
|
apply Nat.Even_EvenT in H3. apply Nat.EvenT_even in H3.
|
|
rewrite Nat.even_add in H3.
|
|
destruct (even (length hd)); destruct (even (length tl)).
|
|
reflexivity. simpl in H3. inversion H3.
|
|
simpl in H3. inversion H3. reflexivity.
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
|
|
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false
|
|
-> 0 < length a
|
|
-> hd_error a = hd_error tl.
|
|
Proof.
|
|
|
|
|
|
|
|
(hd + [a] + [a] + [a])
|
|
-> prouver que le premier caractère qui suit hd suit aussi le troisième a
|
|
quand hd est de taille impaire
|
|
[hd + false] + /a+false/
|
|
|
|
|
|
Prouver que si un cube existe de taille k, il existe aussi un cube
|
|
de même taille précédé par un préfixe de taille pair (par décalage éventuel de 1)
|
|
|
|
Prouver que si un cube existe, de taille paire, précédé par un préfixe pair,
|
|
alors (par référence au morphisme, il existait à la génération précédente
|
|
un cube de taille moitié précédé par un préfixe pair
|
|
|
|
--> absurdité : on ne peut diviser indéfiniment par 2 et rester sur du pair
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* TODO: supprimer head_2 *)
|
|
|
|
(* vérifier si les deux sont nécessaires *)
|
|
Require Import BinPosDef.
|
|
Require Import BinPos.
|
|
|
|
Require Import BinNat.
|
|
|
|
|
|
(* Hamming weight of a positive; argument can not be 0! *)
|
|
Fixpoint hamming_weight_positive (x: positive) :=
|
|
match x with
|
|
| xH => 1
|
|
| xO p => hamming_weight_positive p
|
|
| xI p => 1 + hamming_weight_positive p
|
|
end.
|
|
|
|
Definition hamming_weight_n (x: N) :=
|
|
match x with
|
|
| N0 => 0
|
|
| Npos x => hamming_weight_positive x
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma hamming_weight_positive_nonzero : forall (x: positive),
|
|
hamming_weight_positive x > 0.
|
|
Proof.
|
|
intros x.
|
|
induction x.
|
|
- simpl. apply Arith_prebase.gt_Sn_O_stt.
|
|
- simpl. apply IHx.
|
|
- simpl. apply Arith_prebase.gt_Sn_O_stt.
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma size_double_bin : forall (x: positive),
|
|
Pos.size_nat (Pos.succ (Pos.pred_double x)) = S (Pos.size_nat x).
|
|
Proof.
|
|
intros x.
|
|
rewrite Pos.succ_pred_double.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma succ_succ_pred_double_succ : forall (x: positive),
|
|
Pos.pred_double (Pos.succ x) = Pos.succ (Pos.succ (Pos.pred_double x)).
|
|
Proof.
|
|
intros x.
|
|
rewrite <- Pos.add_1_l.
|
|
rewrite Pos.add_xO_pred_double.
|
|
rewrite <- Pos.add_1_l.
|
|
rewrite <- Pos.add_1_l.
|
|
rewrite Pos.add_assoc.
|
|
reflexivity.
|
|
Qed.
|
|
Lemma size_double_bin2 : forall (x: positive),
|
|
Pos.size_nat (Pos.pred_double (Pos.succ x)) = S (Pos.size_nat x).
|
|
Proof.
|
|
intros x.
|
|
rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma size_succ_double_bin : forall (x: positive),
|
|
Pos.size_nat (Pos.succ (Pos.succ (Pos.pred_double x))) = S (Pos.size_nat x).
|
|
Proof.
|
|
intros x.
|
|
rewrite <- succ_succ_pred_double_succ. rewrite size_double_bin2.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma nat_size_pos_size : forall (x: positive),
|
|
N.size_nat (N.pos x) = Pos.size_nat x.
|
|
Proof.
|
|
intros x. reflexivity.
|
|
Qed.
|
|
|
|
Lemma hamming_weight_increase : forall (x: positive),
|
|
hamming_weight_positive x~1 = S (hamming_weight_positive x).
|
|
Proof.
|
|
intros x. reflexivity.
|
|
Qed.
|
|
|
|
|
|
Fixpoint bin2power (x : positive) (k : N) :=
|
|
match x with
|
|
| xH => (2^k)%N
|
|
| xO y => bin2power y (N.succ k)
|
|
| xI y => (2^k + bin2power y (N.succ k))%N
|
|
end.
|
|
|
|
Lemma bin2power_same : forall (x : positive),
|
|
Npos x = bin2power x 0.
|
|
Proof.
|
|
intros x.
|
|
induction x.
|
|
- simpl.
|
|
|
|
|
|
|
|
(*
|
|
Fixpoint bin2power (x : positive) (k : nat) :=
|
|
match x with
|
|
| xH => 2^k
|
|
| xO y => bin2power y (S k)
|
|
| xI y => 2^k + bin2power y (S k)
|
|
end.
|
|
*)
|
|
|
|
Lemma bin2power_double : forall (x : positive) (k : N),
|
|
bin2power x~0 k = bin2power x (N.succ k).
|
|
Proof.
|
|
intros x. simpl. reflexivity.
|
|
Qed.
|
|
|
|
Lemma bin2power_double2 : forall (x : positive),
|
|
bin2power x~0 0%N = (2 * bin2power x 0)%N.
|
|
Proof.
|
|
intros x.
|
|
destruct x.
|
|
- simpl.
|
|
|
|
|
|
N.testbit_even_succ:
|
|
forall a n : N, (0 <= n)%N -> N.testbit (2 * a) (N.succ n) = N.testbit a n
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
simpl. reflexivity.
|
|
Qed.
|
|
|
|
Lemma bin2power_succ : forall (x : positive) (k : N),
|
|
bin2power (x~1) k = ((2^k)%N + (bin2power (x~0) k))%N.
|
|
Proof.
|
|
intros x k.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma bin2power_double2 : forall (x : positive),
|
|
bin2power x 1%N = (2 * bin2power x 0)%N.
|
|
Proof.
|
|
intros x.
|
|
induction x.
|
|
- rewrite bin2power_succ. rewrite bin2power_succ. rewrite N.pow_0_r.
|
|
rewrite N.mul_add_distr_l. rewrite N.pow_1_r. rewrite N.mul_1_r.
|
|
rewrite N.add_cancel_l.
|
|
replace (bin2power x~0 0) with (bin2power x 1%N).
|
|
|
|
|
|
|
|
|
|
|
|
assert ((2 * bin2power (Pos.succ x~0) 0)%N = (2 + 2*binpower (x~0) 0)%N).
|
|
|
|
replace (x~0) with ((N.pos (N.shiftl (x) 1) 1)%N).
|
|
|
|
|
|
|
|
|
|
induction x.
|
|
- simpl. rewrite Nat.add_0_r. apply eq_S. rewrite <- plus_n_Sm.
|
|
apply eq_S.
|
|
destruct x.
|
|
+ simpl.
|
|
|
|
|
|
|
|
|
|
rewrite Pos.xI_succ_xO.
|
|
rewrite <- bin2power_double.
|
|
|
|
|
|
rewrite bin2power_double.
|
|
|
|
|
|
|
|
- rewrite bin2power_double.
|
|
assert ( I: bin2power x~1 0 = S (bin2power x~0 0) ).
|
|
{ simpl. reflexivity. } rewrite I.
|
|
assert ( J: bin2power x~1 1 = S (S (S (bin2power x~0 1) ))).
|
|
{ rewrite <- I.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
simpl. rewrite Nat.add_0_r.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Qed.
|
|
|
|
Lemma bin2power_same : forall (x: positive),
|
|
bin2power x 0 = Pos.to_nat x.
|
|
Proof.
|
|
intros x.
|
|
induction x.
|
|
- simpl. rewrite <- Pos.pred_double_succ.
|
|
rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
|
|
|
|
rewrite <- Pos.xI_succ_xO.
|
|
rewrite <- bin2power_double.
|
|
|
|
assert (I: bin2power x 1 = 2 * (bin2power x 0)).
|
|
{ induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
|
|
simpl in IHx.
|
|
|
|
|
|
assert (I: bin2power x 1 = 2 * (bin2power x 0)).
|
|
{ induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
|
|
simpl in IHx.
|
|
|
|
|
|
Lemma tm_step_hamming : forall (x: N),
|
|
nth_error (tm_step (N.size_nat x)) (N.to_nat x)
|
|
= Some (odd (hamming_weight_n x)).
|
|
Proof.
|
|
intros x.
|
|
destruct x.
|
|
- reflexivity.
|
|
- induction p.
|
|
+ rewrite <- Pos.pred_double_succ.
|
|
|
|
rewrite nat_size_pos_size.
|
|
rewrite succ_succ_pred_double_succ at 1.
|
|
rewrite size_succ_double_bin.
|
|
|
|
unfold hamming_weight_n. rewrite Pos.pred_double_succ.
|
|
rewrite hamming_weight_increase. rewrite Nat.odd_succ.
|
|
rewrite <- Nat.negb_odd.
|
|
|
|
rewrite tm_build. rewrite nth_error_app1.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
apply map_nth_error.
|
|
|
|
|
|
|
|
|
|
rewrite succ_succ_pred_double_succ.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
simpl. rewrite Pos.succ_pred_double.
|
|
rewrite size_double_bin.
|
|
|
|
|
|
unfold N.to_nat at 2. unfold Pos.to_nat. simpl.
|
|
|
|
rewrite Pos.xI_succ_xO. transforme p~1 en Pos.succ p~0
|
|
Lemma pred_double_succ p : pred_double (succ p) = p~1.
|
|
Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
|
|
Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
|
|
|
|
|
|
|
|
|
|
Theorem tm_step_hamming_index : forall (n : N),
|
|
nth_error (tm_step (N.to_nat n)) (N.to_nat n)
|
|
= Some (odd (hamming_weight_n n)).
|
|
Proof.
|
|
intros n.
|
|
destruct n.
|
|
- reflexivity.
|
|
- induction p. simpl.
|
|
|
|
|
|
|
|
|
|
Theorem tm_step_hamming_index : forall (n m : nat) (k j: N),
|
|
(N.to_nat k) < 2^n -> (N.to_nat j) < 2^m ->
|
|
hamming_weight_n k = hamming_weight_n j ->
|
|
nth_error (tm_step n) (N.to_nat k) = nth_error (tm_step m) (N.to_nat j).
|
|
Proof.
|
|
intros n m k j. intros H I K.
|
|
induction k.
|
|
- simpl in K. assert (j = N0). induction j. reflexivity.
|
|
rewrite <- N.succ_pos_pred.
|
|
unfold hamming_weight_n in K.
|
|
assert (L: hamming_weight_positive p > 0).
|
|
apply hamming_weight_positive_nonzero. rewrite <- K in L.
|
|
apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
|
|
rewrite H0. rewrite H0 in I.
|
|
generalize I. generalize H. apply tm_step_stable.
|
|
- induction j. simpl in K. assert (L: hamming_weight_positive p > 0).
|
|
apply hamming_weight_positive_nonzero. rewrite K in L.
|
|
apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
|
|
(* coeur de l'induction *)
|
|
|
|
|
|
induction p. simpl in K.
|
|
symmetry in K. apply Nat.neq_succ_0 in K. contradiction K.
|
|
|
|
|
|
|
|
Theorem N. succ_0_discr n : succ n <> 0.
|
|
Nat.neq_succ_0: forall n : nat, S n <> 0
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixpoint tm_step (n: nat) : list bool :=
|
|
match n with
|
|
| 0 => false :: nil
|
|
| S n' => tm_morphism (tm_step n')
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_index_split :
|
|
forall (a b n m : nat),
|
|
(* every natural number k can be written according to the following form *)
|
|
a < 2^n -> (a + 2^n * b) < 2^m
|
|
-> nth_error (tm_step m) (a + 2^n * b)
|
|
= nth_error (tm_step (S m)) (a + 2^S n * b).
|
|
Proof.
|
|
intros a b n m. intros H I.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_cancel_high_bits :
|
|
forall (k b n m : nat),
|
|
(* every natural number k can be written according to the following form *)
|
|
S k < 2^m -> k = 2^n - 1 + 2^S n * b
|
|
-> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
|
|
<-> odd n = true.
|
|
Proof.
|
|
intros k b n m. intros H I.
|
|
|
|
assert (L: 2^n - 1 < 2^n). apply Nat.sub_lt. replace (1) with (2^0) at 1.
|
|
apply Nat.pow_le_mono_r. easy.
|
|
apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
|
|
|
|
assert (M: S(2^n - 1) = 2^n). rewrite Nat.sub_1_r. apply Nat.succ_pred.
|
|
apply Nat.pow_nonzero. apply Nat.neq_succ_0.
|
|
|
|
assert (N: 2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
apply Nat.lt_succ_diag_r.
|
|
|
|
assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
|
|
<-> odd n = true).
|
|
rewrite tm_step_single_bit_index.
|
|
assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
|
|
apply tm_step_stable. apply L.
|
|
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
apply Nat.lt_succ_diag_r.
|
|
generalize H0. generalize L. apply Nat.lt_trans. rewrite <- H0.
|
|
rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
|
|
rewrite <- J. rewrite I.
|
|
|
|
|
|
destruct b.
|
|
|
|
(* case b = 0 *)
|
|
rewrite Nat.mul_0_r. rewrite Nat.add_0_r.
|
|
rewrite J. rewrite Nat.mul_0_r in I. rewrite Nat.add_0_r in I.
|
|
rewrite I in H. rewrite M.
|
|
|
|
assert (nth_error (tm_step m) (2^n-1) = nth_error (tm_step n) (2^n-1)).
|
|
generalize L. apply tm_step_stable. apply Nat.lt_succ_l. apply H.
|
|
rewrite H0. rewrite tm_step_repunit_index.
|
|
|
|
assert (nth_error (tm_step m) (2^n) = nth_error (tm_step (S n)) (2 ^ n)).
|
|
generalize N. rewrite M in H. generalize H. apply tm_step_stable.
|
|
rewrite H1. rewrite tm_step_single_bit_index.
|
|
|
|
split. intros. inversion H2. reflexivity. intros. inversion H2.
|
|
reflexivity.
|
|
|
|
(* case b > 0 *)
|
|
assert (S b = Pos.to_nat (Pos.of_nat (S b))).
|
|
|
|
|
|
|
|
|
|
destruct n.
|
|
- rewrite Nat.pow_0_r. rewrite Nat.sub_diag. rewrite plus_O_n.
|
|
rewrite Nat.pow_1_r.
|
|
rewrite Nat.pow_0_r in I. simpl in I. rewrite Nat.add_0_r in I.
|
|
induction m.
|
|
+ rewrite Nat.pow_0_r in H.
|
|
assert (K := H). rewrite Nat.lt_1_r in K.
|
|
apply Nat.neq_succ_0 in K. contradiction K.
|
|
+
|
|
|
|
|
|
|
|
|
|
|
|
induction k.
|
|
- rewrite <- I.
|
|
assert (b=0).
|
|
{ symmetry in I. rewrite Nat.eq_add_0 in I. destruct I.
|
|
apply Nat.mul_eq_0_r in H1. apply H1. apply Nat.pow_nonzero.
|
|
easy. }
|
|
rewrite H0 in I. rewrite Nat.mul_0_r in I.
|
|
rewrite Nat.add_0_r in I. rewrite <- I.
|
|
|
|
replace (2^n) with (S (2^n - 1)). rewrite <- I.
|
|
|
|
split.
|
|
|
|
intros. rewrite tm_step_head_2 at 2. rewrite tm_step_head_1. simpl.
|
|
replace (m) with (S (m-1)) in H1 at 2.
|
|
rewrite tm_step_head_2 in H1. rewrite tm_step_head_1 in H1. simpl in H1.
|
|
apply H1.
|
|
destruct m. simpl in H. apply Nat.lt_irrefl in H. contradiction H.
|
|
rewrite Nat.sub_1_r. simpl. reflexivity.
|
|
|
|
intros. rewrite tm_step_head_2 in H1 at 2.
|
|
rewrite tm_step_head_1 in H1. simpl in H1. inversion H1.
|
|
rewrite <- I.
|
|
apply eq_S in I. rewrite I at 1.
|
|
apply Nat.pred_inj. apply Nat.neq_succ_0. apply Nat.pow_nonzero.
|
|
easy. simpl. rewrite Nat.sub_1_r. reflexivity.
|
|
|
|
- apply IHk. apply Nat.lt_succ_l in H. apply H.
|
|
rewrite <- I.
|
|
|
|
|
|
|
|
|
|
split. intros. apply H1.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
assert (K: S (2 ^ n - 1 + 2 ^ S n * b) = (2 ^ n + 2 ^ S n * b)).
|
|
+ rewrite Nat.sub_1_r. rewrite <- Nat.add_succ_l.
|
|
rewrite Nat.succ_pred_pos. reflexivity.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
+ rewrite K. symmetry.
|
|
split. intros. symmetry.
|
|
apply tm_step_add_range2_flip_two.
|
|
|
|
|
|
(*
|
|
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
|
|
apply tm_step_repunit.
|
|
*)
|
|
Lemma tm_step_add_range2_flip_two : forall (n m j k : 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+j)) (k + 2^(n+j))
|
|
= nth_error (tm_step (S n+j)) (m + 2^(n+j)).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Déclagae vers la droite de k zéros pour un Bins :
|
|
Pos.iter xO xH 3. (ici k = 3)
|
|
--> on ajoute 3 zéros à gauche
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Require Import BinPosDef.
|
|
|
|
|
|
(* Autre construction de la suite, ici n est le nombre de termes *)
|
|
(* la construction se fait à l'envers *)
|
|
(*
|
|
Fixpoint tm_bin_rev (n: nat) : list bool :=
|
|
match n with
|
|
| 0 => nil
|
|
| S n' => let t := tm_bin_rev n' in
|
|
let m := Pos.of_nat n' in
|
|
(xorb (hd true t) (odd (Pos.size_nat
|
|
match Pos.lxor m (Pos.pred m) with
|
|
| N0 => BinNums.xH
|
|
| Npos(p) => p
|
|
end))) :: t
|
|
end.
|
|
*)
|
|
|
|
Fixpoint tm_bin (n: nat) : list bool :=
|
|
match n with
|
|
| 0 => nil
|
|
| S n' => let t := tm_bin n' in
|
|
let m := Pos.of_nat n' in
|
|
t ++ [ xorb (last t true)
|
|
(odd (Pos.size_nat match Pos.lxor m (Pos.pred m) with
|
|
| N0 => BinNums.xH
|
|
| Npos(p) => p
|
|
end)) ]
|
|
end.
|
|
|
|
Theorem tm_morphism_eq_bin : forall (k : nat), tm_step k = tm_bin (2^k).
|
|
Proof.
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
|
|
tm_step n = l1 ++ b1 :: b2 :: l2 ->
|
|
(eqb b1 b2) =
|
|
let ind_b2 := Pos.of_nat (S (length l1)) in (* index of b2 *)
|
|
let ind_b1 := Pos.pred ind_b2 in (* index of b1 *)
|
|
even (Pos.size_nat
|
|
match Pos.lxor ind_b1 ind_b2 with
|
|
| N0 => BinNums.xH
|
|
| Npos(p) => p
|
|
end).
|
|
Proof.
|
|
intros n l1 l2 b1 b2.
|
|
destruct n.
|
|
- simpl. intros H. induction l1.
|
|
+ rewrite app_nil_l in H. discriminate.
|
|
+ destruct l1. rewrite app_nil_l in IHl1. discriminate. discriminate.
|
|
- rewrite tm_build.
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
(*
|
|
intros n l1 l2 b1 b2.
|
|
intros H.
|
|
induction l1.
|
|
- simpl. destruct n. discriminate.
|
|
rewrite app_nil_l in H. assert (I := H).
|
|
rewrite tm_step_head_2 in I. injection I.
|
|
assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
|
|
{ replace (tm_morphism (tm_step n)) with (tm_step (S n)).
|
|
rewrite H. reflexivity. reflexivity. }
|
|
(* rewrite J *) intros. rewrite <- H1. rewrite <- H2. reflexivity.
|
|
- replace (S (length (a :: l1))) with (S (S (length l1))).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
destruct b1 in H.
|
|
+ destruct b2 in H.
|
|
(* Case 1: b1 = true, b2 = true (false) *)
|
|
replace (l2) with (tl (tl (tm_step (S n)))) in H.
|
|
assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
|
|
apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
|
|
(* Case 2: b1 = true, b2 = false (false) *)
|
|
replace (l2) with (tl (tl (tm_step (S n)))) in H.
|
|
assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
|
|
apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
|
|
+ destruct b2.
|
|
(* Case 3: b1 = false, b2 = true (TRUE) *)
|
|
discriminate.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
inversion H.
|
|
discriminate tm_step_head_2.
|
|
rewrite <- tm_step_head_2 in H.
|
|
discriminate H.
|
|
discriminate tm_step_head_2.
|
|
|
|
- simpl. simpl. simpl in H.
|
|
destruct n in H. discriminate H.
|
|
replace (l2) with (tl (tl (tm_step (S n)))) in H.
|
|
specialize (H tm_step_head_2).
|
|
rewrite <- tm_step_head_2 in H.
|
|
|
|
|
|
|
|
Lemma tm_step_head_2 : forall (n : nat),
|
|
tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
|
|
*)
|