The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

You can also understand how the recursion works, and find out what parts of the proofs you did really need to be transparent. The details not being needed for the proofs can be set opaque (for instance using the abstract tactic) letting only the recursion skeleton, so that proofs do not really need to be computed. If I have time, I will give an example on what you did later.

2013/9/5 Robbert Krebbers <mailinglists AT robbertkrebbers.nl>

Hi Colm,

the problem is that you have defined all these lemmas using [Qed] instead of [Defined]. Defining them using [Qed] makes the proof opaque to the kernel, and hence computation will get stuck on it.

PS1: if you use the fact [lt_wf] that [lt] is well-founded, the proof of [wfPairNatOrder] becomes much shorter.

  Theorem wfPairNatOrder : well_founded pairNatOrder.
  Proof.
    intros [n m]; revert m.
    induction (lt_wf n) as [n _ IH1]; intros m.
    induction (lt_wf m) as [m _ IH2].
    constructor. intros [n' m'] [?|??]; simpl in *; subst; auto.
  Defined.

PS2: computation using proofs of well foundedness may be quite slow because the system has to evaluate termination proofs. A trick to avoid this problem is to use

  Fixpoint wf_guard {A} {R : A -> A -> Prop}
      (n : nat) (wfR : well_founded R) : well_founded R :=
    match n with
    | 0 => wfR
    | S n => fun x =>
       Acc_intro x (fun y _ => wf_guard n (wf_guard n wfR) y)
    end.
  Strategy 100 [wf_guard].

Now use [wf_guard 32 wfPairNatOrder] with [wfPairNatOrder] declared opaque using [Qed] as the termination proof of your function. This way it will perform 2^32 steps before actually getting stuck on the proof (you will likely reach some other implementation limit of your system before having done that many steps).

Cheers,

Robbert

On 09/05/2013 06:40 PM, bhandalc AT tcd.ie wrote:

Hi,

I'm trying to define a non-trivial fixpoint function that doesn't simply
structurally decrease on the one argument. However, evaluating this function
is getting stuck. Here is a minimal example to demonstrate, though this
function is clearly practically useless! The function itself is called
"pairHopper". What it does is take a pair of naturals and calls recursively in
a funny way until (0, 0) is reached, then it returns 0. So for any pair of
naturals, this function should return 0. And I've defined the well ordering
relation so we know it always terminates.

However, when I try, say "eval compute in pairHopper (10, 10)" what I get back
is an ugly monstrosity of a term beginning with "let (v, _) := ..." I am stuck
here as I thought I would get back 0? I figure it must be something to do with
how the "Function" command builds a function that doesn't go well with compute
but I'm fairly lost... any help would be much appreciated!

Thanks,

Colm

Code:

Require Import Arith.

(** A special ordering relation on pairs of numbers.*)
Inductive pairNatOrder (x y : nat * nat) : Prop :=
   | pnoNat : fst x<  fst y ->  pairNatOrder x y
   | pnoProc : fst x = fst y ->  snd x<  snd y ->  pairNatOrder x y.

Lemma wfpairNatOrderBase (n : nat) : Acc pairNatOrder (0, n).
   remember n as s. rewrite Heqs. assert (n<= s).
   rewrite Heqs. constructor. clear Heqs. generalize dependent n.
   induction s; intros; constructor; intros; destruct y.
   inversion H0. apply False_ind. eapply lt_n_O. apply H1.
   simpl in H2. apply False_ind. eapply lt_n_O.
   eapply lt_le_trans. apply H2. assumption.
   inversion H0. apply False_ind. eapply lt_n_O. apply H1.
   assert (n1<= s). apply le_S_n. simpl in H2.
   eapply le_trans. apply H2. assumption.
   simpl in H1. rewrite H1. apply IHs. assumption. Qed.

Lemma pairNatOrderLt (m n : nat):
   Acc pairNatOrder (m, n) ->
   (forall (m' n' : nat), m'<  m ->
   Acc pairNatOrder (m', n')). intros. inversion H.
   apply H1. apply pnoNat. simpl. assumption. Qed.

Lemma pairNatOrderLe : forall m : nat,
   (forall (n : nat) , Acc pairNatOrder (m, n)) ->
   (forall (m' n' : nat),
   m'<= m ->  Acc pairNatOrder (m', n')). intros. apply le_lt_eq_dec in H0.
   inversion H0. clear H0. apply (pairNatOrderLt m n'). apply H. assumption.
   rewrite H1. apply H. Qed.

Lemma wfpairNatOrderInd : forall (m n : nat),
   (forall (n' : nat), Acc pairNatOrder (m, n'))
    ->  Acc pairNatOrder (S m, n).
   intros. remember n as s. rewrite Heqs. generalize (pairNatOrderLe m H).
   intro. clear H. assert (n<= s). rewrite Heqs. constructor.
   clear Heqs. generalize dependent n.
   induction s; intros; constructor; intros; destruct y;
   inversion H1; simpl in H2. apply le_S_n in H2. apply H0.
   assumption. simpl in H3. inversion H. rewrite H4 in H3. inversion H3.
   apply le_S_n in H2. apply H0. assumption. simpl in H3.
   rewrite H2. apply IHs. apply le_S_n. eapply le_trans. apply H3.
   assumption. Qed.

(** We need to prove that the ordering relation defined is indeed well
founded.*)
Theorem wfPairNatOrder : well_founded pairNatOrder. unfold well_founded.
   intros. destruct a. generalize dependent n0.
   induction n; intros. apply wfpairNatOrderBase. apply wfpairNatOrderInd.
   intros. apply IHn. Qed.

Require Import Recdef.

(** This function is a bit silly- but I'm using it as a minimal example to
demonstrate the
behaviour in question. The function always returns 0, but in doing so it walks
through an
odd ordering on the pair argument.*)
Function pairHopper (x : nat * nat)
   {wf pairNatOrder x} : nat:=
   match x with
   | (0, 0) =>  0
   | (S m, 0) =>  pairHopper (m, 10)
   | (m, S n) =>  pairHopper (m, n)
   end.
   simpl; intros. apply pnoProc. reflexivity. simpl. constructor.
   simpl; intros; repeat constructor.
   simpl; intros. apply pnoProc. reflexivity. simpl. constructor.
   apply wfPairNatOrder.
   Defined.

--
.../Sedrikov\...