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-10 21:31:26 +01:00
parent a4b2592b01
commit bb3687969e
1 changed files with 11 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
thue-morse.v
View File

@ -769,20 +769,13 @@ Proof.
reflexivity.
Qed.
Lemma tm_size_double : forall n : nat,
length (tm_step (S n)) = length (tm_step n) + length (tm_step n).
Proof.
intros n. rewrite tm_build. rewrite app_length. rewrite map_length.
reflexivity.
Qed.
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
Proof.
intros n.
induction n.
- reflexivity.
- rewrite tm_size_double. replace (2^S n) with (2^n + 2^n).
rewrite IHn. reflexivity.
- rewrite tm_build. rewrite app_length. rewrite map_length.
replace (2^S n) with (2^n + 2^n). rewrite IHn. reflexivity.
simpl. rewrite <- plus_n_O. reflexivity.
Qed.
@ -1262,14 +1255,20 @@ Proof.
generalize H1. generalize I. apply Nat.lt_le_trans.
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.
Require Import BinNat.
Require Import BinPosDef.
Require Import BinPos.