Variable A : Type. Hypothesis dec_A : forall (x y : A), ({x=y}+{~x=y}.

L1 is a Sub-sequence for l2 which means that l1 elements appears in l2 respecting the order of appearance.

We define the predicate subseq:

Inductive subseq : list A -> list A -> Prop := | subseqnil : forall l, subseq nil l | subseqmonoton : forall a l1 l2, subseq l1 l2 -> subseq (a::l1) (a::l2)| subseqr : forall a l1 l2, subseq l1 l2 -> subseq l1 (a::l2)

1- Proof that if a list l is a subsequence of an empty list so l is empty. 2- Proof that if a list l is a subsequence of a singleton [a] so l is empty or it is [a]. 3- Proof that subseq is transitive and reflexive. 4- The notion of inclusion between two lists is defined in the following way Definition sublist (l1 l2 : list A) : Prop := forall x : A, In x l1 -> In x l2. Proof that if a list l1 is a sequence for another list l2 then l1 is included in l2. Theorem subseq_subset : forall l1 l2, subseq l1 l2 -> sublist l1 l2. Is the reciprocal true? If it is proof it, else give a counterexample. 5- The function app realize the concatenation of two lists. Proof the two theorems: Theorem subseq_app_l : forall l1 l2, subseq l1 (l1 ++ l2). Theorem subseq_app_r : forall l1 l2, subseq l2 (l1 ++ l2). 6- Is the filter function also defined in the standard library? Proof the following theorem Theorem subseq_filter : forall (P : A -> bool) l, subseq (filter P l) l. 7- We are now interested in the length of the lists and sub-sequence Proof that the length of a sub-sequence of a list l is less than or equalthe length of the list l. Proof that if a list l1 is a sub-sequence of l2 of the same length as l2 then l1 and l2 are equal (l1=l2). 8- Write the rm_duplicates function that removes duplicates from a list. Show that the result of the rm _duplicates function provides a result that is a sub-sequence of its argument.

\f