Update
This commit is contained in:
Thomas Baruchel
parent
e8fb907c25
commit
a1e852daa3
|
|
@ -1445,7 +1445,7 @@ Proof.
|
|||
rewrite Nat.pow_succ_r; lia || rewrite Nat.pow_succ_r; lia.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_square_rev_even' :
|
||||
Lemma tm_step_square2_rev_even :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 2^m
|
||||
|
|
@ -1524,7 +1524,7 @@ Proof.
|
|||
assumption. lia. lia.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_square_rev_even_swap :
|
||||
Lemma tm_step_square2_rev_even_swap :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 2^m
|
||||
|
|
@ -1559,7 +1559,7 @@ Proof.
|
|||
apply tm_step_square_rev_even.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_square_even_pos :
|
||||
Lemma tm_step_square2_even_pos :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 2^m
|
||||
|
|
@ -1568,14 +1568,14 @@ Lemma tm_step_square_even_pos :
|
|||
Proof.
|
||||
intros m n hd a tl. intros H I J.
|
||||
assert (a = rev a).
|
||||
rewrite tm_step_square_rev_even_swap
|
||||
rewrite tm_step_square2_rev_even_swap
|
||||
with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption.
|
||||
generalize H0. generalize I. generalize H.
|
||||
apply tm_step_square_rev_even'.
|
||||
apply tm_step_square2_rev_even.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma tm_step_square_rev_odd_swap :
|
||||
Lemma tm_step_square3_rev_even_swap :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 3*2^m
|
||||
|
|
@ -1647,26 +1647,108 @@ Lemma tm_step_square3_rev_even :
|
|||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 3 * 2^m
|
||||
-> a = rev a
|
||||
-> 11 = 11.
|
||||
-> length (hd ++ a) mod 2^(S m) = 0.
|
||||
Proof.
|
||||
intros m n hd a tl. intros H I J.
|
||||
|
||||
assert (even m = true).
|
||||
rewrite <- tm_step_square3_rev_even_swap
|
||||
with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption.
|
||||
|
||||
assert (
|
||||
skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a)
|
||||
= rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl))
|
||||
/\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a)
|
||||
/\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl)).
|
||||
generalize H0. generalize H. apply tm_step_square_even_rev'_alpha.
|
||||
destruct H1. rewrite I in H1. rewrite Nat.log2_pow2 in H1.
|
||||
rewrite I in H2. rewrite Nat.log2_pow2 in H2.
|
||||
destruct m.
|
||||
assert (even (length (hd ++ a)) = true).
|
||||
assert (0 < length a). destruct a. inversion I.
|
||||
simpl. lia. generalize H1. generalize H. apply tm_step_square_pos.
|
||||
apply Nat.even_EvenT in H1. apply Nat.EvenT_Even in H1.
|
||||
apply Nat.Even_double in H1. rewrite H1. rewrite Nat.double_twice.
|
||||
rewrite Nat.mul_comm. apply Nat.mod_mul. easy.
|
||||
|
||||
destruct m. inversion H0.
|
||||
|
||||
Lemma tm_step_square_even_rev'_alpha :
|
||||
forall (j n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
|
||||
-> skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a)
|
||||
= rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl))
|
||||
/\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a)
|
||||
/\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl).
|
||||
rewrite app_assoc in H.
|
||||
rewrite <- firstn_skipn with (l := hd ++ a)
|
||||
(n := length (hd++a) - 2^(S (S (S m)))) in H.
|
||||
rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (S (S m)))) in H.
|
||||
rewrite <- firstn_skipn with (l := a)
|
||||
(n := length (a) - 2^(S (S (S m)))) in J at 1.
|
||||
rewrite <- firstn_skipn with (l := a)
|
||||
(n := 2^(S (S (S m)))) in J at 5.
|
||||
|
||||
rewrite skipn_app in H. rewrite skipn_all2 in H.
|
||||
replace (firstn (2^(S (S (S m)))) (a++tl))
|
||||
with (firstn (2^(S (S (S m)))) a
|
||||
++ firstn (2^(S (S (S m))) - length a) tl) in H.
|
||||
|
||||
rewrite rev_app_distr in J. assert (J' := J).
|
||||
apply app_eq_length_head in J.
|
||||
rewrite J in J'. apply app_inv_head in J'.
|
||||
|
||||
rewrite app_nil_l in H.
|
||||
replace (length (hd ++ a) - 2 ^ (S (S (S m))) - length hd)
|
||||
with (length a - 2^(S (S (S m)))) in H.
|
||||
assert (firstn (2^(S (S (S m)))) a
|
||||
= rev (skipn (length a - 2^(S (S (S m)))) a)).
|
||||
rewrite J'. rewrite rev_involutive. reflexivity. rewrite H1 in H.
|
||||
|
||||
assert (length (skipn (length a - 2^(S (S (S m)))) a)
|
||||
= 2^(S (Nat.double (Nat.div2 (S (S m)))))).
|
||||
rewrite skipn_length.
|
||||
replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
|
||||
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
|
||||
rewrite <- Nat.Even_double. reflexivity.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
apply Nat.le_refl. apply Nat.sub_add. rewrite I.
|
||||
rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia.
|
||||
|
||||
assert (6 < length (skipn (length a - 2^(S (S (S m)))) a)).
|
||||
rewrite skipn_length.
|
||||
replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
|
||||
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
|
||||
rewrite Nat.add_0_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
||||
rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.mul_assoc.
|
||||
replace (2*2*2) with 8.
|
||||
assert (6 < 8). lia. assert (8 <= 8*2^m).
|
||||
rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_pos_l. lia.
|
||||
apply Nat.le_succ_l.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
generalize H4. generalize H3. apply Nat.lt_le_trans. reflexivity.
|
||||
lia. lia. lia. lia. apply Nat.sub_add. rewrite I.
|
||||
rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia.
|
||||
|
||||
assert (length
|
||||
(firstn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a) ++
|
||||
skipn (length a - 2 ^ S (S (S m))) a) mod
|
||||
(2 ^ S (Nat.double (Nat.div2 (S (S m))))) = 0).
|
||||
generalize H2. generalize H3.
|
||||
rewrite <- app_assoc in H. rewrite <- app_assoc in H. generalize H.
|
||||
apply tm_step_palindromic_power2_odd.
|
||||
rewrite <- Nat.Even_double in H4.
|
||||
rewrite app_length in H4. rewrite <- Nat.add_mod_idemp_r in H4.
|
||||
replace (
|
||||
length (skipn (length a - 2 ^ S (S (S m))) a) mod 2 ^ S (S (S m))
|
||||
) with (2^(S (S (S m))) mod (2^(S (S (S m))))) in H4.
|
||||
rewrite Nat.add_mod_idemp_r in H4. rewrite firstn_length_le in H4.
|
||||
rewrite Nat.sub_add in H4. assumption.
|
||||
|
||||
rewrite app_length. rewrite I. replace 3 with (1+2).
|
||||
rewrite Nat.mul_add_distr_r. rewrite Nat.add_assoc.
|
||||
rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity.
|
||||
lia. apply Nat.pow_nonzero. easy. rewrite Nat.mod_same.
|
||||
rewrite skipn_length.
|
||||
replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
|
||||
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
|
||||
rewrite Nat.mod_same. reflexivity.
|
||||
apply Nat.pow_nonzero. easy. apply Nat.le_refl. rewrite Nat.sub_add.
|
||||
reflexivity. rewrite I. replace 3 with (1+2).
|
||||
rewrite Nat.mul_add_distr_r.
|
||||
rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity.
|
||||
apply Nat.pow_nonzero. easy.
|
||||
apply Nat.pow_nonzero. easy.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
||||
rewrite <- Nat.sub_add_distr. rewrite Nat.add_comm.
|
||||
rewrite Nat.sub_add_distr.
|
||||
rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
|
||||
reflexivity. apply Nat.le_refl.
|
||||
rewrite rev_length. rewrite firstn_length_le.
|
||||
rewrite skipn_length. reflexivity. apply Nat.le_sub_l.
|
||||
rewrite <- firstn_app. reflexivity.
|
||||
|
|
|
|||
Loading…
Reference in New Issue