The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Indeed the large number of arguments and corresponding projections to build the measure

is bringing the type-checker to its knees.

It will terminate instantaneously if you do this in a section like below. Aside: it's good style

in general to not make the fixpoint depend on things that are parameters and never vary

across recursive calls.

Section Resolve.

  Local Obligation Tactic := idtac.

  Context `{bfc : Buffer buf_t buf_new buf_nth buf_push buf_size buf_to_list}

        (A : Set).

  

  Program Fixpoint resolve

        (buf : buf_t A)

        (l : SequenceWithBackRefs A)

        {measure ((fun l => brlen l + length l) l)} : list (option A) :=

  match l with

  | [] => []

  | inl char :: rest =>

    Some char :: resolve (buf_push A char buf) rest

  | inr (0, dist) :: rest => resolve buf rest

  | inr (S n_, dist) :: rest =>

    match buf_nth A buf (dist - 1) with

    | Some char => Some char :: resolve buf (inr (n_, dist) :: rest)

    | None => [None]

    end

  end.

  Next Obligation.

  Proof.

    intros ? ? ? ? r req.

    rewrite <- req.

    simpl.

    omega.

  Qed.

  Next Obligation.

    intros ? ? ? ? r req.

    rewrite <- req.

    simpl.

    omega.

  Qed.

  Next Obligation.

    intros ? ? ? ? ? ? req ? ? ?.

    rewrite <- req.

    simpl.

    omega.

  Qed.

  Next Obligation.

    apply measure_wf.

    apply lt_wf.

  Defined.

End Resolve.

Best regards,

-- Matthieu

On Mon, Nov 21, 2016 at 4:55 PM Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de> wrote:

Hi.

I attached a code file in which I define a function (for resolution of
backreferences with an abstract array) recursively using Program Fixpoint.

Now, the problem is that the proof of the last obligation works, but
"Defined" hangs (in proofgeneral); maybe because the generated term is
huge – for some reason, though the list itself does not depend on the
given structure of the buffer, all of the typeclass information is
always passed, and there are lots of nested sums that are resolved there.

I know that there would be other ways to define this function, but this
way looks clear which is why I would prefer it.

Do you have any suggestions?

Best Regards
Christoph-Simon Senjak