Update
This commit is contained in:
Thomas Baruchel
parent
1aea07ca1f
commit
0a9f4f3bb5
|
|
@ -970,20 +970,104 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||
rewrite Nat.le_succ_l in T. assumption. easy. easy.
|
||||
|
||||
(* on change de modulo ; on travaille sur 8k+6 maintenant *)
|
||||
(* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
|
||||
assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy.
|
||||
rewrite H1 in H8. rewrite <- Nat.pred_succ with (n := lh/8) in H8.
|
||||
rewrite Nat.mul_pred_r in H8.
|
||||
|
||||
assert (lh + 8 = 8 * S (lh / 8) + 6).
|
||||
rewrite <- Nat.add_cancel_r with (p := 8) in H8.
|
||||
rewrite <- Nat.add_sub_swap in H8. rewrite Nat.sub_add in H8. assumption.
|
||||
rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono.
|
||||
assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ.
|
||||
apply Nat.mul_le_mono_l with (p := 8) in H9.
|
||||
rewrite Nat.mul_1_r in H9. assumption. apply le_0_n.
|
||||
assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ.
|
||||
apply Nat.mul_le_mono_l with (p := 8) in H9.
|
||||
rewrite Nat.mul_1_r in H9. assumption.
|
||||
|
||||
assert (nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 3)
|
||||
= nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 4)).
|
||||
rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
|
||||
rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9.
|
||||
symmetry in H9. rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9.
|
||||
apply Nat.succ_inj in H9. apply Nat.succ_inj in H9.
|
||||
rewrite Nat.mul_comm in H9. rewrite H9.
|
||||
rewrite Nat.add_succ_r in H9. symmetry in H9. rewrite Nat.add_succ_r in H9.
|
||||
apply Nat.succ_inj in H9. rewrite <- H9. rewrite H. unfold lh. unfold hd'.
|
||||
|
||||
rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''.
|
||||
rewrite app_length.
|
||||
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
|
||||
rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
|
||||
rewrite Nat.add_succ_comm.
|
||||
rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc.
|
||||
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. symmetry.
|
||||
rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc.
|
||||
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity.
|
||||
apply Nat.le_refl. rewrite <- Nat.add_0_r at 1.
|
||||
rewrite <- Nat.add_le_mono_l. apply le_0_n. apply Nat.le_refl.
|
||||
rewrite <- Nat.add_0_r at 1.
|
||||
rewrite <- Nat.add_le_mono_l. apply le_0_n. reflexivity.
|
||||
|
||||
rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r.
|
||||
rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
|
||||
rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc.
|
||||
rewrite <- Nat.add_le_mono_l. apply le_0_n.
|
||||
|
||||
rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r.
|
||||
rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
|
||||
rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc.
|
||||
rewrite <- Nat.add_le_mono_l. apply le_0_n.
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
|
||||
rewrite <- tm_step_repeating_patterns in H10. inversion H10.
|
||||
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
|
||||
rewrite Nat.mul_lt_mono_pos_l with (p := 8).
|
||||
rewrite Nat.add_lt_mono_r with (p := 6). rewrite <- H9.
|
||||
replace (8) with (2^3) at 2. rewrite <- Nat.pow_add_r.
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
|
||||
rewrite <- tm_size_power2. rewrite H'. unfold lh.
|
||||
rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
|
||||
rewrite <- Nat.add_assoc.
|
||||
|
||||
rewrite <- Nat.add_lt_mono_l. simpl.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r.
|
||||
rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r.
|
||||
apply Nat.lt_0_succ. apply Nat.le_refl.
|
||||
apply Nat.lt_le_incl. assumption. reflexivity. apply Nat.lt_0_succ.
|
||||
|
||||
(* on arrive à la suite du cas b8 = b9 avec cette fois b9 = b1
|
||||
et non plus b9 = b0 *)
|
||||
assert (b9 = b1). destruct b9; destruct b1; destruct b0.
|
||||
reflexivity. reflexivity. contradiction n6. reflexivity.
|
||||
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
||||
contradiction n6. reflexivity. reflexivity. reflexivity.
|
||||
rewrite H8 in H.
|
||||
|
||||
(* le premier nouveau sous cas est lh mod 4 = 2 en H1
|
||||
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
|
||||
c'est un carré ???
|
||||
*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)
|
||||
|
||||
|
||||
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.
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue