diff options
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Product.v')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v new file mode 100644 index 00000000..8ac178fc --- /dev/null +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -0,0 +1,192 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Lexicographic_Product.v,v 1.12.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Authors: Bruno Barras, Cristina Cornes *) + +Require Import Eqdep. +Require Import Relation_Operators. +Require Import Transitive_Closure. + +(** From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Section WfLexicographic_Product. +Variable A : Set. +Variable B : A -> Set. +Variable leA : A -> A -> Prop. +Variable leB : forall x:A, B x -> B x -> Prop. + +Notation LexProd := (lexprod A B leA leB). + +Hint Resolve t_step Acc_clos_trans wf_clos_trans. + +Lemma acc_A_B_lexprod : + forall x:A, + Acc leA x -> + (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) -> + forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y). +Proof. + induction 1 as [x _ IHAcc]; intros H2 y. + induction 1 as [x0 H IHAcc0]; intros. + apply Acc_intro. + destruct y as [x2 y1]; intro H6. + simple inversion H6; intro. + cut (leA x2 x); intros. + apply IHAcc; auto with sets. + intros. + apply H2. + apply t_trans with x2; auto with sets. + + red in H2. + apply H2. + auto with sets. + + injection H1. + destruct 2. + injection H3. + destruct 2; auto with sets. + + rewrite <- H1. + injection H3; intros _ Hx1. + subst x1. + apply IHAcc0. + elim inj_pair2 with A B x y' x0; assumption. +Qed. + +Theorem wf_lexprod : + well_founded leA -> + (forall x:A, well_founded (leB x)) -> well_founded LexProd. +Proof. + intros wfA wfB; unfold well_founded in |- *. + destruct a. + apply acc_A_B_lexprod; auto with sets; intros. + red in wfB. + auto with sets. +Qed. + + +End WfLexicographic_Product. + + +Section Wf_Symmetric_Product. + Variable A : Set. + Variable B : Set. + Variable leA : A -> A -> Prop. + Variable leB : B -> B -> Prop. + + Notation Symprod := (symprod A B leA leB). + +(*i + Local sig_prod:= + [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end. + +Lemma incl_sym_lexprod: (included (A*B) Symprod + (R_o_f (A*B) {_:A&B} sig_prod (lexprod A [_:A]B leA [_:A]leB))). +Proof. + Red. + Induction x. + (Induction y1;Intros). + Red. + Unfold sig_prod . + Inversion_clear H. + (Apply left_lex;Auto with sets). + + (Apply right_lex;Auto with sets). +Qed. +i*) + + Lemma Acc_symprod : + forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y). + Proof. + induction 1 as [x _ IHAcc]; intros y H2. + induction H2 as [x1 H3 IHAcc1]. + apply Acc_intro; intros y H5. + inversion_clear H5; auto with sets. + apply IHAcc; auto. + apply Acc_intro; trivial. +Qed. + + +Lemma wf_symprod : + well_founded leA -> well_founded leB -> well_founded Symprod. +Proof. + red in |- *. + destruct a. + apply Acc_symprod; auto with sets. +Qed. + +End Wf_Symmetric_Product. + + +Section Swap. + + Variable A : Set. + Variable R : A -> A -> Prop. + + Notation SwapProd := (swapprod A R). + + + Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x). +Proof. + intros. + inversion_clear H. + apply Acc_intro. + destruct y0; intros. + inversion_clear H; inversion_clear H1; apply H0. + apply sp_swap. + apply right_sym; auto with sets. + + apply sp_swap. + apply left_sym; auto with sets. + + apply sp_noswap. + apply right_sym; auto with sets. + + apply sp_noswap. + apply left_sym; auto with sets. +Qed. + + + Lemma Acc_swapprod : + forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y). +Proof. + induction 1 as [x0 _ IHAcc0]; intros H2. + cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)). + clear IHAcc0. + induction H2 as [x1 _ IHAcc1]; intros H4. + cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)). + clear IHAcc1. + intro. + apply Acc_intro. + destruct y; intro H5. + inversion_clear H5. + inversion_clear H0; auto with sets. + + apply swap_Acc. + inversion_clear H0; auto with sets. + + intros. + apply IHAcc1; auto with sets; intros. + apply Acc_inv with (y0, x1); auto with sets. + apply sp_noswap. + apply right_sym; auto with sets. + + auto with sets. +Qed. + + + Lemma wf_swapprod : well_founded R -> well_founded SwapProd. +Proof. + red in |- *. + destruct a; intros. + apply Acc_swapprod; auto with sets. +Qed. + +End Swap.
\ No newline at end of file |