This commit is contained in:
Thomas Baruchel 2023-01-11 14:43:04 +01:00
parent 47686ee05f
commit 4815de3094

View File

@ -559,6 +559,50 @@ Qed.
Lemma xxx : forall (n k j : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ a ++ tl
-> length a = (S (Nat.double k)) * 2^j
-> (k = 0 \/ k = 1).
Proof.
intros n k j hd a tl.
generalize hd. generalize a. generalize tl. induction j.
- intros tl0 a0 hd0. intros H I. simpl in I. rewrite Nat.mul_1_r in I.
assert (odd (length a0) = true). rewrite I.
rewrite Nat.odd_succ. rewrite Nat.double_twice.
apply Nat.even_mul.
assert (J: length a0 < 4). generalize H0. generalize H.
apply tm_step_odd_square.
rewrite I in J.
destruct k. left. reflexivity.
destruct k. right. reflexivity.
apply Nat.succ_lt_mono in J.
apply Nat.lt_lt_succ_r in J.
rewrite Nat.double_twice in J. replace (4) with (2*2) in J.
rewrite <- Nat.mul_lt_mono_pos_l in J.
apply Nat.succ_lt_mono in J.
apply Nat.succ_lt_mono in J.
apply Nat.nlt_0_r in J. contradiction J.
apply Nat.lt_0_2. reflexivity.
- intros tl0 a0 hd0. intros H I.
assert (exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length a0 = Nat.double (length a')).
assert (even (length a0) = true).
rewrite I. rewrite Nat.pow_succ_r'. rewrite Nat.mul_comm.
rewrite <- Nat.mul_assoc. apply Nat.even_mul.
generalize H0. generalize H. apply tm_step_square_half.
destruct H0. destruct H0. destruct H0. destruct H0.
rewrite H1 in I. rewrite Nat.pow_succ_r' in I. rewrite Nat.mul_comm in I.
rewrite <- Nat.mul_assoc in I. rewrite Nat.double_twice in I.
rewrite Nat.mul_cancel_l in I. rewrite Nat.mul_comm in I.
generalize I.
assert (tm_step (S n) = x ++ x0 ++ x0 ++ x1 ++ (map negb (tm_step n))).
rewrite tm_build. rewrite H0.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. apply app_inv_head_iff.
rewrite <- app_assoc. reflexivity.
generalize H2. apply IHj. easy.
Qed.
(*