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 2022-12-15 10:03:42 +01:00
parent 81386e67d4
commit cacda16dd2
1 changed files with 56 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
thue-morse.v
View File

@ -934,7 +934,6 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Require Import Ltac2.Option.
Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
k < 2^n -> m < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) m
@ -1210,20 +1209,19 @@ Proof.
assumption.
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
destruct G as [G1|G2].
(* k = 0 *)
rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
replace (nth_error (tm_step n) 0) with (Some false).
rewrite tm_step_head_1 at 1.
assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
destruct S. rewrite Nat.lt_succ_r in H0.
apply Nat.pow_le_mono_r with (a := 2) in H0.
rewrite <- tm_size_power2 in H0. rewrite <- nth_error_None in H0.
rewrite H0. easy. easy.
rewrite Nat.le_succ_l in H0. apply Nat.pow_lt_mono_r with (a := 2) in H0.
destruct S as [S1|S2]. rewrite Nat.lt_succ_r in S1.
apply Nat.pow_le_mono_r with (a := 2) in S1.
rewrite <- tm_size_power2 in S1. rewrite <- nth_error_None in S1.
rewrite S1. easy. easy.
rewrite Nat.le_succ_l in S2. apply Nat.pow_lt_mono_r with (a := 2) in S2.
rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity.
apply Nat.lt_1_2.
(* k < 0 *)
assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
@ -1269,6 +1267,55 @@ Proof.
Qed.
Lemma tm_step_double_index : forall (n k: nat),
2^n <= k -> k < 2^(S n)
-> nth_error (tm_step (S n)) k = nth_error (tm_step (S (S n))) (2*k).
Proof.
intros n k. intros H I.
destruct n.
- simpl in H. simpl in I. rewrite Nat.lt_succ_r in I.
assert (J: k = 1). generalize H. generalize I. apply Nat.le_antisymm.
rewrite J. reflexivity.
- symmetry. rewrite tm_build. rewrite nth_error_app2.
rewrite tm_size_power2.
assert (J: 2 ^ S (S n) <= 2 * k).
rewrite Nat.pow_succ_r'. apply Nat.mul_le_mono_l. assumption.
assert (K: nth_error (tm_step (S (S n))) (2*k - 2^(S (S n)))
<> nth_error (tm_step (S (S (S n)))) (2*k - 2^(S (S n)) + 2^(S (S n)))).
apply tm_step_next_range2.
apply Nat.add_lt_mono_r with (p := 2^(S (S n))). rewrite Nat.sub_add.
replace (2*k) with (k+k). apply Nat.add_lt_mono ; assumption.
simpl. rewrite Nat.add_0_r. reflexivity. assumption.
rewrite Nat.sub_add in K.
replace (nth_error (tm_step (S (S (S n)))) (2 * k))
with (nth_error (tm_step (S (S n))) (2 * k)) in K.
rewrite nth_error_map.
destruct (nth_error (tm_step (S (S n))) (2 * k - 2 ^ S (S n)));
destruct (nth_error (tm_step (S (S n))) k).
Lemma tm_step_next_range2 :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
(* vérifier si les deux sont nécessaires *)
Require Import BinPosDef.