The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 06/22/2015 11:25 AM, Tej Chajed wrote:
> 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.

Correct, thanks Tej!

> 
> -Tej
> 
> On Mon, Jun 22, 2015 at 2:15 PM Clément Pit--Claudel 
> <clement.pit AT gmail.com
>  
> <mailto: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.
>