(** 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.