Update
This commit is contained in:
parent
141c4ba029
commit
3e96d39b15
@ -1061,17 +1061,17 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ a ++ tl
|
tm_step n = hd ++ a ++ a ++ tl
|
||||||
-> 0 < length a
|
-> 0 < length a
|
||||||
-> odd (length hd) = true
|
-> odd (length hd) = true
|
||||||
-> even (length a) = true
|
-> even (length a) = true
|
||||||
-> exists (hd' a' tl' : list bool),
|
-> exists (hd' a' tl' : list bool),
|
||||||
tm_step n = hd' ++ a' ++ a' ++ tl'
|
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
|
||||||
/\ odd (length hd') = true
|
/\ odd (length hd') = true
|
||||||
/\ even (length a') = true
|
/\ even (length a') = true
|
||||||
/\ length a' < length a
|
/\ length a' < length a.
|
||||||
/\ 0 < length a'.
|
|
||||||
Proof.
|
Proof.
|
||||||
intros n hd a tl. intros H I J K.
|
intros n hd a tl. intros H I J K.
|
||||||
|
|
||||||
@ -1166,11 +1166,8 @@ Proof.
|
|||||||
exists (firstn (Nat.div2 (length a''))
|
exists (firstn (Nat.div2 (length a''))
|
||||||
(skipn (Nat.div2 (length hd'')) (tm_step n))).
|
(skipn (Nat.div2 (length hd'')) (tm_step n))).
|
||||||
exists (skipn (Nat.div2 (length (a'' ++ a'')))
|
exists (skipn (Nat.div2 (length (a'' ++ a'')))
|
||||||
(skipn (Nat.div2 (length hd'')) (tm_step n))
|
(skipn (Nat.div2 (length hd'')) (tm_step n))).
|
||||||
++ map negb (tm_step n)).
|
split. rewrite <- pred_Sn. rewrite M1 at 1. reflexivity.
|
||||||
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)).
|
assert (Nat.div2 (length hd'') <= length (tm_step n)).
|
||||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||||
@ -1218,8 +1215,6 @@ Proof.
|
|||||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||||
assumption.
|
assumption.
|
||||||
|
|
||||||
split.
|
|
||||||
|
|
||||||
rewrite firstn_length.
|
rewrite firstn_length.
|
||||||
assert (min (Nat.div2 (length a''))
|
assert (min (Nat.div2 (length a''))
|
||||||
(length (skipn (Nat.div2 (length hd'')) (tm_step n)))
|
(length (skipn (Nat.div2 (length hd'')) (tm_step n)))
|
||||||
@ -1229,41 +1224,13 @@ Proof.
|
|||||||
apply Nat.lt_div2. assumption.
|
apply Nat.lt_div2. assumption.
|
||||||
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
||||||
|
|
||||||
rewrite firstn_length_le. rewrite M3.
|
|
||||||
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
|
|
||||||
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
|
|
||||||
rewrite <- Nat.Even_double. assumption.
|
|
||||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
||||||
apply Nat.lt_0_2.
|
|
||||||
|
|
||||||
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.
|
|
||||||
|
|
||||||
+ (* case Nat.div2 (length hd') has an odd length *)
|
+ (* case Nat.div2 (length hd') has an odd length *)
|
||||||
exists (firstn (Nat.div2 (length hd')) (tm_step n)).
|
exists (firstn (Nat.div2 (length hd')) (tm_step n)).
|
||||||
exists (firstn (Nat.div2 (length a'))
|
exists (firstn (Nat.div2 (length a'))
|
||||||
(skipn (Nat.div2 (length hd')) (tm_step n))).
|
(skipn (Nat.div2 (length hd')) (tm_step n))).
|
||||||
exists (skipn (Nat.div2 (length (a' ++ a')))
|
exists (skipn (Nat.div2 (length (a' ++ a')))
|
||||||
(skipn (Nat.div2 (length hd')) (tm_step n))
|
(skipn (Nat.div2 (length hd')) (tm_step n))).
|
||||||
++ map negb (tm_step n)).
|
split. rewrite <- pred_Sn. rewrite L1 at 1. reflexivity.
|
||||||
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)).
|
assert (Nat.div2 (length hd') <= length (tm_step n)).
|
||||||
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
||||||
@ -1302,8 +1269,6 @@ Proof.
|
|||||||
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
|
||||||
assumption.
|
assumption.
|
||||||
|
|
||||||
split.
|
|
||||||
|
|
||||||
rewrite firstn_length.
|
rewrite firstn_length.
|
||||||
assert (min (Nat.div2 (length a'))
|
assert (min (Nat.div2 (length a'))
|
||||||
(length (skipn (Nat.div2 (length hd')) (tm_step n)))
|
(length (skipn (Nat.div2 (length hd')) (tm_step n)))
|
||||||
@ -1312,31 +1277,6 @@ Proof.
|
|||||||
assert (Nat.div2 (length a') < length a). rewrite L3.
|
assert (Nat.div2 (length a') < length a). rewrite L3.
|
||||||
apply Nat.lt_div2. assumption.
|
apply Nat.lt_div2. assumption.
|
||||||
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
generalize H3. generalize H2. apply Nat.le_lt_trans.
|
||||||
|
|
||||||
rewrite firstn_length_le. rewrite L3.
|
|
||||||
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
|
|
||||||
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
|
|
||||||
rewrite <- Nat.Even_double. assumption.
|
|
||||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
||||||
apply Nat.lt_0_2.
|
|
||||||
|
|
||||||
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.
|
|
||||||
- (* second case, a'0 is odd and we are looking for an even prefix *)
|
- (* 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'))).
|
assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
|
||||||
apply Nat.Even_or_Odd. destruct H0.
|
apply Nat.Even_or_Odd. destruct H0.
|
||||||
@ -1434,9 +1374,6 @@ Qed.
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(*
|
(*
|
||||||
Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ a ++ tl
|
tm_step n = hd ++ a ++ a ++ tl
|
||||||
@ -1444,11 +1381,10 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
|||||||
-> odd (length hd) = true
|
-> odd (length hd) = true
|
||||||
-> even (length a) = true
|
-> even (length a) = true
|
||||||
-> exists (hd' a' tl' : list bool),
|
-> exists (hd' a' tl' : list bool),
|
||||||
tm_step n = hd' ++ a' ++ a' ++ tl'
|
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
|
||||||
/\ odd (length hd') = true
|
/\ odd (length hd') = true
|
||||||
/\ even (length a') = true
|
/\ even (length a') = true
|
||||||
/\ length a' < length a
|
/\ length a' < length a.
|
||||||
/\ 0 < length a'.
|
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user