Update
This commit is contained in:
Thomas Baruchel
parent
4ba41ee7ef
commit
f19b363b83
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in New Issue