Update
This commit is contained in:
parent
3e96d39b15
commit
12a7ea541c
@ -1069,9 +1069,9 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
|
||||
-> even (length a) = true
|
||||
-> exists (hd' a' tl' : list bool),
|
||||
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
|
||||
/\ 0 < length a'
|
||||
/\ odd (length hd') = true
|
||||
/\ even (length a') = true
|
||||
/\ length a' < length a.
|
||||
/\ even (length a') = true.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I J K.
|
||||
|
||||
@ -1181,6 +1181,32 @@ Proof.
|
||||
|
||||
split.
|
||||
|
||||
rewrite firstn_length_le.
|
||||
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
|
||||
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite M3. 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.
|
||||
|
||||
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.
|
||||
@ -1194,7 +1220,7 @@ Proof.
|
||||
|
||||
assumption.
|
||||
|
||||
split. rewrite firstn_length_le.
|
||||
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'')).
|
||||
@ -1215,15 +1241,6 @@ Proof.
|
||||
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'))
|
||||
@ -1244,11 +1261,38 @@ Proof.
|
||||
|
||||
split.
|
||||
|
||||
rewrite firstn_length_le.
|
||||
rewrite Nat.mul_lt_mono_pos_l with (p := 2).
|
||||
rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
|
||||
rewrite <- Nat.Even_double. rewrite L3. 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.
|
||||
|
||||
split.
|
||||
|
||||
rewrite firstn_length_le.
|
||||
apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
|
||||
assumption.
|
||||
|
||||
split. rewrite firstn_length_le.
|
||||
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')).
|
||||
@ -1268,15 +1312,6 @@ Proof.
|
||||
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.
|
||||
@ -1372,20 +1407,28 @@ Proof.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
(*
|
||||
Lemma tm_step_square_pos_even'' : forall (n : nat) (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' a' tl' : list bool),
|
||||
tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl'
|
||||
/\ odd (length hd') = true
|
||||
/\ even (length a') = true
|
||||
/\ length a' < length a.
|
||||
*)
|
||||
Lemma tm_step_square_pos_even''' : forall (n : nat),
|
||||
(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' a' tl' : list bool),
|
||||
tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
|
||||
/\ odd (length hd') = true /\ even (length a') = true).
|
||||
Proof.
|
||||
intro n. intro.
|
||||
induction n.
|
||||
- destruct H. destruct H. destruct H.
|
||||
exists x. exists x0. exists x1. assumption.
|
||||
- assert (exists hd' a' tl' : list bool,
|
||||
tm_step (Nat.pred (S n)) = hd' ++ a' ++ a' ++ tl' /\
|
||||
0 < length a' /\
|
||||
odd (length hd') = true /\ even (length a') = true).
|
||||
destruct H. destruct H. destruct H.
|
||||
destruct H. destruct H0. destruct H1.
|
||||
generalize H2. generalize H1. generalize H0. generalize H.
|
||||
apply tm_step_square_pos_even''. rewrite <- pred_Sn in H0.
|
||||
apply IHn in H0. assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user