Require Export Definitions.
Implicit Types x y z : var.
Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.

Lemma int_O U : U * OMEGA = U.
now destruct U. Qed.

Lemma int_comm_O U : U * OMEGA = OMEGA * U.
now destruct U. Qed.

Lemma int_eq_O U V : U * V = OMEGA -> U = OMEGA /\ V = OMEGA.
now destruct U, V. Qed.

Lemma te_refl U : U == U.
Proof with auto.
induction U... induction A... Qed.

Lemma te_sym U V : U == V -> V == U.
induction 1 ; eauto.
Qed.

Lemma te_trans U V W : U == V -> V == W -> U == W.
destruct U as [A|], V as [B|], W as [C|] ; eauto.
  - inversion 2.
  - inversion 1.
  - inversion 1.
Qed.

Hint Resolve te_refl te_sym te_trans.

Instance te_equiv : Equivalence type_equiv.
constructor ; eauto.
Qed.

Lemma te_inv_OMEGA U : U == OMEGA -> U = OMEGA.
now inversion 1. Qed.

Lemma te_inv_A {U A} : U == A -> exists B, U = B.
revert U A.
cut (forall U V, U == V -> (exists A, V = A) -> exists B, U = B) ; eauto.
induction 1 ; eauto.
Qed.

Lemma te_O_l U V : (U * V) == OMEGA -> U == OMEGA.
destruct U, V ; inversion 1 ; auto.
Qed.

Lemma te_O_r U V : (U * V) == OMEGA -> V == OMEGA.
destruct U, V ; inversion 1 ; auto.
Qed.

Hint Resolve te_O_l te_O_r.

Lemma te_inv_F U F : U == F -> U = F.
cut (forall V, type_equiv U V -> V = F -> U = F) ; eauto.
induction 1 ; auto ; discriminate.
Qed.

Hint Resolve te_inv_OMEGA te_inv_F.

Lemma te_comp_int_l U U' V : U == U' -> U * V == U' * V.
induction 1 ; destruct V ; simpl ; eauto.
Qed.

Lemma te_comp_int_r U V V' : V == V' -> U * V == U * V'.
induction 1 ; destruct U ; simpl ; eauto.
Qed.

Lemma te_comp_int U U' V V' : U == U' -> V == V' -> (U * V) == (U' * V').
eauto using te_comp_int_l, te_comp_int_r.
Qed.

Instance te_Proper_int : Proper (type_equiv ==> type_equiv ==> type_equiv) int.
cbv ; eauto using te_comp_int.
Qed.

Lemma te_comm_int U V : U * V == V * U.
destruct U, V ; simpl ; auto.
Qed.

Lemma te_assoc_int U V W : (U * V) * W == U * (V * W).
destruct U, V, W ; simpl ; auto.
Qed.

Hint Immediate te_comm_int.
Hint Resolve te_assoc_int te_comp_int_l te_comp_int_r.

Fixpoint count A : nat :=
 match A with
 | Int A B => S (count A + count B)
 | _ => 0
 end.

Definition tcount U : nat :=
 match U with
 | UpI A => count A
 | _ => 0
 end.

Lemma te_tcount_stable U V : U == V -> tcount U = tcount V.
induction 1 ; simpl in * ; omega.
Qed.

Lemma te_inv U V : U * V == U -> V = OMEGA.
intros e.
assert (tcount (U * V) = tcount U).
{ now apply te_tcount_stable. }
destruct V, U ; simpl in * ; auto.
Qed.

Hint Resolve te_inv.