This commit is contained in:
Thomas Baruchel 2023-02-09 22:19:26 +01:00
parent 83e015e505
commit 2a689a4bd8
1 changed files with 222 additions and 77 deletions

View File

@ -160,83 +160,7 @@ Proof.
Qed.
(*
Lemma xxx :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
-> a = rev a \/ a = map negb (rev a).
Proof.
intros n hd a tl. intros H I.
destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
rewrite app_length in H0. rewrite Nat.add_comm in H0.
destruct a. inversion I. rewrite <- Nat.add_assoc in H0.
rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
assert (exists k j, length a = S (Nat.double k) * 2^j).
apply trailing_zeros; assumption. destruct H0. destruct H0.
assert (x = 0 \/ x = 1). generalize H0. generalize H.
apply tm_step_square_size.
generalize dependent n. generalize dependent hd. generalize dependent a.
generalize dependent tl. generalize dependent x.
induction x0; intros x K tl a J I hd n H.
- destruct K; rewrite H0 in I; destruct a.
inversion J. destruct a. left. reflexivity. inversion I.
inversion I. destruct a. inversion I. destruct a. inversion I.
destruct a.
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e. left. reflexivity.
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
apply tm_step_consecutive_identical' in H. inversion H.
rewrite <- app_assoc. reflexivity.
assert (b = b0). destruct b; destruct b0; destruct b1;
reflexivity || contradiction n0 || contradiction n1; reflexivity.
rewrite H1 in H.
replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
inversion I.
- assert (even (length a) = true).
rewrite Nat.mul_comm in I. rewrite Nat.pow_succ_r in I. rewrite I.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l.
assert (even (length (hd ++ a)) = true).
generalize J. generalize H. apply tm_step_square_pos.
assert (even (length hd) = true).
rewrite app_length in H1. rewrite Nat.even_add in H1.
rewrite H0 in H1. destruct (Nat.even (length hd)). reflexivity.
inversion H1.
(se débarrasser du S x0 en I)
generalize H. generalize n. generalize hd. generalize I. generalize J.
apply IHx0.
Lemma tm_step_morphism4 :
forall (n : nat) (hd a b tl : list bool),
tm_step (S n) = hd ++ a ++ b ++ tl
-> even (length hd) = true
-> even (length a) = true
-> even (length b) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
*)
Lemma xxx :
Lemma tm_step_square_even_rev :
forall (j n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
@ -575,6 +499,227 @@ Proof.
Qed.
Lemma tm_step_square_odd_rev :
forall (j n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j))
-> a = map negb (rev a).
Proof.
intros j n hd a tl. intros H I.
assert (even (length a) = true).
destruct I; rewrite H0; rewrite Nat.pow_succ_r.
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
assert (0 < length a). destruct I; rewrite H1.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.mul_pos_pos. lia.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (even (length (hd ++ a)) = true). generalize H1. generalize H.
apply tm_step_square_pos.
assert (even (length hd) = true). rewrite app_length in H2.
rewrite Nat.even_add in H2. rewrite H0 in H2.
destruct (even (length hd)). reflexivity. inversion H2.
assert (0 < n).
assert (length (tm_step n) = length (tm_step n)). reflexivity.
rewrite H in H4 at 2. rewrite app_length in H4.
rewrite Nat.add_comm in H4.
destruct a. inversion H1. simpl in H4. rewrite app_length in H4.
simpl in H4. rewrite Nat.add_succ_r in H4.
destruct n. inversion H4. lia.
destruct n. inversion H4.
assert(
tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n))).
generalize H0. generalize H0. generalize H3. generalize H.
apply tm_step_morphism4.
pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)).
pose (a' := firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n))).
pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n)).
fold hd' in H5. fold a' in H5. fold tl' in H5.
assert (length hd' = Nat.div2 (length hd)). unfold hd'.
rewrite firstn_length_le. reflexivity.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.
assert (length hd = length (tm_morphism hd')).
rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
assert (length a' = Nat.div2 (length a)). unfold a'.
rewrite firstn_length_le. reflexivity. rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (length a = length (tm_morphism a')).
rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite H in H5. rewrite tm_morphism_app in H5.
assert (hd = tm_morphism hd'). generalize H7. generalize H5.
apply app_eq_length_head. rewrite <- H10 in H5.
apply app_inv_head in H5. rewrite tm_morphism_app in H5.
assert (a = tm_morphism a'). generalize H9. generalize H5.
apply app_eq_length_head. rewrite <- H11 in H5.
apply app_inv_head in H5. rewrite tm_morphism_app in H5.
assert (length a = length (tm_morphism (
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n))))).
rewrite tm_morphism_length. rewrite firstn_length_le.
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_assoc.
rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite app_length. lia. apply Nat.le_refl.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (a = tm_morphism (
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize H12. generalize H5. apply app_eq_length_head.
rewrite <- H13 in H5. apply app_inv_head in H5.
assert (H' := H).
rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'.
rewrite <- tm_morphism_app in H'.
rewrite <- tm_morphism_app in H'.
rewrite <- tm_morphism_app in H'.
rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'.
assert (length a = 2 * length a'). rewrite tm_morphism_length in H9.
assumption.
assert (length a' = 2^(Nat.double j) \/ length a' = 3 * 2^(Nat.double j)).
destruct I; [left | right]; rewrite <- Nat.mul_cancel_l with (p := 2).
rewrite <- tm_morphism_length. rewrite <- H11.
rewrite <- Nat.pow_succ_r. assumption. lia. lia.
rewrite <- tm_morphism_length. rewrite <- H11.
rewrite Nat.mul_assoc. replace (2*3) with (3*2).
rewrite <- Nat.mul_assoc.
rewrite <- Nat.pow_succ_r. assumption. lia. lia. easy.
assert (Z := H11).
assert (a' = rev a'). generalize H15. generalize H'.
apply tm_step_square_even_rev. rewrite H16 in H11.
rewrite <- tm_morphism_rev2 in H11. rewrite <- Z in H11.
assumption.
(*
Lemma xxx :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
-> a = rev a \/ a = map negb (rev a).
Proof.
intros n hd a tl. intros H I.
destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
rewrite app_length in H0. rewrite Nat.add_comm in H0.
destruct a. inversion I. rewrite <- Nat.add_assoc in H0.
rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
assert (exists k j, length a = S (Nat.double k) * 2^j).
apply trailing_zeros; assumption. destruct H0. destruct H0.
assert (x = 0 \/ x = 1). generalize H0. generalize H.
apply tm_step_square_size.
generalize dependent n. generalize dependent hd. generalize dependent a.
generalize dependent tl. generalize dependent x.
induction x0; intros x K tl a J I hd n H.
- destruct K; rewrite H0 in I; destruct a.
inversion J. destruct a. left. reflexivity. inversion I.
inversion I. destruct a. inversion I. destruct a. inversion I.
destruct a.
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e. left. reflexivity.
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
apply tm_step_consecutive_identical' in H. inversion H.
rewrite <- app_assoc. reflexivity.
assert (b = b0). destruct b; destruct b0; destruct b1;
reflexivity || contradiction n0 || contradiction n1; reflexivity.
rewrite H1 in H.
replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
inversion I.
- assert (even (length a) = true).
rewrite Nat.mul_comm in I. rewrite Nat.pow_succ_r in I. rewrite I.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l.
assert (even (length (hd ++ a)) = true).
generalize J. generalize H. apply tm_step_square_pos.
assert (even (length hd) = true).
rewrite app_length in H1. rewrite Nat.even_add in H1.
rewrite H0 in H1. destruct (Nat.even (length hd)). reflexivity.
inversion H1.
(se débarrasser du S x0 en I)
generalize H. generalize n. generalize hd. generalize I. generalize J.
apply IHx0.
Lemma tm_step_morphism4 :
forall (n : nat) (hd a b tl : list bool),
tm_step (S n) = hd ++ a ++ b ++ tl
-> even (length hd) = true
-> even (length a) = true
-> even (length b) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
*)