The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hello,

Pierre's answer is probably what you want.  Here are a few more ideas:


1/ You may also wish to show that the order you defined is included in 
the order Pierre defined,
and use the lemma wf_incl from the file Wellfounded/Inclusion.v to prove 
that yours
is wellfounded.


2/ About the purpose of sigS, it is a generalization of the cartesian 
product, where you
allow the second component to have its type depend on the first component.
If you want to have a type that contains both
 1/ a pair whose first component is true and the second is 0,
 2/ a pair whose first component is false and the second is false,

You can do it with sigS.

Check (existS bool (fun x => if x then nat else bool) true 0).
Check (existS bool (fun x => if x then nat else bool) false false).

3/ Last ,if you want to prove that PairOrderedTypeNatNat.lt is 
well-founded directly,
you need to perform nested proofs by induction.  Here is an example 
proof, to be
added at the end of the Coq excerpt in your message (Coq8.1pl3).

Lemma wf_POTNNlt : well_founded PairOrderedTypeNatNat.lt.
intros [x]; induction x; intros y; induction y.
apply Acc_intro; intros [x' y'] [h1 | [_ h1]]; case (Lt.lt_n_O _ h1).
apply Acc_intro; intros [x' y'] [h1 | [h1 h2]].
case (Lt.lt_n_O _ h1).
case (Lt.le_lt_or_eq _ _ h2).
unfold snd; intros y'y; case IHy; intros IHy'.
apply (IHy' (x', y')).
right; split;[exact h1 | simpl; apply Le.le_S_n; exact y'y].
simpl; intros q; injection q; clear q; intro; subst y'.
simpl in h1; subst x'; auto.
apply Acc_intro; intros [x' y'] [h1 | [h1 h2]].
case (Lt.le_lt_or_eq _ _ h1); intros l.
case (IHx 0); intros IHx'; apply IHx'.
left; apply Le.le_S_n; exact l.
simpl in l; injection l; intro; subst x'; apply IHx.
case (Lt.lt_n_O _ h2).
apply Acc_intro; intros [x' y'] [h1 | [h1 h2]].
case IHy; intros IHy'; apply IHy'; left; exact h1.
case (Lt.le_lt_or_eq _ _ h2); intros l.
case IHy; intros IHy'; apply IHy'; right; split; auto.
apply Le.le_S_n; exact l.
simpl in l, h1; injection l; intro; subst; auto.
Qed.

With my best regards,

Yves

Pierre Casteran wrote:
> 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.
>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club