Functional induction with remember

Using Coq
1

Hello, I am playing with a formalization mergesort based on the following merge function:

Definition len (p: list nat * list nat) :=
   length (fst p) + length (snd p).

Function merge (p: list nat * list nat) {measure len p} :=
match p with
  | (nil, l2) => l2
  | (l1, nil) => l1
  | ((hd1 :: tl1) as l1, (hd2 :: tl2) as l2) =>
if hd1 <=? hd2 then hd1 :: merge (tl1, l2)
      else hd2 :: merge (l1, tl2)
   end.

Now I want to prove that merge outputs a sorted list, if it receives a pair of sorted lists as arguments. I can write this property in two different ways. The first way is:

Theorem merge_sorts: forall p, sorted_pair_lst p -> sorted (merge p).

where

Definition sorted_pair_lst (p: list nat * list nat) := sorted (fst p) /\ sorted (snd p).

and everything works fine. I managed to prove it using functional induction (merge p).

But I could also write the same property with explicit reference to the elements of the pair:

Theorem merge_sorts: forall l1 l2, sorted l1 -> sorted l2 -> sorted(merge(l1,l2)).

But now I am no longer able to prove it using functional induction (merge (l1,l2)). In fact, the non-recursive cases generates a new variable l0 without any relation with l1 and l2:

4 goals (ID 1671)
  
  l1, l2, l0 : list nat
  ============================
  sorted l1 -> sorted l2 -> sorted l0

goal 2 (ID 1674) is:
 sorted l1 -> sorted l2 -> sorted l0
goal 3 (ID 1677) is:
 sorted l1 -> sorted l2 -> sorted (hd1 :: merge (tl1, hd2 :: tl2))
goal 4 (ID 1680) is:
 sorted l1 -> sorted l2 -> sorted (hd2 :: merge (hd1 :: tl1, tl2))

If I do remember (l1,l2) as l_pair then I manage to solve the non-recursive cases, but then the recursive cases can no longer be proved. Here is the first recursive case:

1 goal (ID 1688)
  
  l1, l2 : list nat
  hd1 : nat
  tl1 : list nat
  hd2 : nat
  tl2 : list nat
  Heql_pair : (hd1 :: tl1, hd2 :: tl2) = (l1, l2)
  e0 : (hd1 <=? hd2) = true
  IHl : (tl1, hd2 :: tl2) = (l1, l2) -> sorted l1 -> sorted l2 -> sorted (merge (tl1, hd2 :: tl2))
  ============================
  sorted l1 -> sorted l2 -> sorted (hd1 :: merge (tl1, hd2 :: tl2))

The problem is that l1 in the hypothesis Heql_pair is hd1::tl1, while in the induction hypothesis the very same l1 is tl1. So the problem is that Coq uses the same variable l1 to represent the first component of the pair before and after the application of the function merge. Is it a bug in the functional induction tactic? If not, is there a way to prove this last theorem using functional induction? I managed to prove it doing nested induction (first in l1, and then in l2), but I would like to better understand the functional induction tactic. Best, Flávio.

1 Like
2

The issue is that your induction hypothesis is not general enough. You should try to revert l1, l2, the hypothesis that they are sorted, and Heql_pair before doing your induction. That way, your induction hypothesis should be usable with the list you want to apply it on. The standard induction tactic provides a way to do this natively (using the in keyword), but I don’t think functional induction does, so you have to do it manually.

2 Likes
3

Yes, thanks. In fact, a reversion with generalize dependent for both l1 and l2 before the functional induction step makes the trick.

1 Like