baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

This commit is contained in:
Thomas Baruchel 2023-02-12 21:00:02 +01:00
parent 3371e25740
commit e8fb907c25
1 changed files with 100 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

103
src/thue_morse4.v
View File

@ -1524,7 +1524,7 @@ Proof.
assumption. lia. lia.
Qed.
Lemma tm_step_square_rev_even'' :
Lemma tm_step_square_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_rev_even''' :
Lemma tm_step_square_even_pos :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^m
@ -1568,8 +1568,105 @@ Lemma tm_step_square_rev_even''' :
Proof.
intros m n hd a tl. intros H I J.
assert (a = rev a).
rewrite tm_step_square_rev_even''
rewrite tm_step_square_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'.
Qed.
Lemma tm_step_square_rev_odd_swap :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 3*2^m
-> (even m = true <-> a = rev a).
Proof.
intros m n hd a tl. intros H I.
split. intro J.
assert (( (a = rev a /\ exists j,
length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
\/ (a = map negb (rev a) /\ exists j,
length a = 2^(S (Nat.double j))
\/ length a = 3 * 2^(S (Nat.double j))))).
assert (0 < length a). destruct a.
symmetry in I. rewrite Nat.eq_mul_0 in I. destruct I. inversion H0.
apply Nat.pow_nonzero in H0. contradiction. easy.
simpl. lia. generalize H0. generalize H. apply tm_step_square_rev.
destruct H0. destruct H0. assumption. destruct H0. destruct H1.
destruct H1.
assert (Nat.log2 (3*2^m) = Nat.log2 (3*2^m)). reflexivity.
rewrite <- I in H2 at 1. rewrite H1 in H2.
rewrite Nat.log2_pow2 in H2.
rewrite Nat.log2_mul_pow2 in H2. replace (Nat.log2 3) with 1 in H2.
rewrite H2 in H1. rewrite Nat.add_succ_r in H1.
rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1.
rewrite I in H1. apply Nat.mul_cancel_r in H1. inversion H1.
apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
rewrite I in H1. apply Nat.mul_cancel_l in H1.
apply Nat.pow_inj_r in H1.
rewrite H1 in J. rewrite Nat.even_succ in J. rewrite Nat.double_twice in J.
rewrite Nat.odd_mul in J. inversion J. lia. easy.
intro J.
assert (( (a = rev a /\ exists j,
length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
\/ (a = map negb (rev a) /\ exists j,
length a = 2^(S (Nat.double j))
\/ length a = 3 * 2^(S (Nat.double j))))).
assert (0 < length a). destruct a.
symmetry in I. rewrite Nat.eq_mul_0 in I. destruct I. inversion H0.
apply Nat.pow_nonzero in H0. contradiction. easy.
simpl. lia. generalize H0. generalize H. apply tm_step_square_rev.
destruct H0. destruct H0. destruct H1. destruct H1.
assert (Nat.log2 (3*2^m) = Nat.log2 (3*2^m)). reflexivity.
rewrite <- I in H2 at 1. rewrite H1 in H2.
rewrite Nat.log2_pow2 in H2.
rewrite Nat.log2_mul_pow2 in H2. replace (Nat.log2 3) with 1 in H2.
rewrite H2 in H1. rewrite Nat.add_succ_r in H1.
rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1.
rewrite I in H1. apply Nat.mul_cancel_r in H1. inversion H1.
apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
rewrite I in H1. apply Nat.mul_cancel_l in H1.
apply Nat.pow_inj_r in H1. rewrite H1. rewrite Nat.double_twice.
rewrite Nat.even_mul. reflexivity. lia. easy.
destruct H0. rewrite <- J in H0.
destruct a. symmetry in I. rewrite Nat.eq_mul_0 in I.
destruct I. inversion H2.
apply Nat.pow_nonzero in H2. contradiction.
easy. simpl in H0. inversion H0.
destruct b; inversion H3.
Qed.
Lemma tm_step_square3_rev_even :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 3 * 2^m
-> a = rev a
-> 11 = 11.
Proof.
intros m n hd a tl. intros H I J.
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.
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).