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-01-14 20:34:03 +01:00
parent db1b42ac8c
commit aae08b747a
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/thue_morse.v
View File

@ -392,11 +392,11 @@ Proof.
Qed.
Lemma tm_step_consecutive_identical :
forall (n : nat) (hd a tl : list bool) (b : bool),
forall (n : nat) (hd tl : list bool) (b : bool),
tm_step n = hd ++ (b::b::nil) ++ tl
-> odd (length hd) = true.
Proof.
intros n hd a tl b. intro H.
intros n hd tl b. intro H.
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
apply bool_dec. destruct J.
- rewrite <- Nat.negb_even. rewrite e. reflexivity.
@ -423,10 +423,10 @@ Lemma tm_step_consecutive_identical' :
Proof.
intros n hd a tl b1 b2. intros H.
assert (Nat.odd (length hd) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
generalize H. apply tm_step_consecutive_identical.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (Nat.odd (length ((hd ++ [b1;b1])++a)) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
generalize H. apply tm_step_consecutive_identical.
rewrite app_length in H1. rewrite Nat.odd_add in H1.
rewrite app_length in H1. rewrite Nat.odd_add in H1. rewrite H0 in H1.
replace (Nat.odd (length a)) with (negb (Nat.even (length a))) in H1.

2
src/thue_morse2.v
View File

@ -402,7 +402,7 @@ Proof.
assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square.
destruct a. inversion I. destruct a.
rewrite <- negb_true_iff. rewrite Nat.negb_even.
generalize H. apply tm_step_consecutive_identical. apply hd.
generalize H. apply tm_step_consecutive_identical.
destruct a. inversion I.
destruct a.
apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl).