1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Transitive_Closure.v 9598 2007-02-06 19:45:52Z herbelin $ i*)
11
(** Author: Bruno Barras *)
13
Require Import Relation_Definitions.
14
Require Import Relation_Operators.
16
Section Wf_Transitive_Closure.
18
Variable R : relation A.
20
Notation trans_clos := (clos_trans A R).
22
Lemma incl_clos_trans : inclusion A R trans_clos.
23
red in |- *; auto with sets.
26
Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x.
27
induction 1 as [x0 _ H1].
30
induction H2; auto with sets.
31
apply Acc_inv with y; auto with sets.
34
Hint Resolve Acc_clos_trans.
36
Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
38
induction 1 as [| x y]; auto with sets.
39
intro; apply Acc_inv with y; assumption.
42
Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
44
unfold well_founded in |- *; auto with sets.
47
End Wf_Transitive_Closure.