Teach Coq to check termination

Link:: https://stackoverflow.com/q/48173854

Display all goals and responses

Question

Coq, unlike many others, accepts an optional explicit parameter, which can be used to indicate the decreasing structure of a fixpoint definition.

From Gallina specification, 1.3.4,

Fixpoint ident params {struct ident0} : type0 := term0

defines the syntax. but from it, we've known that it must be an identifier, instead of a general measure.

However, in general, there are recursive functions, that the termination is not quite obvious, or it in fact is, but just difficult for the termination checker to find a decreasing structure. For example, following program interleaves two lists,

Fixpoint interleave (A : Set) (l1 l2 : list A) : list A :=
  match l1 with
  | [] => []
  | h :: t => h :: interleave l2 t
  end.In environment
interleave : forall A : Set,
             list A -> list A -> list A
A : Set
l1 : list A
l2 : list A
h : A
t : list A
The term "l2" has type "list A"
while it is expected to have type "Set".

This function clearly terminates, while Coq just couldn't figure it out. The reason is neither l1 nor l2 are decreasing every cycle. But what if we consider a measure, defined to be length l1 + length l2? Then this measure clearly decreases every recursion.

So my question is, in the case of sophisticated situation, where code is not straightforward to be organized in a termination checkable way, how do you educate Coq and convince it to accept the fixpoint definition?

Answer

You have multiple options and all of them boil down to structural recursion in the end.

Preamble

From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.

Structural recursion

Sometimes you can reformulate your algorithm in a structurally recursive way:

Fixpoint interleave1 {A} (l1 l2 : list A) {struct l1} : list A :=
  match l1, l2 with
  | [], _ => l2
  | _, [] => l1
  | h1 :: t1, h2 :: t2 => h1 :: h2 :: interleave1 t1 t2
  end.

