The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Merlin,

`Program` usually does some magic to be able to provide the "context" you are
missing here inside the `match`.  However, this magic cannot be used together
with `return` clauses, which explains the behavior you are seeing.

To get the missing context when using `return`, you can do the necessary magic
yourself.  For example, you can look at the term that is generated by 
`Program`
in your example that works (`Print rule_transform'.`).  I can't compile your
code as there's lots of missing context, but this shows the principle:

Program Definition test_0 (n: nat) :=
  match n with
  | O => true
  | S _ => false
  end.

Print test_0.

test_0 =
λ (n : nat) (program_branch_0 := λ _ : 0 = n, true)
(program_branch_1 := λ (wildcard' : nat) (_ : S wildcard' = n), false),
match n as n' return (n' = n → bool) with
| 0 => program_branch_0
| S wildcard' => program_branch_1 wildcard'
end eq_refl
     : nat → bool

So, the "magic" consists of match returning a function from an equality proof
relating the original discriminee (n) to the result of the match in the return
type (n').

The following proof term should help understanding what is going on:

Definition foo (n: nat) (H: forall m, n <> S m) : n = 0 :=
  match n as n' return n = n' -> n = 0 with
  | O => fun (EQ: n = 0) => EQ
  | S n' => fun (EQ: n = S n') =>
    (* match on something of type False *)
    match H _ EQ with end
  end eq_refl.

As you can see, both match arms actually produce a *function*, with the
function's argument being an equality proof reflecting the match arm we are 
in.
This equality proof is provided on the outside by just eq_refl, because the
entire match has the type `n = n -> n = 0`.

Kind regards,
Ralf

On 30.01.2018 13:58, Merlin Göttlinger wrote:
> Hi,
> 
> it took me quite a while to figure out why my Program Fixpoint (and refine 
> with
> Fix as well) generates missing contextual witnesses in the proof obligations
> making the goal unprovable. I had that happening previously when the 
> recursive
> calls were made inside a higher order function (which did no longer seem to 
> be
> unfolded when a measure function was involved) but that could be resolved by
> specialising that higher order function to pass the necessary proof along as
> well. But here the recursive call is "direct" and not nested in some other 
> fuzz
> that could confuse Coq.
> 
> Self contained example showing this
> behaviour: 
> https://gist.github.com/mgttlinger/ea0654dcf71b8937a7c67231e0c625f9
> 
> Can someone explain why this is happening?
> 
> Cheers,
> Merlin