Library UniMath.MoreFoundations.Tactics

Require Import UniMath.Foundations.All.

A version of "easy" specialized for the needs of UniMath. This tactic is supposed to be simple and predictable. The goal is to use it to finish "trivial" goals
Ltac easy :=
  trivial; intros; solve
   [ repeat (solve [trivial | apply pathsinv0; trivial] || split)
   | match goal with | H : |- _induction H end
   | match goal with | H : ¬ _ |- _induction H; trivial end
   | match goal with | H : _ |- _induction H; trivial end
   | match goal with | H : _ _ |- _induction H; trivial end ].

Override the Coq now tactic so that it uses unimath_easy instead
Tactic Notation "now" tactic(t) := t; easy.

Ltac hSet_induction f e := generalize f; apply hSet_rect; intro e; clear f.

Ltac show_id_type := match goal with |- @paths ?ID _ _set (TYPE := ID); simpl in TYPE end.

Require Import UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom.

Definition post_cat {X} {x y z:X} {p:y = z} : x = y x = z.
Proof. intros q. exact (pathscomp0 q p). Defined.

Definition pre_cat {X} {x y z:X} {p:x = y} : y = z x = z.
Proof. intros q. exact (pathscomp0 p q). Defined.

Ltac maponpaths_pre_post_cat :=
  repeat rewrite path_assoc; repeat apply (maponpaths post_cat); repeat rewrite <- path_assoc;
  repeat apply (maponpaths pre_cat); repeat rewrite path_assoc; repeat rewrite maponpathsinv0;
  try reflexivity.

Ltac prop_logic :=
  abstract (intros; simpl;
            repeat (try (apply isapropdirprod);try (apply isapropishinh);apply impred ;intro);
            try (apply isapropiscontr); try assumption) using _L_.

Lemma iscontrweqb' {X Y} (is:iscontr Y) (w:X Y) : iscontr X.
Proof. intros. apply (iscontrweqb (Y:=Y)). assumption. assumption. Defined.

Ltac intermediate_iscontr Y' := apply (iscontrweqb (Y := Y')).
Ltac intermediate_iscontr' Y' := apply (iscontrweqb' (Y := Y')).

Ltac isaprop_goal x :=
  let G := match goal with |- ?Gconstr:(G) end in
  assert (x : isaprop(G)).

Definition isaprop_goal X (ig:isaprop X) (f:isaprop X X) : X.
Proof. intros. exact (f ig). Defined.

Ltac isaset_goal x :=
  let G := match goal with |- ?Gconstr:(G) end in
  assert (x : isaset(G)).