The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Well, it did not work as good as I thought, very little parts of my Acc
proof could be abstracted…

=====================================================================
(** 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 lt_n_0 n (H : n<0) : False.
Proof.
  change (match O with O => False | S _ => True end); case H; split.
Qed.

(** We need to prove that the ordering relation defined is indeed well
founded.*)
Theorem wfPairNatOrder : well_founded pairNatOrder.
Proof.
  unfold well_founded.
  intros []; fix 1; intros [|a]; [|generalize (wfPairNatOrder a)];
clear.
  + fix 1; intros [|a]; [|generalize (wfPairNatOrder a)]; clear; split.
    - abstract (intros [x y] [K|_ K]; case (lt_n_0 _ K)).
    - intros y [K|L K]; simpl in *.
      * case (lt_n_0 _ K).
      * revert H; change a with (pred (S a)); case K; case L; case y;
simpl. { clear; intros x y H; exact H. }
        { clear; intros x y z K [H]; apply H; right; auto. }
  + intros K; fix 1; intros [|b]; [|generalize (wfPairNatOrder b)];
clear - K; split.
    - intros y [H|_ H]; simpl in *.
      * revert K; change a with (pred (S a)); case H; simpl; clear.
        { case y; intros a b H; exact (H b). }
        { abstract (intros m Hm L; apply (L O); clear - Hm; left; exact
Hm). }
      * case (lt_n_0 _ H).
    - clear - H; intros y [M|L M]; simpl in *.
      * abstract (case H as [P]; apply P; left; exact M).
      * revert H; change b with (pred (S b)); case M; simpl in *; clear
- L. { revert L; case y; simpl; clear; intros u v []; auto. }
        { abstract (case L;intros m Hm [K];apply K;right;[split|exact
Hm]). } Defined.

Fixpoint pairHopper_ (x : nat * nat) (X : Acc pairNatOrder x) {struct
X} : nat. refine (
  let (X) := X in
  match x as pair return (forall y, pairNatOrder y pair -> _) -> _ with
  (x, y) =>
    match y as z return (forall u, pairNatOrder u (_, z) -> _) -> _ with
    | O => match x as t return (forall u, pairNatOrder u (t, _) -> _)
-> _ with | O => fun _ => O
           | S m => fun pairHopper =>
                    pairHopper (m, 10) (_:pairNatOrder _ (S m, 0))
           end
    | S n => fun pairHopper => pairHopper (x, n) (_:pairNatOrder _ (x,
S n)) end
  end (fun y H => pairHopper_ y (X y H))
).
Proof. clear; left; simpl. left.
Proof. right; simpl; clear. split. left.
Defined.

Definition pairHopper (x : nat * nat) : nat :=
  pairHopper_ x (wfPairNatOrder x).

Eval compute in pairHopper (10, 10).