Hello,

Please see attached screenshot. I am trying to solve Exercise: 4 stars, advanced (filter_challenge).

I have 2 questions.

Question 1.

They suggest this example:

[1;4;6;2;3]

is an in-order merge of

[1;6;2] and [4;3].

I am not able to figure out what is the algorithm of merging? why 2 is in front of 3 in the result list?

Question 2.

Is that correct : Inductive Relation should be defined on nat, not on the abstract type X as they ask in theorems verbal specification. It is not possible to do it for X, type should be precise, how can we check relation on elements of lists if type is abstract?

My attempt to solve exercise:

(this definition of le was given previously in chapterâ€¦)

```
Inductive le : nat â†’ nat â†’ Prop :=
| le_n n : le n n
| le_S n m (H : le n m) : le n (S m).
Inductive mergeTLists : list nat -> list nat -> list nat -> Prop :=
| EmptFirst xs : mergeTLists [] xs xs
| EmptSec xs : mergeTLists xs [] xs
| TwoListsL (x y : nat) (H0 : le x y) (xs ys zs : list nat)
(H : mergeTLists xs ys zs) : mergeTLists (x :: xs) (y :: ys) (x :: y :: zs)
| TwoListsR (x y : nat) (H0 : le y x) (xs ys zs : list nat)
(H : mergeTLists xs ys zs) : mergeTLists (x :: xs) (y :: ys) (y :: x :: zs).
Theorem filter_matches_abstract_spec : forall {X : Type} (test : X -> bool) (l l1 l2 : list X),
mergeTLists l1 l2 l ->
filter test l1 = l1 ->
filter test l2 = [] ->
filter test l = l1.
```

Sorry for my English, itâ€™s my second language.