The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

When you do [Next Obligation], [program_simpl] is automatically applied before you enter proof-editing mode.  The obligation in your example can't be solved with [program_simpl], but two applications does solve it, so [Solve Obligations with (program_simpl; program_simpl)] will work.

-Tej

On Mon, Jun 22, 2015 at 2:15 PM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

Hi list,

In both 8.4 and trunk, the following program leaves one obligation:

  Require Import List Program.

  Program Fixpoint zip
          {A B : Set} (a : list A) (b : list B)
          (p: length a = length b) : { l: list (A * B) | (length l = length a) } :=
    match a, b with
    | [], [] => []
    | x :: y, x' :: y' => (x, x') :: (zip y y' _)
    | x :: y, [] => !
    | [], x :: y => !
    end.

[Solve Obligations using program_simpl] doesn't solve that remaining obligation, but the following does:

  Next Obligation.
    program_simpl.
  Defined.

Is there something fishy going on here, or am I making an incorrect assumption?

Clément.