The Coq mailing list

["Sunil Kothari" <skothari AT uwyo.edu>]

Title: How to show lexicographic product of three well-founded sets is well-founded

Many thanks to Pierre Casteran, Yves Bertot,  Pierre Lescanne and

Frederic Blanqui for responding to my queries.

 

Sunil

---

From: Sunil Kothari
Sent: Sun 7/20/2008 7:48 PM
To: Sunil Kothari; coq-club AT pauillac.inria.fr
Subject: How to show lexicographic product of three well-founded sets is well-founded

Hello Coq Users,
   I am trying to show that a 3-tuple of type nat* nat * nat is well-founded for lexicographic ordering. I know there have been discussions on this mailing-list before  on lexicographic ordering on pairs in the context of Ackermann's function.
For instance, the discussion in 2004 between Stefan Karrmann and Pierre Casteran http://pauillac.inria.fr/pipermail/coq-club/2004/001343.html
I tried using their code since a 3-product can be considered as a product of a pair and an element but I am stuck. The script is below:

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


Definition A : Set := nat.
Definition B (_: A) := nat.

Definition ltA : A -> A -> Prop := lt.
Definition ltB  (x:A) : B x -> B x -> Prop := lt.

(* the defines the lt for pairs *)
Module PairOrderedTypeNatNat := PairOrderedType Nat_as_OT Nat_as_OT.

Definition ltAP : AP -> AP -> Prop:= PairOrderedTypeNatNat.lt.
Definition ltBP (x:AP): BP x-> BP x -> Prop:= lt.

Definition lex_ord_n2 := (lexprod A B ltA ltB).

(* defines the lt relation for product of a pair and an element*)
Definition lex_ord_np := (lexprod AP BP ltAP ltBP).

Definition dom_ack : Set := sigS B.
Definition dom_ackP:Set := sigS BP.

Lemma wf_lt : well_founded lt.
Proof.
exact (well_founded_ltof nat (fun x : nat => x)).
Qed.

Lemma wf_ack : well_founded (A:=dom_ack) lex_ord_n2.
Proof.
exact (wf_lexprod A B ltA ltB wf_lt (fun x:A => wf_lt)).
Qed.

(* well-foundedness lemma for lex_ord_np  *)
Lemma wf_lexprod:well_founded (AP:= dom_ackP) lex_ord_np.

Coe doesn't like the name AP. I am not sure whether my formulation of the well-foundedness lemma is correct.

How do I proceed from here ? What is the purpose of sigS ?

I tried the other alternative of NOT using the dependent products but I was unable to
prove well-foundedness directly.

I will very much appreciate your suggestions/hints.

Thanks in advance,
Sunil