aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Reflection/ExprInversion.v2
-rw-r--r--src/Util/Equality.v10
2 files changed, 11 insertions, 1 deletions
diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 0cb35f4b7..6bf813bf7 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -140,12 +140,12 @@ Global Arguments invert_Return {_ _ _ _} _.
Ltac invert_expr_subst_step :=
match goal with
- | _ => progress subst
| [ H : invert_Var ?e = Some _ |- _ ] => apply invert_Var_Some in H
| [ H : invert_Op ?e = Some _ |- _ ] => apply invert_Op_Some in H
| [ H : invert_LetIn ?e = Some _ |- _ ] => apply invert_LetIn_Some in H
| [ H : invert_Pair ?e = Some _ |- _ ] => apply invert_Pair_Some in H
| [ H : invert_Abs ?e = _ |- _ ] => apply invert_Abs_Some in H
| [ H : invert_Return ?e = _ |- _ ] => apply invert_Return_Some in H
+ | _ => progress subst
end.
Ltac invert_expr_subst := repeat invert_expr_subst_step.
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index b128305f0..b7bce062d 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -41,6 +41,9 @@ Proof. case q; case p; reflexivity. Defined.
Lemma inv_V {A x y} (p : x = y :> A)
: eq_sym (eq_sym p) = p.
Proof. case p; reflexivity. Defined.
+Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
+ : eq_rect _ P u _ p = eq_rect _ (fun T => T) u _ (f_equal P p).
+Proof. case p; reflexivity. Defined.
(** To classify the equalities of a type [A] at a point [a : A], we
must give a "code" that stands in for the type [a = x] for each
@@ -112,3 +115,10 @@ Section hprop.
apply f_equal; apply allpath_hprop.
Qed.
End hprop.
+
+
+Lemma commute_eq_rect {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H : a = b :> A)
+ (v : P a)
+ : f b (eq_rect _ P v _ H)
+ = eq_rect _ Q (f a v) _ H.
+Proof. destruct H; reflexivity. Defined.