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 2023-02-01 21:02:44 +01:00
parent 5253fb526d
commit 9aa2a2c6cd
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/thue_morse3.v
View File

@ -1819,7 +1819,7 @@ Proof.
Qed. Qed.
Lemma tm_step_palindromic_power2_even : Lemma tm_step_palindromic_power2_even_alpha :
forall (m n : nat) (hd a tl : list bool), forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl tm_step n = hd ++ a ++ (rev a) ++ tl
-> 6 < length a -> 6 < length a
@ -1892,7 +1892,7 @@ Proof.
Qed. Qed.
Lemma tm_step_palindromic_power2_even' : Lemma tm_step_palindromic_power2_even_beta :
forall (m n : nat) (hd a tl : list bool), forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl tm_step n = hd ++ a ++ (rev a) ++ tl
-> 6 < length a -> 6 < length a
@ -1981,7 +1981,7 @@ Proof.
Qed. Qed.
Theorem xxx : Theorem tm_step_palindromic_power2_even :
forall (m n : nat) (hd a tl : list bool), forall (m n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl tm_step n = hd ++ a ++ (rev a) ++ tl
-> 6 < length a -> 6 < length a
@ -1992,7 +1992,7 @@ Proof.
assert (E: length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 assert (E: length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
\/ 2^6 <= length a). \/ 2^6 <= length a).
generalize J. generalize I. generalize H. generalize J. generalize I. generalize H.
apply tm_step_palindromic_power2_even'. apply tm_step_palindromic_power2_even_beta.
destruct m. rewrite J in I. inversion I. inversion H1. destruct m. rewrite J in I. inversion I. inversion H1.
destruct m. rewrite J in I. inversion I. inversion H1. destruct m. rewrite J in I. inversion I. inversion H1.
@ -2011,7 +2011,7 @@ Proof.
contradiction H8. apply Nat.lt_1_2. contradiction H8. apply Nat.lt_1_2.
- intros n tl a I J hd H E. assert (E' := E). - intros n tl a I J hd H E. assert (E' := E).
destruct E as [E0 | E1]. assumption. destruct E as [E0 | E1]. assumption.
rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl). rewrite tm_step_palindromic_power2_even_alpha with (n := n) (tl := tl).
rewrite <- pred_Sn. rewrite <- pred_Sn.
@ -2090,7 +2090,7 @@ Proof.
apply IHm with (n := n) (tl := tl'). apply IHm with (n := n) (tl := tl').
assumption. assumption. assumption. assumption. assumption. assumption.
generalize Y. generalize Y'. generalize H. generalize Y. generalize Y'. generalize H.
apply tm_step_palindromic_power2_even'. apply tm_step_palindromic_power2_even_beta.
easy. reflexivity. reflexivity. easy. reflexivity. reflexivity.
assumption. assumption. assumption. assumption. assumption. assumption.
Qed. Qed.