summaryrefslogtreecommitdiff
path: root/theories/Wellfounded
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r--theories/Wellfounded/Disjoint_Union.v2
-rw-r--r--theories/Wellfounded/Inclusion.v2
-rw-r--r--theories/Wellfounded/Inverse_Image.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v269
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v2
-rw-r--r--theories/Wellfounded/Transitive_Closure.v2
-rw-r--r--theories/Wellfounded/Union.v2
-rw-r--r--theories/Wellfounded/Well_Ordering.v2
-rw-r--r--theories/Wellfounded/Wellfounded.v2
9 files changed, 108 insertions, 177 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index c1a5f1b2..ee4329bd 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 2250aec1..d09c4112 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 551dd110..aa6fa6ee 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index fb3ef1be..dd9e4c98 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,8 +13,11 @@
Require Import List.
Require Import Relation_Operators.
+Require Import Operators_Properties.
Require Import Transitive_Closure.
+Import ListNotations.
+
Section Wf_Lexicographic_Exponentiation.
Variable A : Set.
Variable leA : A -> A -> Prop.
@@ -25,14 +28,11 @@ Section Wf_Lexicographic_Exponentiation.
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.
+ Lemma left_prefix : forall x y z : List, ltl (x ++ y) z -> ltl x z.
Proof.
simple induction x.
simple induction z.
@@ -50,8 +50,9 @@ Section Wf_Lexicographic_Exponentiation.
Lemma right_prefix :
- forall x y z:List,
- ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
+ 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.
@@ -70,172 +71,98 @@ Section Wf_Lexicographic_Exponentiation.
right; exists x2; auto with sets.
Qed.
- Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
+ Lemma desc_prefix : forall (x : List) (a : A), Descl (x ++ [a]) -> 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 using d_nil with sets.
- discriminate H5.
- generalize (app_inj_tail _ _ _ _ H0).
- simple induction 1; intros.
- rewrite <- H4; auto with sets.
+ - apply app_cons_not_nil in H1 as ().
+ - assert (x ++ [a] = [x0]) by auto with sets.
+ apply app_eq_unit in H0 as [(->, _)| (_, [=])].
+ auto using d_nil.
+ - apply app_inj_tail in H0 as (<-, _).
+ assumption.
Qed.
Lemma desc_tail :
- forall (x:List) (a b:A),
- Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
+ forall (x : List) (a b : A),
+ Descl (b :: x ++ [a]) -> clos_refl_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.
+ (P :=
+ fun x : List =>
+ forall a b : A, Descl (b :: x ++ [a]) -> clos_refl_trans A leA a b);
+ intros.
+ - inversion H.
+ assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets.
+ destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)/app_inj_tail, <-).
+ inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
+ - inversion H0.
+ + apply app_cons_not_nil in H3 as ().
+ + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0.
+ pose proof (H x0 b H0).
+ apply rt_trans with (y := x0); auto with sets.
+ enough (H5 : clos_refl A leA a x0)
+ by (inversion H5; subst; [ apply rt_step | apply rt_refl ];
+ assumption).
+ apply app_inj_tail in H1 as (H1, ->).
+ rewrite app_comm_cons in H1.
+ apply app_inj_tail in H1 as (_, <-).
+ assumption.
Qed.
Lemma dist_aux :
- forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y.
+ 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.
- 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.
+ induction D as [| | * H D Hind]; intros.
+ - assert (H0 : x ++ y = []) by auto with sets.
+ apply app_eq_nil in H0 as (->, ->).
+ split; apply d_nil.
+ - assert (E : x0 ++ y = [x]) by auto with sets.
+ apply app_eq_unit in E as [(->, ->)| (->, ->)].
+ + split.
+ apply d_nil.
+ apply d_one.
+ + split.
+ apply d_one.
+ apply d_nil.
+ - induction y0 using rev_ind in x0, H0 |- *.
+ + rewrite <- app_nil_end in H0.
+ rewrite <- H0.
+ split.
+ apply d_conc; auto with sets.
+ apply d_nil.
+ + induction y0 using rev_ind in x1, x0, H0 |- *.
+ * simpl.
+ split.
+ apply app_inj_tail in H0 as (<-, _). assumption.
+ apply d_one.
+ * rewrite <- 2!app_assoc_reverse in H0.
+ apply app_inj_tail in H0 as (H0, <-).
+ pose proof H0 as H0'.
+ apply app_inj_tail in H0' as (_, ->).
+ rewrite app_assoc_reverse in H0.
+ apply Hind in H0 as ().
+ split.
+ assumption.
+ apply d_conc; auto with sets.
Qed.
Lemma dist_Desc_concat :
- forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
+ 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.
+ forall (a b : A) (x : List),
+ Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] -> clos_trans A leA a b.
Proof.
intros a b x.
case x.
@@ -246,11 +173,11 @@ Section Wf_Lexicographic_Exponentiation.
inversion H3.
simple induction 1.
- generalize (app_comm_cons l (Cons a Nil) a0).
+ generalize (app_comm_cons l [a] 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.
+ eapply clos_rt_t; [ eassumption | apply t_step; assumption ].
inversion H4.
Qed.
@@ -259,9 +186,8 @@ Section Wf_Lexicographic_Exponentiation.
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).
+ forall (x : List) (a b : A),
+ Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b].
Proof.
intro.
case x.
@@ -276,9 +202,10 @@ Section Wf_Lexicographic_Exponentiation.
Lemma acc_app :
- forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
+ 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 >>.
+ 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 >>)).
@@ -297,8 +224,10 @@ Section Wf_Lexicographic_Exponentiation.
unfold lex_exp at 1; simpl.
apply rev_ind with
(A := A)
- (P := fun x:List =>
- forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>).
+ (P :=
+ fun x : List =>
+ forall (x0 : List) (y : Descl x0),
+ ltl x0 x -> Acc Lex_Exp << x0, y >>).
intros.
inversion_clear H0.
@@ -306,14 +235,15 @@ Section Wf_Lexicographic_Exponentiation.
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 >>).
+ (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 ++ [x0]) -> Acc Lex_Exp << x1, y >>).
intro; intros HInd; intros.
- generalize (right_prefix x2 l (Cons x1 Nil) H1).
+ generalize (right_prefix x2 l [x1] H1).
simple induction 1.
intro; apply (H0 x2 y1 H3).
@@ -324,9 +254,10 @@ Section Wf_Lexicographic_Exponentiation.
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 >>).
+ (P :=
+ fun x3 : List =>
+ forall y1 : Descl (l ++ x3),
+ ltl x3 [x1] -> Acc Lex_Exp << l ++ x3, y1 >>).
intros.
generalize (app_nil_end l); intros Heq.
generalize y1.
@@ -340,15 +271,15 @@ Section Wf_Lexicographic_Exponentiation.
apply (H0 x4 y3); auto with sets.
intros.
- generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1).
+ generalize (dist_Desc_concat l (l0 ++ [x4]) 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.
+ rewrite <- (app_assoc_reverse l l0 [x4]); 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).
+ generalize (dist_Desc_concat (l ++ l0) [x4] y2).
simple induction 1; intros.
generalize (H4 H12 H10); intro.
generalize (Acc_inv H14).
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 7e3035d0..0d8ed8dd 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 9e0b22f2..b76e9661 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index c5b2d53e..b2e8ea92 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 56b8f985..f8a17b56 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v
index 971c589e..a76d5e95 100644
--- a/theories/Wellfounded/Wellfounded.v
+++ b/theories/Wellfounded/Wellfounded.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-06 01:49:21 +0000