The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 I couldn't check your development, since it lacks definitions of AP 
and BP.
 Nevertheless, the following script allows you to get a well-founded 
order on
 nat*(nat*nat)   (done with V8.2). All the steps are quite explicit, 
and I'm sure this can be simplified.

Hope this helps,

Pierre
Require Import Wf.
Require Import Relation_Operators.
Require Import Lexicographic_Product.
Require Import OrderedType.
Require Import OrderedTypeEx.
Require Import Wf_nat.

Definition dep2 := sigT (A:=nat) (fun a => nat).

Definition dep3 := sigT (A:=nat) (fun a => dep2).

Definition mk2  : nat*nat -> dep2.
intros (p,q).
exists p.
exact q.
Defined.


Definition mk3 :(nat*(nat*nat)) -> dep3.
intros (n, p_q).
exists n.
exact (mk2 p_q).
Qed.

Definition lt_pq :dep2->dep2->Prop :=
    (lexprod nat (fun a => nat) Peano.lt (fun a:nat =>Peano.lt)).


Definition lt_npq : dep3 -> dep3 -> Prop :=
    (lexprod nat (fun a => dep2) Peano.lt (fun a:nat =>lt_pq)).

Lemma wf_lexprod:well_founded lt_npq.
unfold lt_npq;apply wf_lexprod.
apply lt_wf.
intro n.
unfold lt_pq;apply wf_lexprod.
apply lt_wf.
i ntro _n;apply lt_wf.
Qed.

Require Import Inverse_Image.

Lemma wf_nat3 : well_founded  
   (fun x y : nat * (nat * nat) => lt_npq (mk3 x) (mk3 y)).
apply wf_inverse_image.
apply wf_lexprod.
Qed.