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-10-31 09:07:36 +01:00
parent 23a6870a6a
commit f2e18972d0
1 changed files with 8 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/subsequences.v
View File

@ -142,21 +142,19 @@ Qed.
Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X), Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
subsequence (a::l1) (a::l2) <-> subsequence l1 l2. subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
Proof. Proof.
intros l s a. split; intro H. intros l s a. split; intro H; destruct H; destruct H; destruct H.
destruct H. destruct H. destruct H.
destruct x. destruct x0. destruct x. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
simpl in H0. inversion H0. exists l0. exists x0. simpl in H0. inversion H0. exists l0. exists x0.
inversion H. rewrite H3. split; reflexivity. inversion H. rewrite H3. split; reflexivity.
destruct x0. simpl in H0. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity. exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff. inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
rewrite app_comm_cons. reflexivity. rewrite app_comm_cons. reflexivity.
destruct H. destruct H. destruct H. exists nil. exists (x::x0). simpl.
exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity. split; [ rewrite H | rewrite H0 ]; reflexivity.
rewrite H0. reflexivity.
Qed. Qed.
@ -165,19 +163,19 @@ Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
Proof. Proof.
intros l s a. split; intro H; destruct H; destruct H. intros l s a. split; intro H; destruct H; destruct H.
destruct x. inversion H0. destruct x. inversion H0.
destruct b. exists (x). split. inversion H. rewrite H2. reflexivity. simpl in H0. destruct b. exists (x). split. inversion H. rewrite H2. reflexivity.
inversion H0. reflexivity. simpl in H0. inversion H. inversion H0. reflexivity. simpl in H0. inversion H.
assert (subsequence2 l (a::s)). exists x. split; assumption. assert (subsequence2 l (a::s)). exists x. split; assumption.
apply subsequence2_cons_r with (a := a). assumption. apply subsequence2_cons_r with (a := a). assumption.
exists (true :: x). exists (true :: x).
split. simpl. apply eq_S. assumption. rewrite H0. reflexivity. split. apply eq_S. assumption. rewrite H0. reflexivity.
Qed. Qed.
Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X), Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2. subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
Proof. Proof.
intros l s a. split. intro H. intros l s a. split; intro H.
destruct H. destruct H. destruct H. destruct H. destruct H. destruct H.
destruct x. inversion H. assumption. destruct x. inversion H. assumption.
destruct s. apply subsequence3_nil_r. destruct s. apply subsequence3_nil_r.
@ -185,7 +183,7 @@ Proof.
exists (x1 ++ (a::x3)). exists x4. exists (x1 ++ (a::x3)). exists x4.
inversion H. rewrite H0. rewrite <- app_assoc. inversion H. rewrite H0. rewrite <- app_assoc.
rewrite app_comm_cons. split. reflexivity. assumption. rewrite app_comm_cons. split. reflexivity. assumption.
intro H. exists nil. exists l. split. reflexivity. assumption. exists nil. exists l. split. reflexivity. assumption.
Qed. Qed.