Update
This commit is contained in:
parent
f7d32e6a75
commit
75e2fb9acd
|
@ -15,73 +15,47 @@ Import ListNotations.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
Lemma tm_step_consecutive_identical :
|
Lemma tm_step_consecutive_identical :
|
||||||
|
forall (n : nat) (hd a tl : list bool) (b : bool),
|
||||||
|
tm_step n = hd ++ (b::b::nil) ++ tl
|
||||||
|
-> odd (length hd) = true.
|
||||||
|
Proof.
|
||||||
|
intros n hd a tl b. intro H.
|
||||||
|
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
|
||||||
|
apply bool_dec. destruct J.
|
||||||
|
- rewrite <- Nat.negb_even. rewrite e. reflexivity.
|
||||||
|
- apply not_false_is_true in n0.
|
||||||
|
assert (K: count_occ Bool.bool_dec hd true
|
||||||
|
= count_occ Bool.bool_dec hd false).
|
||||||
|
generalize n0. generalize H. apply tm_step_count_occ.
|
||||||
|
assert (L: count_occ Bool.bool_dec (hd ++ [b;b]) true
|
||||||
|
= count_occ Bool.bool_dec (hd ++ [b;b]) false).
|
||||||
|
assert (even (length (hd ++ [b;b])) = true).
|
||||||
|
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
||||||
|
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
||||||
|
generalize H0. rewrite app_assoc in H. generalize H.
|
||||||
|
apply tm_step_count_occ.
|
||||||
|
rewrite count_occ_app in L. rewrite count_occ_app in L.
|
||||||
|
rewrite K in L. rewrite Nat.add_cancel_l in L.
|
||||||
|
destruct b. simpl in L. inversion L. simpl in L. inversion L.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_step_consecutive_identical' :
|
||||||
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
|
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
|
||||||
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
|
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
|
||||||
-> even (length a) = true.
|
-> even (length a) = true.
|
||||||
Proof.
|
Proof.
|
||||||
intros n hd a tl b1 b2. intros H.
|
intros n hd a tl b1 b2. intros H.
|
||||||
assert (I: even (length hd) = false).
|
assert (Nat.odd (length hd) = true).
|
||||||
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
|
generalize H. apply tm_step_consecutive_identical. apply hd.
|
||||||
apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
|
rewrite app_assoc in H. rewrite app_assoc in H.
|
||||||
assert (K: count_occ Bool.bool_dec hd true
|
assert (Nat.odd (length ((hd ++ [b1;b1])++a)) = true).
|
||||||
= count_occ Bool.bool_dec hd false).
|
generalize H. apply tm_step_consecutive_identical. apply hd.
|
||||||
generalize n0. generalize H. apply tm_step_count_occ.
|
rewrite app_length in H1. rewrite Nat.odd_add in H1.
|
||||||
rewrite app_assoc in H.
|
rewrite app_length in H1. rewrite Nat.odd_add in H1. rewrite H0 in H1.
|
||||||
assert (L: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
|
replace (Nat.odd (length a)) with (negb (Nat.even (length a))) in H1.
|
||||||
= count_occ Bool.bool_dec (hd ++ [b1;b1]) false).
|
destruct (even (length a)). reflexivity. inversion H1.
|
||||||
assert (even (length (hd ++ [b1;b1])) = true).
|
reflexivity.
|
||||||
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
|
||||||
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
||||||
generalize H0. generalize H. apply tm_step_count_occ.
|
|
||||||
rewrite count_occ_app in L. rewrite count_occ_app in L.
|
|
||||||
rewrite K in L. rewrite Nat.add_cancel_l in L.
|
|
||||||
destruct b1. simpl in L. inversion L. simpl in L. inversion L.
|
|
||||||
|
|
||||||
assert (J: {even (length (hd ++ [b1;b1] ++ a))
|
|
||||||
= false} + { ~ (even (length (hd ++ [b1;b1] ++ a))) = false}).
|
|
||||||
apply bool_dec. destruct J.
|
|
||||||
|
|
||||||
rewrite app_length in e. rewrite app_length in e.
|
|
||||||
rewrite Nat.add_assoc in e. rewrite Nat.add_shuffle0 in e.
|
|
||||||
rewrite Nat.even_add_even in e. rewrite Nat.even_add in e.
|
|
||||||
rewrite I in e. destruct (Nat.even (length a)). reflexivity.
|
|
||||||
simpl in e. inversion e. simpl.
|
|
||||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
||||||
|
|
||||||
apply not_false_is_true in n0.
|
|
||||||
assert (K: even (length (hd ++ [b1;b1] ++ a ++ [b2;b2])) = true).
|
|
||||||
replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
|
|
||||||
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]).
|
|
||||||
rewrite app_length. rewrite Nat.even_add.
|
|
||||||
rewrite n0. reflexivity.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. reflexivity.
|
|
||||||
|
|
||||||
assert (N: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) true
|
|
||||||
= count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) false).
|
|
||||||
replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
|
|
||||||
with ((hd ++ [b1;b1] ++ a ++ [b2;b2]) ++ tl) in H.
|
|
||||||
generalize K. generalize H. apply tm_step_count_occ.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. reflexivity.
|
|
||||||
|
|
||||||
assert (M: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) true
|
|
||||||
= count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) false).
|
|
||||||
replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
|
|
||||||
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2] ++ tl) in H.
|
|
||||||
generalize n0. generalize H. apply tm_step_count_occ.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. reflexivity.
|
|
||||||
|
|
||||||
replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
|
|
||||||
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]) in N.
|
|
||||||
rewrite count_occ_app in N. symmetry in N.
|
|
||||||
rewrite count_occ_app in N. rewrite M in N.
|
|
||||||
rewrite Nat.add_cancel_l in N.
|
|
||||||
destruct b2. simpl in N. inversion N. simpl in N. inversion N.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. reflexivity.
|
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
@ -103,7 +77,7 @@ Proof.
|
||||||
|
|
||||||
replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
|
replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
|
||||||
with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
|
with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
|
||||||
apply tm_step_consecutive_identical in H.
|
apply tm_step_consecutive_identical' in H.
|
||||||
|
|
||||||
assert (J: even (length (x0 ++ x)) = false).
|
assert (J: even (length (x0 ++ x)) = false).
|
||||||
rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
|
rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
|
||||||
|
@ -450,29 +424,29 @@ Proof.
|
||||||
- destruct b; destruct b0; destruct b1.
|
- destruct b; destruct b0; destruct b1.
|
||||||
+ replace ([true;true;true] ++ [true;true;true] ++ tl)
|
+ replace ([true;true;true] ++ [true;true;true] ++ tl)
|
||||||
with ([true;true] ++ [true] ++ [true;true] ++ [true] ++ tl) in H.
|
with ([true;true] ++ [true] ++ [true;true] ++ [true] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
+ replace ([true;true;false] ++ [true;true;false] ++ tl)
|
+ replace ([true;true;false] ++ [true;true;false] ++ tl)
|
||||||
with ([true;true] ++ [false] ++ [true;true] ++ [false] ++ tl) in H.
|
with ([true;true] ++ [false] ++ [true;true] ++ [false] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
+ left. reflexivity.
|
+ left. reflexivity.
|
||||||
+ replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl)
|
+ replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl)
|
||||||
with ((hd ++ [true]) ++ [false; false] ++ [true] ++ [false;false] ++ tl) in H.
|
with ((hd ++ [true]) ++ [false; false] ++ [true] ++ [false;false] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
rewrite <- app_assoc. reflexivity.
|
rewrite <- app_assoc. reflexivity.
|
||||||
+ replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl)
|
+ replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl)
|
||||||
with ((hd ++ [false]) ++ [true; true] ++ [false] ++ [true;true] ++ tl) in H.
|
with ((hd ++ [false]) ++ [true; true] ++ [false] ++ [true;true] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
rewrite <- app_assoc. reflexivity.
|
rewrite <- app_assoc. reflexivity.
|
||||||
+ right. reflexivity.
|
+ right. reflexivity.
|
||||||
+ replace ([false;false;true] ++ [false;false;true] ++ tl)
|
+ replace ([false;false;true] ++ [false;false;true] ++ tl)
|
||||||
with ([false;false] ++ [true] ++ [false;false] ++ [true] ++ tl) in H.
|
with ([false;false] ++ [true] ++ [false;false] ++ [true] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
+ replace ([false;false;false] ++ [false;false;false] ++ tl)
|
+ replace ([false;false;false] ++ [false;false;false] ++ tl)
|
||||||
with ([false;false] ++ [false] ++ [false;false] ++ [false] ++ tl) in H.
|
with ([false;false] ++ [false] ++ [false;false] ++ [false] ++ tl) in H.
|
||||||
apply tm_step_consecutive_identical in H. inversion H.
|
apply tm_step_consecutive_identical' in H. inversion H.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
- inversion I.
|
- inversion I.
|
||||||
- assert (K: count_occ Bool.bool_dec hd true
|
- assert (K: count_occ Bool.bool_dec hd true
|
||||||
|
|
Loading…
Reference in New Issue
Block a user