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:58:44 +01:00
parent d295196e00
commit 73e23b3b2a
1 changed files with 27 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
thue-morse.v
View File

@ -741,6 +741,23 @@ Proof.
reflexivity.
Qed.
Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
nth_error l k = nth_error (tm_morphism l) (2*k).
Proof.
intros l.
induction l.
- intro k.
simpl. replace (nth_error [] k) with (None : option bool).
rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
- intro k. induction k.
+ rewrite Nat.mul_0_r. reflexivity.
+ simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
reflexivity.
Qed.
Lemma tm_build_negb : forall (l : list bool),
tm_morphism (map negb l) = map negb (tm_morphism l).
Proof.
@ -822,6 +839,16 @@ Proof.
reflexivity.
Qed.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
Proof.
intros n k.
destruct k.
- rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
rewrite tm_step_head_1. reflexivity.
- rewrite <- tm_step_lemma.
rewrite tm_morphism_double_index. reflexivity.
Qed.
Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
@ -1266,35 +1293,6 @@ Proof.
generalize P. generalize I. apply Nat.lt_le_trans.
Qed.
Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
nth_error l k = nth_error (tm_morphism l) (2*k).
Proof.
intros l.
induction l.
- intro k.
simpl. replace (nth_error [] k) with (None : option bool).
rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
- intro k. induction k.
+ rewrite Nat.mul_0_r. reflexivity.
+ simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
reflexivity.
Qed.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
Proof.
intros n k.
destruct k.
- rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
rewrite tm_step_head_1. reflexivity.
- replace (tm_step (S n)) with (tm_morphism (tm_step n)).
rewrite tm_morphism_double_index. reflexivity. reflexivity.
Qed.
(* vérifier si les deux sont nécessaires *)