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

Authors: Bruno Barras, Cristina Cornes

Require Import Eqdep.
Require Import Relation_Operators.
Require Import Transitive_Closure.

From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355

Section WfLexicographic_Product.
  Variable A : Type.
  Variable B : A -> Type.
  Variable leA : A -> A -> Prop.
  Variable leB : forall x:A, B x -> B x -> Prop.

  Notation LexProd := (lexprod A B leA leB).

  Lemma acc_A_B_lexprod :
    forall x:A,
      Acc leA x ->
      (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
      forall y:B x, Acc (leB x) y -> Acc LexProd (existT B x y).A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x : A, B x -> B x -> Prop
forall x : A,
Acc leA x ->
(forall x0 : A,
 clos_trans A leA x0 x -> well_founded (leB x0)) ->
forall y : B x,
Acc (leB x) y -> Acc LexProd (existT B x y)
  Proof.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x : A, B x -> B x -> Prop
forall x : A,
Acc leA x ->
(forall x0 : A,
 clos_trans A leA x0 x -> well_founded (leB x0)) ->
forall y : B x,
Acc (leB x) y -> Acc LexProd (existT B x y)
    induction 1 as [x _ IHAcc]; intros H2 y.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x0 : A, B x0 -> B x0 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x0 : A,
 clos_trans A leA x0 y0 ->
 well_founded (leB x0)) ->
forall y1 : B y0,
Acc (leB y0) y1 ->
Acc LexProd (existT B y0 y1)
H2:forall x0 : A,
clos_trans A leA x0 x -> well_founded (leB x0)
y:B x
Acc (leB x) y -> Acc LexProd (existT B x y)
    induction 1 as [x0 H IHAcc0]; intros.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x1 : A, B x1 -> B x1 -> Prop
x:A
IHAcc:forall y : A,
leA y x ->
(forall x1 : A,
 clos_trans A leA x1 y ->
 well_founded (leB x1)) ->
forall y0 : B y,
Acc (leB y) y0 -> Acc LexProd (existT B y y0)
H2:forall x1 : A,
clos_trans A leA x1 x -> well_founded (leB x1)
x0:B x
H:forall y : B x, leB x y x0 -> Acc (leB x) y
IHAcc0:forall y : B x,
leB x y x0 -> Acc LexProd (existT B x y)
Acc LexProd (existT B x x0)
    apply Acc_intro.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x1 : A, B x1 -> B x1 -> Prop
x:A
IHAcc:forall y : A,
leA y x ->
(forall x1 : A,
 clos_trans A leA x1 y ->
 well_founded (leB x1)) ->
forall y0 : B y,
Acc (leB y) y0 -> Acc LexProd (existT B y y0)
H2:forall x1 : A,
clos_trans A leA x1 x -> well_founded (leB x1)
x0:B x
H:forall y : B x, leB x y x0 -> Acc (leB x) y
IHAcc0:forall y : B x,
leB x y x0 -> Acc LexProd (existT B x y)
forall y : {x : A & B x},
LexProd y (existT B x x0) -> Acc LexProd y
    destruct y as [x2 y1]; intro H6.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x1 : A, B x1 -> B x1 -> Prop
x:A
IHAcc:forall y : A,
leA y x ->
(forall x1 : A,
 clos_trans A leA x1 y ->
 well_founded (leB x1)) ->
forall y0 : B y,
Acc (leB y) y0 -> Acc LexProd (existT B y y0)
H2:forall x1 : A,
clos_trans A leA x1 x -> well_founded (leB x1)
x0:B x
H:forall y : B x, leB x y x0 -> Acc (leB x) y
IHAcc0:forall y : B x,
leB x y x0 -> Acc LexProd (existT B x y)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
Acc LexProd (existT B x2 y1)
    simple inversion H6; intro.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
Acc LexProd (existT B x2 y1)
A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1:A
y, y':B x1
H1:existT B x1 y = existT B x2 y1
H3:existT B x1 y' = existT B x x0
H0:leB x1 y y'
Acc LexProd (existT B x2 y1)
    -A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
Acc LexProd (existT B x2 y1) cut (leA x2 x); intros.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
Acc LexProd (existT B x2 y1)
A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
leA x2 x
      +A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
