From 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 17 Oct 2006 12:53:34 +0000 Subject: Mise en forme des theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Lexicographic_Product.v | 259 ++++++++++++--------------- 1 file changed, 119 insertions(+), 140 deletions(-) (limited to 'theories/Wellfounded/Lexicographic_Product.v') diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 94e97e6ee..82bede919 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -18,58 +18,56 @@ Require Import Transitive_Closure. 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. + 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). + + 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. @@ -83,50 +81,31 @@ Section Wf_Symmetric_Product. 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. + 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. @@ -134,59 +113,59 @@ Section Swap. 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. + 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. - - + 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. + Proof. + red in |- *. + destruct a; intros. + apply Acc_swapprod; auto with sets. + Qed. End Swap. \ No newline at end of file -- cgit v1.2.3