# Functional induction with remember

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

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

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

1 Like