Some Properties of Well-foundation |
Require Import List.
| Accessible => no direct cycles |
Lemma well_foundation1:
forall (A: Set) (R: A -> A -> Prop) (x: A),
(Acc R x) ->
forall (y: A),
(R x y) ->
(R y x) -> False.
| Well-founded => no direct cycles |
Lemma well_foundation2:
forall (A: Set) (R: A -> A -> Prop),
(well_founded R) ->
forall (x y: A),
(R x y) ->
(R y x) -> False.
| Function extension of a binary relation |
Definition fun_extension (A B: Set) (f: A -> B) (R: B -> B -> Prop) (x y: A): Prop :=
(R (f x) (f y))
.
| accessible interpretation |
Lemma well_foundation3:
forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),
forall (x: B),
(Acc R x) ->
forall (x': A),
(x = (f x')) ->
(Acc (fun_extension A B f R) x')
.
| Well-founded interpretation |
Lemma well_foundation4:
forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),
(well_founded R) ->
(well_founded (fun_extension A B f R))
.