Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import List.

Require Import base final_result.

Module Msorts <: term_sig.
Inductive iSorts : Set :=
 | U : iSorts
 | V : iSorts
 | V' : iSorts
 | W : iSorts
 | W': iSorts
 .

Definition Sorts := iSorts.
End Msorts.

Module Mpts <: pts_sig Msorts.
Import Msorts.
Inductive iAx : Sorts -> Sorts -> Prop :=
 | Ax0 : iAx U V
 | Ax1 : iAx U V'
 | Ax2 : iAx V W
 | Ax3 : iAx V' W'
.

Inductive iRel : Sorts -> Sorts -> Sorts -> Prop :=
 | Rel0 : iRel W W W
 | Rel1 : iRel W' W' W'
 | Rel2 : iRel V V U
 | Rel3 : iRel V' V' U.

Definition Ax := iAx.
Definition Rel := iRel.
End Mpts.

Module CE <: Theory Msorts Mpts.
Import Msorts Mpts.
Include Theory Msorts Mpts.

Hint Constructors iAx iRel.
Hint Unfold Ax Rel.

Definition PTSe_PiInj := forall Γ A B C D u, Γ ⊢e Π(A),B = Π(C),D : !u -> exists s, exists t, Rel s t u /\
 Γ ⊢e A = C : !s /\ A::Γ ⊢e B = D : !t.

Definition D1 := (λ[!V],#0)·!U. Lemma D1_ok : nil ⊢e D1 : !V.
change !V with !V[← !U]. unfold D1. econstructor.
econstructor. apply Rel0. eauto. constructor. intuition. econstructor. eauto.
constructor. eauto. exists !V. intuition. eauto.
Qed.

Lemma D1_typ : forall T, nil ⊢e D1 : T -> T ≡ !V.
intros. apply PTS_equiv_PTSe in H. unfold D1 in H. apply gen_app in H. destruct H as (A & B & ? & ? & ?).
apply gen_la in H0 as (s & t & u & D & h); decompose [and] h; clear h. apply PiInj in H0 as (? & ?).
apply gen_var in H4 as ( VV & ? & ?). destruct H7 as (VVV & ? & ?). inversion H8; subst; clear H8.
simpl in H4. apply Betac_trans with B [← !U]. trivial. change !V with !V[← !U]. eauto.
Qed.

Definition D2 := (λ[!V'],#0)·!U. Lemma D2_ok : nil ⊢e D2 : !V'.
change !V' with !V'[← !U]. unfold D2. econstructor.
econstructor. apply Rel1. intuition. constructor. intuition. eauto. constructor. eauto.
exists !V'; intuition. eauto.
Qed.

Lemma D2_typ : forall T, nil ⊢e D2 : T -> T ≡ !V'.
intros. apply PTS_equiv_PTSe in H. unfold D2 in H. apply gen_app in H. destruct H as (A & B & ? & ? & ?).
apply gen_la in H0 as (s & t & u & D & h); decompose [and] h; clear h. apply PiInj in H0 as (? & ?).
apply gen_var in H4 as ( VV & ? & ?). destruct H7 as (VVV & ? & ?). inversion H8; subst; clear H8.
simpl in H4. apply Betac_trans with B[← !U]. trivial. change !V' with !V'[← !U]. eauto.
Qed.

Lemma ze_pi_eq : nil ⊢e Π(D1),!U = Π(D2),!U : !U.
apply cTrans with (Π(!U),!U). eapply cPi_eq. apply Rel2.
change !U with #0[← !U]; change !V with !V[← !U]. unfold D1.
eapply cBeta. apply Rel0. intuition. constructor. intuition. eauto.
constructor. eauto. exists !V; intuition. intuition.
constructor. constructor. intuition. econstructor. apply D1_ok.

eapply cPi_eq. apply Rel3. apply cSym.
change !U with #0[← !U]; change !V' with !V'[← !U]. unfold D2.
eapply cBeta. apply Rel1. intuition. constructor; eauto. constructor; eauto.
exists !V'; intuition. eauto.
constructor. constructor. intuition. eauto.
Qed.

Lemma Dom_ce : forall s, nil ⊢e D1 = D2 : !s -> False.
intros.
assert (nil ⊢e D1 : !s). apply left_reflexivity in H; trivial.
assert (nil ⊢e D2 : !s). apply right_reflexivity in H; trivial.
apply D1_typ in H0. apply D2_typ in H1. apply conv_sort in H0; subst.
apply conv_sort in H1; discriminate.
Qed.

Lemma PTSe_dont_have_PiInj : ~ PTSe_PiInj .
intro. red in H.
destruct (H nil D1 !U D2 !U U ze_pi_eq) as (s & t & ? & ? & ?).
apply Dom_ce in H1.
trivial.
Qed.

End CE.