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

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-02-11 06:58:58 +01:00
parent abc598e4bd
commit 5eab5fb067
1 changed files with 35 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
src/thue_morse4.v
View File

@ -693,7 +693,7 @@ Proof.
Qed.
Lemma tm_square_rev' :
Lemma tm_step_square_rev_even :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^m
@ -730,50 +730,58 @@ Proof.
Qed.
Lemma xxx :
Lemma tm_step_square_rev_odd :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^m
-> a = rev a
-> even m = true /\ length (hd ++ a) mod (2^(S m)) = 0.
-> a = map negb (rev a)
-> odd m = true.
Proof.
intros m n hd a tl. intros H I J.
assert (0 < length a). rewrite I.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (even m = true).
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)))).
generalize H0. generalize H. apply tm_step_square_rev.
destruct H1. destruct H1. destruct H2. destruct H2.
destruct H1. destruct H1. rewrite J in H1 at 1.
destruct a. inversion H0. simpl in H1.
rewrite map_app in H1. apply app_inj_tail in H1.
destruct H1. destruct b. inversion H3. inversion H3.
destruct H1. destruct H2. destruct H2.
rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2.
rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia.
rewrite Nat.odd_succ. rewrite Nat.double_twice.
rewrite Nat.even_mul. reflexivity. lia.
rewrite I in H2.
assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2.
rewrite Nat.log2_pow2 in H3.
rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3.
rewrite H3 in H2. rewrite Nat.add_succ_r in H2.
rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2.
rewrite Nat.mul_cancel_r in H2. inversion H2.
apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
Qed.
assert (even (length (hd ++ a)) = true).
generalize H0. generalize H. apply tm_step_palindromic_even_center.
replace (List.hd false a) with (negb (List.hd false (rev a))).
Theorem tm_step_square_rev :
forall (n : nat) (hd a tl : list bool),
Lemma xxx :
forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
-> ( (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)))).
-> length a = 2^m
-> a = rev a
-> length (hd ++ a) mod (2^(S m)) = 0.
Proof.
intros m n hd a tl. intros H I J.
assert (0 < length a). rewrite I.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (even m = true). generalize J. generalize I. generalize H.
apply tm_step_square_rev_even.