The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 27 juin 09 à 15:54, Adam Koprowski a écrit :

>    Dear all, (or should I say: Dear Matthieu? ;)

Hi Adam,

>   This is a follow-up question to what I wrote few days ago (http://logical.saclay.inria.fr/coq-puma/messages/4810f6a2bb3fff04 
> ). Then I was having problems with reducibility of a Program-defined  
> function, which I needed to prove an accompanying lemma about this  
> function. As a matter of fact, I'd rather make this lemma a part of  
> the specification of this function. However I have a dependently  
> typed pattern matching with two nested recursive calls in one of the  
> branches and I'm lost as to how to obtain post-conditions for those  
> recursive calls. Please see the attached code (btw. is there a  
> better way to get equalities for the dependent pattern matching?).  
> All help greatly appreciated.

The problem comes from the fact that [eval_obligation_2] has type:

 forall (T : Type) (x : X T) (n : nat)
        (eval : forall (T0 : Type) (x0 : X T0) (n0 : nat),
                x_measure (build_ctx x0 n0) (build_ctx x n) ->
                {r : Res T0 | correct x0 n0 r}) (Anonymous  
Anonymous0 : Type)
        (e1 : X Anonymous) (e2 : X Anonymous0)
        (H : [x : (X T)]= [Seq e1 e2 : (X (Anonymous * Anonymous0))])
        (n' : nat) (r : Anonymous),
      Ok n' r = `(eval Anonymous e1 n (eval_obligation_1 eval H)) ->
      x_measure (build_ctx e2 n') (build_ctx x n)

The important part here being the [Ok n' r = `(eval ...)] assumption.
In the term, this obligation is applied to [Heq_anonymous], whose type  
would
gets abstracted if we abstract [eval A x1 n (eval_obligation_1 eval  
(eval_obligation_3 eval)],
to become [Ok n' r = s], making the new term ill-typed.
Under this circumstance, the only solution I know is to unfold the  
obligation
so that the abstraction works: the only way you can use this  
hypothesis in the
definition of the obligation is by destructing the [eval] anyway,  
making the
obligation abstract with respect to the result as well. You really  
need to
look at the term to see how it goes.

In short, this works:

Next Obligation. Proof. Admitted.
Next Obligation. Proof.
  destruct_call eval.
  (* You have to destruct it here so that you don't get another
     rigid constant with an [Ok n' r = `(eval ...)] argument. *)
 admit. Defined.

Next Obligation. Proof.
  destruct x; simpl.
  apply correct_Nil.
  unfold eval_obligation_2. destruct_call eval. simpl. destruct x ;  
simpl.
  destruct_call eval ; simpl. destruct x ; simpl. admit. admit. admit.
Qed.

Next Obligation.
Proof with auto.
  apply measure_wf. apply x_measure_wf.
Defined.

For the generation of equalities for the toplevel dependent pattern- 
matching,
you should get them for free ! The automatic inference of the return  
predicate
was not getting the dependency of the return type in [x], but this can  
be fixed.
As a result, you get to prove the [correct] tcc in each branch instead  
of having
to destruct the whole term again and get into these dependency problems.

-- Matthieu