Acc LexProd (existT B x2 y1) apply IHAcc; auto with sets.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
forall x3 : A,
clos_trans A leA x3 x2 -> well_founded (leB x3)
A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
Acc (leB x2) y1
        *A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
forall x3 : A,
clos_trans A leA x3 x2 -> well_founded (leB x3) intros.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x4 : A, B x4 -> B x4 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x4 : A,
 clos_trans A leA x4 y0 ->
 well_founded (leB x4)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x4 : A,
clos_trans A leA x4 x -> well_founded (leB x4)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
x3:A
H5:clos_trans A leA x3 x2
well_founded (leB x3)
          apply H2.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x4 : A, B x4 -> B x4 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x4 : A,
 clos_trans A leA x4 y0 ->
 well_founded (leB x4)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x4 : A,
clos_trans A leA x4 x -> well_founded (leB x4)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
x3:A
H5:clos_trans A leA x3 x2
clos_trans A leA x3 x
          apply t_trans with x2; auto with sets.

        *A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
Acc (leB x2) y1 red in H2.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x ->
forall a : B x3, Acc (leB x3) a
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
Acc (leB x2) y1
          apply H2.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x ->
forall a : B x3, Acc (leB x3) a
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
H4:leA x2 x
clos_trans A leA x2 x
          auto with sets.

      +A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1, x':A
y:B x1
y':B x'
H1:existT B x1 y = existT B x2 y1
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
leA x2 x injection H1 as <- _.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x2 : A, B x2 -> B x2 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x2 : A,
 clos_trans A leA x2 y0 ->
 well_founded (leB x2)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x2 : A,
clos_trans A leA x2 x -> well_founded (leB x2)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x1:A
y1:B x1
H6:LexProd (existT B x1 y1) (existT B x x0)
x':A
y:B x1
y':B x'
H3:existT B x' y' = existT B x x0
H0:leA x1 x'
leA x1 x
        injection H3 as <- _; auto with sets.

    -A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1:A
y, y':B x1
H1:existT B x1 y = existT B x2 y1
H3:existT B x1 y' = existT B x x0
H0:leB x1 y y'
Acc LexProd (existT B x2 y1) rewrite <- H1.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x3 : A, B x3 -> B x3 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x3 : A,
 clos_trans A leA x3 y0 ->
 well_founded (leB x3)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x3 : A,
clos_trans A leA x3 x -> well_founded (leB x3)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
x1:A
y, y':B x1
H1:existT B x1 y = existT B x2 y1
H3:existT B x1 y' = existT B x x0
H0:leB x1 y y'
Acc LexProd (existT B x1 y)
      injection H3 as -> H3.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x1 : A, B x1 -> B x1 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x1 : A,
 clos_trans A leA x1 y0 ->
 well_founded (leB x1)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x1 : A,
clos_trans A leA x1 x -> well_founded (leB x1)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
y:B x
H1:existT B x y = existT B x2 y1
y':B x
H3:existT (fun x1 : A => B x1) x y' =
existT (fun x1 : A => B x1) x x0
H0:leB x y y'
Acc LexProd (existT B x y)
      apply IHAcc0.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x1 : A, B x1 -> B x1 -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
(forall x1 : A,
 clos_trans A leA x1 y0 ->
 well_founded (leB x1)) ->
forall y2 : B y0,
Acc (leB y0) y2 ->
Acc LexProd (existT B y0 y2)
H2:forall x1 : A,
clos_trans A leA x1 x -> well_founded (leB x1)
x0:B x
H:forall y0 : B x, leB x y0 x0 -> Acc (leB x) y0
IHAcc0:forall y0 : B x,
leB x y0 x0 -> Acc LexProd (existT B x y0)
x2:A
y1:B x2
H6:LexProd (existT B x2 y1) (existT B x x0)
y:B x
H1:existT B x y = existT B x2 y1
y':B x
H3:existT (fun x1 : A => B x1) x y' =
existT (fun x1 : A => B x1) x x0
H0:leB x y y'
leB x y x0
      elim inj_pair2 with A B x y' x0; assumption.
  Defined.

  Theorem wf_lexprod :
    well_founded leA ->
    (forall x:A, well_founded (leB x)) -> well_founded LexProd.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x : A, B x -> B x -> Prop
