Union.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Author: Bruno Barras

Require Import Relation_Operators.
Require Import Relation_Definitions.
Require Import Transitive_Closure.

Section WfUnion.
  Variable A : Type.
  Variables R1 R2 : relation A.

  Notation Union := (union A R1 R2).

  Remark strip_commut :
    commut A R1 R2 ->
    forall x y:A,
      clos_trans A R1 y x ->
      forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.A:Type
R1, R2:relation A
commut A R1 R2 ->
forall x y : A,
clos_trans A R1 y x ->
forall z : A,
R2 z y ->
exists2 y' : A, R2 y' x & clos_trans A R1 z y'
  Proof.A:Type
R1, R2:relation A
commut A R1 R2 ->
forall x y : A,
clos_trans A R1 y x ->
forall z : A,
R2 z y ->
exists2 y' : A, R2 y' x & clos_trans A R1 z y'
    induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
x, y:A
H0:R1 x y
z:A
H1:R2 z x
exists2 y' : A, R2 y' y & clos_trans A R1 z y'
A:Type
R1, R2:relation A
H:commut A R1 R2
x, y, z:A
H0:clos_trans A R1 x y
H1:clos_trans A R1 y z
IH1:forall z1 : A, R2 z1 x -> exists2 y' : A, R2 y' y & clos_trans A R1 z1 y'
IH2:forall z1 : A, R2 z1 y -> exists2 y' : A, R2 y' z & clos_trans A R1 z1 y'
z0:A
H2:R2 z0 x
exists2 y' : A, R2 y' z & clos_trans A R1 z0 y'
    -A:Type
R1, R2:relation A
H:commut A R1 R2
x, y:A
H0:R1 x y
z:A
H1:R2 z x
exists2 y' : A, R2 y' y & clos_trans A R1 z y' elim H with y x z; auto with sets; intros x0 H2 H3.A:Type
R1, R2:relation A
H:commut A R1 R2
x, y:A
H0:R1 x y
z:A
H1:R2 z x
x0:A
H2:R2 x0 y
H3:R1 z x0
exists2 y' : A, R2 y' y & clos_trans A R1 z y'
      exists x0; auto with sets.

    -A:Type
R1, R2:relation A
H:commut A R1 R2
x, y, z:A
H0:clos_trans A R1 x y
H1:clos_trans A R1 y z
IH1:forall z1 : A, R2 z1 x -> exists2 y' : A, R2 y' y & clos_trans A R1 z1 y'
IH2:forall z1 : A, R2 z1 y -> exists2 y' : A, R2 y' z & clos_trans A R1 z1 y'
z0:A
H2:R2 z0 x
exists2 y' : A, R2 y' z & clos_trans A R1 z0 y' elim IH1 with z0; auto with sets; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
x, y, z:A
H0:clos_trans A R1 x y
H1:clos_trans A R1 y z
IH1:forall z1 : A, R2 z1 x -> exists2 y' : A, R2 y' y & clos_trans A R1 z1 y'
IH2:forall z1 : A, R2 z1 y -> exists2 y' : A, R2 y' z & clos_trans A R1 z1 y'
z0:A
H2:R2 z0 x
x0:A
H3:R2 x0 y
H4:clos_trans A R1 z0 x0
exists2 y' : A, R2 y' z & clos_trans A R1 z0 y'
      elim IH2 with x0; auto with sets; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
x, y, z:A
H0:clos_trans A R1 x y
H1:clos_trans A R1 y z
IH1:forall z1 : A, R2 z1 x -> exists2 y' : A, R2 y' y & clos_trans A R1 z1 y'
IH2:forall z1 : A, R2 z1 y -> exists2 y' : A, R2 y' z & clos_trans A R1 z1 y'
z0:A
H2:R2 z0 x
x0:A
H3:R2 x0 y
H4:clos_trans A R1 z0 x0
x1:A
H5:R2 x1 z
H6:clos_trans A R1 x0 x1
exists2 y' : A, R2 y' z & clos_trans A R1 z0 y'
      exists x1; auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
