diff --git a/thue-morse.v b/thue-morse.v index a2c625d..8e84ab3 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -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 ->