Bove-Capretta method in Coq

Question

As an exercice on defining general recursive functions in Coq, I'm trying to implement a list merge function using an ad-hoc predicate, the so-called Bove-Capretta method.

For this, I'm following the pattern in the example for the log2 function on Chapter 15 of Bertot and Castéran. First, I have defined a domain predicate for merge as follows:

Inductive merge_acc : list nat -> list nat -> Prop :=
 | Merge1 : forall xs, merge_acc xs nil
 | Merge2 : forall ys, merge_acc nil ys 
 | Merge3 : forall x y xs ys,
      x <= y -> merge_acc xs (y :: ys) -> merge_acc (x :: xs) (y :: ys)
 | Merge4 : forall x y xs ys,
      x > y -> merge_acc (x :: xs) ys -> merge_acc (x :: xs) (y :: ys).

Next, I defined the relevant inversion lemmas for the recursive calls of merge:

 Ltac inv H := inversion H ; subst ; clear H.

 Lemma merge_acc_inv3
     : forall xs ys x y,
        merge_acc (x :: xs) (y :: ys) -> 
        x <= y -> 
        merge_acc xs (y :: ys).
 Proof.
    induction xs ; destruct ys ; intros x y H Hle ; inv H ; eauto ; try omega.
 Defined.

 Lemma merge_acc_inv4
    : forall xs ys x y, 
        merge_acc (x :: xs) (y :: ys) -> 
        x > y -> 
       merge_acc (x :: xs) ys.
 Proof.
   induction xs ; destruct ys ; intros x y H Hxy ; inv H ; eauto ; try omega.
 Defined.

After these definitions, I've tried the following implementation of merge:

 Fixpoint merge_bc 
     (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
     match xs, ys with
     | nil, ys => ys
     | xs , nil => xs
     | (x :: xs) , (y :: ys) =>
        match le_gt_dec x y with
        | left _ h1 => x :: merge_bc (merge_acc_inv3 xs ys x y H h1) 
        | right _ h2 => y :: merge_bc (x :: xs) ys (merge_acc_inv4 _ _ _ _ H h2)
        end 
     end.

But, I'm getting a error message that seems related to a lack of type refinement in pattern matching:

    The term "H" has type "merge_acc xs ys" while it is expected to have type
       "merge_acc (x :: xs0) (y :: ys0)".

Next, I tried to define merge using the refine tactic:

  Definition merge_bc : forall xs ys, merge_acc xs ys -> list nat.
     refine (fix merge_bc xs ys (H : merge_acc xs ys) {struct H}: list nat :=
        match xs as xs' return xs = xs' -> list nat with
        | nil => fun _ => ys
        | x :: xs => fun _ =>
          (match ys as ys' return ys = ys' -> list nat with
           | nil => fun _ => x :: xs
           | y :: ys => fun _ =>
             match le_gt_dec x y with
             | left _ Hle => x :: merge_bc xs (y :: ys) _
             | right _ Hgt => y :: merge_bc (x :: xs) ys _
             end
           end (eq_refl ys))
        end (eq_refl xs)).
     +
       subst.
       apply merge_acc_inv3 with (x := x).
       exact H. exact Hle.
    +
       subst.
       apply merge_acc_inv4 with (y := y).
       exact H.
       exact Hgt.
  Defined.

And Coq returns the following error message:

 Recursive call to merge_bc has principal argument equal to
    "eq_ind_r
        (fun xs1 : list nat => merge_acc xs1 ys -> merge_acc xs0 (y :: ys0))
        (fun H : merge_acc (x :: xs0) ys => ...

which I had simplified a bit. It seems that the recursion isn't been done on a structurally smaller subterm of merge_acc xs ys.

My question is, what am I doing wrong? Am I missing something?

The complete working example is at the following gist.

EDIT: Fixing the spelling of Castéran.

The correct spelling for Castéran has the accent on the e, not the a. — Yves

gallais gallais · Accepted Answer · 2018-06-04T13:58:04

I think the problem here is that the fact you're using a subterm of H is hidden by the needless complication you have put into the definitions of merge_acc_inv3 and merge_acc_inv4. There is no need for induction xs.

Additionally, during the pattern-matching on xs and ys you're losing the connection with the xs and the ys in the type of H. So here is what I have:

Inversion lemmas without induction and easier to use (cf. the use of equality constraints xxs = x :: xs)

  Lemma merge_acc_inv3
     : forall xs ys x y xxs yys,
        xxs = x :: xs -> yys = y :: ys ->
        merge_acc xxs yys ->
        x <= y ->
        merge_acc xs yys.
 Proof.
    intros xs ys x y xxs yys eqx eqy H Hle;
    subst; inv H ; eauto ; try omega.
 Defined.

 Lemma merge_acc_inv4
    : forall xs ys x y xxs yys,
      xxs = x :: xs -> yys = y :: ys ->
      merge_acc xxs yys ->
      x > y ->
     merge_acc xxs ys.
 Proof.
   intros xs ys x y xxs yys eqx eqy H Hxy ;
   subst ; inv H ; eauto ; try omega.
 Defined.

A dependent pattern-match which retains the connection between what the match looks like and the original xs / ys:

 Fixpoint merge_bc
     (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
   (match xs as us, ys as vs return xs = us -> ys = vs -> list nat with
     | nil, ys => fun _ _ => ys
     | xs , nil => fun _ _ => xs
     | (x :: xs) , (y :: ys) =>
        match le_gt_dec x y with
        | left _ h1 => fun eqx eqy =>
            let H' := merge_acc_inv3 _ _ x y _ _ eqx eqy H h1
            in x :: merge_bc _ _ H'
        | right _ h2 => fun eqx eqy =>
            let H' := merge_acc_inv4 _ _ x y _ _ eqx eqy H h2
            in y :: merge_bc _ _ H'
        end 
     end) eq_refl eq_refl.

Bove-Capretta method in Coq

1 Answers