Set Implicit Arguments.

Require Import SN.
Require Import RelUtil.

Section lexp.

Variable (A : Type) (gtA eqA : relation A) (Hcomp : eqA @ gtA << gtA).

Lemma SN_compat : ∀ a, SN gtA a → ∀ a', eqA a a' → SN gtA a'.

Proof.
intros a SN_a a' eqaa'. apply SN_intro. intros a'' gta'a''.
inversion SN_a. apply H. apply (incl_elim Hcomp). ∃ a'. auto.
Qed.

Variable (B : Type) (gtB : relation B).

Inductive lexp : relation (prod A B) :=
| lexp1 : ∀ a a' b b', gtA a a' → lexp (a,b) (a',b')
| lexp2 : ∀ a a' b b', eqA a a' → gtB b b' → lexp (a,b) (a',b').

Lemma lexp_intro : ∀ a a' b b',
  gtA a a' ∨ (eqA a a' ∧ gtB b b') → lexp (a,b) (a',b').

Proof.
intros. destruct H. apply lexp1. exact H. destruct H. apply lexp2.
exact H. exact H0.
Qed.

Variable (WF_gtB : WF gtB) (eqA_trans : transitive eqA).

Lemma lexp_SN_eq : ∀ a b,
  SN lexp (a,b) → ∀ a', eqA a a' → SN lexp (a',b).

Proof.
intros a b SN_ab a' eqaa'. inversion SN_ab. apply SN_intro.
destruct y as (a'',b'). intro H'. inversion H'; subst a'0 b'0 a0 b0; apply H.
apply lexp1. apply (incl_elim Hcomp). ∃ a'. auto.
apply lexp2. apply (eqA_trans eqaa' H4). exact H6.
Qed.

Lemma lexp_SN :
  ∀ a, SN gtA a → ∀ b, SN gtB b → SN lexp (a, b).

Proof.
induction 1 as [a Ha1 Ha2]. induction 1 as [b Hb1 Hb2]. apply SN_intro.
destruct y as (a'',b'). intro H. inversion H; subst a'' b'0 a0 b0.
apply Ha2. exact H1. apply WF_gtB.
apply (@lexp_SN_eq a). 2: exact H3. apply Hb2. exact H5.
Qed.

Variable WF_gtA : WF gtA.

Lemma WF_lexp : WF lexp.

Proof.
unfold WF. destruct x as (a,b). apply lexp_SN. apply WF_gtA. apply WF_gtB.
Qed.

End lexp.

Section lex.

Variable (A : Type) (gtA eqA gtA' : relation A)
  (eqA_trans : transitive eqA) (Hcomp : eqA @ gtA << gtA)
  (WF_gtA : WF gtA) (WF_gtA' : WF gtA').

Definition lex x y := lexp gtA eqA gtA' (x,x) (y,y).

Lemma WF_lex : WF lex.

Proof.
exact (WF_inverse (fun x:A ⇒ (x,x)) (WF_lexp Hcomp WF_gtA' eqA_trans WF_gtA)).
Qed.

End lex.

Section lex'.

Variable (A : Type) (gt1 gt2 : relation A)
  (WF_gt1 : WF gt1) (WF_gt2 : WF gt2)
  (trans_gt2 : transitive gt2) (Hcomp : gt2 @ gt1 << gt1).

Definition lex' := lex gt1 gt2 gt2.

Lemma WF_lex' : WF lex'.

Proof.
unfold lex'. apply WF_lex; assumption.
Qed.

Lemma lex'_intro : gt1 U gt2 << lex'.

Proof.
unfold lex', lex, inclusion. intros. apply lexp_intro. destruct H; auto.

Qed.

End lex'.