Update
This commit is contained in:
Thomas Baruchel
parent
de483aef11
commit
03eed617c7
|
|
@ -629,6 +629,7 @@ Proof.
|
|||
destruct M as [hd'' M2]. destruct M2 as [a'' M3]. destruct M3 as [tl'' M].
|
||||
destruct L as [L1 L2]. destruct L2 as [L2 L3].
|
||||
destruct M as [M1 M2]. destruct M2 as [M2 M3].
|
||||
assert (L0 := L1). assert (M0 := M1).
|
||||
|
||||
assert (N: 0 < n).
|
||||
generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even.
|
||||
|
|
@ -690,42 +691,231 @@ Proof.
|
|||
rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_app in M1.
|
||||
rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_eq in M1.
|
||||
|
||||
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
|
||||
apply Nat.Even_or_Odd. destruct H0.
|
||||
(* now we easily discard the case where a'0 would be odd since we
|
||||
can freely choose either L1 or M1 to find an even prefix *)
|
||||
assert (Nat.Even (Nat.div2 (length a)) \/ Nat.Odd (Nat.div2 (length a))).
|
||||
apply Nat.Even_or_Odd. destruct H0 as [Z | Z].
|
||||
- (* first case, a'0 is even and we are looking for an odd prefix *)
|
||||
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
|
||||
apply Nat.Even_or_Odd. destruct H0.
|
||||
|
||||
(* case Nat.div2 (length hd'') has an odd length *)
|
||||
- assert( odd (Nat.div2 (length hd'')) = true).
|
||||
apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
|
||||
apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
|
||||
+ (* case Nat.div2 (length hd'') has an odd length *)
|
||||
exists (firstn (Nat.div2 (length hd'')) (tm_step n)).
|
||||
exists (firstn (Nat.div2 (length a''))
|
||||
(skipn (Nat.div2 (length hd'')) (tm_step n))).
|
||||
exists (skipn (Nat.div2 (length (a'' ++ a'')))
|
||||
(skipn (Nat.div2 (length hd'')) (tm_step n))
|
||||
++ map negb (tm_step n)).
|
||||
split. rewrite tm_build. rewrite M1 at 1.
|
||||
rewrite <- app_assoc. rewrite <- app_assoc.
|
||||
rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (Nat.div2 (length hd'') <= length (tm_step n)).
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
||||
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
|
||||
rewrite <- tm_size_power2. rewrite M0.
|
||||
rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
|
||||
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
||||
assumption. apply Nat.lt_0_2.
|
||||
|
||||
split.
|
||||
|
||||
rewrite firstn_length_le.
|
||||
apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
|
||||
apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
|
||||
rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
|
||||
apply Nat.Even_succ in H0. apply Nat.Odd_OddT in H0.
|
||||
apply Nat.OddT_odd in H0. apply H0.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
|
||||
assumption.
|
||||
destruct (length hd). inversion J. apply Nat.lt_0_succ.
|
||||
|
||||
assumption.
|
||||
|
||||
split. rewrite firstn_length_le.
|
||||
rewrite M3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
|
||||
assumption. rewrite skipn_length.
|
||||
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
|
||||
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
|
||||
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
|
||||
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
|
||||
reflexivity.
|
||||
apply le_0_n.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||
assumption.
|
||||
|
||||
rewrite firstn_length.
|
||||
assert (min (Nat.div2 (length a''))
|
||||
(length (skipn (Nat.div2 (length hd'')) (tm_step n)))
|
||||
<= (Nat.div2 (length a''))).
|
||||
apply Nat.le_min_l.
|
||||
assert (Nat.div2 (length a'') < length a). rewrite M3.
|
||||
apply Nat.lt_div2. assumption.
|
||||
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
||||
+ (* case Nat.div2 (length hd') has an odd length *)
|
||||
exists (firstn (Nat.div2 (length hd')) (tm_step n)).
|
||||
exists (firstn (Nat.div2 (length a'))
|
||||
(skipn (Nat.div2 (length hd')) (tm_step n))).
|
||||
exists (skipn (Nat.div2 (length (a' ++ a')))
|
||||
(skipn (Nat.div2 (length hd')) (tm_step n))
|
||||
++ map negb (tm_step n)).
|
||||
split. rewrite tm_build. rewrite L1 at 1.
|
||||
rewrite <- app_assoc. rewrite <- app_assoc.
|
||||
rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (Nat.div2 (length hd') <= length (tm_step n)).
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
||||
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
|
||||
rewrite <- tm_size_power2. rewrite L0.
|
||||
rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
|
||||
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
||||
assumption. apply Nat.lt_0_2.
|
||||
|
||||
split.
|
||||
|
||||
rewrite firstn_length_le.
|
||||
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
|
||||
assumption.
|
||||
|
||||
split. rewrite firstn_length_le.
|
||||
rewrite L3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
|
||||
assumption. rewrite skipn_length.
|
||||
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
|
||||
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
|
||||
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
|
||||
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
|
||||
reflexivity.
|
||||
apply le_0_n.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||
assumption.
|
||||
|
||||
rewrite firstn_length.
|
||||
assert (min (Nat.div2 (length a'))
|
||||
(length (skipn (Nat.div2 (length hd')) (tm_step n)))
|
||||
<= (Nat.div2 (length a'))).
|
||||
apply Nat.le_min_l.
|
||||
assert (Nat.div2 (length a') < length a). rewrite L3.
|
||||
apply Nat.lt_div2. assumption.
|
||||
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
||||
- (* second case, a'0 is odd and we are looking for an even prefix *)
|
||||
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
|
||||
apply Nat.Even_or_Odd. destruct H0.
|
||||
+ assert (Nat.div2 (length hd') <= length (tm_step n)).
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
||||
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
|
||||
rewrite <- tm_size_power2. rewrite L0.
|
||||
rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
|
||||
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
||||
assumption. apply Nat.lt_0_2.
|
||||
|
||||
assert (even (length (firstn (Nat.div2 (length hd')) (tm_step n))) = false).
|
||||
assert (odd (length (firstn (Nat.div2 (length a'))
|
||||
(skipn (Nat.div2 (length hd')) (tm_step n)))) = true).
|
||||
rewrite firstn_length_le. rewrite L3.
|
||||
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
|
||||
rewrite skipn_length.
|
||||
|
||||
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
|
||||
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
|
||||
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
|
||||
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
|
||||
reflexivity.
|
||||
apply le_0_n.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||
assumption.
|
||||
generalize H2. generalize L1. apply tm_step_odd_prefix_square.
|
||||
|
||||
rewrite firstn_length_le in H2.
|
||||
apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
|
||||
rewrite H0 in H2. inversion H2. assumption.
|
||||
+ assert (Nat.div2 (length hd'') <= length (tm_step n)).
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
||||
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
|
||||
rewrite <- tm_size_power2. rewrite M0.
|
||||
rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
|
||||
apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
||||
assumption. apply Nat.lt_0_2.
|
||||
|
||||
assert (even (length (firstn (Nat.div2 (length hd'')) (tm_step n))) = false).
|
||||
assert (odd (length (firstn (Nat.div2 (length a''))
|
||||
(skipn (Nat.div2 (length hd'')) (tm_step n)))) = true).
|
||||
rewrite firstn_length_le. rewrite M3.
|
||||
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
|
||||
rewrite skipn_length.
|
||||
|
||||
rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
rewrite Nat.sub_diag. rewrite Nat.add_0_l.
|
||||
|
||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||
rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
|
||||
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
|
||||
rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
|
||||
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
|
||||
apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
|
||||
reflexivity.
|
||||
apply le_0_n.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||
assumption.
|
||||
generalize H2. generalize M1. apply tm_step_odd_prefix_square.
|
||||
|
||||
rewrite firstn_length_le in H2.
|
||||
|
||||
|
||||
|
||||
(*
|
||||
assert (L9: a' ++ a' = a' ++ a'). reflexivity.
|
||||
rewrite L8 in L9 at 4. rewrite L8 in L9 at 3.
|
||||
rewrite <- tm_morphism_app in L9.
|
||||
|
||||
assert (M9: a'' ++ a'' = a'' ++ a''). reflexivity.
|
||||
rewrite M8 in M9 at 4. rewrite M8 in M9 at 3.
|
||||
rewrite <- tm_morphism_app in M9.
|
||||
*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
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)
|
||||
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).
|
||||
apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
|
||||
apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
|
||||
rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
|
||||
apply Nat.Even_succ in H0. rewrite Nat.Even_succ_succ in H0.
|
||||
apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
|
||||
rewrite H0 in H2. inversion H2.
|
||||
|
||||
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
|
||||
assumption.
|
||||
destruct (length hd). inversion J. apply Nat.lt_0_succ.
|
||||
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user