baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

This commit is contained in:
Thomas Baruchel 2023-10-30 17:43:24 +01:00
parent e748e26915
commit d44ad56bea
1 changed files with 60 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
src/subsequences.v
View File

@ -3,8 +3,6 @@ Require Import PeanoNat.
Require Import List.
Import ListNotations.
Require Import Lia.
Definition subsequence {X: Type} (l s : list X) :=
exists (l1: list X) (l2 : list (list X)),
@ -15,6 +13,12 @@ Definition subsequence2 {X: Type} (l s : list X) :=
exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)).
Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
match s with
| nil => True
| hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ subsequence3 l2 tl
end.
(*
TODO: problème, les éléments de l ne sont pas uniques ; or
il doit pouvoir y avoir des différences dans la décision de les
@ -60,6 +64,21 @@ Proof.
Qed.
Theorem subsequence3_nil_r {X: Type} : forall (l : list X), subsequence3 l nil.
Proof.
intro l. reflexivity.
Qed.
Theorem subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence3 nil (a::l).
Proof.
intros l a. unfold not. intro H. destruct H. destruct H. destruct H.
destruct x. simpl in H. apply nil_cons in H. contradiction H.
simpl in H. apply nil_cons in H. contradiction H.
Qed.
Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
subsequence l s -> subsequence (a::l) s.
Proof.
@ -80,6 +99,17 @@ Proof.
Qed.
Theorem subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
subsequence3 l s -> subsequence3 (a::l) s.
Proof.
intros l s a. intro H.
destruct s. apply subsequence3_nil_r.
destruct H. destruct H. destruct H.
exists (a::x0). exists x1. rewrite H.
split. reflexivity. assumption.
Qed.
Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
subsequence l (a::s) -> subsequence l s.
Proof.
@ -104,6 +134,18 @@ Proof.
Qed.
Theorem subsequence3_cons_r {X: Type} : forall (l s: list X) (a: X),
subsequence3 l (a::s) -> subsequence3 l s.
Proof.
intros l s a. intro H. simpl in H. destruct H. destruct H.
destruct s. apply subsequence3_nil_r. destruct H. simpl in H0.
destruct H0. destruct H0. destruct H0.
exists (x ++ a::x2). exists x3.
rewrite H. rewrite H0. split. rewrite <- app_assoc.
rewrite app_comm_cons. reflexivity. assumption.
Qed.
Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
Proof.
@ -139,6 +181,22 @@ Proof.
Qed.
Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
Proof.
intros l s a. split. intro H.
destruct H. destruct H. destruct H.
destruct x. inversion H. assumption.
destruct s. apply subsequence3_nil_r.
destruct H0. destruct H0. destruct H0.
exists (x1 ++ (a::x3)). exists x4.
inversion H. rewrite H0. rewrite <- app_assoc.
rewrite app_comm_cons. split. reflexivity.
assumption.
intro H. exists nil. exists l. split. reflexivity. assumption.
Qed.
(*
assert (forall (l s: list Type) t,
s = map snd (filter fst (combine t l))