Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Program Fixpoint obligation hanging

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Program Fixpoint obligation hanging


Chronological Thread 
  • From: Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Program Fixpoint obligation hanging
  • Date: Mon, 21 Nov 2016 16:54:44 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christoph.senjak AT ifi.lmu.de; spf=None smtp.mailfrom=christoph.senjak AT ifi.lmu.de; spf=None smtp.helo=postmaster AT acheron.ifi.lmu.de
  • Ironport-phdr: 9a23:hPpQABPJS+tvOYdFjKAl6mtUPXoX/o7sNwtQ0KIMzox0Iv7+rarrMEGX3/hxlliBBdydsKMfzbCN+P+/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6zbL9oMhm7owrdu8sUjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktJ+gqJGrhyiqRJwzYHbb52OOfp7Yq/QZ8kXSXZPU8tTUSFKH4Oyb5EID+oEJetVsYn9p0EPrRulGQmsA/vvyj9RinHr3K061uMhEQfb1wI9Ad0OtnbUo8/2NKwPVu260KnIzS/Cb/NNxTf975DIchA7rfGXQ71wd8jRxlMsFw7ej1WQp43lMymR1uQIrmiX9fdvWvy2hmMhtgp/oSCvy98xhoXXgo8Z0E3I+CZ7zYovO9G0VUF2bcS5HJZetyyWL5V6Tdk+T211vSs3xbMGtJ2+cSQX1Jgr2hvSZ+KEfoSV5x/uVvyeLip4iX9gZb6zmwq+/Ealx+HgU8S4zVBHpTdfnNbWrHACzRnT59CHSvRj+keh3i6C2BrP5eFEP080j63bK5g7zr4xmJoTsF7PHivzmEXrlqOZa1sr9vCp6+ThfLrmuoeRO5Jqhgz6KKgih8+yDOYiPgQQQmSW9v6w2KDt8ED5WLlKi+c5kqjdsJDUP8Qboau5DhdJ3YYj8Ra/Diym0MgfnXkfLFJJYgmHgJbvO1HMOv/4Duyyg1WikDdq3fzGOrjhAojXInfejrjtZax95FJEyAov0dBf4IpZBa0GIPLqQ0P+qNjYDgIiPAGv2ObmCNB91psEVm6VA6+ZNrnSsV6S6e41LemMftxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FNI1+YembrmtdEKmYPuQx2d+HsilSBGWpYZ2yzRL47/jF9E4+gD47AboGjgfqF2Tr9EpAANTMOMUyFDXq9L9bMYPwLci/HesI=

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.



Archive powered by MHonArc 2.6.18.

Top of Page