well_founded leA ->
(forall x : A, well_founded (leB x)) ->
well_founded LexProd
  Proof.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x : A, B x -> B x -> Prop
well_founded leA ->
(forall x : A, well_founded (leB x)) ->
well_founded LexProd
    intros wfA wfB; unfold well_founded.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x : A, B x -> B x -> Prop
wfA:well_founded leA
wfB:forall x : A, well_founded (leB x)
forall a : {x : A & B x}, Acc LexProd a
    destruct a.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x0 : A, B x0 -> B x0 -> Prop
wfA:well_founded leA
wfB:forall x0 : A, well_founded (leB x0)
x:A
b:B x
Acc LexProd (existT B x b)
    apply acc_A_B_lexprod; auto with sets; intros.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x0 : A, B x0 -> B x0 -> Prop
wfA:well_founded leA
wfB:forall x0 : A, well_founded (leB x0)
x:A
b:B x
Acc (leB x) b
    red in wfB.A:Type
B:A -> Type
leA:A -> A -> Prop
leB:forall x0 : A, B x0 -> B x0 -> Prop
wfA:well_founded leA
wfB:forall (x0 : A) (a : B x0), Acc (leB x0) a
x:A
b:B x
Acc (leB x) b
    auto with sets.
  Defined.


End WfLexicographic_Product.


Section Wf_Symmetric_Product.
  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.

  Notation Symprod := (symprod A B leA leB).

  Lemma Acc_symprod :
    forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
forall x : A,
Acc leA x ->
forall y : B, Acc leB y -> Acc Symprod (x, y)
  Proof.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
forall x : A,
Acc leA x ->
forall y : B, Acc leB y -> Acc Symprod (x, y)
    induction 1 as [x _ IHAcc]; intros y H2.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
forall y1 : B,
Acc leB y1 -> Acc Symprod (y0, y1)
y:B
H2:Acc leB y
Acc Symprod (x, y)
    induction H2 as [x1 H3 IHAcc1].A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
x:A
IHAcc:forall y : A,
leA y x ->
forall y0 : B,
Acc leB y0 -> Acc Symprod (y, y0)
x1:B
H3:forall y : B, leB y x1 -> Acc leB y
IHAcc1:forall y : B, leB y x1 -> Acc Symprod (x, y)
Acc Symprod (x, x1)
    apply Acc_intro; intros y H5.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
forall y1 : B,
Acc leB y1 -> Acc Symprod (y0, y1)
x1:B
H3:forall y0 : B, leB y0 x1 -> Acc leB y0
IHAcc1:forall y0 : B,
leB y0 x1 -> Acc Symprod (x, y0)
y:(A * B)%type
H5:Symprod y (x, x1)
Acc Symprod y
    inversion_clear H5; auto with sets.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
forall y1 : B,
Acc leB y1 -> Acc Symprod (y0, y1)
x1:B
H3:forall y0 : B, leB y0 x1 -> Acc leB y0
IHAcc1:forall y0 : B,
leB y0 x1 -> Acc Symprod (x, y0)
y:(A * B)%type
x0:A
H:leA x0 x
Acc Symprod (x0, x1)
    apply IHAcc; auto.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
x:A
IHAcc:forall y0 : A,
leA y0 x ->
forall y1 : B,
Acc leB y1 -> Acc Symprod (y0, y1)
x1:B
H3:forall y0 : B, leB y0 x1 -> Acc leB y0
IHAcc1:forall y0 : B,
leB y0 x1 -> Acc Symprod (x, y0)
y:(A * B)%type
x0:A
H:leA x0 x
Acc leB x1
    apply Acc_intro; trivial.
  Defined.


  Lemma wf_symprod :
    well_founded leA -> well_founded leB -> well_founded Symprod.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
well_founded leA ->
well_founded leB -> well_founded Symprod
  Proof.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
well_founded leA ->
well_founded leB -> well_founded Symprod
    red.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
well_founded leA ->
well_founded leB -> forall a : A * B, Acc Symprod a
    destruct a.A, B:Type
leA:A -> A -> Prop
leB:B -> B -> Prop
H:well_founded leA
H0:well_founded leB
a:A
b:B
Acc Symprod (a, b)
    apply Acc_symprod; auto with sets.
  Defined.

