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 2022-11-25 12:01:21 +01:00
parent 099a6a85e9
commit e9dac82ba3
1 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
thue-morse.v
View File

@ -839,7 +839,7 @@ Proof.
apply Nat.lt_0_succ.
Qed.
Lemma tm_step_next_range' :
Lemma tm_step_next_range :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
Proof.
@ -860,7 +860,7 @@ Proof.
generalize H. apply nth_error_nth'.
rewrite H0 in IHm. symmetry in IHm.
rewrite H0. symmetry. generalize IHm.
apply tm_step_next_range'.
apply tm_step_next_range.
Qed.
Theorem tm_step_stable : forall (n m k : nat),
@ -885,7 +885,7 @@ Proof.
reflexivity.
Qed.
Lemma tm_step_next_range2'' :
Lemma tm_step_next_range2 :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Proof.
@ -902,7 +902,7 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
S k < 2^n ->
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
<->
@ -913,9 +913,9 @@ Proof.
(* Part 1: preamble *)
assert (I := H). apply Nat.lt_succ_l in I.
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
generalize I. apply tm_step_next_range2''.
generalize I. apply tm_step_next_range2.
assert (nth_error (tm_step n) (S k) <> nth_error (tm_step (S n)) (S k + 2^n)).
generalize H. apply tm_step_next_range2''.
generalize H. apply tm_step_next_range2.
assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
@ -986,13 +986,13 @@ Proof.
split.
- induction m.
+ intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
apply K.
rewrite <- tm_step_next_range2_neighbor'.
apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
rewrite <- tm_step_next_range2_neighbor.
apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
apply K.
rewrite <- tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
rewrite <- tm_step_next_range2_neighbor'. apply L.
rewrite <- tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
rewrite <- tm_step_next_range2_neighbor. apply L.
apply H. rewrite <- Nat.add_succ_l. apply K.
rewrite <- Nat.add_succ_l. apply K.
+ intros L.
@ -1007,7 +1007,7 @@ Proof.
generalize H0. generalize H. apply Nat.lt_trans.
assert (H1 := H0). apply Nat.lt_succ_l in H1.
rewrite <- tm_step_next_range2_neighbor'.
rewrite <- tm_step_next_range2_neighbor.
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
generalize H1. generalize I. apply tm_step_stable.
@ -1018,7 +1018,7 @@ Proof.
apply H0.
- induction m.
+ intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
apply tm_step_next_range2_neighbor'. apply H. apply L.
apply tm_step_next_range2_neighbor. apply H. apply L.
+ intros L.
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
@ -1030,7 +1030,7 @@ Proof.
generalize H0. generalize H. apply Nat.lt_trans.
assert (H1 := H0). apply Nat.lt_succ_l in H1.
rewrite <- tm_step_next_range2_neighbor' in L.
rewrite <- tm_step_next_range2_neighbor in L.
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
generalize H1. generalize I. apply tm_step_stable.