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-22 16:11:28 +01:00
parent 9975cd0e5a
commit 00babc1c42
1 changed files with 19 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
thue-morse.v
View File

@ -846,12 +846,13 @@ Require Import BinPosDef.
(* Autre construction de la suite, ici n est le nombre de termes *)
Fixpoint tm_bin (n: nat) : list bool :=
(* la construction se fait à l'envers *)
Fixpoint tm_bin_rev (n: nat) : list bool :=
match n with
| 0 => nil
| S n' => let t := tm_bin n' in
| S n' => let t := tm_bin_rev n' in
let m := Pos.of_nat n' in
(xorb (hd false t)
(xorb (hd true t)
(odd (Pos.size_nat
match Pos.lxor m (Pos.pred m) with
| N0 => BinNums.xH
@ -859,6 +860,21 @@ Fixpoint tm_bin (n: nat) : list bool :=
end))) :: t
end.
Fixpoint tm_bin (n: nat) : list bool :=
match n with
| 0 => nil
| S n' => let t := tm_bin n' in
let m := Pos.of_nat n' in
t ++ [ xorb (last t true)
(odd (Pos.size_nat
match Pos.lxor m (Pos.pred m) with
| N0 => BinNums.xH
| Npos(p) => p
end)) ]
end.
Compute tm_bin 16 = tm_step 4.
Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
tm_step n = l1 ++ b1 :: b2 :: l2 ->