ExtLib.Data.SigT

Require Coq.Classes.EquivDec.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Structures.EqDep.
Require Import ExtLib.Tactics.Injection.
Require Import ExtLib.Tactics.EqDep.
Require Import ExtLib.Tactics.TypeTac.

Set Implicit Arguments.
Set Strict Implicit.
Set Printing Universes.

Section type.
  Variable T : Type.
  Variable F : T -> Type.
  Variable ED : EquivDec.EqDec _ (@eq T).
  Variable tT : type T.
  Variable typF : forall x, type (F x).

  Global Instance type_sigT : type (sigT F) :=
  { equal := fun x y =>
    equal (projT1 x) (projT1 y) /\
    exists pf : projT1 y = projT1 x,
      equal (projT2 x) (match pf in _ = t return F t with
                          | eq_refl => projT2 y
                        end)
  ; proper := fun x => proper (projT1 x) /\ proper (projT2 x)
  }.

  Variable typeOkT : typeOk tT.
  Variable typOkF : forall x, typeOk (typF x).

  Global Instance typeOk_sigT : typeOk type_sigT.
  Proof.
    constructor.
    { destruct x; destruct y; intros. simpl in *. destruct H. destruct H0. subst.
      apply only_proper in H; [ | eauto with typeclass_instances ].
      apply only_proper in H0; [ | eauto with typeclass_instances ]. intuition. }
    { red. destruct x; intros. do 2 red in H.
      do 2 red; simpl in *. intuition.
      try solve [ apply equiv_prefl; eauto ].
      exists eq_refl.
      eapply Proper.preflexive; [ | eapply H1 ].
      eauto with typeclass_instances. }
    { red; destruct x; destruct y; intros; simpl in *.
      intuition. destruct H1; subst. exists eq_refl. symmetry; assumption. }
    { red; destruct x; destruct y; destruct z; intros; simpl in *; intuition.
      etransitivity; eauto.
      destruct H2; destruct H3; subst. exists eq_refl. etransitivity; eauto. }
  Qed.

  Global Instance proper_existT a b : proper a -> proper b -> proper (existT F a b).
  Proof.
    red; simpl. intuition.
  Qed.

  Global Instance proper_projT1 a : proper a -> proper (projT1 a).
  Proof.
    red; simpl. intuition.
  Qed.

  Global Instance proper_projT2 a : proper a -> proper (projT2 a).
  Proof.
    red; simpl. intuition.
  Qed.

End type.

Section injective.
  Variable T : Type.
  Variable F : T -> Type.
  Variable ED : EquivDec.EqDec _ (@eq T).

  Global Instance Injective_existT a b d
    : Injective (existT F a b = existT F a d) | 1.
  refine {| result := b = d |}.
  abstract (eauto using inj_pair2).
  Defined.

  Global Instance Injective_existT_dif a b c d
  : Injective (existT F a b = existT F c d) | 2.
  refine {| result := exists pf : c = a,
            b = match pf in _ = t return F t with
                  | eq_refl => d
                end |}.
  abstract (inversion 1; subst; exists eq_refl; auto).
  Defined.
End injective.

Lemma eq_sigT_rw
: forall T U F (a b : T) (pf : a = b) s,
    match pf in _ = x return @sigT U (F x) with
    | eq_refl => s
    end =
    @existT U (F b) (projT1 s)
            match pf in _ = x return F x (projT1 s) with
            | eq_refl => (projT2 s)
            end.
Proof. destruct pf. destruct s; reflexivity. Qed.

Hint Rewrite eq_sigT_rw : eq_rw.