Incidentally, in some cases you can use a trick with nested fixes -- see this definition of Ackermann function (it wouldn't work with just Fixpoint).

Program Fixpoint

You can use Program Fixpoint mechanism which lets you write your program naturally and later prove that it always terminates.

From Coq Require Import Program Arith.

Program Fixpoint interleave2 {A} (l1 l2 : list A)
        {measure (length l1 + length l2)} : list A :=
  match l1 with
  | [] => l2
  | h :: t => h :: interleave2 l2 t
  end.
Next Obligation.A: Type
l2: list A
h: A
t: list A
interleave2: forall (A0 : Type) (l1 l3 : list A0),
length l1 + length l3 <
length (h :: t) + length l2 -> 
list A0
length l2 + length t < length (h :: t) + length l2 simpl.A: Type
l2: list A
h: A
t: list A
interleave2: forall (A0 : Type) (l1 l3 : list A0),
length l1 + length l3 <
length (h :: t) + length l2 -> 
list A0
length l2 + length t < S (length t + length l2) rewrite Nat.add_comm.A: Type
l2: list A
h: A
t: list A
interleave2: forall (A0 : Type) (l1 l3 : list A0),
length l1 + length l3 <
length (h :: t) + length l2 -> 
list A0
length t + length l2 < S (length t + length l2) trivial with arith. Qed.

Function

Another option is to use the Function command which can be somewhat limited compared to Program Fixpoint. You can find out more about their differences here.

From Coq Require Recdef.

Definition sum_len {A} (ls : (list A * list A)) : nat :=
  length (fst ls) + length (snd ls).

Function interleave3 {A} (ls : (list A * list A))
         {measure sum_len ls} : list A :=
  match ls with
  | ([], _) => []
  | (h :: t, l2) => h :: interleave3 (l2, t)
  end.forall (A : Type) (ls : list A * list A)
  (l l2 : list A) (h : A) (t : list A),
l = h :: t ->
ls = (h :: t, l2) ->
sum_len (l2, t) < sum_len (h :: t, l2)
Proof.forall (A : Type) (ls : list A * list A)
  (l l2 : list A) (h : A) (t : list A),
l = h :: t ->
ls = (h :: t, l2) ->
sum_len (l2, t) < sum_len (h :: t, l2)
  intros A ls l1 l2 h t -> ->.A: Type
l2: list A
h: A
t: list A
sum_len (l2, t) < sum_len (h :: t, l2) unfold sum_len.A: Type
l2: list A
h: A
t: list A
length (fst (l2, t)) + length (snd (l2, t)) <
length (fst (h :: t, l2)) + length (snd (h :: t, l2))
  simpl.A: Type
l2: list A
h: A
t: list A
length l2 + length t < S (length t + length l2) rewrite Nat.add_comm.A: Type
l2: list A
h: A
t: list A
length t + length l2 < S (length t + length l2) trivial with arith.
Defined.

Equations plugin

This is an external plugin which addresses many issues with defining functions in Coq, including dependent types and termination.

From Equations Require Import Equations.

Equations interleave4 {A} (l1 l2 : list A) : list A
  by wf (length l1 + length l2) lt :=
  interleave4 nil l2 := l2;
  interleave4 (cons h t) l2 := cons h (interleave4 l2 t).
Next Obligation.A: Type
h: A
t, l2: list A
interleave4: forall (x : Type) (x0 x1 : list x),
length x0 + length x1 <
S (length t + length l2) -> 
list x
length l2 + length t < S (length t + length l2) rewrite Nat.add_comm.A: Type
h: A
t, l2: list A
interleave4: forall (x : Type) (x0 x1 : list x),
length x0 + length x1 <
S (length t + length l2) -> 
list x
length t + length l2 < S (length t + length l2) trivial with arith. Qed.

Fix / Fix_F_2 combinators

You can learn more about this (manual) approach if you follow the links from this question about mergeSort function. By the way, the mergeSort function can be defined without using Fix if you apply the nested fix trick I mentioned earlier. Here is a solution which uses Fix_F_2 combinator since we have two arguments and not one like mergeSort:

Definition ordering {A} (l1 l2 : list A * list A) : Prop :=
  length (fst l1) + length (snd l1) < length (fst l2) + length (snd l2).

Lemma ordering_wf' {A} : forall (m : nat) (p : list A * list A),
    length (fst p) + length (snd p) <= m -> Acc (@ordering A) p.A: Type
forall (m : nat) (p : list A * list A),
length (fst p) + length (snd p) <= m -> Acc ordering p
Proof.A: Type
forall (m : nat) (p : list A * list A),
length (fst p) + length (snd p) <= m -> Acc ordering p
  unfold ordering.A: Type
forall (m : nat) (p : list A * list A),
length (fst p) + length (snd p) <= m ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p induction m; intros p H; constructor; intros p'.A: Type
p: (list A * list A)%type
H: length (fst p) + length (snd p) <= 0
p': (list A * list A)%type
length (fst p') + length (snd p') <
length (fst p) + length (snd p) ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p'
A: Type
m: nat
IHm: forall p : list A * list A,
length (fst p) + length (snd p) <= m ->
Acc
(fun l1 l2 : list A * list A =>
length (fst l1) + length (snd l1) < length (fst l2) + length (snd l2)) p
p: (list A * list A)%type
H: length (fst p) + length (snd p) <= S m
p': (list A * list A)%type
length (fst p') + length (snd p') <
length (fst p) + length (snd p) ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p'
  -A: Type
p: (list A * list A)%type
H: length (fst p) + length (snd p) <= 0
p': (list A * list A)%type
length (fst p') + length (snd p') <
length (fst p) + length (snd p) ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p' apply Nat.le_0_r, Nat.eq_add_0 in H as [-> ->].A: Type
p, p': (list A * list A)%type
length (fst p') + length (snd p') < 0 + 0 ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p'
    intros contra%Nat.nlt_0_r.A: Type
p, p': (list A * list A)%type
contra: False
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p' contradiction.
  -A: Type
m: nat
IHm: forall p : list A * list A,
length (fst p) + length (snd p) <= m ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p
p: (list A * list A)%type
H: length (fst p) + length (snd p) <= S m
p': (list A * list A)%type
length (fst p') + length (snd p') <
length (fst p) + length (snd p) ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p' intros H'.A: Type
m: nat
IHm: forall p : list A * list A,
length (fst p) + length (snd p) <= m ->
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p
p: (list A * list A)%type
H: length (fst p) + length (snd p) <= S m
p': (list A * list A)%type
H': length (fst p') + length (snd p') <
length (fst p) + length (snd p)
Acc
  (fun l1 l2 : list A * list A =>
   length (fst l1) + length (snd l1) <
   length (fst l2) + length (snd l2)) p' eapply IHm, Nat.lt_succ_r, Nat.lt_le_trans; eauto.
Defined.

Lemma ordering_wf {A} : well_founded (@ordering A).A: Type
well_founded ordering
Proof.A: Type
well_founded ordering now red; intro; eapply ordering_wf'. Defined.

(* it's in the stdlib but unfortunately opaque -- this blocks evaluation *)
Lemma destruct_list {A} (l : list A) :
  { x : A & {tl : list A | l = x :: tl} } + { l = [] }.A: Type
l: list A
{x : A & {tl : list A | l = x :: tl}} + {l = []}
Proof.A: Type
l: list A
{x : A & {tl : list A | l = x :: tl}} + {l = []}
  induction l as [|h tl]; [right | left]; trivial.A: Type
h: A
tl: list A
IHtl: {x : A & {tl0 : list A | tl = x :: tl0}} +
{tl = []}
{x : A & {tl0 : list A | h :: tl = x :: tl0}}
  exists h, tl.A: Type
h: A
tl: list A
IHtl: {x : A & {tl0 : list A | tl = x :: tl0}} +
{tl = []}
h :: tl = h :: tl reflexivity.
Defined.

Definition interleave5 {A} (xs ys : list A) : list A.A: Type
xs, ys: list A
list A
  refine (Fix_F_2
            (fun _ _ => list A)
            (fun (l1 l2 : list A)
                 (interleave :
                    (forall l1' l2', ordering (l1', l2') (l1, l2) -> list A)) =>
               match destruct_list l1 with
               | inright _ => l2
               | inleft pf => let '(existT _ h (exist _ tl eq)) := pf
                              in h :: interleave l2 tl _
               end) (ordering_wf (xs, ys))).A: Type
xs, ys, l1, l2: list A
interleave: forall l1' l2' : list A,
ordering (l1', l2') (l1, l2) -> list A
pf: {x : A & {tl : list A | l1 = x :: tl}}
h: A
s: {tl : list A | l1 = h :: tl}
tl: list A
eq: l1 = h :: tl
ordering (l2, tl) (l1, l2)
  Proof.A: Type
xs, ys, l1, l2: list A
interleave: forall l1' l2' : list A,
ordering (l1', l2') (l1, l2) -> list A
pf: {x : A & {tl : list A | l1 = x :: tl}}
h: A
s: {tl : list A | l1 = h :: tl}
tl: list A
eq: l1 = h :: tl
ordering (l2, tl) (l1, l2)
    unfold ordering.A: Type
xs, ys, l1, l2: list A
interleave: forall l1' l2' : list A,
ordering (l1', l2') (l1, l2) -> list A
pf: {x : A & {tl : list A | l1 = x :: tl}}
h: A
s: {tl : list A | l1 = h :: tl}
tl: list A
eq: l1 = h :: tl
length (fst (l2, tl)) + length (snd (l2, tl)) <
length (fst (l1, l2)) + length (snd (l1, l2)) rewrite eq, Nat.add_comm.A: Type
xs, ys, l1, l2: list A
interleave: forall l1' l2' : list A,
ordering (l1', l2') (l1, l2) -> list A
pf: {x : A & {tl : list A | l1 = x :: tl}}
h: A
s: {tl : list A | l1 = h :: tl}
tl: list A
eq: l1 = h :: tl
length (snd (l2, tl)) + length (fst (l2, tl)) <
length (fst (h :: tl, l2)) +
length (snd (h :: tl, l2)) auto.
  Defined.

Evaluation tests

Check eq_refl : interleave1 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6].eq_refl
:
interleave1 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6]
     : interleave1 [1; 2; 3] [4; 5; 6] =
       [1; 4; 2; 5; 3; 6]
Check eq_refl : interleave2 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6].eq_refl
:
interleave2 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6]
     : interleave2 [1; 2; 3] [4; 5; 6] =
       [1; 4; 2; 5; 3; 6]
Check eq_refl : interleave3 ([1; 2; 3], [4; 5; 6]) = [1; 4; 2; 5; 3; 6].eq_refl
:
interleave3 ([1; 2; 3], [4; 5; 6]) =
[1; 4; 2; 5; 3; 6]
     : interleave3 ([1; 2; 3], [4; 5; 6]) =
       [1; 4; 2; 5; 3; 6]
Check eq_refl : interleave4 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6].eq_refl
:
interleave4 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6]
     : interleave4 [1; 2; 3] [4; 5; 6] =
       [1; 4; 2; 5; 3; 6]
Check eq_refl : interleave5 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6].eq_refl
:
interleave5 [1; 2; 3] [4; 5; 6] = [1; 4; 2; 5; 3; 6]
     : interleave5 [1; 2; 3] [4; 5; 6] =
       [1; 4; 2; 5; 3; 6]

Exercise: what happens with this last check if you comment out destruct_list lemma?