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-02 14:37:17 +01:00
parent d7568ec506
commit 2099d9f563
1 changed files with 16 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
thue-morse.v
View File

@ -799,19 +799,20 @@ Proof.
rewrite tm_morphism_eq in J.
rewrite tm_morphism_app in J. rewrite H in J.
apply app_eq_app in J.
assert (H2: length (tm_morphism l) = length hd + length tl).
rewrite H. apply app_length.
assert (H3: length hd <= length (tm_morphism l)).
rewrite H2. apply Nat.le_add_r.
rewrite tm_morphism_length in H3.
destruct J. destruct H0; destruct H0.
assert (L: length hd = length hd). reflexivity.
rewrite H0 in L at 2. rewrite app_length in L.
rewrite tm_morphism_length in L.
assert (length (tm_morphism l) = length hd + length tl).
rewrite H. apply app_length.
assert (length hd <= length (tm_morphism l)).
rewrite H2. apply Nat.le_add_r.
rewrite tm_morphism_length in H3.
assert (Nat.div2 (length hd) <= length l).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.add_0_r at 1.
@ -835,13 +836,6 @@ Proof.
reflexivity. rewrite H0 in L at 2. rewrite app_length in L.
rewrite tm_morphism_length in L.
assert (length (tm_morphism l) = length hd + length tl).
rewrite H. apply app_length.
assert (length hd <= length (tm_morphism l)).
rewrite H2. apply Nat.le_add_r.
rewrite tm_morphism_length in H3.
assert (Nat.div2 (length hd) <= length l).
rewrite Nat.mul_le_mono_pos_l with (p := 2).
rewrite <- Nat.add_0_r at 1.
@ -869,26 +863,27 @@ Qed.
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
TODO Search "count_occ"
*)
Theorem tm_step_count_occ : forall (hd tl : list bool) (k : nat),
tm_step k = hd ++ tl -> even (length hd) = true
Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
tm_step n = hd ++ tl -> even (length hd) = true
-> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
Proof.
intros hd tl k. intros H I.
destruct k.
intros hd tl n. intros H I.
destruct n.
- assert (J: hd = nil). destruct hd. reflexivity.
simpl in H. inversion H.
symmetry in H2. apply app_eq_nil in H2.
destruct H2. rewrite H0 in I. simpl in I. inversion I.
rewrite J. reflexivity.
- rewrite <- tm_step_lemma in H.
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step k))).
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
rewrite J. apply tm_morphism_count_occ.
Qed.
Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
Proof.