The Coq mailing list

[<bhandalc AT tcd.ie>]

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.