This commit is contained in:
Thomas Baruchel 2022-11-26 20:33:13 +01:00
parent 00fd7e39f1
commit c2b3b67b87

View File

@ -1106,10 +1106,67 @@ Proof.
rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
rewrite <- J. rewrite I.
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.
-
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)).
@ -1117,6 +1174,12 @@ Proof.
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
@ -1161,12 +1224,6 @@ Admitted.
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
Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
tm_step n = l1 ++ b1 :: b2 :: l2 ->