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 13:08:18 +01:00
parent 646f516c8c
commit 5af9d44f02
1 changed files with 6 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
thue-morse.v
View File

@ -58,10 +58,8 @@ Proof.
- reflexivity. - reflexivity.
- simpl. rewrite negb_map_explode. - simpl. rewrite negb_map_explode.
rewrite IHl. rewrite tm_morphism_concat. rewrite IHl. rewrite tm_morphism_concat.
rewrite <- app_assoc. rewrite <- app_assoc. simpl.
replace (map negb [a]) with ([negb a]). simpl.
rewrite negb_involutive. reflexivity. rewrite negb_involutive. reflexivity.
reflexivity.
Qed. Qed.
Lemma tm_morphism_double_index : forall (l : list bool) (k : nat), Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
@ -393,9 +391,9 @@ Proof.
apply H1. apply H2. apply H1. apply H2.
- induction j. - induction j.
+ intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L. + intro L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
apply tm_step_next_range2_flip_two. apply H. apply I. apply L. apply tm_step_next_range2_flip_two. apply H. apply I. apply L.
+ intros L. + intro L.
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
assert (2^n < 2^(S n + j)). assert (2^n < 2^(S n + j)).
@ -611,33 +609,19 @@ Qed.
(* vérifier si les deux sont nécessaires *)
Require Import BinPosDef.
Require Import BinPos.
Theorem tm_step_double_index : forall (p : positive),
nth_error (tm_step (Pos.size_nat p)) (Pos.to_nat p)
= nth_error (tm_step (S (Pos.size_nat p))) (Pos.to_nat (xO p)).
Proof.
intros p.
induction p.
(* TODO: supprimer head_2 *) (* TODO: supprimer head_2 *)
(* vérifier si les deux sont nécessaires *)
Require Import BinPosDef.
Require Import BinPos.
Require Import BinNat. Require Import BinNat.
(* Hamming weight of a positive; argument can not be 0! *) (* Hamming weight of a positive; argument can not be 0! *)
Fixpoint hamming_weight_positive (x: positive) := Fixpoint hamming_weight_positive (x: positive) :=
match x with match x with