InductiveRelations hints

Hint: Helper lemma for union_sorted

You may want to prove a helper lemma, sorted_cons, to construct a new sorted list by adding an element that is smaller than every element in the list.

Lemma sorted_cons : forall x l,
  sorted l ->
  (forall y, In y l -> x < y) ->
  sorted (x :: l).

With this, every time you need to prove sorted (x :: lu), you only need to prove that lu is sorted and x is smaller than any element in lu.

Hint: Helper lemma n°2 for union_sorted

You may want to prove a helper lemma, union_in, to extract information from a union:

Lemma union_in : forall l1 l2 lu x,
  union l1 l2 lu ->
  In x lu ->
  In x l1 \/ In x l2.

It will help when you need to prove x < y with x being the head of some list l1 and y is in the union of l1 and l2.

Hint: Proving union_correct

You may want to convert the goal from contains n lu = contains n l1 || contains n l2 to contains n lu = true <-> contains n l1 = true \/ contains n l2 = true.

Hint: Proving union_correct, continued

You may want to further convert the goal from contains n lu = true <-> contains n l1 = true \/ contains n l2 = true to In n lu <-> In n l1 \/ In n l2.

Hint: Helper lemma for union_correct

You may want to prove the backward version of union_in, that is,

Lemma union_in_backward : forall l1 l2 lu x,
  union l1 l2 lu ->
  In x l1 \/ In x l2 ->
  In x lu.