(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Section Inverse_Image.

  Variables A B : Type.
  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.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
forall y : B,
Acc R y -> forall x : A, y = f x -> Acc Rof x
  Proof.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
forall y : B,
Acc R y -> forall x : A, y = f x -> Acc Rof x
    induction 1 as [y _ IHAcc]; intros x H.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x0 y0 : A => R (f x0) (f y0):A -> A -> Prop
y:B
IHAcc:forall y0 : B,
R y0 y ->
forall x0 : A, y0 = f x0 -> Acc Rof x0
x:A
H:y = f x
Acc Rof x
    apply Acc_intro; intros y0 H1.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x0 y1 : A => R (f x0) (f y1):A -> A -> Prop
y:B
IHAcc:forall y1 : B,
R y1 y ->
forall x0 : A, y1 = f x0 -> Acc Rof x0
x:A
H:y = f x
y0:A
H1:Rof y0 x
Acc Rof y0
    apply (IHAcc (f y0)); try trivial.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x0 y1 : A => R (f x0) (f y1):A -> A -> Prop
y:B
IHAcc:forall y1 : B,
R y1 y ->
forall x0 : A, y1 = f x0 -> Acc Rof x0
x:A
H:y = f x
y0:A
H1:Rof y0 x
R (f y0) y
    rewrite H; trivial.
  Qed.

  Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
forall x : A, Acc R (f x) -> Acc Rof x
  Proof.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
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.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
well_founded R -> well_founded Rof
  Proof.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
well_founded R -> well_founded Rof
    red; 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.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x y : A =>
exists2 b : B,
  F x b & forall c : B, F y c -> R b c:A -> A -> Prop
forall b : B,
Acc R b -> forall x : A, F x b -> Acc RoF x
  Proof.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x y : A =>
exists2 b : B,
  F x b & forall c : B, F y c -> R b c:A -> A -> Prop
forall b : B,
Acc R b -> forall x : A, F x b -> Acc RoF x
    induction 1 as [x _ IHAcc]; intros x0 H2.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x1 y : A => R (f x1) (f y):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x1 y : A =>
exists2 b : B,
  F x1 b & forall c : B, F y c -> R b c:A -> A -> Prop
x:B
IHAcc:forall y : B,
R y x -> forall x1 : A, F x1 y -> Acc RoF x1
x0:A
H2:F x0 x
Acc RoF x0
    constructor; intros y H3.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x1 y0 : A => R (f x1) (f y0):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x1 y0 : A =>
exists2 b : B,
  F x1 b & forall c : B, F y0 c -> R b c:A -> A -> Prop
x:B
IHAcc:forall y0 : B,
R y0 x -> forall x1 : A, F x1 y0 -> Acc RoF x1
x0:A
H2:F x0 x
y:A
H3:RoF y x0
Acc RoF y
    destruct H3.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x2 y0 : A => R (f x2) (f y0):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x2 y0 : A =>
exists2 b : B,
  F x2 b & forall c : B, F y0 c -> R b c:A -> A -> Prop
x:B
IHAcc:forall y0 : B,
R y0 x -> forall x2 : A, F x2 y0 -> Acc RoF x2
x0:A
H2:F x0 x
y:A
x1:B
H:F y x1
H0:forall c : B, F x0 c -> R x1 c
Acc RoF y
    apply (IHAcc x1); auto.
  Qed.


  Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x y : A =>
exists2 b : B,
  F x b & forall c : B, F y c -> R b c:A -> A -> Prop
well_founded R -> well_founded RoF
  Proof.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y : A => R (f x) (f y):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x y : A =>
exists2 b : B,
  F x b & forall c : B, F y c -> R b c:A -> A -> Prop
well_founded R -> well_founded RoF
    red; constructor; intros.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x y0 : A => R (f x) (f y0):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x y0 : A =>
exists2 b : B,
  F x b & forall c : B, F y0 c -> R b c:A -> A -> Prop
H:well_founded R
a, y:A
H0:RoF y a
Acc RoF y
    case H0; intros.
A, B:Type
R:B -> B -> Prop
f:A -> B
Rof:=fun x0 y0 : A => R (f x0) (f y0):A -> A -> Prop
F:A -> B -> Prop
RoF:=fun x0 y0 : A =>
exists2 b : B,
  F x0 b & forall c : B, F y0 c -> R b c:A -> A -> Prop
H:well_founded R
a, y:A
H0:RoF y a
x:B
H1:F y x
H2:forall c : B, F a c -> R x c
Acc RoF y
    apply (Acc_inverse_rel x); auto.
  Qed.

End Inverse_Image.