Library UniMath.Tactics.Utilities
Author: Michael A. Warren (maw@mawarren.net). Date: Spring 2015. Description: Some helper tactics.
Imports
Require Import UniMath.Foundations.PartD
UniMath.Foundations.Propositions
UniMath.Foundations.Sets.
Arguments tpair {_ _} _ _.
We introduce the notation ap for maponpaths as in KTheory.
Module Export Notation.
Notation ap := maponpaths.
Notation "p # x" := (transportf _ p x) (right associativity, at level 65) : transport.
Open Scope transport.
Notation "{ x : X & P }" := (total2 (λ x:X, P)) : type_scope.
Notation "X ** Y" := (X × Y) (right associativity, at level 80) : type_scope.
End Notation.
Definition neq (X : UU) : X → X → hProp
:= λ x y : X, make_hProp (x != y) (isapropneg (x = y)).
Ltac check_cons f g :=
let h T :=
f T; g T
in
h.
Ltac id_check T := idtac.
Ltac make_hyp_check e :=
let T0 := type of e in
let f T :=
match T with
| T0 ⇒ fail 1
| _ ⇒ idtac
end
in f.
In some cases we may need to obtain the current left-hand side of a goal equation (it may have been rewritten since initially being passed in via a match clause and a subsequent match on the new state should be performed. E.g., in matched_rewrite below.
Ltac get_current_lhs :=
match goal with
| |- ?lhs = ?rhs ⇒ lhs
end.
Ltac get_current_rhs :=
match goal with
| |- ?lhs = ?rhs ⇒ rhs
end.
Ltac get_current_lhs_in H :=
let T := type of H in
match T with
| ?lhs = ?rhs ⇒ lhs
end.
Ltac get_current_rhs_in H :=
let T := type of H in
match T with
| ?lhs = ?rhs ⇒ rhs
end.
Ltac matched_rewrite e :=
match type of e with
| ?l = ?r ⇒
let lhs := get_current_lhs in
match lhs with
| context [l] ⇒ rewrite e
| context [r] ⇒ rewrite <- e
end
end.
match goal with
| |- ?lhs = ?rhs ⇒ lhs
end.
Ltac get_current_rhs :=
match goal with
| |- ?lhs = ?rhs ⇒ rhs
end.
Ltac get_current_lhs_in H :=
let T := type of H in
match T with
| ?lhs = ?rhs ⇒ lhs
end.
Ltac get_current_rhs_in H :=
let T := type of H in
match T with
| ?lhs = ?rhs ⇒ rhs
end.
Ltac matched_rewrite e :=
match type of e with
| ?l = ?r ⇒
let lhs := get_current_lhs in
match lhs with
| context [l] ⇒ rewrite e
| context [r] ⇒ rewrite <- e
end
end.