diff --git a/src/thue_morse.v b/src/thue_morse.v index c9f29de..48a0f12 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -545,11 +545,11 @@ Proof. intros n hd a tl. intros H I J. assert (M: 1 < length (tm_step n)). rewrite H. rewrite app_length. rewrite app_length. - assert (0 <= length hd). apply le_0_n. + assert (0 <= length hd). apply Nat.le_0_l. assert (2 <= length a + length tl). rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. destruct a. inversion I. - destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply le_0_n. - apply le_0_n. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l. + destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply Nat.le_0_l. + apply Nat.le_0_l. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l. rewrite plus_n_Sm. apply Nat.add_le_mono; assumption. rewrite tm_size_power2 in M. rewrite Nat.pow_lt_mono_r_iff with (a := 2). simpl. assumption. diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 6f4c1b5..d4709ec 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -726,7 +726,7 @@ Proof. rewrite H7. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite Nat.add_0_l. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l. - apply le_0_n. apply le_n. easy. + apply Nat.le_0_l. apply le_n. easy. rewrite <- Nat.Even_double in H7. rewrite <- Nat.Even_double in H7. rewrite Nat.add_assoc in H7. @@ -1179,7 +1179,7 @@ Proof. rewrite <- tm_size_power2. rewrite M0. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. split. @@ -1203,7 +1203,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1238,7 +1238,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1259,7 +1259,7 @@ Proof. rewrite <- tm_size_power2. rewrite L0. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. split. @@ -1283,7 +1283,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1310,7 +1310,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1325,7 +1325,7 @@ Proof. rewrite <- tm_size_power2. rewrite L0. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. assert (even (length (firstn (Nat.div2 (length hd')) (tm_step n))) = false). @@ -1347,7 +1347,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1364,7 +1364,7 @@ Proof. rewrite <- tm_size_power2. rewrite M0. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. assert (even (length (firstn (Nat.div2 (length hd'')) (tm_step n))) = false). @@ -1386,7 +1386,7 @@ Proof. rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. reflexivity. - apply le_0_n. + apply Nat.le_0_l. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. @@ -1489,7 +1489,7 @@ Proof. rewrite tm_step_stable with (k := S (2*0)) (m := n) in H1. rewrite H in H1. simpl in H1. contradiction H1. reflexivity. rewrite Nat.pow_succ_r. replace (S (2*0)) with (1*1). apply Nat.mul_lt_mono. apply Nat.lt_1_2. - assumption. reflexivity. apply le_0_n. assumption. left. assumption. + assumption. reflexivity. apply Nat.le_0_l. assumption. left. assumption. destruct a. assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec. @@ -1505,7 +1505,7 @@ Proof. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. rewrite Nat.pow_succ_r. apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_succ. - apply Nat.lt_succ_l. assumption. apply le_0_n. assumption. + apply Nat.lt_succ_l. assumption. apply Nat.le_0_l. assumption. left. assumption. destruct a. @@ -1523,12 +1523,12 @@ Proof. apply Nat.lt_succ_l. replace (S (S (2*2))) with (2*3). apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_2. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. reflexivity. - apply le_0_n. assumption. left. assumption. + apply Nat.le_0_l. assumption. left. assumption. pose (a' := b::b0::b1::b2::a). fold a' in H. assert (J : 4 <= length a'). unfold a'. simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. - rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply le_0_n. + rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l. assert (K: {odd (length a') = true} + {~ odd (length a') = true}). apply bool_dec. destruct K. @@ -1556,7 +1556,7 @@ Proof. rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. rewrite H. rewrite app_assoc. rewrite app_length. rewrite <- app_length. apply Nat.le_add_r. - apply le_0_n. replace (length a' + length a') with (2 * length a') in H0. + apply Nat.le_0_l. replace (length a' + length a') with (2 * length a') in H0. rewrite <- Nat.mul_le_mono_pos_l in H0. assert (length a' = length diff --git a/src/thue_morse3.v b/src/thue_morse3.v index f322b24..9013980 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -147,7 +147,7 @@ Proof. rewrite <- firstn_firstn. rewrite app_assoc. rewrite firstn_skipn. rewrite firstn_skipn. reflexivity. apply Nat.min_l. rewrite <- Nat.add_0_r at 1. - apply Nat.add_le_mono_l. apply le_0_n. + apply Nat.add_le_mono_l. apply Nat.le_0_l. assert (Nat.Even (length a - 5)). apply Nat.EvenT_Even. apply Nat.even_EvenT. rewrite Nat.even_sub. @@ -186,13 +186,13 @@ Proof. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl. rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl. assumption. simpl. apply le_n_S. apply le_n_S. apply le_n_S. apply le_n_S. - apply le_n_S. apply le_0_n. apply Nat.lt_le_incl. assumption. + apply le_n_S. apply Nat.le_0_l. apply Nat.lt_le_incl. assumption. assumption. assumption. easy. unfold t. rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. simpl. rewrite Nat.add_0_r. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. - apply Nat.le_sub_l. apply le_0_n. assumption. apply Nat.lt_0_2. + apply Nat.le_sub_l. apply Nat.le_0_l. assumption. apply Nat.lt_0_2. assert (v = rev v). rewrite H2 in I. rewrite rev_app_distr in I. rewrite rev_app_distr in I. @@ -276,7 +276,7 @@ Proof. apply Nat.add_lt_mono_l. rewrite app_length. rewrite <- Nat.add_0_r at 1. apply Nat.add_lt_mono_l. rewrite app_length. rewrite rev_length. - assert (0 <= length tl). apply le_0_n. rewrite <- Nat.add_0_r at 1. + assert (0 <= length tl). apply Nat.le_0_l. rewrite <- Nat.add_0_r at 1. apply Nat.add_lt_le_mono; assumption. Qed. @@ -353,7 +353,7 @@ Proof. assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl) <= length hd + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)). - apply Nat.add_le_mono. apply le_0_n. apply Nat.le_refl. + apply Nat.add_le_mono. apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J. rewrite tm_size_power2 in J. destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1. @@ -936,7 +936,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. - simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity. + simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity. rewrite Y''. rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. @@ -946,7 +946,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. - simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity. + simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity. apply Nat.lt_le_incl. assumption. rewrite <- tm_step_repeating_patterns in H10. inversion H10. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. @@ -984,7 +984,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.mul_le_mono_l with (p := 8) in H9. - rewrite Nat.mul_1_r in H9. assumption. apply le_0_n. + rewrite Nat.mul_1_r in H9. assumption. apply Nat.le_0_l. assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.mul_le_mono_l with (p := 8) in H9. rewrite Nat.mul_1_r in H9. assumption. @@ -1009,19 +1009,19 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity. apply Nat.le_refl. rewrite <- Nat.add_0_r at 1. - rewrite <- Nat.add_le_mono_l. apply le_0_n. apply Nat.le_refl. + rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. apply Nat.le_refl. rewrite <- Nat.add_0_r at 1. - rewrite <- Nat.add_le_mono_l. apply le_0_n. reflexivity. + rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. reflexivity. rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. - rewrite <- Nat.add_le_mono_l. apply le_0_n. + rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. - rewrite <- Nat.add_le_mono_l. apply le_0_n. + rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. apply Nat.lt_le_incl. assumption. rewrite <- tm_step_repeating_patterns in H10. inversion H10. @@ -1433,7 +1433,7 @@ Proof. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc. rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc. - apply Nat.mod_mul. easy. apply le_0_n. apply le_0_n. + apply Nat.mod_mul. easy. apply Nat.le_0_l. apply Nat.le_0_l. rewrite app_length in L. rewrite <- Nat.add_mod_idemp_l in L. rewrite K in L. @@ -1839,7 +1839,7 @@ Proof. rewrite Nat.mul_assoc in J. replace (2*2) with 4 in J. rewrite J. rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. + easy. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. assert (length (hd ++ a) mod 4 = 0). assert (W' := W). @@ -1865,7 +1865,7 @@ Proof. rewrite <- pred_Sn. rewrite Nat.double_S. rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity. rewrite Nat.neq_0_lt_0. rewrite Nat.double_S. - apply Nat.lt_0_succ. apply le_0_n. apply le_0_n. + apply Nat.lt_0_succ. apply Nat.le_0_l. apply Nat.le_0_l. reflexivity. apply Nat.pow_nonzero. easy. easy. easy. @@ -1885,7 +1885,7 @@ Proof. rewrite <- pred_Sn. rewrite Nat.double_S. rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity. rewrite Nat.neq_0_lt_0. rewrite Nat.double_S. - apply Nat.lt_0_succ. apply le_0_n. apply le_0_n. + apply Nat.lt_0_succ. apply Nat.le_0_l. apply Nat.le_0_l. reflexivity. apply Nat.pow_nonzero. easy. easy. easy. @@ -1977,7 +1977,7 @@ Proof. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. - apply le_0_n. + apply Nat.le_0_l. Qed. @@ -2021,7 +2021,7 @@ Proof. rewrite Nat.mul_assoc in J. replace (2*2) with 4 in J. rewrite J. rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. + easy. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. assert ( hd = tm_morphism (tm_morphism (firstn (length hd / 4) @@ -2072,7 +2072,7 @@ Proof. rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N. rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity. - apply le_0_n. apply le_0_n. + apply Nat.le_0_l. apply Nat.le_0_l. assert (Y': 6 < length a'). rewrite N in E1. @@ -2085,7 +2085,7 @@ Proof. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. generalize E1. generalize H0. apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity. - apply le_0_n. apply le_0_n. + apply Nat.le_0_l. apply Nat.le_0_l. apply IHm with (n := n) (tl := tl'). assumption. assumption. assumption. @@ -2433,7 +2433,7 @@ Proof. rewrite firstn_length_le. apply Nat.sub_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ. rewrite <- Nat.sub_0_r. - apply Nat.sub_le_mono_l. apply le_0_n. + apply Nat.sub_le_mono_l. apply Nat.le_0_l. rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. @@ -2512,7 +2512,7 @@ Proof. rewrite H0. rewrite Nat.add_0_r. reflexivity. rewrite <- pred_Sn. rewrite Nat.double_S. reflexivity. - apply le_0_n. apply le_0_n. reflexivity. + apply Nat.le_0_l. apply Nat.le_0_l. reflexivity. apply Nat.pow_nonzero. easy. easy. easy. - intro P. @@ -2529,7 +2529,7 @@ Proof. rewrite H0. rewrite Nat.add_0_r. reflexivity. rewrite <- pred_Sn. rewrite Nat.double_S. reflexivity. - apply le_0_n. apply le_0_n. reflexivity. + apply Nat.le_0_l. apply Nat.le_0_l. reflexivity. apply Nat.pow_nonzero. easy. easy. easy. Qed. @@ -2554,7 +2554,7 @@ Proof. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. - apply le_0_n. + apply Nat.le_0_l. Qed. @@ -2594,7 +2594,7 @@ Proof. rewrite Nat.mul_assoc in J. replace (2*2) with 4 in J. rewrite J. rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. + easy. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. assert ( hd = tm_morphism (tm_morphism (firstn (length hd / 4) @@ -2645,7 +2645,7 @@ Proof. rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N. rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity. - apply le_0_n. apply le_0_n. + apply Nat.le_0_l. apply Nat.le_0_l. assert (Y': 6 < length a'). rewrite N in E1. @@ -2658,7 +2658,7 @@ Proof. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. generalize E1. generalize H0. apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity. - apply le_0_n. apply le_0_n. + apply Nat.le_0_l. apply Nat.le_0_l. apply IHm with (n := n) (tl := tl'). assumption. assumption. assumption. diff --git a/src/thue_morse4.v b/src/thue_morse4.v index 9cb2c54..ce73732 100644 --- a/src/thue_morse4.v +++ b/src/thue_morse4.v @@ -88,7 +88,7 @@ Proof. rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity. apply Nat.pow_nonzero. easy. rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity. - apply le_0_n. apply Nat.mul_1_r. apply Nat.le_sub_l. + apply Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l. assert ( skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m)