End Wf_Symmetric_Product.


Section Swap.

  Variable A : Type.
  Variable R : A -> A -> Prop.

  Notation SwapProd := (swapprod A R).


  Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x).A:Type
R:A -> A -> Prop
forall x y : A,
Acc SwapProd (x, y) -> Acc SwapProd (y, x)
  Proof.A:Type
R:A -> A -> Prop
forall x y : A,
Acc SwapProd (x, y) -> Acc SwapProd (y, x)
    intros.A:Type
R:A -> A -> Prop
x, y:A
H:Acc SwapProd (x, y)
Acc SwapProd (y, x)
    inversion_clear H.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
Acc SwapProd (y, x)
    apply Acc_intro.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
forall y0 : A * A,
SwapProd y0 (y, x) -> Acc SwapProd y0
    destruct y0; intros.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:SwapProd (a, a0) (y, x)
Acc SwapProd (a, a0)
    inversion_clear H; inversion_clear H1; apply H0.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a y
SwapProd (a, x) (x, y)
A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 x
SwapProd (y, a0) (x, y)
A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 y
SwapProd (x, a0) (x, y)
A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a x
SwapProd (a, y) (x, y)
    -A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a y
SwapProd (a, x) (x, y) apply sp_swap.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a y
symprod A A R R (x, a) (x, y)
      apply right_sym; auto with sets.

    -A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 x
SwapProd (y, a0) (x, y) apply sp_swap.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 x
symprod A A R R (a0, y) (x, y)
      apply left_sym; auto with sets.

    -A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 y
SwapProd (x, a0) (x, y) apply sp_noswap.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a0 y
symprod A A R R (x, a0) (x, y)
      apply right_sym; auto with sets.

    -A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a x
SwapProd (a, y) (x, y) apply sp_noswap.A:Type
R:A -> A -> Prop
x, y:A
H0:forall y0 : A * A,
SwapProd y0 (x, y) -> Acc SwapProd y0
a, a0:A
H:R a x
symprod A A R R (a, y) (x, y)
      apply left_sym; auto with sets.
  Defined.


  Lemma Acc_swapprod :
    forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).A:Type
R:A -> A -> Prop
forall x y : A,
Acc R x -> Acc R y -> Acc SwapProd (x, y)
  Proof.A:Type
R:A -> A -> Prop
forall x y : A,
Acc R x -> Acc R y -> Acc SwapProd (x, y)
    induction 1 as [x0 _ IHAcc0]; intros H2.A:Type
R:A -> A -> Prop
y, x0:A
IHAcc0:forall y0 : A,
R y0 x0 -> Acc R y -> Acc SwapProd (y0, y)
H2:Acc R y
Acc SwapProd (x0, y)
    cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).A:Type
