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-11-23 16:42:39 +01:00
parent f60b5673a7
commit 7d8b5cad3e
1 changed files with 0 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
thue-morse.v
View File

@ -903,55 +903,6 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
(*
Theorem tm_fullrange : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Proof.
intros n m k. rewrite <- tm_size_power2. intros.
induction n.
- destruct m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H.
replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
symmetry. apply tm_step_head_1.
- (* prouver d'abord que k < 2^n !!! *)
assert (I := H0). rewrite <- tm_size_power2 in I.
rewrite <- nth_error_Some in I.
- destruct m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
symmetry. apply tm_step_head_1.
assert (nth_error (tm_step (S n)) k = nth_error (tm_step m) k).
apply IHm.
- induction m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H.
replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
symmetry. apply tm_step_head_1.
- induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
symmetry. apply tm_step_head_1.
replace (nth_error (tm_step m) k) with (nth_error (tm_step (S m)) k) in IHm.
apply IHm.
nth_error_nth':
forall [A : Type] (l : list A) [n : nat] (d : A),
n < length l -> nth_error l n = Some (nth n l d)
*)
Lemma tm_add_range : forall (n m k : nat),
k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
Proof.
@ -990,21 +941,6 @@ Qed.
Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p
rewrite <- H2. rewrite <- Nat.sub_max_distr_r. rewrite H2.
rewrite Nat.sub_diag. rewrite Nat.max_0_l.
assert (I: nth_error(tm_step (min n m)) k = nth_error (tm_step (max n m)) k).
Nat.max_spec:
forall n m : nat, n < m /\ Nat.max n m = m \/ m <= n /\ Nat.max n m = n