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-03 06:02:13 +01:00
parent 6cbbe7e52b
commit bcada12f4b
1 changed files with 23 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
thue-morse.v
View File

@ -979,18 +979,16 @@ Qed.
Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl
-> 0 < length a
-> even (length hd) = even (length tl).
tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n.
Proof.
intros n a hd tl. intros H J.
intros n a hd tl. intros H I.
destruct n.
- assert (3 <= length (a ++ a ++ a)).
rewrite app_length. rewrite app_length.
rewrite <- Nat.le_succ_l in J.
rewrite <- Nat.le_succ_l in I.
assert (2 <= length a + length a).
generalize J. generalize J. apply Nat.add_le_mono.
generalize H0. generalize J. apply Nat.add_le_mono.
generalize I. generalize I. apply Nat.add_le_mono.
generalize H0. generalize I. apply Nat.add_le_mono.
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
rewrite H in H1 at 2.
assert (0 <= length hd). apply Nat.le_0_l.
@ -1007,6 +1005,19 @@ Proof.
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
- apply Nat.lt_0_succ.
Qed.
Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl
-> 0 < length a
-> even (length hd) = even (length tl).
Proof.
intros n a hd tl. intros H J.
assert (K : 0 < n). generalize J. generalize H. apply tm_step_cube2.
destruct n.
- apply Nat.lt_irrefl in K. contradiction K.
- assert (Nat.Even (length (tm_step (S n)))).
rewrite tm_size_power2. rewrite Nat.pow_succ_r'.
apply Nat.Even_mul_l. apply Nat.EvenT_Even.
@ -1032,14 +1043,14 @@ Proof.
Qed.
Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool),
Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false
-> 0 < length a
-> hd_error a = hd_error tl.
Proof.
intros n a hd tl. intros H I J.
assert (even (length hd) = even (length tl)).
generalize J. generalize H. apply tm_step_cube2.
generalize J. generalize H. apply tm_step_cube3.
assert (even (length a) = true). generalize H. apply tm_step_cube1.
rewrite I in H0.
destruct a.
@ -1160,7 +1171,7 @@ Proof.
Qed.
Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool),
Lemma tm_step_cube5 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl
-> 0 < length a
-> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
@ -1181,12 +1192,12 @@ Proof.
destruct a.
+ simpl in I. apply Nat.lt_irrefl in I. contradiction I.
+ assert (Nat.even (length hd) = Nat.even (length tl)).
generalize I. generalize H. apply tm_step_cube2.
generalize I. generalize H. apply tm_step_cube3.
rewrite H0 in H1.
destruct tl.
* simpl in H1. inversion H1.
* assert (hd_error (b::a) = hd_error (b0::tl)).
generalize I. generalize H0. generalize H. apply tm_step_cube3.
generalize I. generalize H0. generalize H. apply tm_step_cube4.
simpl in H2. inversion H2. rewrite <- H4 in H.
exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl.
split. rewrite H.