Library UniMath.MoreFoundations.Tactics
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 ].
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.
Show proof.
Definition pre_cat {X} {x y z:X} {p:x = y} : y = z -> x = z.
Show proof.
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.
Show proof.
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 |- ?G => constr:(G) end in
assert (x : isaprop(G)).
Definition isaprop_goal X (ig:isaprop X) (f:isaprop X -> X) : X.
Show proof.
Ltac isaset_goal x :=
let G := match goal with |- ?G => constr:(G) end in
assert (x : isaset(G)).
Ltac split3 := split; [| split].
Ltac split4 := split; [| split3].
Ltac split5 := split; [| split4].
Ltac split6 := split; [| split5].
Ltac split7 := split; [| split6].
Ltac split8 := split; [| split7].
Ltac split9 := split; [| split8].
Ltac split10 := split; [| split9].
Ltac split11 := split; [| split10].
Ltac split12 := split; [| split11].
Ltac split13 := split; [| split12].
Ltac split14 := split; [| split13].
Ltac split15 := split; [| split14].
Ltac split16 := split; [| split15].
Ltac split17 := split; [| split16].
Ltac split18 := split; [| split17].
Ltac split19 := split; [| split18].
Ltac split20 := split; [| split19].
Ltac split21 := split; [| split20].
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.
Show proof.
Definition pre_cat {X} {x y z:X} {p:x = y} : y = z -> x = z.
Show proof.
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.
Show proof.
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 |- ?G => constr:(G) end in
assert (x : isaprop(G)).
Definition isaprop_goal X (ig:isaprop X) (f:isaprop X -> X) : X.
Show proof.
intros. exact (f ig).
Ltac isaset_goal x :=
let G := match goal with |- ?G => constr:(G) end in
assert (x : isaset(G)).
Ltac split3 := split; [| split].
Ltac split4 := split; [| split3].
Ltac split5 := split; [| split4].
Ltac split6 := split; [| split5].
Ltac split7 := split; [| split6].
Ltac split8 := split; [| split7].
Ltac split9 := split; [| split8].
Ltac split10 := split; [| split9].
Ltac split11 := split; [| split10].
Ltac split12 := split; [| split11].
Ltac split13 := split; [| split12].
Ltac split14 := split; [| split13].
Ltac split15 := split; [| split14].
Ltac split16 := split; [| split15].
Ltac split17 := split; [| split16].
Ltac split18 := split; [| split17].
Ltac split19 := split; [| split18].
Ltac split20 := split; [| split19].
Ltac split21 := split; [| split20].
this allows to decompose a goal for prebicat_laws