HoTT + Ltac + typeclasses implementation of a split_sig tactic

hott_ltac_split_sig.v

(* Coq's build in tactics don't work so well with things like [iff]
   so split them up into multiple hypotheses *)
Ltac split_in_context ident funl funr :=
  repeat match goal with
           | [ H : context p [ident] |- _ ] =>
            let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (apply H);
            let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (apply H);
            clear H
         end.
 
Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a).
 
Ltac split_and' :=
  repeat match goal with
           | [ H : ?a /\ ?b |- _ ] => destruct H
         end.
Ltac split_and := split_and'; split_in_context and (fun a b : Type => a) (fun a b : Type => b).
 
 
 
 
 

Require Import HoTT.Overture HoTT.types.Sigma HoTT.Equivalences HoTT.types.Forall.

Local Open Scope equiv_scope.

Class can_transform A B := do_transform : A <~> B.

Instance can_transform_sigT_base {A} {P : A -> Type}
: can_transform (sigT P) (sigT P) | 0
  := BuildEquiv _ _ idmap _.

Instance can_transform_sigT `{Funext} {A B B' C'}
         `{H' : forall x : A, can_transform (B x) (@sigT (B' x) (C' x))}
: can_transform (forall x : A, B x)
                (@sigT (forall x, B' x) (fun b => forall x, C' x (b x))) | 0
  := @transitivity
       _ Equiv _ _ _ _
       (@equiv_functor_forall_id _ A B _ H')
       (@symmetry _ Equiv _ _ _ (@equiv_sigT_corect _ A _ C')).

Ltac split_sig' :=
  match goal with
    | [ H : _ |- _ ]
      => let term := constr:(eissect (@do_transform _ _ _) H) in
         generalize term;
           match goal with
             | [ |- ?f (?g H) = H -> _ ] => generalize (g H)
           end;
           intros [? ?] [];
           clear H
  end;
  simpl;
  unfold compose, equiv_functor_forall_id, functor_forall, isequiv_functor_forall;
  simpl.

Ltac split_sig := repeat split_sig'.