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:21:40 +01:00
parent 0d4ca42439
commit 3788b1eeed
1 changed files with 72 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

73
thue-morse.v
View File

@ -778,6 +778,16 @@ Proof.
reflexivity.
Qed.
Lemma tm_morphism_length : forall (l : list bool),
length (tm_morphism l) = 2 * (length l).
Proof.
induction l.
- reflexivity.
- simpl. rewrite Nat.add_0_r. rewrite IHl.
rewrite Nat.add_succ_r.
simpl. rewrite Nat.add_0_r. reflexivity.
Qed.
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
tm_morphism l = hd ++ tl
-> even (length hd) = true
@ -787,8 +797,69 @@ Proof.
assert (J : l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
symmetry. apply firstn_skipn.
rewrite tm_morphism_eq in J.
rewrite tm_morphism_app in J.
rewrite tm_morphism_app in J. rewrite H in J.
apply app_eq_app in J.
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.
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
rewrite <- Nat.div2_odd. assumption.
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
apply firstn_length_le in H4. rewrite H4 in L.
replace (2 * Nat.div2 (length hd))
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
rewrite <- Nat.div2_odd in L.
rewrite <- Nat.add_0_r in L at 1.
apply Nat.add_cancel_l in L. symmetry in L.
apply length_zero_iff_nil in L.
rewrite L in H0. rewrite <- app_nil_end in H0. assumption.
rewrite <- Nat.negb_even. rewrite I. simpl.
rewrite Nat.add_0_r. reflexivity.
assert (L: length (tm_morphism (firstn (Nat.div2 (length hd)) l))
= length (tm_morphism (firstn (Nat.div2 (length hd)) l))).
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.
replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
rewrite <- Nat.div2_odd. assumption.
rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.
apply firstn_length_le in H4. rewrite H4 in L.
replace (2 * Nat.div2 (length hd))
with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
rewrite <- Nat.div2_odd in L.
rewrite <- Nat.add_0_r in L at 1.
apply Nat.add_cancel_l in L. symmetry in L.
apply length_zero_iff_nil in L.
rewrite L in H0. rewrite <- app_nil_end in H0. symmetry. assumption.
rewrite <- Nat.negb_even. rewrite I. simpl.
rewrite Nat.add_0_r. reflexivity.
Qed.