R:A -> A -> Prop
y, x0:A
IHAcc0:forall y0 : A,
R y0 x0 -> Acc R y -> Acc SwapProd (y0, y)
H2:Acc R y
(forall y0 : A, R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
A:Type
R:A -> A -> Prop
y, x0:A
IHAcc0:forall y0 : A,
R y0 x0 -> Acc R y -> Acc SwapProd (y0, y)
H2:Acc R y
forall y0 : A, R y0 x0 -> Acc SwapProd (y0, y)
    -A:Type
R:A -> A -> Prop
y, x0:A
IHAcc0:forall y0 : A,
R y0 x0 -> Acc R y -> Acc SwapProd (y0, y)
H2:Acc R y
(forall y0 : A, R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y) clear IHAcc0.A:Type
R:A -> A -> Prop
y, x0:A
H2:Acc R y
(forall y0 : A, R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
      induction H2 as [x1 _ IHAcc1]; intros H4.A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y : A,
R y x1 ->
(forall y0 : A,
 R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
Acc SwapProd (x0, x1)
      cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y : A,
R y x1 ->
(forall y0 : A,
 R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
(forall y : A, R y x1 -> Acc SwapProd (x0, y)) ->
Acc SwapProd (x0, x1)
A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y : A,
R y x1 ->
(forall y0 : A,
 R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
forall y : A, R y x1 -> Acc SwapProd (x0, y)
      +A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y : A,
R y x1 ->
(forall y0 : A,
 R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
(forall y : A, R y x1 -> Acc SwapProd (x0, y)) ->
Acc SwapProd (x0, x1) clear IHAcc1.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
(forall y : A, R y x1 -> Acc SwapProd (x0, y)) ->
Acc SwapProd (x0, x1)
        intro.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
Acc SwapProd (x0, x1)
        apply Acc_intro.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
forall y : A * A,
SwapProd y (x0, x1) -> Acc SwapProd y
        destruct y; intro H5.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H5:SwapProd (a, a0) (x0, x1)
Acc SwapProd (a, a0)
        inversion_clear H5.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H0:symprod A A R R (a, a0) (x0, x1)
Acc SwapProd (a, a0)
A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H0:symprod A A R R (a0, a) (x0, x1)
Acc SwapProd (a, a0)
        *A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H0:symprod A A R R (a, a0) (x0, x1)
Acc SwapProd (a, a0) inversion_clear H0; auto with sets.

        *A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H0:symprod A A R R (a0, a) (x0, x1)
Acc SwapProd (a, a0) apply swap_Acc.A:Type
R:A -> A -> Prop
x0, x1:A
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
H:forall y : A, R y x1 -> Acc SwapProd (x0, y)
a, a0:A
H0:symprod A A R R (a0, a) (x0, x1)
Acc SwapProd (a0, a)
          inversion_clear H0; auto with sets.

      +A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y : A,
R y x1 ->
(forall y0 : A,
 R y0 x0 -> Acc SwapProd (y0, y)) ->
Acc SwapProd (x0, y)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
forall y : A, R y x1 -> Acc SwapProd (x0, y) intros.A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y0 : A,
R y0 x1 ->
(forall y1 : A,
 R y1 x0 -> Acc SwapProd (y1, y0)) ->
Acc SwapProd (x0, y0)
H4:forall y0 : A, R y0 x0 -> Acc SwapProd (y0, x1)
y:A
H:R y x1
Acc SwapProd (x0, y)
        apply IHAcc1; auto with sets; intros.A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y1 : A,
R y1 x1 ->
(forall y2 : A,
 R y2 x0 -> Acc SwapProd (y2, y1)) ->
Acc SwapProd (x0, y1)
H4:forall y1 : A, R y1 x0 -> Acc SwapProd (y1, x1)
y:A
H:R y x1
y0:A
H0:R y0 x0
Acc SwapProd (y0, y)
        apply Acc_inv with (y0, x1); auto with sets.A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y1 : A,
R y1 x1 ->
(forall y2 : A,
 R y2 x0 -> Acc SwapProd (y2, y1)) ->
Acc SwapProd (x0, y1)
H4:forall y1 : A, R y1 x0 -> Acc SwapProd (y1, x1)
y:A
H:R y x1
y0:A
H0:R y0 x0
SwapProd (y0, y) (y0, x1)
        apply sp_noswap.A:Type
R:A -> A -> Prop
x0, x1:A
IHAcc1:forall y1 : A,
R y1 x1 ->
(forall y2 : A,
 R y2 x0 -> Acc SwapProd (y2, y1)) ->
Acc SwapProd (x0, y1)
H4:forall y1 : A, R y1 x0 -> Acc SwapProd (y1, x1)
y:A
H:R y x1
y0:A
H0:R y0 x0
symprod A A R R (y0, y) (y0, x1)
        apply right_sym; auto with sets.

    -A:Type
R:A -> A -> Prop
y, x0:A
IHAcc0:forall y0 : A,
R y0 x0 -> Acc R y -> Acc SwapProd (y0, y)
H2:Acc R y
forall y0 : A, R y0 x0 -> Acc SwapProd (y0, y) auto with sets.
  Defined.


  Lemma wf_swapprod : well_founded R -> well_founded SwapProd.A:Type
R:A -> A -> Prop
well_founded R -> well_founded SwapProd
  Proof.A:Type
R:A -> A -> Prop
well_founded R -> well_founded SwapProd
    red.A:Type
R:A -> A -> Prop
well_founded R -> forall a : A * A, Acc SwapProd a
    destruct a; intros.A:Type
R:A -> A -> Prop
H:well_founded R
a, a0:A
Acc SwapProd (a, a0)
    apply Acc_swapprod; auto with sets.
  Defined.

End Swap.