Library WellFoundation

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))
.

Index
This page has been generated by coqdoc