diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 55 | ||||
| -rw-r--r-- | theories/Wellfounded/Inclusion.v | 32 | ||||
| -rw-r--r-- | theories/Wellfounded/Inverse_Image.v | 55 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 374 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 192 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 47 | ||||
| -rw-r--r-- | theories/Wellfounded/Union.v | 77 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 72 | ||||
| -rw-r--r-- | theories/Wellfounded/Wellfounded.v | 19 | ||||
| -rwxr-xr-x | theories/Wellfounded/intro.tex | 4 |
10 files changed, 927 insertions, 0 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v new file mode 100644 index 00000000..a3f16888 --- /dev/null +++ b/theories/Wellfounded/Disjoint_Union.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* 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: Disjoint_Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Cristina Cornes + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Require Import Relation_Operators. + +Section Wf_Disjoint_Union. +Variables A B : Set. +Variable leA : A -> A -> Prop. +Variable leB : B -> B -> Prop. + +Notation Le_AsB := (le_AsB A B leA leB). + +Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). +Proof. + induction 1. + apply Acc_intro; intros y H2. + inversion_clear H2. + auto with sets. +Qed. + +Lemma acc_B_sum : + well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). +Proof. + induction 2. + apply Acc_intro; intros y H3. + inversion_clear H3; auto with sets. + apply acc_A_sum; auto with sets. +Qed. + + +Lemma wf_disjoint_sum : + well_founded leA -> well_founded leB -> well_founded Le_AsB. +Proof. + intros. + unfold well_founded in |- *. + destruct a as [a| b]. + apply (acc_A_sum a). + apply (H a). + + apply (acc_B_sum H b). + apply (H0 b). +Qed. + +End Wf_Disjoint_Union.
\ No newline at end of file diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v new file mode 100644 index 00000000..1677659c --- /dev/null +++ b/theories/Wellfounded/Inclusion.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* 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: Inclusion.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Bruno Barras *) + +Require Import Relation_Definitions. + +Section WfInclusion. + Variable A : Set. + Variables R1 R2 : A -> A -> Prop. + + Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z. + Proof. + induction 2. + apply Acc_intro; auto with sets. + Qed. + + Hint Resolve Acc_incl. + + Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. + Proof. + unfold well_founded in |- *; auto with sets. + Qed. + +End WfInclusion.
\ No newline at end of file diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v new file mode 100644 index 00000000..f2cf1d2e --- /dev/null +++ b/theories/Wellfounded/Inverse_Image.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* 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: Inverse_Image.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Bruno Barras *) + +Section Inverse_Image. + + Variables A B : Set. + Variable R : B -> B -> Prop. + Variable f : A -> B. + + Let Rof (x y:A) : Prop := R (f x) (f y). + + Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x. + induction 1 as [y _ IHAcc]; intros x H. + apply Acc_intro; intros y0 H1. + apply (IHAcc (f y0)); try trivial. + rewrite H; trivial. + Qed. + + Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x. + intros; apply (Acc_lemma (f x)); trivial. + Qed. + + Theorem wf_inverse_image : well_founded R -> well_founded Rof. + red in |- *; intros; apply Acc_inverse_image; auto. + Qed. + + Variable F : A -> B -> Prop. + Let RoF (x y:A) : Prop := + exists2 b : B, F x b & (forall c:B, F y c -> R b c). + +Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x. +induction 1 as [x _ IHAcc]; intros x0 H2. +constructor; intros y H3. +destruct H3. +apply (IHAcc x1); auto. +Qed. + + +Theorem wf_inverse_rel : well_founded R -> well_founded RoF. + red in |- *; constructor; intros. + case H0; intros. + apply (Acc_inverse_rel x); auto. +Qed. + +End Inverse_Image. + diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v new file mode 100644 index 00000000..d8a4d37c --- /dev/null +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -0,0 +1,374 @@ +(************************************************************************) +(* 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_Exponentiation.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Cristina Cornes + + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Require Import Eqdep. +Require Import List. +Require Import Relation_Operators. +Require Import Transitive_Closure. + +Section Wf_Lexicographic_Exponentiation. +Variable A : Set. +Variable leA : A -> A -> Prop. + +Notation Power := (Pow A leA). +Notation Lex_Exp := (lex_exp A leA). +Notation ltl := (Ltl A leA). +Notation Descl := (Desc A leA). + +Notation List := (list A). +Notation Nil := (nil (A:=A)). +(* useless but symmetric *) +Notation Cons := (cons (A:=A)). +Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100). + +Hint Resolve d_one d_nil t_step. + +Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z. +Proof. + simple induction x. + simple induction z. + simpl in |- *; intros H. + inversion_clear H. + simpl in |- *; intros; apply (Lt_nil A leA). + intros a l HInd. + simpl in |- *. + intros. + inversion_clear H. + apply (Lt_hd A leA); auto with sets. + apply (Lt_tl A leA). + apply (HInd y y0); auto with sets. +Qed. + + +Lemma right_prefix : + forall x y z:List, + ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). +Proof. + intros x y; generalize x. + elim y; simpl in |- *. + right. + exists x0; auto with sets. + intros. + inversion H0. + left; apply (Lt_nil A leA). + left; apply (Lt_hd A leA); auto with sets. + generalize (H x1 z H3). + simple induction 1. + left; apply (Lt_tl A leA); auto with sets. + simple induction 1. + simple induction 1; intros. + rewrite H8. + right; exists x2; auto with sets. +Qed. + + + +Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x. +Proof. + intros. + inversion H. + generalize (app_cons_not_nil _ _ _ H1); simple induction 1. + cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets. + intro. + generalize (app_eq_unit _ _ H0). + simple induction 1; simple induction 1; intros. + rewrite H4; auto with sets. + discriminate H5. + generalize (app_inj_tail _ _ _ _ H0). + simple induction 1; intros. + rewrite <- H4; auto with sets. +Qed. + +Lemma desc_tail : + forall (x:List) (a b:A), + Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b. +Proof. + intro. + apply rev_ind with + (A := A) + (P := fun x:List => + forall a b:A, + Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b). + intros. + + inversion H. + cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil); + auto with sets; intro. + generalize H0. + intro. + generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4); + simple induction 1. + intros. + + generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. + generalize H1. + rewrite <- H10; rewrite <- H7; intro. + apply (t_step A leA); auto with sets. + + + + intros. + inversion H0. + generalize (app_cons_not_nil _ _ _ H3); intro. + elim H1. + + generalize H0. + generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b); + simple induction 1. + intro. + generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro. + generalize (H x0 b H6). + intro. + apply t_trans with (A := A) (y := x0); auto with sets. + + apply t_step. + generalize H1. + rewrite H4; intro. + + generalize (app_inj_tail _ _ _ _ H8); simple induction 1. + intros. + generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b). + intro. + generalize H10. + rewrite H12; intro. + generalize (app_inj_tail _ _ _ _ H13); simple induction 1. + intros. + rewrite <- H11; rewrite <- H16; auto with sets. +Qed. + + +Lemma dist_aux : + forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y. +Proof. + intros z D. + elim D. + intros. + cut (x ++ y = Nil); auto with sets; intro. + generalize (app_eq_nil _ _ H0); simple induction 1. + intros. + rewrite H2; rewrite H3; split; apply d_nil. + + intros. + cut (x0 ++ y = Cons x Nil); auto with sets. + intros E. + generalize (app_eq_unit _ _ E); simple induction 1. + simple induction 1; intros. + rewrite H2; rewrite H3; split. + apply d_nil. + + apply d_one. + + simple induction 1; intros. + rewrite H2; rewrite H3; split. + apply d_one. + + apply d_nil. + + do 5 intro. + intros Hind. + do 2 intro. + generalize x0. + apply rev_ind with + (A := A) + (P := fun y0:List => + forall x0:List, + (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 -> + Descl x0 /\ Descl y0). + + intro. + generalize (app_nil_end x1); simple induction 1; simple induction 1. + split. apply d_conc; auto with sets. + + apply d_nil. + + do 3 intro. + generalize x1. + apply rev_ind with + (A := A) + (P := fun l0:List => + forall (x1:A) (x0:List), + (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil -> + Descl x0 /\ Descl (l0 ++ Cons x1 Nil)). + + + simpl in |- *. + split. + generalize (app_inj_tail _ _ _ _ H2); simple induction 1. + simple induction 1; auto with sets. + + apply d_one. + do 5 intro. + generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)). + simple induction 1. + generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1. + intro E. + generalize (app_inj_tail _ _ _ _ E). + simple induction 1; intros. + generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. + rewrite <- H7; rewrite <- H10; generalize H6. + generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1. + rewrite E1. + intro. + generalize (Hind x4 (l1 ++ Cons x2 Nil) H11). + simple induction 1; split. + auto with sets. + + generalize H14. + rewrite <- H10; intro. + apply d_conc; auto with sets. +Qed. + + + +Lemma dist_Desc_concat : + forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y. +Proof. + intros. + apply (dist_aux (x ++ y) H x y); auto with sets. +Qed. + + +Lemma desc_end : + forall (a b:A) (x:List), + Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) -> + clos_trans A leA a b. + +Proof. + intros a b x. + case x. + simpl in |- *. + simple induction 1. + intros. + inversion H1; auto with sets. + inversion H3. + + simple induction 1. + generalize (app_comm_cons l (Cons a Nil) a0). + intros E; rewrite <- E; intros. + generalize (desc_tail l a a0 H0); intro. + inversion H1. + apply t_trans with (y := a0); auto with sets. + + inversion H4. +Qed. + + + + +Lemma ltl_unit : + forall (x:List) (a b:A), + Descl (x ++ Cons a Nil) -> + ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil). +Proof. + intro. + case x. + intros; apply (Lt_nil A leA). + + simpl in |- *; intros. + inversion_clear H0. + apply (Lt_hd A leA a b); auto with sets. + + inversion_clear H1. +Qed. + + +Lemma acc_app : + forall (x1 x2:List) (y1:Descl (x1 ++ x2)), + Acc Lex_Exp << x1 ++ x2, y1 >> -> + forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>. +Proof. + intros. + apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)). + auto with sets. + + unfold lex_exp in |- *; simpl in |- *; auto with sets. +Qed. + + +Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp. +Proof. + unfold well_founded at 2 in |- *. + simple induction a; intros x y. + apply Acc_intro. + simple induction y0. + unfold lex_exp at 1 in |- *; simpl in |- *. + apply rev_ind with + (A := A) + (P := fun x:List => + forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>). + intros. + inversion_clear H0. + + intro. + generalize (well_founded_ind (wf_clos_trans A leA H)). + intros GR. + apply GR with + (P := fun x0:A => + forall l:List, + (forall (x1:List) (y:Descl x1), + ltl x1 l -> Acc Lex_Exp << x1, y >>) -> + forall (x1:List) (y:Descl x1), + ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>). + intro; intros HInd; intros. + generalize (right_prefix x2 l (Cons x1 Nil) H1). + simple induction 1. + intro; apply (H0 x2 y1 H3). + + simple induction 1. + intro; simple induction 1. + clear H4 H2. + intro; generalize y1; clear y1. + rewrite H2. + apply rev_ind with + (A := A) + (P := fun x3:List => + forall y1:Descl (l ++ x3), + ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>). + intros. + generalize (app_nil_end l); intros Heq. + generalize y1. + clear y1. + rewrite <- Heq. + intro. + apply Acc_intro. + simple induction y2. + unfold lex_exp at 1 in |- *. + simpl in |- *; intros x4 y3. intros. + apply (H0 x4 y3); auto with sets. + + intros. + generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1). + simple induction 1. + intros. + generalize (desc_end x4 x1 l0 (conj H8 H5)); intros. + generalize y1. + rewrite <- (app_ass l l0 (Cons x4 Nil)); intro. + generalize (HInd x4 H9 (l ++ l0)); intros HInd2. + generalize (ltl_unit l0 x4 x1 H8 H5); intro. + generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2). + simple induction 1; intros. + generalize (H4 H12 H10); intro. + generalize (Acc_inv H14). + generalize (acc_app l l0 H12 H14). + intros f g. + generalize (HInd2 f); intro. + apply Acc_intro. + simple induction y3. + unfold lex_exp at 1 in |- *; simpl in |- *; intros. + apply H15; auto with sets. +Qed. + + +End Wf_Lexicographic_Exponentiation. 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 diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v new file mode 100644 index 00000000..2e9d497b --- /dev/null +++ b/theories/Wellfounded/Transitive_Closure.v @@ -0,0 +1,47 @@ +(************************************************************************) +(* 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: Transitive_Closure.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Bruno Barras *) + +Require Import Relation_Definitions. +Require Import Relation_Operators. + +Section Wf_Transitive_Closure. + Variable A : Set. + Variable R : relation A. + + Notation trans_clos := (clos_trans A R). + + Lemma incl_clos_trans : inclusion A R trans_clos. + red in |- *; auto with sets. + Qed. + + Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x. + induction 1 as [x0 _ H1]. + apply Acc_intro. + intros y H2. + induction H2; auto with sets. + apply Acc_inv with y; auto with sets. + Qed. + + Hint Resolve Acc_clos_trans. + + Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. + Proof. + induction 1 as [| x y]; auto with sets. + intro; apply Acc_inv with y; assumption. + Qed. + + Theorem wf_clos_trans : well_founded R -> well_founded trans_clos. + Proof. + unfold well_founded in |- *; auto with sets. + Qed. + +End Wf_Transitive_Closure.
\ No newline at end of file diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v new file mode 100644 index 00000000..8f31ce9f --- /dev/null +++ b/theories/Wellfounded/Union.v @@ -0,0 +1,77 @@ +(************************************************************************) +(* 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: Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Bruno Barras *) + +Require Import Relation_Operators. +Require Import Relation_Definitions. +Require Import Transitive_Closure. + +Section WfUnion. + Variable A : Set. + Variables R1 R2 : relation A. + + Notation Union := (union A R1 R2). + + Hint Resolve Acc_clos_trans wf_clos_trans. + +Remark strip_commut : + commut A R1 R2 -> + forall x y:A, + clos_trans A R1 y x -> + forall z:A, R2 z y -> exists2 y' : A, R2 y' x & clos_trans A R1 z y'. +Proof. + induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. + elim H with y x z; auto with sets; intros x0 H2 H3. + exists x0; auto with sets. + + elim IH1 with z0; auto with sets; intros. + elim IH2 with x0; auto with sets; intros. + exists x1; auto with sets. + apply t_trans with x0; auto with sets. +Qed. + + + Lemma Acc_union : + commut A R1 R2 -> + (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a. +Proof. + induction 3 as [x H1 H2]. + apply Acc_intro; intros. + elim H3; intros; auto with sets. + cut (clos_trans A R1 y x); auto with sets. + elimtype (Acc (clos_trans A R1) y); intros. + apply Acc_intro; intros. + elim H8; intros. + apply H6; auto with sets. + apply t_trans with x0; auto with sets. + + elim strip_commut with x x0 y0; auto with sets; intros. + apply Acc_inv_trans with x1; auto with sets. + unfold union in |- *. + elim H11; auto with sets; intros. + apply t_trans with y1; auto with sets. + + apply (Acc_clos_trans A). + apply Acc_inv with x; auto with sets. + apply H0. + apply Acc_intro; auto with sets. +Qed. + + + Theorem wf_union : + commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. +Proof. + unfold well_founded in |- *. + intros. + apply Acc_union; auto with sets. +Qed. + +End WfUnion.
\ No newline at end of file diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v new file mode 100644 index 00000000..4a20c518 --- /dev/null +++ b/theories/Wellfounded/Well_Ordering.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* 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: Well_Ordering.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Cristina Cornes. + From: Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) + +Require Import Eqdep. + +Section WellOrdering. +Variable A : Set. +Variable B : A -> Set. + +Inductive WO : Set := + sup : forall (a:A) (f:B a -> WO), WO. + + +Inductive le_WO : WO -> WO -> Prop := + le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f). + + +Theorem wf_WO : well_founded le_WO. +Proof. + unfold well_founded in |- *; intro. + apply Acc_intro. + elim a. + intros. + inversion H0. + apply Acc_intro. + generalize H4; generalize H1; generalize f0; generalize v. + rewrite H3. + intros. + apply (H v0 y0). + cut (f = f1). + intros E; rewrite E; auto. + symmetry in |- *. + apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). +Qed. + +End WellOrdering. + + +Section Characterisation_wf_relations. + +(** Wellfounded relations are the inverse image of wellordering types *) +(* in course of development *) + + +Variable A : Set. +Variable leA : A -> A -> Prop. + +Definition B (a:A) := {x : A | leA x a}. + +Definition wof : well_founded leA -> A -> WO A B. +Proof. + intros. + apply (well_founded_induction H (fun a:A => WO A B)); auto. + intros. + apply (sup A B x). + unfold B at 1 in |- *. + destruct 1 as [x0]. + apply (H1 x0); auto. +Qed. + +End Characterisation_wf_relations.
\ No newline at end of file diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v new file mode 100644 index 00000000..87c00b47 --- /dev/null +++ b/theories/Wellfounded/Wellfounded.v @@ -0,0 +1,19 @@ +(************************************************************************) +(* 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: Wellfounded.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +Require Export Disjoint_Union. +Require Export Inclusion. +Require Export Inverse_Image. +Require Export Lexicographic_Exponentiation. +Require Export Lexicographic_Product. +Require Export Transitive_Closure. +Require Export Union. +Require Export Well_Ordering. + diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex new file mode 100755 index 00000000..126071e2 --- /dev/null +++ b/theories/Wellfounded/intro.tex @@ -0,0 +1,4 @@ +\section{Well-founded relations}\label{Wellfounded} + +This library gives definitions and results about well-founded relations. + |