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-12 17:19:16 +01:00
parent efb81d2bba
commit 3371e25740
1 changed files with 19 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/thue_morse4.v
View File

@ -1528,11 +1528,10 @@ 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
-> even m = true
-> length (hd ++ a) mod 2^(S m) = 0.
-> (even m = true <-> a = rev a).
Proof.
intros m n hd a tl. intros H I J.
assert (a = rev a).
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,
@ -1554,7 +1553,23 @@ Proof.
rewrite Nat.add_0_r in H1. rewrite Nat.pow_succ_r in H1.
rewrite Nat.mul_cancel_r in H1. inversion H1.
apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
intro J.
generalize J. generalize I. generalize H.
apply tm_step_square_rev_even.
Qed.
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
-> even m = true
-> length (hd ++ a) mod 2^(S m) = 0.
Proof.
intros m n hd a tl. intros H I J.
assert (a = rev a).
rewrite tm_step_square_rev_even''
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.