The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

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

  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.

   Cheers,
   Adam


Require Import Relations Program Wf.
Set Implicit Arguments.

Inductive X : Type -> Type :=
| Nil : X True

| Seq : forall A B, X A -> X B -> X (A * B).

Definition Xtype T (x : X T) := T.

Inductive Res (T : Type) : Type :=
| Ok (n : nat) (res : T)

| Fail.
Implicit Arguments Fail [T].

Definition ctx := { T : Type & (X T * nat)%type }.
Definition build_ctx (T : Type) (x : X T) (n : nat) : ctx := existT _ T (x, n).

Axiom x_measure : relation ctx.
Axiom x_measure_wf : well_founded x_measure.

Axiom correct : forall T, X T -> nat -> Res T -> Prop.
Axiom correct_Nil : forall n, correct Nil n Fail.

Axiom correct_Seq_fail_l : forall A B n n' (el : X A) (er : X B),
  correct el n Fail -> correct (Seq el er) n' Fail.

Axiom correct_Seq_fail_r : forall A B n n' r (el : X A) (er : X B),
  correct el n (Ok n' r) -> correct er n' Fail -> correct (Seq el er) n' Fail.

Axiom correct_Seq_ok : forall A B n n' n'' r r' (el : X A) (er : X B),
  correct el n (Ok n' r) -> correct er n' (Ok n'' r') -> correct (Seq el er) n'' (Ok n'' (r, r')).

Program Fixpoint eval (T : Type) (x : X T) (n : nat)
  {measure (build_ctx x n) (x_measure)} : 

  { r : Res T | correct x n r } :=

  match x as x' return JMeq x x' -> Res (Xtype x') with

  | Nil => fun H => Fail
  | Seq _ _ e1 e2 => fun H =>

      match eval e1 n with
      | Fail => Fail

      | Ok n' r => 
          match eval e2 n' with

          | Fail => Fail
          | Ok n'' r' =>

              Ok n'' (r, r')
          end

      end
  end _.

Next Obligation. Proof. Admitted.
Next Obligation. Proof. Admitted.

Next Obligation. 
Proof.

  destruct x; simpl.
  apply correct_Nil.

   (* ? *)
  (* [destruct_call eval] fails, because:

     [destruct (eval A x1 n (eval_obligation_1 eval (eval_obligation_3 eval)))]
    gives error:

     [Abstracting over the term "..." leads to a term "..." which is ill-typed]
  *)

Admitted.
Next Obligation.

Proof with auto.
  apply measure_wf. apply x_measure_wf.

Defined.


-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================