baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
coqbooks/thue-morse.v

2242 lines
118 KiB
Coq
Raw Blame History

(*
A010060 Thue-Morse sequence: let A_k denote the first 2^k terms; then A_0 = 0 and for k >= 0, A_{k+1} 541
= A_k B_k, where B_k is obtained from A_k by interchanging 0's and 1's.
0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0,
1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1,
1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1
(list; graph; refs; listen; history; text; internal format)
OFFSET 0,1
COMMENTS Named after Axel Thue, whose name is pronounced as if it were spelled "Tü" where the ü sound
is roughly as in the German word üben. (It is incorrect to say "Too-ee" or "Too-eh".) - N. J.
A. Sloane, Jun 12 2018
Also called the Thue-Morse infinite word, or the Morse-Hedlund sequence, or the parity
sequence.
Fixed point of the morphism 0 --> 01, 1 --> 10, see example. - Joerg Arndt, Mar 12 2013
The sequence is cubefree (does not contain three consecutive identical blocks) [see Offner for
a direct proof] and is overlap-free (does not contain XYXYX where X is 0 or 1 and Y is any
string of 0's and 1's).
a(n) = "parity sequence" = parity of number of 1's in binary representation of n.
To construct the sequence: alternate blocks of 0's and 1's of successive lengths A003159(k) -
A003159(k-1), k = 1, 2, 3, ... (A003159(0) = 0). Example: since the first seven differences of
A003159 are 1, 2, 1, 1, 2, 2, 2, the sequence starts with 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0. -
Emeric Deutsch, Jan 10 2003
Characteristic function of A000069 (odious numbers). - Ralf Stephan, Jun 20 2003
a(n) = S2(n) mod 2, where S2(n) = sum of digits of n, n in base-2 notation. There is a class
of generalized Thue-Morse sequences: Let Sk(n) = sum of digits of n; n in base-k notation. Let
F(t) be some arithmetic function. Then a(n)= F(Sk(n)) mod m is a generalized Thue-Morse
sequence. The classical Thue-Morse sequence is the case k=2, m=2, F(t)= 1*t. - Ctibor O.
Zizka, Feb 12 2008 (with correction from Daniel Hug, May 19 2017)
More generally, the partial sums of the generalized Thue-Morse sequences a(n) = F(Sk(n)) mod m
are fractal, where Sk(n) is sum of digits of n, n in base k; F(t) is an arithmetic function; m
integer. - Ctibor O. Zizka, Feb 25 2008
Starting with offset 1, = running sums mod 2 of the kneading sequence (A035263, 1, 0, 1, 1, 1,
0, 1, 0, 1, 0, 1, 1, 1, ...); also parity of A005187: (1, 3, 4, 7, 8, 10, 11, 15, 16, 18, 19,
...). - Gary W. Adamson, Jun 15 2008
Generalized Thue-Morse sequences mod n (n>1) = the array shown in A141803. As n -> infinity
the sequences -> (1, 2, 3, ...). - Gary W. Adamson, Jul 10 2008
The Thue-Morse sequence for N = 3 = A053838, (sum of digits of n in base 3, mod 3): (0, 1, 2,
1, 2, 0, 2, 0, 1, 1, 2, ...) = A004128 mod 3. - Gary W. Adamson, Aug 24 2008
For all positive integers k, the subsequence a(0) to a(2^k-1) is identical to the subsequence
a(2^k+2^(k-1)) to a(2^(k+1)+2^(k-1)-1). That is to say, the first half of A_k is identical to
the second half of B_k, and the second half of A_k is identical to the first quarter of
B_{k+1}, which consists of the k/2 terms immediately following B_k.
Proof: The subsequence a(2^k+2^(k-1)) to a(2^(k+1)-1), the second half of B_k, is by
definition formed from the subsequence a(2^(k-1)) to a(2^k-1), the second half of A_k, by
interchanging its 0's and 1's. In turn, the subsequence a(2^(k-1)) to a(2^k-1), the second
half of A_k, which is by definition also B_{k-1}, is by definition formed from the subsequence
a(0) to a(2^(k-1)-1), the first half of A_k, which is by definition also A_{k-1}, by
interchanging its 0's and 1's. Interchanging the 0's and 1's of a subsequence twice leaves it
unchanged, so the subsequence a(2^k+2^(k-1)) to a(2^(k+1)-1), the second half of B_k, must be
identical to the subsequence a(0) to a(2^(k-1)-1), the first half of A_k.
Also, the subsequence a(2^(k+1)) to a(2^(k+1)+2^(k-1)-1), the first quarter of B_{k+1}, is by
definition formed from the subsequence a(0) to a(2^(k-1)-1), the first quarter of A_{k+1}, by
interchanging its 0's and 1's. As noted above, the subsequence a(2^(k-1)) to a(2^k-1), the
second half of A_k, which is by definition also B_{k-1}, is by definition formed from the
subsequence a(0) to a(2^(k-1)-1), which is by definition A_{k-1}, by interchanging its 0's and
1's, as well. If two subsequences are formed from the same subsequence by interchanging its
0's and 1's then they must be identical, so the subsequence a(2^(k+1)) to
a(2^(k+1)+2^(k-1)-1), the first quarter of B_{k+1}, must be identical to the subsequence
a(2^(k-1)) to a(2^k-1), the second half of A_k.
Therefore the subsequence a(0), ..., a(2^(k-1)-1), a(2^(k-1)), ..., a(2^k-1) is identical to
the subsequence a(2^k+2^(k-1)), ..., a(2^(k+1)-1), a(2^(k+1)), ..., a(2^(k+1)+2^(k-1)-1), QED.
According to the German chess rules of 1929 a game of chess was drawn if the same sequence of
moves was repeated three times consecutively. Euwe, see the references, proved that this rule
could lead to infinite games. For his proof he reinvented the Thue-Morse sequence. - Johannes
W. Meijer, Feb 04 2010
"Thue-Morse 0->01 & 1->10, at each stage append the previous with its complement. Start with
0, 1, 2, 3 and write them in binary. Next calculate the sum of the digits (mod 2) - that is
divide the sum by 2 and use the remainder." Pickover, The Math Book.
Let s_2(n) be the sum of the base-2 digits of n and epsilon(n) = (-1)^s_2(n), the Thue-Morse
sequence, then prod(n >= 0, ((2*n+1)/(2*n+2))^epsilon(n) ) = 1/sqrt(2). - Jonathan Vos Post,
Jun 06 2012
Dekking shows that the constant obtained by interpreting this sequence as a binary expansion
is transcendental; see also "The Ubiquitous Prouhet-Thue-Morse Sequence". - Charles R
Greathouse IV, Jul 23 2013
Drmota, Mauduit, and Rivat proved that the subsequence a(n^2) is normal--see A228039. -
Jonathan Sondow, Sep 03 2013
Although the probability of a 0 or 1 is equal, guesses predicated on the latest bit seen
produce a correct match 2 out of 3 times. - Bill McEachen, Mar 13 2015
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan
Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
REFERENCES J.-P. Allouche and J. Shallit, Automatic Sequences, Cambridge Univ. Press, 2003, p. 15.
Jason Bell, Michael Coons, and Eric Rowland, "The Rational-Transcendental Dichotomy of Mahler
Functions", Journal of Integer Sequences, Vol. 16 (2013), #13.2.10.
J. Berstel and J. Karhumaki, Combinatorics on words - a tutorial, Bull. EATCS, #79 (2003), pp.
178-228.
B. Bollobas, The Art of Mathematics: Coffee Time in Memphis, Cambridge, 2006, p. 224.
S. Brlek, Enumeration of factors in the Thue-Morse word, Discrete Applied Math., 24 (1989),
83-96. doi:10.1016/0166-218X(92)90274-E.
Yann Bugeaud and Guo-Niu Han, A combinatorial proof of the non-vanishing of Hankel
determinants of the Thue-Morse sequence, Electronic Journal of Combinatorics 21(3) (2014),
#P3.26.
Y. Bugeaud and M. Queffélec, On Rational Approximation of the Binary Thue-Morse-Mahler Number,
Journal of Integer Sequences, 16 (2013), #13.2.3.
J. Cooper and A. Dutle, Greedy Galois Games, Amer. Math. Mnthly, 120 (2013), 441-451.
Currie, James D. "Non-repetitive words: Ages and essences." Combinatorica 16.1 (1996): 19-40
A. de Luca and S. Varricchio, Some combinatorial properties of the Thue-Morse sequence and a
problem in semigroups, Theoret. Comput. Sci. 63 (1989), 333-348.
Colin Defant, Anti-Power Prefixes of the Thue-Morse Word Journal of Combinatorics, 24(1)
(2017), #P1.32
F. M. Dekking, Transcendance du nombre de Thue-Morse, Comptes Rendus de l'Academie des
Sciences de Paris 285 (1977), pp. 157-160.
F. M. Dekking, On repetitions of blocks in binary sequences. J. Combinatorial Theory Ser. A 20
(1976), no. 3, pp. 292-299. MR0429728(55 #2739)
Dekking, Michel, Michel Mendès France, and Alf van der Poorten. "Folds." The Mathematical
Intelligencer, 4.3 (1982): 130-138 & front cover, and 4:4 (1982): 173-181 (printed in two
parts).
Dubickas, Artūras. On a sequence related to that of Thue-Morse and its applications. Discrete
Math. 307 (2007), no. 9-10, 1082--1093. MR2292537 (2008b:11086).
Fabien Durand, Julien Leroy, and Gwenaël Richomme, "Do the Properties of an S-adic
Representation Determine Factor Complexity?", Journal of Integer Sequences, Vol. 16 (2013),
#13.2.6.
M. Euwe, Mengentheoretische Betrachtungen Über das Schachspiel, Proceedings Koninklijke
Nederlandse Akademie van Wetenschappen, Amsterdam, Vol. 32 (5): 633-642, 1929.
S. Ferenczi, Complexity of sequences and dynamical systems, Discrete Math., 206 (1999),
145-154.
S. R. Finch, Mathematical Constants, Cambridge, 2003, Section 6.8.
W. H. Gottschalk and G. A. Hedlund, Topological Dynamics. American Mathematical Society,
Colloquium Publications, Vol. 36, Providence, RI, 1955, p. 105.
J. Grytczuk, Thue type problems for graphs, points and numbers, Discrete Math., 308 (2008),
4419-4429.
A. Hof, O. Knill and B. Simon, Singular continuous spectrum for palindromic Schroedinger
operators, Commun. Math. Phys. 174 (1995), 149-159.
Mari Huova and Juhani Karhumäki, "On Unavoidability of k-abelian Squares in Pure Morphic
Words", Journal of Integer Sequences, Vol. 16 (2013), #13.2.9.
B. Kitchens, Review of "Computational Ergodic Theory" by G. H. Choe, Bull. Amer. Math. Soc.,
44 (2007), 147-155.
Le Breton, Xavier, Linear independence of automatic formal power series. Discrete Math. 306
(2006), no. 15, 1776-1780.
M. Lothaire, Combinatorics on Words. Addison-Wesley, Reading, MA, 1983, p. 23.
Donald MacMurray, A mathematician gives an hour to chess, Chess Review 6 (No. 10, 1938), 238.
[Discusses Marston's 1938 article]
Mauduit, Christian. Multiplicative properties of the Thue-Morse sequence. Period. Math.
Hungar. 43 (2001), no. 1-2, 137--153. MR1830572 (2002i:11081)
Mignosi, F.; Restivo, A.; Sciortino, M. Words and forbidden factors. WORDS (Rouen, 1999).
Theoret. Comput. Sci. 273 (2002), no. 1-2, 99--117. MR1872445 (2002m:68096)
Marston Morse, Title?, Bull. Amer. Math. Soc., 44 (No. 9, 1938), p. 632. [Mentions an
application to chess]
C. A. Pickover, Wonders of Numbers, Adventures in Mathematics, Mind and Meaning, Chapter 17,
'The Pipes of Papua,' Oxford University Press, Oxford, England, 2000, pages 34-38.
C. A. Pickover, A Passion for Mathematics, Wiley, 2005; see p. 60.
Clifford A. Pickover, The Math Book, From Pythagoras to the 57th Dimension, 250 Milestones in
the History of Mathematics, Sterling Publ., NY, 2009, page 316.
Narad Rampersad and Elise Vaslet, "On Highly Repetitive and Power Free Words", Journal of
Integer Sequences, Vol. 16 (2013), #13.2.7.
G. Richomme, K. Saari, L. Q. Zamboni, Abelian complexity in minimal subshifts, J. London Math.
Soc. 83(1) (2011) 79-95.
Michel Rigo, Formal Languages, Automata and Numeration Systems, 2 vols., Wiley, 2014. Mentions
this sequence - see "List of Sequences" in Vol. 2.
M. Rigo, P. Salimov, and E. Vandomme, "Some Properties of Abelian Return Words", Journal of
Integer Sequences, Vol. 16 (2013), #13.2.5.
Benoit Rittaud, Elise Janvresse, Emmanuel Lesigne and Jean-Christophe Novelli, Quand les maths
se font discrètes, Le Pommier, 2008 (ISBN 978-2-7465-0370-0).
A. Salomaa, Jewels of Formal Language Theory. Computer Science Press, Rockville, MD, 1981, p.
6.
Shallit, J. O. "On Infinite Products Associated with Sums of Digits." J. Number Th. 21,
128-134, 1985.
Ian Stewart, "Feedback", Mathematical Recreations Column, Scientific American, 274 (No. 3,
1996), page 109 [Historical notes on this sequence]
Thomas Stoll, On digital blocks of polynomial values and extractions in the Rudin-Shapiro
sequence, RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2016,
50, pp. 93-99. <hal-01278708>.
A. Thue. Über unendliche Zeichenreihen, Norske Vid. Selsk. Skr. I. Mat. Nat. Kl. Christiania,
No. 7 (1906), 1-22.
A. Thue, Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen, Norske Vid. Selsk.
Skr. I. Mat. Nat. Kl. Christiania, 1 (1912), 1-67.
S. Wolfram, A New Kind of Science, Wolfram Media, 2002; p. 890.
LINKS N. J. A. Sloane, Table of n, a(n) for n = 0..16383
A. G. M. Ahmed, AA Weaving. In: Proceedings of Bridges 2013: Mathematics, Music, Art, ...,
2013.
A. Aksenov, The Newman phenomenon and Lucas sequence, arXiv preprint arXiv:1108.5352
[math.NT], 2011-2012.
Max A. Alekseyev and N. J. A. Sloane, On Kaprekar's Junction Numbers, arXiv:2112.14365, 2021;
Journal of Combinatorics and Number Theory, 2022 (to appear).
J.-P. Allouche, Series and infinite products related to binary expansions of integers,
Behaviour, 4.4 (1992): p. 5.
J.-P. Allouche, Lecture notes on automatic sequences, Krakow October 2013.
J.-P. Allouche, Thue, Combinatorics on words, and conjectures inspired by the Thue-Morse
sequence, J. de Théorie des Nombres de Bordeaux, 27, no. 2 (2015), 375-388.
J.-P. Allouche, Andre Arnold, Jean Berstel, Srecko Brlek, William Jockusch, Simon Plouffe and
Bruce E. Sagan, A relative of the Thue-Morse sequence, Discrete Math., 139 (1995), 455-461.
Jean-Paul Allouche, Julien Cassaigne, Jeffrey Shallit and Luca Q. Zamboni, A Taxonomy of
Morphic Sequences, arXiv preprint arXiv:1711.10807 [cs.FL], Nov 29 2017.
J.-P. Allouche and H. Cohen, Dirichlet Series and Curious Infinite Products, Bull. London
Math. Soc. 17, 531-538, 1985.
J.-P. Allouche and M. Mendes France, Automata and Automatic Sequences, in: Axel F. and Gratias
D. (eds), Beyond Quasicrystals. Centre de Physique des Houches, vol 3. Springer, Berlin,
Heidelberg, pp. 293-367, 1995; DOI https://doi.org/10.1007/978-3-662-03130-8_11.
J.-P. Allouche and M. Mendes France, Automata and Automatic Sequences, in: Axel F. and Gratias
D. (eds), Beyond Quasicrystals. Centre de Physique des Houches, vol 3. Springer, Berlin,
Heidelberg, pp. 293-367, 1995; DOI https://doi.org/10.1007/978-3-662-03130-8_11. [Local copy]
J.-P. Allouche and Jeffrey Shallit, The Ubiquitous Prouhet-Thue-Morse Sequence, in C. Ding. T.
Helleseth and H. Niederreiter, eds., Sequences and Their Applications: Proceedings of SETA
'98, Springer-Verlag, 1999, pp. 1-16.
J.-P. Allouche and J. Shallit, The Ring of k-regular Sequences, II, Theoretical Computer
Science 307.1 (2003): 3-29. doi:10.1016/S0304-3975(03)00090-2
Jorge Almeida and Ondrej Klíma, Binary patterns in the Prouhet-Thue-Morse sequence,
arXiv:1904.07137 [math.CO], 2019.
Joerg Arndt, Matters Computational (The Fxtbook), p. 44.
G. N. Arzhantseva, C. H. Cashen, D. Gruber and D. Hume, Contracting geodesics in infinitely
presented graphical small cancellation groups, arXiv preprint arXiv:1602.03767 [math.GR],
2016-2018.
Ricardo Astudillo, On a Class of Thue-Morse Type Sequences, J. Integer Seqs., Vol. 6, 2003.
F. Axel et al., Vibrational modes in a one dimensional "quasi-alloy": the Morse case, J. de
Physique, Colloq. C3, Supp. to No. 7, Vol. 47 (Jul 1986), pp. C3-181-C3-186; see Eq. (10).
M. Baake, U. Grimm and J. Nilsson, Scaling of the Thue-Morse diffraction measure, arXiv
preprint arXiv:1311.4371 [math-ph], 2013.
Scott Balchin and Dan Rust, Computations for Symbolic Substitutions, Journal of Integer
Sequences, Vol. 20 (2017), Article 17.4.1.
Lucilla Baldini and Josef Eschgfäller, Random functions from coupled dynamical systems, arXiv
preprint arXiv:1609.01750 [math.CO], 2016. See Example 3.11.
J. Berstel, Axel Thue's papers on repetitions in words: a translation, July 21 1994.
Publications du LaCIM, Département de mathématiques et d'informatique 20, Université du Québec
à Montréal, 1995, 85 pages. [Cached copy]
J.-F. Bertazzon, Resolution of an integral equation with the Thue-Morse sequence,
arXiv:1201.2502v1 [math.CO], Jan 12, 2012.
Françoise Dejean, Sur un Théorème de Thue, J. Combinatorial Theory, vol. 13 A, iss. 1 (1972)
90-99.
F. Michel Dekking, Morphisms, Symbolic sequences, and their Standard Forms, arXiv:1509.00260
[math.CO], 2015.
E. Deutsch and B. E. Sagan, Congruences for Catalan and Motzkin numbers and related sequences,
J. Num. Theory 117 (2006), 191-215.
M. Drmota, C. Mauduit and J. Rivat, The Thue-Morse Sequence Along The Squares is Normal,
Abstract, ÖMG-DMV Congress, 2013.
Arthur Dolgopolov, Equitable Sequencing and Allocation Under Uncertainty, Preprint, 2016.
J. Endrullis, D. Hendriks and J. W. Klop, Degrees of streams, Journal of Integers B 11 (2011):
1-40..
A. S. Fraenkel, New games related to old and new sequences, INTEGERS, Electronic J. of
Combinatorial Number Theory, Vol. 4, Paper G6, 2004.
Hao Fu and G.-N. Han, Computer assisted proof for Apwenian sequences related to Hankel
determinants, arXiv preprint arXiv:1601.04370 [math.NT], 2016.
Maciej Gawro and Maciej Ulas, "On formal inverse of the Prouhet-Thue-Morse sequence." Discrete
Mathematics 339.5 (2016): 1459-1470. Also arXiv:1601.04840, 2016.
Michael Gilleland, Some Self-Similar Integer Sequences
Daniel Goc, Luke Schaeffer and Jeffrey Shallit, The Subword Complexity of k-Automatic
Sequences is k-Synchronized, arXiv 1206.5352 [cs.FL], Jun 28 2012.
G. A. Hedlund, Remarks on the work of Axel Thue on sequences, Nordisk Mat. Tid., 15 (1967),
148-150.
Dimitri Hendriks, Frits G. W. Dannenberg, Jorg Endrullis, Mark Dow and Jan Willem Klop,
Arithmetic Self-Similarity of Infinite Sequences, arXiv preprint 1201.3786 [math.CO], 2012.
A. M. Hinz, S. Klavžar, U. Milutinović and C. Petr, The Tower of Hanoi - Myths and Maths,
Birkhäuser 2013. See page 79. Website for book
Tanya Khovanova, There are no coincidences, arXiv preprint 1410.2193 [math.CO], 2014.
Clark Kimberling, Intriguing infinite words composed of zeros and ones, Elemente der
Mathematik (2021).
Naoki Kobayashi, Kazutaka Matsuda and Ayumi Shinohara, Functional Programs as Compressed Data,
Higher-Order and Symbolic Computation, 25, no. 1 (2012): 39-84..
Philip Lafrance, Narad Rampersad and Randy Yee, Some properties of a Rudin-Shapiro-like
sequence, arXiv:1408.2277 [math.CO], 2014.
C. Mauduit, J. Rivat, La somme des chiffres des carres, Acta Mathem. 203 (1) (2009) 107-148.
M. Morse, Recurrent geodesics on a surface of negative curvature, Trans. Amer. Math. Soc., 22
(1921), 84-100.
K. Nakano, Shall We Juggle, Coinductively?, in Certified Programs and Proofs, Lecture Notes in
Computer Science Volume 7679, 2012, pp. 160-172.
Hieu D. Nguyen, A mixing of Prouhet-Thue-Morse sequences and Rademacher functions, arXiv
preprint arXiv:1405.6958 [math.NT], 2014.
Hieu D. Nguyen, A Generalization of the Digital Binomial Theorem , J. Int. Seq. 18 (2015) #
15.5.7.
C. D. Offner, Repetitions of Words and the Thue-Morse sequence. Preprint, no date.
Matt Parker, The Fairest Sharing Sequence Ever, YouTube video, Nov 27 2015
A. Parreau, M. Rigo, E. Rowland and E. Vandomme, A new approach to the 2-regularity of the
l-abelian complexity of 2-automatic sequences, arXiv preprint arXiv:1405.3532 [cs.FL], 2014.
C. A. Pickover, "Wonders of Numbers, Adventures in Mathematics, Mind and Meaning,"
Zentralblatt review
E. Prouhet, Mémoire sur quelques relations entre les puissances des nombres, Comptes Rendus
Acad. des Sciences, 33 (No. 8, 1851), p. 225. [Said to implicitly mention this sequence]
Michel Rigo, Relations on words, arXiv preprint arXiv:1602.03364 [cs.FL], 2016.
Luke Schaeffer and Jeffrey Shallit, Closed, Palindromic, Rich, Privileged, Trapezoidal, and
Balanced Words in Automatic Sequences, Electronic Journal of Combinatorics 23(1) (2016),
#P1.25.
M. R. Schroeder & N. J. A. Sloane, Correspondence, 1991
R. Schroeppel and R. W. Gosper, HACKMEM #122 (1972).
Vladimir Shevelev, Two analogs of Thue-Morse sequence, arXiv preprint arXiv:1603.04434
[math.NT], 2016-2017.
N. J. A. Sloane, The first 1000 terms as a string
L. Spiegelhofer, Normality of the Thue-Morse Sequence along Piatetski-Shapiro sequences,
Quart. J. Math. 66 (3) (2015).
Hassan Tarfaoui, Concours Général 1990 - Exercice 1 (in French).
Eric Weisstein's World of Mathematics, Thue-Morse Sequence
Eric Weisstein's World of Mathematics, Thue-Morse Constant
Eric Weisstein's World of Mathematics, Parity
Joost Winter, Marcello M. Bonsangue, and Jan J. M. M. Rutten, Context-free coalgebras, Journal
of Computer and System Sciences, 81.5 (2015): 911-939.
Hans Zantema, Complexity of Automatic Sequences, International Conference on Language and
Automata Theory and Applications (LATA 2020): Language and Automata Theory and Applications,
260-271.
Index entries for sequences that are fixed points of mappings
Index entries for "core" sequences
Index entries for sequences related to binary expansion of n
Index entries for characteristic functions
Index to sequences related to Olympiads and other Mathematical competitions.
FORMULA a(2n) = a(n), a(2n+1) = 1 - a(n), a(0) = 0. Also, a(k+2^m) = 1 - a(k) if 0 <= k < 2^m.
If n = Sum b_i*2^i is the binary expansion of n then a(n) = Sum b_i (mod 2).
Let S(0) = 0 and for k >= 1, construct S(k) from S(k-1) by mapping 0 -> 01 and 1 -> 10;
sequence is S(infinity).
G.f.: (1/(1 - x) - Product_{k >= 0} (1 - x^(2^k)))/2. - Benoit Cloitre, Apr 23 2003
a(0) = 0, a(n) = (n + a(floor(n/2))) mod 2; also a(0) = 0, a(n) = (n - a(floor(n/2))) mod 2. -
Benoit Cloitre, Dec 10 2003
a(n) = -1 + (Sum_{k=0..n} binomial(n,k) mod 2) mod 3 = -1 + A001316(n) mod 3. - Benoit
Cloitre, May 09 2004
Let b(1) = 1 and b(n) = b(ceiling(n/2)) - b(floor(n/2)) then a(n-1) = (1/2)*(1 - b(2n-1)). -
Benoit Cloitre, Apr 26 2005
a(n) = 1 - A010059(n) = A001285(n) - 1. - Ralf Stephan, Jun 20 2003
a(n) = A001969(n) - 2n. - Franklin T. Adams-Watters, Aug 28 2006
a(n) = A115384(n) - A115384(n-1) for n > 0. - Reinhard Zumkeller, Aug 26 2007
For n >= 0, a(A004760(n+1)) = 1 - a(n). - Vladimir Shevelev, Apr 25 2009
a(A160217(n)) = 1 - a(n). - Vladimir Shevelev, May 05 2009
a(n) == A000069(n) (mod 2). - Robert G. Wilson v, Jan 18 2012
a(n) = A000035(A000120(n)). - Omar E. Pol, Oct 26 2013
a(n) = A000035(A193231(n)). - Antti Karttunen, Dec 27 2013
a(n) + A181155(n-1) = 2n for n >= 1. - Clark Kimberling, Oct 06 2014
G.f. A(x) satisfies: A(x) = x / (1 - x^2) + (1 - x) * A(x^2). - Ilya Gutkovskiy, Jul 29 2021
From Bernard Schott, Jan 21 2022: (Start)
a(n) = a(n*2^k) for k >= 0.
a((2^m-1)^2) = (1-(-1)^m))/2 (see Hassan Tarfaoui link, Concours Général 1990). (End)
EXAMPLE The evolution starting at 0 is:
.0
.0, 1
.0, 1, 1, 0
.0, 1, 1, 0, 1, 0, 0, 1
.0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0
.0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0,
1
.......
A_2 = 0 1 1 0, so B_2 = 1 0 0 1 and A_3 = A_2 B_2 = 0 1 1 0 1 0 0 1.
From Joerg Arndt, Mar 12 2013: (Start)
The first steps of the iterated substitution are
Start: 0
Rules:
0 --> 01
1 --> 10
-------------
0: (#=1)
0
1: (#=2)
01
2: (#=4)
0110
3: (#=8)
01101001
4: (#=16)
0110100110010110
5: (#=32)
01101001100101101001011001101001
6: (#=64)
0110100110010110100101100110100110010110011010010110100110010110
(End)
From Omar E. Pol, Oct 28 2013: (Start)
Written as an irregular triangle in which row lengths is A011782, the sequence begins:
0;
1;
1,0;
1,0,0,1;
1,0,0,1,0,1,1,0;
1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1;
1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1,0,1,1,0,1,0,0,1,1,0,0,1,0,1,1,0;
It appears that: row j lists the first A011782(j) terms of A010059, with j >= 0; row sums give
A166444 which is also 0 together with A011782; right border gives A000035.
(End)
MAPLE s := proc(k) local i, ans; ans := [ 0, 1 ]; for i from 0 to k do ans := [ op(ans),
op(map(n->(n+1) mod 2, ans)) ] od; return ans; end; t1 := s(6); A010060 := n->t1[n]; # s(k)
gives first 2^(k+2) terms.
a := proc(k) b := [0]: for n from 1 to k do b := subs({0=[0, 1], 1=[1, 0]}, b) od: b; end; #
a(k), after the removal of the brackets, gives the first 2^k terms. # Example: a(3); gives
[[[[0, 1], [1, 0]], [[1, 0], [0, 1]]]]
A010060:=proc(n)
add(i, i=convert(n, base, 2)) mod 2 ;
end proc:
seq(A010060(n), n=0..104); # Emeric Deutsch, Mar 19 2005
map(`-`, convert(StringTools[ThueMorse](1000), bytes), 48); # Robert Israel, Sep 22 2014
MATHEMATICA Table[ If[ OddQ[ Count[ IntegerDigits[n, 2], 1]], 1, 0], {n, 0, 100}];
mt = 0; Do[ mt = ToString[mt] <> ToString[(10^(2^n) - 1)/9 - ToExpression[mt] ], {n, 0, 6} ];
Prepend[ RealDigits[ N[ ToExpression[mt], 2^7] ] [ [1] ], 0]
Mod[ Count[ #, 1 ]& /@Table[ IntegerDigits[ i, 2 ], {i, 0, 2^7 - 1} ], 2 ] (* Harlan J.
Brothers, Feb 05 2005 *)
Nest[ Flatten[ # /. {0 -> {0, 1}, 1 -> {1, 0}}] &, {0}, 7] (* Robert G. Wilson v Sep 26 2006
*)
a[n_] := If[n == 0, 0, If[Mod[n, 2] == 0, a[n/2], 1 - a[(n - 1)/2]]] (* Ben Branman, Oct 22
2010 *)
a[n_] := Mod[Length[FixedPointList[BitAnd[#, # - 1] &, n]], 2] (* Jan Mangaldan, Jul 23 2015
*)
Table[2/3 (1 - Cos[Pi/3 (n - Sum[(-1)^Binomial[n, k], {k, 1, n}])]), {n, 0, 100}] (* or, for
version 10.2 or higher *) Table[ThueMorse[n], {n, 0, 100}] (* Vladimir Reshetnikov, May 06
2016 *)
ThueMorse[Range[0, 100]] (* The program uses the ThueMorse function from Mathematica version
11 *) (* Harvey P. Dale, Aug 11 2016 *)
PROG (Haskell)
a010060 n = a010060_list !! n
a010060_list =
0 : interleave (complement a010060_list) (tail a010060_list)
where complement = map (1 - )
interleave (x:xs) ys = x : interleave ys xs
-- Doug McIlroy (doug(AT)cs.dartmouth.edu), Jun 29 2003
-- Edited by Reinhard Zumkeller, Oct 03 2012
(PARI) a(n)=if(n<1, 0, sum(k=0, length(binary(n))-1, bittest(n, k))%2)
(PARI) a(n)=if(n<1, 0, subst(Pol(binary(n)), x, 1)%2)
(PARI) default(realprecision, 6100); x=0.0; m=20080; for (n=1, m-1, x=x+x; x=x+sum(k=0,
length(binary(n))-1, bittest(n, k))%2); x=2*x/2^m; for (n=0, 20000, d=floor(x); x=(x-d)*2;
write("b010060.txt", n, " ", d)); \\ Harry J. Smith, Apr 28 2009
(PARI) a(n)=hammingweight(n)%2 \\ Charles R Greathouse IV, Mar 22 2013
(Python)
A010060_list = [0]
for _ in range(14):
A010060_list += [1-d for d in A010060_list] # Chai Wah Wu, Mar 04 2016
(R)
maxrow <- 8 # by choice
b01 <- 1
for(m in 0:maxrow) for(k in 0:(2^m-1)){
b01[2^(m+1)+ k] <- b01[2^m+k]
b01[2^(m+1)+2^m+k] <- 1-b01[2^m+k]
}
(b01 <- c(0, b01))
# Yosu Yurramendi, Apr 10 2017
CROSSREFS Cf. A001285 (for 1, 2 version), A010059 (for 1, 0 version), A106400 (for +1, -1 version),
A048707. A010060(n)=A000120(n) mod 2.
Cf. A007413, A080813, A080814, A036581, A108694. See also the Thue (or Roth) constant A014578,
also A014571.
Cf. also A001969, A035263, A005187, A115384, A132680, A141803, A104248, A193231.
Run lengths give A026465. Backward first differences give A029883.
Cf. A004128, A053838, A059448, A171900, A161916, A214212, A005942 (subword complexity),
A010693 (Abelian complexity), A225186 (squares), A228039 (a(n^2)), A282317.
Sequences mentioned in the Allouche et al. "Taxonomy" paper, listed by example number: 1:
A003849, 2: A010060, 3: A010056, 4: A020985 and A020987, 5: A191818, 6: A316340 and A273129,
18: A316341, 19: A030302, 20: A063438, 21: A316342, 22: A316343, 23: A003849 minus its first
term, 24: A316344, 25: A316345 and A316824, 26: A020985 and A020987, 27: A316825, 28: A159689,
29: A049320, 30: A003849, 31: A316826, 32: A316827, 33: A316828, 34: A316344, 35: A043529, 36:
A316829, 37: A010060.
Sequence in context: A143222 A286490 A217831 * A316569 A284848 A286484
Adjacent sequences: A010057 A010058 A010059 * A010061 A010062 A010063
KEYWORD nonn,core,easy,nice
AUTHOR N. J. A. Sloane
STATUS approved
Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recents
The OEIS Community | Maintained by The OEIS Foundation Inc.
License Agreements, Terms of Use, Privacy Policy. .
Last modified November 20 14:06 EST 2022. Contains 358247 sequences. (Running on oeis4.)
*)
Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Bool.
Import ListNotations.
Fixpoint tm_morphism (l:list bool) : list bool :=
match l with
| nil => []
| h :: t => h :: (negb h) :: (tm_morphism t)
end.
Fixpoint tm_step (n: nat) : list bool :=
match n with
| 0 => false :: nil
| S n' => tm_morphism (tm_step n')
end.
(* ad hoc more or less general lemmas *)
Lemma negb_map_explode : forall (l1 l2 : list bool),
map negb (l1 ++ l2) = map negb l1 ++ map negb l2.
Proof.
intros l1 l2.
induction l1.
- reflexivity.
- simpl. rewrite IHl1. reflexivity.
Qed.
Lemma negb_double_map : forall (l : list bool),
map negb (map negb l) = l.
Proof.
intros l.
induction l.
- reflexivity.
- simpl. rewrite IHl. replace (negb (negb a)) with (a).
reflexivity. rewrite negb_involutive. reflexivity.
Qed.
Lemma tm_morphism_concat : forall (l1 l2 : list bool),
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
intros l1 l2.
induction l1.
- reflexivity.
- simpl. rewrite IHl1. reflexivity.
Qed.
Lemma tm_morphism_rev : forall (l : list bool),
rev (tm_morphism l) = tm_morphism (map negb (rev l)).
Proof.
intros l. induction l.
- reflexivity.
- simpl. rewrite negb_map_explode.
rewrite IHl. rewrite tm_morphism_concat.
rewrite <- app_assoc.
replace (map negb [a]) with ([negb a]). simpl.
rewrite negb_involutive. reflexivity.
reflexivity.
Qed.
Lemma tm_build_negb : forall (l : list bool),
tm_morphism (map negb l) = map negb (tm_morphism l).
Proof.
intros l.
induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
Qed.
(* Thue-Morse related lemmas and theorems *)
Lemma tm_step_lemma : forall n : nat,
tm_morphism (tm_step n) = tm_step (S n).
Proof.
intros n. reflexivity.
Qed.
Theorem tm_build : forall (n : nat),
tm_step (S n) = tm_step n ++ map negb (tm_step n).
Proof.
intros n.
induction n.
- reflexivity.
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
rewrite negb_map_explode. rewrite negb_double_map.
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.
simpl. rewrite <- plus_n_O. reflexivity.
Qed.
Lemma tm_step_head_2 : forall (n : nat),
tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
Proof.
intros n.
induction n.
- reflexivity.
- simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
rewrite IHn. simpl. reflexivity.
simpl. reflexivity.
Qed.
Lemma tm_step_end_2 : forall (n : nat),
rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))).
Proof.
intros n. induction n.
- reflexivity.
- simpl tm_step. rewrite tm_morphism_rev.
replace (tm_morphism (tm_step n)) with (tm_step (S n)).
rewrite IHn. simpl tm_morphism. simpl tl.
rewrite Nat.even_succ.
rewrite Nat.odd_succ.
rewrite negb_involutive.
reflexivity. reflexivity.
Qed.
Lemma tm_step_head_1 : forall (n : nat),
tm_step n = false :: tl (tm_step n).
Proof.
intros n. destruct n.
- reflexivity.
- rewrite tm_step_head_2. reflexivity.
Qed.
Lemma tm_step_end_1 : forall (n : nat),
rev (tm_step n) = odd n :: tl (rev (tm_step n)).
Proof.
intros n.
destruct n.
- reflexivity.
- rewrite tm_step_end_2. simpl.
rewrite Nat.odd_succ.
reflexivity.
Qed.
Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
intros n.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
replace (true) with (negb false). apply map_nth_error.
rewrite tm_step_head_1. simpl. reflexivity.
reflexivity. rewrite tm_size_power2. easy.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intros n.
rewrite nth_error_nth' with (d := false).
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_nth. rewrite rev_length.
rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
rewrite Nat.sub_diag. rewrite tm_step_end_1.
simpl. reflexivity.
rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
simpl in IHn. rewrite Nat.mul_comm in IHn.
rewrite <- Nat.pow_succ_r in IHn. apply IHn.
apply Nat.le_0_l. apply Nat.lt_0_2.
rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
rewrite rev_involutive. reflexivity.
rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
apply Nat.pow_nonzero. easy.
Qed.
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
l = l1 ++ b :: l2 -> length l1 < length l.
Proof.
intros l l1 l2 b. intros H. rewrite H.
rewrite app_length. simpl. apply Nat.lt_add_pos_r.
apply Nat.lt_0_succ.
Qed.
Lemma tm_step_next_range :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
Proof.
intros n k b. intros H. assert (I := H).
apply nth_error_split in H. destruct H. destruct H. inversion H.
rewrite tm_build. rewrite nth_error_app1. apply I.
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
Qed.
Lemma tm_step_add_range : forall (n m k : nat),
k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
Proof.
intros n m k. intros H.
induction m.
- rewrite Nat.add_comm. reflexivity.
- rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. apply nth_error_nth'.
rewrite H0 in IHm. symmetry in IHm.
rewrite H0. symmetry. generalize IHm.
apply tm_step_next_range.
Qed.
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Proof.
intros n m k. intros.
assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
apply Nat.max_spec. destruct I.
- destruct H1. replace (m) with (n + (m-n)). apply tm_step_add_range. apply H.
apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (n <= n). apply le_n. symmetry.
replace (m) with (m + (n-n)) at 1. generalize H3.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
reflexivity.
- destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
apply H0. replace (n) with (m + n - m) at 2. generalize H1.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (m <= m). apply le_n. symmetry.
replace (n) with (n + (m-m)) at 1. generalize H3.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
reflexivity.
Qed.
Lemma tm_step_next_range2 :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Proof.
intros n k. intros H.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
rewrite H0.
assert (nth_error (map negb (tm_step n)) k
= Some (negb (nth k (tm_step n) false))).
generalize H0. apply map_nth_error. rewrite H1.
destruct (nth k (tm_step n) false). easy. easy.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Require Import Ltac2.Option.
Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
k < 2^n -> m < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) m
<->
nth_error (tm_step (S n)) (k + 2^n)
= nth_error (tm_step (S n)) (m + 2^n).
Proof.
intros n k m. intros H. intros I.
(* Part 1: preamble *)
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
generalize H. apply tm_step_next_range2.
assert (nth_error (tm_step n) m <> nth_error (tm_step (S n)) (m + 2^n)).
generalize I. apply tm_step_next_range2.
assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize H. apply Nat.add_lt_mono_r.
assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize I. apply Nat.add_lt_mono_r.
(* Part 2: main proof *)
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step n) m = Some (nth m (tm_step n) false)).
generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
Some (nth (k + 2^n) (tm_step (S n)) false)).
generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
apply nth_error_nth'.
assert (nth_error (tm_step (S n)) (m + 2 ^ n) =
Some (nth (m + 2^n) (tm_step (S n)) false)).
generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
apply nth_error_nth'.
rewrite H2. rewrite H3. rewrite H4. rewrite H5.
(* Part 3: handling 16 different cases *)
destruct (nth k (tm_step n) false).
destruct (nth m (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
easy.
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth m (tm_step n) false).
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
easy.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
easy.
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
easy.
Qed.
Lemma tm_step_add_range2_flip_two : forall (n m j k : nat),
k < 2^n -> m < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) m
<->
nth_error (tm_step (S n+j)) (k + 2^(n+j))
= nth_error (tm_step (S n+j)) (m + 2^(n+j)).
Proof.
intros n m j k. intros H I.
assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize H. apply Nat.add_lt_mono_r.
assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
generalize I. apply Nat.add_lt_mono_r.
split.
- induction j.
+ intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
rewrite <- tm_step_next_range2_flip_two. apply L. apply H. apply I.
+ intros L.
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
assert (2^n < 2^(S n + j)).
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
generalize H0. apply Nat.lt_lt_add_r.
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
assert (k < 2^(S n + j)).
generalize H0. generalize H. apply Nat.lt_trans.
assert (m < 2^(S n + j)).
generalize H0. generalize I. apply Nat.lt_trans.
rewrite <- tm_step_next_range2_flip_two.
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
generalize H1. generalize H. apply tm_step_stable.
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
generalize H2. generalize I. apply tm_step_stable.
rewrite <- H3. rewrite <- H4. apply L.
apply H1. apply H2.
- induction j.
+ intros 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.
+ intros L.
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
assert (2^n < 2^(S n + j)).
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
generalize H0. apply Nat.lt_lt_add_r.
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
assert (k < 2^(S n + j)).
generalize H0. generalize H. apply Nat.lt_trans.
assert (m < 2^(S n + j)).
generalize H0. generalize I. apply Nat.lt_trans.
rewrite <- tm_step_next_range2_flip_two in L.
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
generalize H1. generalize H. apply tm_step_stable.
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
generalize H2. generalize I. apply tm_step_stable.
rewrite <- H3 in L. rewrite <- H4 in L. apply L.
apply H1. apply H2.
Qed.
(*
Lemma tm_step_enlarge_window : forall (n m k i j k': nat),
k * 2^m < 2^n ->
k' * 2^m < 2^(S n) -> (
j < m -> i < 2^j ->
nth_error (tm_step n) (k*2^m + i) = nth_error (tm_step n) (k*2^m + i + 2^j)
<->
nth_error (tm_step (S n)) (k'*2^m + i) = nth_error (tm_step (S n)) (k'*2^m + i + 2^j)).
Proof.
intros n m k i j k'. intros I J K L.
split.
- intros M. rewrite tm_build.
assert (S: k' * 2^m < 2^n \/ 2^n <= k' * 2^m). apply Nat.lt_ge_cases.
rewrite nth_error_app1. rewrite nth_error_app1. apply M.
distinguer selon k4*2^m < 2^n ou non
*)
Lemma lt_even_even : forall (a b : nat),
even a = true -> even b = true -> a < b -> S a < b.
Proof.
intros a b. intros H I J.
rewrite <- Nat.le_succ_l in J. rewrite Nat.lt_eq_cases in J.
destruct J.
- apply H0.
- rewrite <- H0 in I. rewrite Nat.even_succ in I.
rewrite <- I in H. rewrite <- Nat.negb_even in H.
destruct (even a).
+ simpl in H. apply Bool.diff_true_false in H. contradiction H.
+ simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
Qed.
(* TODO: écrire deux lemmes, avec
- une implication vers la première moitié de la construction suivante
- une implication vers la seconde moitié de la construction suivante
ENSUITE : voir si on peut itérer sur le facteur multiplicatif k *)
Lemma tm_step_add_small_power :
forall (n m k j : nat),
0 < k -> k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j)
-> nth_error (tm_step (S n)) ((S k) * 2^m) <> nth_error (tm_step (S n)) ((S k) * 2^m + 2^j).
Proof.
intros n m k j. intros G H I J.
assert (N0: 2^m < 2^n). assert (2^m <= k * 2^m).
replace (k * 2^m) with (1*2^m + (k-1)*2^m).
simpl. rewrite Nat.add_0_r. apply Nat.le_add_r.
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_l.
rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_1_r. rewrite Nat.add_sub.
reflexivity. rewrite Nat.le_succ_l. apply G.
generalize H. generalize H0. apply Nat.le_lt_trans.
assert (N1: m < n). apply Nat.pow_lt_mono_r_iff in N0. apply N0.
apply Nat.lt_1_2.
assert (N2: 0 < m). assert (0 <= j). apply Nat.le_0_l.
generalize I. generalize H0. apply Nat.le_lt_trans.
assert (N3: 0 < n). destruct k. apply Nat.lt_irrefl in G. contradiction G.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
assert (2^m <= 2^m + k*2^m). apply Nat.le_add_r.
generalize H1. generalize H0. apply Nat.le_trans.
assert (2^0 < 2^n). generalize H. generalize H0.
apply Nat.le_lt_trans.
rewrite <- Nat.pow_lt_mono_r_iff in H1.
apply H1. apply Nat.lt_1_2.
assert (N4: 0 < m-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
replace (m-j+j) with (m). apply I. symmetry. apply Nat.sub_add.
generalize I. apply Nat.lt_le_incl.
assert (N5: j < n). generalize N1. generalize I. apply Nat.lt_trans.
assert (N6: 0 < n-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
replace (n-j+j) with (n). apply N5. symmetry. apply Nat.sub_add.
generalize N5. apply Nat.lt_le_incl.
assert (O: k * 2^m + 2^j < 2^n).
replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
apply Nat.mul_lt_mono_pos_r.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite Nat.add_1_r. apply lt_even_even.
- destruct (m-j).
+ apply Nat.lt_irrefl in N4. contradiction N4.
+ rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_mul.
rewrite Nat.even_2. rewrite orb_true_r. reflexivity. apply Nat.le_0_l.
- destruct (n-j).
+ apply Nat.lt_irrefl in N6. contradiction N6.
+ rewrite Nat.pow_succ_r. rewrite Nat.even_mul.
rewrite Nat.even_2. rewrite orb_true_l. reflexivity. apply Nat.le_0_l.
- apply Nat.mul_lt_mono_pos_r with (p := 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite <- Nat.pow_add_r.
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
rewrite Nat.sub_add. rewrite Nat.sub_add. apply H.
apply Nat.lt_le_incl. apply N5.
apply Nat.lt_le_incl. apply I.
- rewrite Nat.mul_add_distr_r.
rewrite <- Nat.mul_assoc.
rewrite <- Nat.pow_add_r. rewrite Nat.mul_1_l. rewrite Nat.sub_add.
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. reflexivity.
apply Nat.lt_le_incl. apply N5.
apply Nat.lt_le_incl. apply I.
- assert ((S k)*2^m + 2^j < 2^(S n)). rewrite Nat.add_comm.
apply Nat.add_lt_mono with (p := 2^m) (q := 2^n) in O.
rewrite <- Nat.add_assoc in O. rewrite Nat.add_shuffle3 in O.
replace (2^m) with (1 * 2^m) in O at 2. rewrite <- Nat.mul_add_distr_r in O.
rewrite Nat.add_1_r in O. rewrite Nat.pow_succ_r'.
replace (2^n) with (1*2^n) in O. rewrite <- Nat.mul_add_distr_r in O.
rewrite Nat.add_1_r in O. apply O.
rewrite Nat.mul_1_l. reflexivity. rewrite Nat.mul_1_l. reflexivity.
apply N0.
Lemma tm_step_add_small_power :
forall (n m k j : nat),
1 < k -> k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros J H I.
assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (m-j+j) with (m). apply I. symmetry. apply Nat.sub_add.
generalize I. apply Nat.lt_le_incl.
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
- rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
+
(* m < n *)
assert (N: m < n). apply Nat.lt_le_incl in H0.
apply Nat.log2_le_mono in H0.
rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
generalize H0. assert (m < m + Nat.log2 k).
apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
generalize H1. apply Nat.lt_le_trans.
apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
apply Nat.le_0_l.
assert (0 < n-m).
rewrite Nat.add_lt_mono_l with (p := m).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (n-m+m) with (n). apply N. symmetry. apply Nat.sub_add.
generalize N. apply Nat.lt_le_incl.
assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (n-j+j) with (n). generalize N. generalize I. apply Nat.lt_trans.
symmetry. apply Nat.sub_add.
assert (j < n). generalize N. generalize I. apply Nat.lt_trans.
generalize H2. apply Nat.lt_le_incl.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
apply Nat.mul_lt_mono_pos_r.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
generalize I. generalize H3. apply Nat.le_lt_trans.
assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
assert (2^m <= 2^m + k*2^m). apply Nat.le_add_r.
generalize H5. generalize H4. apply Nat.le_trans.
assert (2^0 < 2^n). generalize H0. generalize H4.
apply Nat.le_lt_trans.
rewrite <- Nat.pow_lt_mono_r_iff in H5.
apply H5. apply Nat.lt_1_2.
assert (S (k*2^m) < 2^n). apply lt_even_even.
rewrite Nat.even_mul.
assert (Nat.even (2^m) = true). destruct m.
* apply Nat.lt_irrefl in H3. contradiction H3.
* rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
destruct n.
apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* apply H0.
* rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
apply Nat.mul_lt_mono_pos_r with (p := 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite <- Nat.pow_add_r.
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
rewrite Nat.sub_add. rewrite Nat.sub_add.
apply H0.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite <- Nat.pow_add_r.
rewrite Nat.mul_add_distr_r.
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
rewrite Nat.mul_1_l. rewrite Nat.sub_add. rewrite Nat.sub_add.
reflexivity.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite tm_size_power2. apply H0.
+
rewrite nth_error_app2. rewrite nth_error_app2.
rewrite tm_size_power2.
rewrite nth_error_nth' with (d := false).
rewrite nth_error_nth' with (d := false).
(*
Lemma tm_step_add_small_power :
forall (n m k j : nat),
1 < k -> k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros J H I.
assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply I.
generalize I. apply Nat.lt_le_incl.
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
- rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
+
(* m < n *)
assert (N: m < n). apply Nat.lt_le_incl in H0.
apply Nat.log2_le_mono in H0.
rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
generalize H0. assert (m < m + Nat.log2 k).
apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
generalize H1. apply Nat.lt_le_trans.
apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
apply Nat.le_0_l.
assert (0 < n-m).
rewrite Nat.add_lt_mono_l with (p := m).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply N.
generalize N. apply Nat.lt_le_incl.
assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. generalize N. generalize I. apply Nat.lt_trans.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
apply Nat.mul_lt_mono_pos_r.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
generalize I. generalize H3. apply Nat.le_lt_trans.
assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
generalize H4. apply Arith_prebase.le_plus_trans_stt.
assert (2^0 < 2^n). generalize H0. generalize H4.
apply Nat.le_lt_trans. rewrite <- Nat.pow_lt_mono_r_iff in H5.
apply H5. apply Nat.lt_1_2.
assert (S (k*2^m) < 2^n). apply lt_even_even.
rewrite Nat.even_mul.
assert (Nat.even (2^m) = true). destruct m.
* apply Nat.lt_irrefl in H3. contradiction H3.
* rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
destruct n.
apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* apply H0.
* rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
apply Nat.mul_lt_mono_pos_r with (p := 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite <- Nat.pow_add_r.
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
rewrite Nat.sub_add. rewrite Nat.sub_add.
apply H0.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite <- Nat.pow_add_r.
rewrite Nat.mul_add_distr_r.
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
rewrite Nat.mul_1_l. rewrite Nat.sub_add. rewrite Nat.sub_add.
reflexivity.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite tm_size_power2. apply H0.
+
rewrite nth_error_app2. rewrite nth_error_app2.
rewrite tm_size_power2.
rewrite nth_error_map.
rewrite nth_error_map.
Lemma tm_step_add_small_power :
forall (n m k j : nat),
k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros H I.
(*
assert(J: nth_error (tm_step (S j)) 0 <> nth_error (tm_step (S j)) (2 ^ j)).
rewrite tm_build. rewrite nth_error_app1. rewrite nth_error_app2.
rewrite tm_size_power2. rewrite Nat.sub_diag.
rewrite tm_step_head_1. simpl. easy.
rewrite tm_size_power2. easy.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
replace (nth_error (tm_step (S j)) 0) with (nth_error (tm_step m) 0) in J.
replace (nth_error (tm_step (S j)) (2^j)) with (nth_error (tm_step m) (2^j)) in J.
*)
(* à raccourcir avec tm_step build ! *)
assert (J: nth_error (tm_step j) 0 <> nth_error (tm_step (S j)) (2^j)).
replace (2^j) with (0 + 2^j).
apply tm_step_next_range2 with (k := 0).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. reflexivity.
assert (K: nth_error (tm_step j) 0 = nth_error (tm_step m) 0).
apply tm_step_stable.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (L: nth_error (tm_step (S j)) (2^j) = nth_error (tm_step m) (2^j)).
apply tm_step_stable. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_diag_r.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply I.
rewrite K in J. rewrite L in J. clear K. clear L.
(* fin du à raccourcir *)
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
-
rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
rewrite <- tm_size_power2 in H0.
rewrite <- nth_error_None in H0.
(*
induction k. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
assert(K: nth_error (tm_step n) 0 = nth_error (tm_step m) 0).
replace (nth_error (tm_step n) 0) with (Some false).
rewrite tm_step_head_1. simpl. reflexivity.
rewrite tm_step_head_1. simpl. reflexivity.
assert(L: nth_error (tm_step n) (2^j) = nth_error (tm_step m) (2^j)).
apply tm_step_stable.
*)
Lemma tm_step_next_range2 :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
*)
Lemma greedy_power2 : forall (n m : nat),
0 < n -> n = 2^(Nat.log2 n) + m -> m < 2^(Nat.log2 n).
Proof.
intros n m. intros H I.
rewrite Nat.add_lt_mono_l with (p := 2^(Nat.log2 n)).
rewrite <- I.
replace (2^(Nat.log2 n) + 2^(Nat.log2 n)) with (2* (2^(Nat.log2 n))).
rewrite <- Nat.pow_succ_r.
apply Nat.log2_spec. apply H. apply Nat.log2_nonneg.
simpl. rewrite Nat.add_0_r. reflexivity.
Qed.
Require Import BinNat.
Require Import BinPosDef.
Require Import BinPos.
(*
PeanoNat.Nat.log2_spec_alt:
forall a : nat,
0 < a ->
exists r : nat,
a = 2 ^ PeanoNat.Nat.log2 a + r /\ 0 <= r < 2 ^ PeanoNat.Nat.log2 a
N.log2_spec_alt:
forall a : N,
(0 < a)%N ->
exists r : N, a = (2 ^ N.log2 a + r)%N /\ (0 <= r < 2 ^ N.log2 a)%N
PeanoNat.Nat.log2_shiftl:
forall a n : nat,
a <> 0 ->
PeanoNat.Nat.log2 (PeanoNat.Nat.shiftl a n) = PeanoNat.Nat.log2 a + n
*)
(* Hamming weight of a positive; argument can not be 0! *)
Fixpoint hamming_weight_positive (x: positive) :=
match x with
| xH => 1
| xO p => hamming_weight_positive p
| xI p => 1 + hamming_weight_positive p
end.
Definition hamming_weight_n (x: N) :=
match x with
| N0 => 0
| Npos x => hamming_weight_positive x
end.
Lemma hamming_weight_remove_high : forall (x : N),
(0 < x)%N -> hamming_weight_n x = S (hamming_weight_n (x - 2^(N.log2 x))).
Proof.
intros x.
N.shiftl_spec_alt:
forall a n m : N, N.testbit (N.shiftl a n) (m + n) = N.testbit a m
Lemma hamming_weight_positive_nonzero : forall (x: positive),
hamming_weight_positive x > 0.
Proof.
intros x.
induction x.
- simpl. apply Arith_prebase.gt_Sn_O_stt.
- simpl. apply IHx.
- simpl. apply Arith_prebase.gt_Sn_O_stt.
Qed.
Lemma size_double_bin : forall (x: positive),
Pos.size_nat (Pos.succ (Pos.pred_double x)) = S (Pos.size_nat x).
Proof.
intros x.
rewrite Pos.succ_pred_double.
reflexivity.
Qed.
Lemma succ_succ_pred_double_succ : forall (x: positive),
Pos.pred_double (Pos.succ x) = Pos.succ (Pos.succ (Pos.pred_double x)).
Proof.
intros x.
rewrite <- Pos.add_1_l.
rewrite Pos.add_xO_pred_double.
rewrite <- Pos.add_1_l.
rewrite <- Pos.add_1_l.
rewrite Pos.add_assoc.
reflexivity.
Qed.
Lemma size_double_bin2 : forall (x: positive),
Pos.size_nat (Pos.pred_double (Pos.succ x)) = S (Pos.size_nat x).
Proof.
intros x.
rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
reflexivity.
Qed.
Lemma size_succ_double_bin : forall (x: positive),
Pos.size_nat (Pos.succ (Pos.succ (Pos.pred_double x))) = S (Pos.size_nat x).
Proof.
intros x.
rewrite <- succ_succ_pred_double_succ. rewrite size_double_bin2.
reflexivity.
Qed.
Lemma nat_size_pos_size : forall (x: positive),
N.size_nat (N.pos x) = Pos.size_nat x.
Proof.
intros x. reflexivity.
Qed.
Lemma hamming_weight_increase : forall (x: positive),
hamming_weight_positive x~1 = S (hamming_weight_positive x).
Proof.
intros x. reflexivity.
Qed.
Fixpoint bin2power (x : positive) (k : N) :=
match x with
| xH => (2^k)%N
| xO y => bin2power y (N.succ k)
| xI y => (2^k + bin2power y (N.succ k))%N
end.
Lemma bin2power_same : forall (x : positive),
Npos x = bin2power x 0.
Proof.
intros x.
induction x.
- simpl.
(*
Fixpoint bin2power (x : positive) (k : nat) :=
match x with
| xH => 2^k
| xO y => bin2power y (S k)
| xI y => 2^k + bin2power y (S k)
end.
*)
Lemma bin2power_double : forall (x : positive) (k : N),
bin2power x~0 k = bin2power x (N.succ k).
Proof.
intros x. simpl. reflexivity.
Qed.
Lemma bin2power_double2 : forall (x : positive),
bin2power x~0 0%N = (2 * bin2power x 0)%N.
Proof.
intros x.
destruct x.
- simpl.
N.testbit_even_succ:
forall a n : N, (0 <= n)%N -> N.testbit (2 * a) (N.succ n) = N.testbit a n
simpl. reflexivity.
Qed.
Lemma bin2power_succ : forall (x : positive) (k : N),
bin2power (x~1) k = ((2^k)%N + (bin2power (x~0) k))%N.
Proof.
intros x k.
reflexivity.
Qed.
Lemma bin2power_double2 : forall (x : positive),
bin2power x 1%N = (2 * bin2power x 0)%N.
Proof.
intros x.
induction x.
- rewrite bin2power_succ. rewrite bin2power_succ. rewrite N.pow_0_r.
rewrite N.mul_add_distr_l. rewrite N.pow_1_r. rewrite N.mul_1_r.
rewrite N.add_cancel_l.
replace (bin2power x~0 0) with (bin2power x 1%N).
assert ((2 * bin2power (Pos.succ x~0) 0)%N = (2 + 2*binpower (x~0) 0)%N).
replace (x~0) with ((N.pos (N.shiftl (x) 1) 1)%N).
induction x.
- simpl. rewrite Nat.add_0_r. apply eq_S. rewrite <- plus_n_Sm.
apply eq_S.
destruct x.
+ simpl.
rewrite Pos.xI_succ_xO.
rewrite <- bin2power_double.
rewrite bin2power_double.
- rewrite bin2power_double.
assert ( I: bin2power x~1 0 = S (bin2power x~0 0) ).
{ simpl. reflexivity. } rewrite I.
assert ( J: bin2power x~1 1 = S (S (S (bin2power x~0 1) ))).
{ rewrite <- I.
simpl. rewrite Nat.add_0_r.
Qed.
Lemma bin2power_same : forall (x: positive),
bin2power x 0 = Pos.to_nat x.
Proof.
intros x.
induction x.
- simpl. rewrite <- Pos.pred_double_succ.
rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
rewrite <- Pos.xI_succ_xO.
rewrite <- bin2power_double.
assert (I: bin2power x 1 = 2 * (bin2power x 0)).
{ induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
simpl in IHx.
assert (I: bin2power x 1 = 2 * (bin2power x 0)).
{ induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
simpl in IHx.
Lemma tm_step_hamming : forall (x: N),
nth_error (tm_step (N.size_nat x)) (N.to_nat x)
= Some (odd (hamming_weight_n x)).
Proof.
intros x.
destruct x.
- reflexivity.
- induction p.
+ rewrite <- Pos.pred_double_succ.
rewrite nat_size_pos_size.
rewrite succ_succ_pred_double_succ at 1.
rewrite size_succ_double_bin.
unfold hamming_weight_n. rewrite Pos.pred_double_succ.
rewrite hamming_weight_increase. rewrite Nat.odd_succ.
rewrite <- Nat.negb_odd.
rewrite tm_build. rewrite nth_error_app1.
apply map_nth_error.
rewrite succ_succ_pred_double_succ.
simpl. rewrite Pos.succ_pred_double.
rewrite size_double_bin.
unfold N.to_nat at 2. unfold Pos.to_nat. simpl.
rewrite Pos.xI_succ_xO. transforme p~1 en Pos.succ p~0
Lemma pred_double_succ p : pred_double (succ p) = p~1.
Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
Theorem tm_step_hamming_index : forall (n : N),
nth_error (tm_step (N.to_nat n)) (N.to_nat n)
= Some (odd (hamming_weight_n n)).
Proof.
intros n.
destruct n.
- reflexivity.
- induction p. simpl.
Theorem tm_step_hamming_index : forall (n m : nat) (k j: N),
(N.to_nat k) < 2^n -> (N.to_nat j) < 2^m ->
hamming_weight_n k = hamming_weight_n j ->
nth_error (tm_step n) (N.to_nat k) = nth_error (tm_step m) (N.to_nat j).
Proof.
intros n m k j. intros H I K.
induction k.
- simpl in K. assert (j = N0). induction j. reflexivity.
rewrite <- N.succ_pos_pred.
unfold hamming_weight_n in K.
assert (L: hamming_weight_positive p > 0).
apply hamming_weight_positive_nonzero. rewrite <- K in L.
apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
rewrite H0. rewrite H0 in I.
generalize I. generalize H. apply tm_step_stable.
- induction j. simpl in K. assert (L: hamming_weight_positive p > 0).
apply hamming_weight_positive_nonzero. rewrite K in L.
apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
(* coeur de l'induction *)
induction p. simpl in K.
symmetry in K. apply Nat.neq_succ_0 in K. contradiction K.
Theorem N. succ_0_discr n : succ n <> 0.
Nat.neq_succ_0: forall n : nat, S n <> 0
Fixpoint tm_step (n: nat) : list bool :=
match n with
| 0 => false :: nil
| S n' => tm_morphism (tm_step n')
Lemma tm_step_index_split :
forall (a b n m : nat),
(* every natural number k can be written according to the following form *)
a < 2^n -> (a + 2^n * b) < 2^m
-> nth_error (tm_step m) (a + 2^n * b)
= nth_error (tm_step (S m)) (a + 2^S n * b).
Proof.
intros a b n m. intros H I.
Lemma tm_step_cancel_high_bits :
forall (k b n m : nat),
(* every natural number k can be written according to the following form *)
S k < 2^m -> k = 2^n - 1 + 2^S n * b
-> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
<-> odd n = true.
Proof.
intros k b n m. intros H I.
assert (L: 2^n - 1 < 2^n). apply Nat.sub_lt. replace (1) with (2^0) at 1.
apply Nat.pow_le_mono_r. easy.
apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
assert (M: S(2^n - 1) = 2^n). rewrite Nat.sub_1_r. apply Nat.succ_pred.
apply Nat.pow_nonzero. apply Nat.neq_succ_0.
assert (N: 2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_diag_r.
assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
<-> odd n = true).
rewrite tm_step_single_bit_index.
assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
apply tm_step_stable. apply L.
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_diag_r.
generalize H0. generalize L. apply Nat.lt_trans. rewrite <- H0.
rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
rewrite <- J. rewrite I.
destruct b.
(* case b = 0 *)
rewrite Nat.mul_0_r. rewrite Nat.add_0_r.
rewrite J. rewrite Nat.mul_0_r in I. rewrite Nat.add_0_r in I.
rewrite I in H. rewrite M.
assert (nth_error (tm_step m) (2^n-1) = nth_error (tm_step n) (2^n-1)).
generalize L. apply tm_step_stable. apply Nat.lt_succ_l. apply H.
rewrite H0. rewrite tm_step_repunit_index.
assert (nth_error (tm_step m) (2^n) = nth_error (tm_step (S n)) (2 ^ n)).
generalize N. rewrite M in H. generalize H. apply tm_step_stable.
rewrite H1. rewrite tm_step_single_bit_index.
split. intros. inversion H2. reflexivity. intros. inversion H2.
reflexivity.
(* case b > 0 *)
assert (S b = Pos.to_nat (Pos.of_nat (S b))).
destruct n.
- rewrite Nat.pow_0_r. rewrite Nat.sub_diag. rewrite plus_O_n.
rewrite Nat.pow_1_r.
rewrite Nat.pow_0_r in I. simpl in I. rewrite Nat.add_0_r in I.
induction m.
+ rewrite Nat.pow_0_r in H.
assert (K := H). rewrite Nat.lt_1_r in K.
apply Nat.neq_succ_0 in K. contradiction K.
+
induction k.
- rewrite <- I.
assert (b=0).
{ symmetry in I. rewrite Nat.eq_add_0 in I. destruct I.
apply Nat.mul_eq_0_r in H1. apply H1. apply Nat.pow_nonzero.
easy. }
rewrite H0 in I. rewrite Nat.mul_0_r in I.
rewrite Nat.add_0_r in I. rewrite <- I.
replace (2^n) with (S (2^n - 1)). rewrite <- I.
split.
intros. rewrite tm_step_head_2 at 2. rewrite tm_step_head_1. simpl.
replace (m) with (S (m-1)) in H1 at 2.
rewrite tm_step_head_2 in H1. rewrite tm_step_head_1 in H1. simpl in H1.
apply H1.
destruct m. simpl in H. apply Nat.lt_irrefl in H. contradiction H.
rewrite Nat.sub_1_r. simpl. reflexivity.
intros. rewrite tm_step_head_2 in H1 at 2.
rewrite tm_step_head_1 in H1. simpl in H1. inversion H1.
rewrite <- I.
apply eq_S in I. rewrite I at 1.
apply Nat.pred_inj. apply Nat.neq_succ_0. apply Nat.pow_nonzero.
easy. simpl. rewrite Nat.sub_1_r. reflexivity.
- apply IHk. apply Nat.lt_succ_l in H. apply H.
rewrite <- I.
split. intros. apply H1.
assert (K: S (2 ^ n - 1 + 2 ^ S n * b) = (2 ^ n + 2 ^ S n * b)).
+ rewrite Nat.sub_1_r. rewrite <- Nat.add_succ_l.
rewrite Nat.succ_pred_pos. reflexivity.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+ rewrite K. symmetry.
split. intros. symmetry.
apply tm_step_add_range2_flip_two.
(*
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
apply tm_step_repunit.
*)
Lemma tm_step_add_range2_flip_two : forall (n m j k : nat),
k < 2^n -> m < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) m
<->
nth_error (tm_step (S n+j)) (k + 2^(n+j))
= nth_error (tm_step (S n+j)) (m + 2^(n+j)).
Déclagae vers la droite de k zéros pour un Bins :
Pos.iter xO xH 3. (ici k = 3)
--> on ajoute 3 zéros à gauche
Require Import BinPosDef.
(* Autre construction de la suite, ici n est le nombre de termes *)
(* 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_rev n' in
let m := Pos.of_nat n' in
(xorb (hd true t) (odd (Pos.size_nat
match Pos.lxor m (Pos.pred m) with
| N0 => BinNums.xH
| Npos(p) => p
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.
Theorem tm_morphism_eq_bin : forall (k : nat), tm_step k = tm_bin (2^k).
Proof.
Admitted.
Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
tm_step n = l1 ++ b1 :: b2 :: l2 ->
(eqb b1 b2) =
let ind_b2 := Pos.of_nat (S (length l1)) in (* index of b2 *)
let ind_b1 := Pos.pred ind_b2 in (* index of b1 *)
even (Pos.size_nat
match Pos.lxor ind_b1 ind_b2 with
| N0 => BinNums.xH
| Npos(p) => p
end).
Proof.
intros n l1 l2 b1 b2.
destruct n.
- simpl. intros H. induction l1.
+ rewrite app_nil_l in H. discriminate.
+ destruct l1. rewrite app_nil_l in IHl1. discriminate. discriminate.
- rewrite tm_build.
Admitted.
(*
intros n l1 l2 b1 b2.
intros H.
induction l1.
- simpl. destruct n. discriminate.
rewrite app_nil_l in H. assert (I := H).
rewrite tm_step_head_2 in I. injection I.
assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
{ replace (tm_morphism (tm_step n)) with (tm_step (S n)).
rewrite H. reflexivity. reflexivity. }
(* rewrite J *) intros. rewrite <- H1. rewrite <- H2. reflexivity.
- replace (S (length (a :: l1))) with (S (S (length l1))).
destruct b1 in H.
+ destruct b2 in H.
(* Case 1: b1 = true, b2 = true (false) *)
replace (l2) with (tl (tl (tm_step (S n)))) in H.
assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
(* Case 2: b1 = true, b2 = false (false) *)
replace (l2) with (tl (tl (tm_step (S n)))) in H.
assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
+ destruct b2.
(* Case 3: b1 = false, b2 = true (TRUE) *)
discriminate.
inversion H.
discriminate tm_step_head_2.
rewrite <- tm_step_head_2 in H.
discriminate H.
discriminate tm_step_head_2.
- simpl. simpl. simpl in H.
destruct n in H. discriminate H.
replace (l2) with (tl (tl (tm_step (S n)))) in H.
specialize (H tm_step_head_2).
rewrite <- tm_step_head_2 in H.
Lemma tm_step_head_2 : forall (n : nat),
tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
*)
Reference in New Issue View Git Blame Copy Permalink