Update
This commit is contained in:
parent
4e3641242d
commit
0d4ca42439
141
thue-morse.v
141
thue-morse.v
|
@ -744,28 +744,105 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_morphism_count_occ : forall (l : list bool),
|
||||||
|
count_occ Bool.bool_dec (tm_morphism l) true
|
||||||
|
= count_occ Bool.bool_dec (tm_morphism l) false.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Require Import BinPosDef.
|
|
||||||
Require Import BinNatDef.
|
|
||||||
|
|
||||||
Lemma tm_step_double_index_pos : 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 (p~0)).
|
|
||||||
Proof.
|
Proof.
|
||||||
intro p.
|
intro l. induction l.
|
||||||
simpl.
|
- reflexivity.
|
||||||
|
- destruct a.
|
||||||
|
+ simpl. apply eq_S. assumption.
|
||||||
|
+ simpl. apply eq_S. assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma tm_morphism_app : 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_eq : forall (l1 l2 : list bool),
|
||||||
|
l1 = l2 <-> tm_morphism l1 = tm_morphism l2.
|
||||||
|
Proof.
|
||||||
|
intros l1 l2. split.
|
||||||
|
- intro H. rewrite H. reflexivity.
|
||||||
|
- generalize l2. induction l1.
|
||||||
|
+ intro l. intro H. simpl in H.
|
||||||
|
induction l. reflexivity. simpl in H. inversion H.
|
||||||
|
+ simpl. intro l0. intro H.
|
||||||
|
induction l0. simpl in H. inversion H.
|
||||||
|
simpl in H. inversion H. apply IHl1 in H3. rewrite H3.
|
||||||
|
reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
||||||
|
tm_morphism l = hd ++ tl
|
||||||
|
-> even (length hd) = true
|
||||||
|
-> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
|
||||||
|
Proof.
|
||||||
|
intros l hd tl. intros H I.
|
||||||
|
assert (J : l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
|
||||||
|
symmetry. apply firstn_skipn.
|
||||||
|
rewrite tm_morphism_eq in J.
|
||||||
|
rewrite tm_morphism_app in J.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
||||||
|
tm_morphism l = hd ++ tl -> even (length hd) = true
|
||||||
|
-> exists l2, hd = tm_morphism l2.
|
||||||
|
Proof.
|
||||||
|
intros l hd tl. intros H I.
|
||||||
|
exists (firstn (Nat.div2 (length hd)) l).
|
||||||
|
generalize I. generalize H.
|
||||||
|
induction l.
|
||||||
|
|
||||||
|
- assert (J: hd = nil). destruct hd. reflexivity.
|
||||||
|
simpl in H. inversion H.
|
||||||
|
rewrite J. reflexivity.
|
||||||
|
-
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
induction tl.
|
||||||
|
rewrite <- app_nil_end in H.
|
||||||
|
exists l. symmetry. assumption.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_step_even_prefix : forall (hd tl : list bool) (k : nat),
|
||||||
|
tm_step k = hd ++ tl -> even (length hd) = true
|
||||||
|
-> exists l, hd = tm_morphism l.
|
||||||
|
Proof.
|
||||||
|
intros hd tl k. intros H I.
|
||||||
|
destruct k.
|
||||||
|
- assert (J: hd = nil). destruct hd. reflexivity.
|
||||||
|
simpl in H. inversion H.
|
||||||
|
symmetry in H2. apply app_eq_nil in H2.
|
||||||
|
destruct H2. rewrite H0 in I. simpl in I. inversion I.
|
||||||
|
rewrite J. exists []. reflexivity.
|
||||||
|
- rewrite <- tm_step_lemma in H.
|
||||||
|
exists (firstn (Nat.div2 (length hd)) (tm_step k)).
|
||||||
|
apply app_inv_tail with (l := tl).
|
||||||
|
rewrite <- H.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem tm_step_double_index : forall (n k : nat),
|
|
||||||
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -790,6 +867,11 @@ Proof.
|
||||||
destruct H2. rewrite H0 in I. simpl in I. inversion I.
|
destruct H2. rewrite H0 in I. simpl in I. inversion I.
|
||||||
rewrite J. reflexivity.
|
rewrite J. reflexivity.
|
||||||
- rewrite <- tm_step_lemma in H.
|
- rewrite <- tm_step_lemma in H.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
generalize I. generalize H. induction hd.
|
generalize I. generalize H. induction hd.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
|
|
||||||
|
@ -807,6 +889,31 @@ PeanoNat.Nat.neq_succ_0: forall n : nat, S n <> 0
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Prouver l'énoncé du concours général
|
||||||
|
(parmi les n premiers termes avec n pairs, il y en a autant de chaque)
|
||||||
|
|
||||||
|
Prouver que si un cube existe il est de taille paire
|
||||||
|
|
||||||
|
Prouver que si un cube existe de taille k, il existe aussi un cube
|
||||||
|
de même taille précédé par un préfixe de taille pair (par décalage éventuel de 1)
|
||||||
|
|
||||||
|
Prouver que si un cube existe, de taille paire, précédé par un préfixe pair,
|
||||||
|
alors (par référence au morphisme, il existait à la génération précédente
|
||||||
|
un cube de taille moitié précédé par un préfixe pair
|
||||||
|
|
||||||
|
--> absurdité : on ne peut diviser indéfiniment par 2 et rester sur du pair
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(* TODO: supprimer head_2 *)
|
(* TODO: supprimer head_2 *)
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user