x, y, z:A
H0:clos_trans A R1 x y
H1:clos_trans A R1 y z
IH1:forall z1 : A, R2 z1 x -> exists2 y' : A, R2 y' y & clos_trans A R1 z1 y'
IH2:forall z1 : A, R2 z1 y -> exists2 y' : A, R2 y' z & clos_trans A R1 z1 y'
z0:A
H2:R2 z0 x
x0:A
H3:R2 x0 y
H4:clos_trans A R1 z0 x0
x1:A
H5:R2 x1 z
H6:clos_trans A R1 x0 x1
clos_trans A R1 z0 x1
      apply t_trans with x0; auto with sets.
  Qed.


  Lemma Acc_union :
    commut A R1 R2 ->
    (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.A:Type
R1, R2:relation A
commut A R1 R2 ->
(forall x : A, Acc R2 x -> Acc R1 x) ->
forall a : A, Acc R2 a -> Acc Union a
  Proof.A:Type
R1, R2:relation A
commut A R1 R2 ->
(forall x : A, Acc R2 x -> Acc R1 x) ->
forall a : A, Acc R2 a -> Acc Union a
    induction 3 as [x H1 H2].A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y : A, R2 y x -> Acc R2 y
H2:forall y : A, R2 y x -> Acc Union y
Acc Union x
    apply Acc_intro; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
Acc Union y
    elim H3; intros; auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc Union y
    cut (clos_trans A R1 y x); auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
clos_trans A R1 y x -> Acc Union y
    elimtype (Acc (clos_trans A R1) y); intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y0 : A,
clos_trans A R1 y0 x0 -> Acc (clos_trans A R1) y0
H6:forall y0 : A,
clos_trans A R1 y0 x0 ->
clos_trans A R1 y0 x -> Acc Union y0
H7:clos_trans A R1 x0 x
Acc Union x0
A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc (clos_trans A R1) y
    -A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y0 : A,
clos_trans A R1 y0 x0 -> Acc (clos_trans A R1) y0
H6:forall y0 : A,
clos_trans A R1 y0 x0 ->
clos_trans A R1 y0 x -> Acc Union y0
H7:clos_trans A R1 x0 x
Acc Union x0 apply Acc_intro; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
Acc Union y0
      elim H8; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R1 y0 x0
Acc Union y0
A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
Acc Union y0
      +A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R1 y0 x0
Acc Union y0 apply H6; auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R1 y0 x0
clos_trans A R1 y0 x
        apply t_trans with x0; auto with sets.

      +A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x1 : A, Acc R2 x1 -> Acc R1 x1
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
Acc Union y0 elim strip_commut with x x0 y0; auto with sets; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x2 : A, Acc R2 x2 -> Acc R1 x2
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
x1:A
H10:R2 x1 x
H11:clos_trans A R1 y0 x1
Acc Union y0
        apply Acc_inv_trans with x1; auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x2 : A, Acc R2 x2 -> Acc R1 x2
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
x1:A
H10:R2 x1 x
H11:clos_trans A R1 y0 x1
clos_trans A Union y0 x1
        unfold union.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x2 : A, Acc R2 x2 -> Acc R1 x2
x:A
H1:forall y1 : A, R2 y1 x -> Acc R2 y1
H2:forall y1 : A, R2 y1 x -> Acc Union y1
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y1 : A,
clos_trans A R1 y1 x0 -> Acc (clos_trans A R1) y1
H6:forall y1 : A,
clos_trans A R1 y1 x0 ->
clos_trans A R1 y1 x -> Acc Union y1
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
x1:A
H10:R2 x1 x
H11:clos_trans A R1 y0 x1
clos_trans A (fun x2 y1 : A => R1 x2 y1 \/ R2 x2 y1)
  y0 x1
        elim H11; auto with sets; intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x3 : A, Acc R2 x3 -> Acc R1 x3
x:A
H1:forall y2 : A, R2 y2 x -> Acc R2 y2
H2:forall y2 : A, R2 y2 x -> Acc Union y2
y:A
H3:Union y x
H4:R1 y x
x0:A
H5:forall y2 : A,
clos_trans A R1 y2 x0 -> Acc (clos_trans A R1) y2
H6:forall y2 : A,
clos_trans A R1 y2 x0 ->
clos_trans A R1 y2 x -> Acc Union y2
H7:clos_trans A R1 x0 x
y0:A
H8:Union y0 x0
H9:R2 y0 x0
x1:A
H10:R2 x1 x
H11:clos_trans A R1 y0 x1
x2, y1, z:A
H12:clos_trans A R1 x2 y1
H13:clos_trans A (fun x3 y2 : A => R1 x3 y2 \/ R2 x3 y2) x2 y1
H14:clos_trans A R1 y1 z
H15:clos_trans A (fun x3 y2 : A => R1 x3 y2 \/ R2 x3 y2) y1 z
clos_trans A (fun x3 y2 : A => R1 x3 y2 \/ R2 x3 y2)
  x2 z
        apply t_trans with y1; auto with sets.

    -A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc (clos_trans A R1) y apply (Acc_clos_trans A).A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc R1 y
      apply Acc_inv with x; auto with sets.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc R1 x
      apply H0.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall x0 : A, Acc R2 x0 -> Acc R1 x0
x:A
H1:forall y0 : A, R2 y0 x -> Acc R2 y0
H2:forall y0 : A, R2 y0 x -> Acc Union y0
y:A
H3:Union y x
H4:R1 y x
Acc R2 x
      apply Acc_intro; auto with sets.
  Qed.


  Theorem wf_union :
    commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.A:Type
R1, R2:relation A
commut A R1 R2 ->
well_founded R1 ->
well_founded R2 -> well_founded Union
  Proof.A:Type
R1, R2:relation A
commut A R1 R2 ->
well_founded R1 ->
well_founded R2 -> well_founded Union
    unfold well_founded.A:Type
R1, R2:relation A
commut A R1 R2 ->
(forall a : A, Acc R1 a) ->
(forall a : A, Acc R2 a) -> forall a : A, Acc Union a
    intros.A:Type
R1, R2:relation A
H:commut A R1 R2
H0:forall a0 : A, Acc R1 a0
H1:forall a0 : A, Acc R2 a0
a:A
Acc Union a
    apply Acc_union; auto with sets.
  Qed.

End WfUnion.