Merging 2 lists : Inductive Relation

Using Coq
1

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?

filter_challenge
filter_challenge1920Ă—1080 293 KB

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.

2

Don’t think of it as an “algorithm”. The property just says that there is some way to interleave [1;6;2] and [4;3] to get the list [1;4;6;2;3], but there is no constraint on the interleaving other than the fact that the elements in the merged list must appear in the same order as in the separated lists.

If you can line up the lists like this, then you have an in-order merge:

1 4 6 2 3
---------  is an in-order merge of
1   6 2
  4     3

The definitions should be parameterized by X. They can be specialized to nat for examples, but there is nothing about the exercise that fundamentally relies on nat.

1 Like
3

Thank you for your answer.

4

Solved it finally… so happy.