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-01-03 18:44:28 +01:00
parent cde0ed1453
commit 4f74ecf870
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
thue-morse.v
View File

@ -151,15 +151,6 @@ Proof.
+ simpl. apply eq_S. assumption.
Qed.
Lemma tm_morphism_app : forall (l1 l2 : list bool),
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
intros l1 l2.
induction l1.
- reflexivity.
- simpl. rewrite IHl1. reflexivity.
Qed.
Lemma tm_morphism_eq : forall (l1 l2 : list bool),
l1 = l2 <-> tm_morphism l1 = tm_morphism l2.
Proof.
@ -184,6 +175,15 @@ Proof.
simpl. rewrite Nat.add_0_r. reflexivity.
Qed.
Lemma tm_morphism_app : forall (l1 l2 : list bool),
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
intros l1 l2.
induction l1.
- reflexivity.
- simpl. rewrite IHl1. reflexivity.
Qed.
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
tm_morphism l = hd ++ tl
-> even (length hd) = true