The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

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
Require Import Program.
Require Import List.
Import ListNotations.
Require Import Omega.

Function SequenceWithBackRefs A := (list (A+(nat*nat))%type).

Fixpoint brlen {A} (l : SequenceWithBackRefs A) : nat :=
  match l with
    | nil => 0
    | inl _ :: l' => S (brlen l')
    | inr (n, _) :: l' => n + brlen l'
  end.

Fixpoint take {A : Set} (n : nat) (l : list A) : list A :=
  match n with
  | 0 => []
  | S n_ => match l with
            | [] => []
            | x :: l_ => x :: take n_ l_
            end
  end.

(* TODO: smurf naming *)
Class Buffer
      (buf_t : Set -> Set)
      (buf_new : forall (A : Set), buf_t A)
      (buf_nth : forall {A : Set}, buf_t A -> nat -> Exc A)
      (buf_push : forall {A : Set}, A -> buf_t A -> buf_t A)
      (buf_size : forall {A : Set}, buf_t A -> nat)
      (buf_to_list : forall {A : Set}, buf_t A -> list A) :=
      {
        nillist : forall (A : Set), buf_to_list (buf_new A) = nil;
        nthlist : forall (A : Set) (l : buf_t A) n,
            buf_nth l n = nth_error (buf_to_list l) n;
        sizelist : forall (A : Set) (l : buf_t A),
            buf_size l = length (buf_to_list l);
        pushlist : forall (A : Set) (x : A) (l : buf_t A),
            buf_to_list (buf_push x l) = take (buf_size l) (x :: buf_to_list 
l)
      }.

Generalizable Variables buf_t buf_new buf_nth buf_push buf_size buf_to_list.

Local Obligation Tactic := idtac.

Program Fixpoint resolve
        `{bfc : Buffer buf_t buf_new buf_nth buf_push buf_size buf_to_list}
        (A : Set)
        (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 A (buf_push A char buf) rest
  | inr (0, dist) :: rest => resolve A buf rest
  | inr (S n_, dist) :: rest =>
    match buf_nth A buf (dist - 1) with
    | Some char => Some char :: resolve A 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.