diff options
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Product.v')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 223 |
1 files changed, 112 insertions, 111 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index b8f74c9ff..d457e4190 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -10,64 +10,65 @@ (** Authors: Bruno Barras, Cristina Cornes *) -Require Eqdep. -Require Relation_Operators. -Require Transitive_Closure. +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: (x:A)(B x)->(B x)->Prop. +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). -Hints Resolve t_step Acc_clos_trans wf_clos_trans. +Hint Resolve t_step Acc_clos_trans wf_clos_trans. -Lemma acc_A_B_lexprod : (x:A)(Acc A leA x) - ->((x0:A)(clos_trans A leA x0 x)->(well_founded (B x0) (leB x0))) - ->(y:(B x))(Acc (B x) (leB x) y) - ->(Acc (sigS A B) LexProd (existS A B x y)). +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. - NewInduction 1 as [x _ IHAcc]; Intros H2 y. - NewInduction 1 as [x0 H IHAcc0];Intros. - Apply Acc_intro. - NewDestruct 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. - NewDestruct 2. - Injection H3. - NewDestruct 2;Auto with sets. - - Rewrite <- H1. - Injection H3; Intros _ Hx1. - Subst x1. - Apply IHAcc0. - Elim inj_pair2 with A B x y' x0; Assumption. + 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 A leA) ->((x:A) (well_founded (B x) (leB x))) - -> (well_founded (sigS A B) LexProd). +Theorem wf_lexprod : + well_founded leA -> + (forall x:A, well_founded (leB x)) -> well_founded LexProd. Proof. - Intros wfA wfB;Unfold well_founded . - NewDestruct a. - Apply acc_A_B_lexprod;Auto with sets;Intros. - Red in wfB. - Auto with sets. + 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. @@ -75,10 +76,10 @@ End WfLexicographic_Product. Section Wf_Symmetric_Product. - Variable A:Set. - Variable B:Set. - Variable leA: A->A->Prop. - Variable leB: B->B->Prop. + Variable A : Set. + Variable B : Set. + Variable leA : A -> A -> Prop. + Variable leB : B -> B -> Prop. Notation Symprod := (symprod A B leA leB). @@ -101,24 +102,24 @@ Proof. Qed. i*) - Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) - ->(Acc (A*B) Symprod (x,y)). + Lemma Acc_symprod : + forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y). Proof. - NewInduction 1 as [x _ IHAcc]; Intros y H2. - NewInduction H2 as [x1 H3 IHAcc1]. - Apply Acc_intro;Intros y H5. - Inversion_clear H5;Auto with sets. - Apply IHAcc; Auto. - Apply Acc_intro;Trivial. + 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 A leA)->(well_founded B leB) - ->(well_founded (A*B) Symprod). +Lemma wf_symprod : + well_founded leA -> well_founded leB -> well_founded Symprod. Proof. - Red. - NewDestruct a. - Apply Acc_symprod;Auto with sets. + red in |- *. + destruct a. + apply Acc_symprod; auto with sets. Qed. End Wf_Symmetric_Product. @@ -126,66 +127,66 @@ End Wf_Symmetric_Product. Section Swap. - Variable A:Set. - Variable R:A->A->Prop. + Variable A : Set. + Variable R : A -> A -> Prop. - Notation SwapProd :=(swapprod A R). + Notation SwapProd := (swapprod A R). - Lemma swap_Acc: (x,y:A)(Acc A*A SwapProd (x,y))->(Acc A*A SwapProd (y,x)). + Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x). Proof. - Intros. - Inversion_clear H. - Apply Acc_intro. - NewDestruct 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. + 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: (x,y:A)(Acc A R x)->(Acc A R y) - ->(Acc A*A SwapProd (x,y)). + Lemma Acc_swapprod : + forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y). Proof. - NewInduction 1 as [x0 _ IHAcc0];Intros H2. - Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)). - Clear IHAcc0. - NewInduction H2 as [x1 _ IHAcc1]; Intros H4. - Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)). - Clear IHAcc1. - Intro. - Apply Acc_intro. - NewDestruct 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. + 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 A R)->(well_founded A*A SwapProd). + Lemma wf_swapprod : well_founded R -> well_founded SwapProd. Proof. - Red. - NewDestruct a;Intros. - Apply Acc_swapprod;Auto with sets. + red in |- *. + destruct a; intros. + apply Acc_swapprod; auto with sets. Qed. -End Swap. +End Swap.
\ No newline at end of file |