Update
This commit is contained in:
parent
12a7ea541c
commit
688a9b1892
@ -1430,6 +1430,39 @@ Proof.
|
||||
apply IHn in H0. assumption.
|
||||
Qed.
|
||||
|
||||
Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> 0 < length a -> even (length (hd ++ a)) = true.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
assert (J: Nat.even (length a) || Nat.odd (length a) = true).
|
||||
apply Nat.orb_even_odd. apply orb_prop in J.
|
||||
assert (K: Nat.even (length hd) || Nat.odd (length hd) = true).
|
||||
apply Nat.orb_even_odd. apply orb_prop in K.
|
||||
destruct J; destruct K.
|
||||
- rewrite app_length. rewrite Nat.even_add. rewrite H0. rewrite H1.
|
||||
reflexivity.
|
||||
- assert (exists (hd' a' tl' : list bool),
|
||||
tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
|
||||
/\ odd (length hd') = true /\ even (length a') = true).
|
||||
assert (exists (hd' a' tl' : list bool),
|
||||
tm_step n = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
|
||||
/\ odd (length hd') = true /\ even (length a') = true).
|
||||
exists hd. exists a. exists tl. split. assumption.
|
||||
split. assumption. split. assumption. assumption.
|
||||
generalize H2. apply tm_step_square_pos_even'''.
|
||||
destruct H2. destruct H2. destruct H2.
|
||||
destruct H2. destruct H3. destruct H4.
|
||||
|
||||
assert (0 < 0). generalize H5. generalize H3. generalize H2.
|
||||
apply tm_step_not_nil_factor_even. inversion H6.
|
||||
- assert (even (length hd) = false).
|
||||
generalize H0. generalize H. apply tm_step_odd_prefix_square.
|
||||
rewrite H1 in H2. inversion H2.
|
||||
- rewrite app_length. rewrite Nat.even_add.
|
||||
rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd.
|
||||
rewrite H0. rewrite H1. reflexivity.
|
||||
Qed.
|
||||
|
||||
|
||||
(* TODO: la taille du facteur divise la taille du préfixe ? *)
|
||||
|
Loading…
Reference in New Issue
Block a user