This commit is contained in:
Thomas Baruchel 2023-01-03 18:05:23 +01:00
parent 7336a590d1
commit 2d33df42b6

View File

@ -76,6 +76,33 @@ Proof.
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
Qed. 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_morphism_concat : forall (l1 l2 : list bool), Lemma tm_morphism_concat : forall (l1 l2 : list bool),
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2. tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof. Proof.
@ -131,6 +158,129 @@ Proof.
- simpl. rewrite IHl. reflexivity. - simpl. rewrite IHl. reflexivity.
Qed. 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.
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
tm_morphism l = hd ++ tl
-> even (length hd) = true
-> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
Proof.
intros l hd tl. intros H I.
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) l)).
generalize I. generalize H. apply tm_morphism_app2.
assert (K: l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
symmetry. apply firstn_skipn.
assert (L: tm_morphism l = (tm_morphism (firstn (Nat.div2 (length hd)) l))
++ (tm_morphism (skipn (Nat.div2 (length hd)) l))).
rewrite K at 1. apply tm_morphism_app.
rewrite H in L. rewrite <- J in L.
rewrite app_inv_head_iff in L. assumption.
Qed.
(* Thue-Morse related lemmas and theorems *) (* Thue-Morse related lemmas and theorems *)
Lemma tm_step_lemma : forall n : nat, Lemma tm_step_lemma : forall n : nat,
tm_morphism (tm_step n) = tm_step (S n). tm_morphism (tm_step n) = tm_step (S n).
@ -754,129 +904,6 @@ Proof.
Qed. 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.
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
tm_morphism l = hd ++ tl
-> even (length hd) = true
-> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
Proof.
intros l hd tl. intros H I.
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) l)).
generalize I. generalize H. apply tm_morphism_app2.
assert (K: l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
symmetry. apply firstn_skipn.
assert (L: tm_morphism l = (tm_morphism (firstn (Nat.div2 (length hd)) l))
++ (tm_morphism (skipn (Nat.div2 (length hd)) l))).
rewrite K at 1. apply tm_morphism_app.
rewrite H in L. rewrite <- J in L.
rewrite app_inv_head_iff in L. assumption.
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 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" TODO Search "count_occ"
@ -899,32 +926,6 @@ Proof.
Qed. 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), Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true. tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
Proof. Proof.
@ -1344,7 +1345,6 @@ Proof.
assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec. assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
destruct J. rewrite <- e in H. destruct J. rewrite <- e in H.
(* assert (0 < n). generalize I. generalize H. apply tm_step_cube2. *)
assert (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl assert (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
/\ 0 < length a). /\ 0 < length a).
@ -1365,624 +1365,3 @@ Qed.
(* 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))).
*)