aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jagro@google.com>2018-06-13 15:27:00 -0400
committerJason Gross <jagro@google.com>2018-06-13 15:27:00 -0400
commit86136b962eddd6bdc47d1e99b03fff2bac0578a8 (patch)
tree4bdb3f817916b9baa4df7f6f2bcd68200a7f46d6 /src/Util/Equality.v
parent5efc05b747b6edcdbd2c298855d9de53d8567369 (diff)
Minor refactoring
Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index affdb933a..04335dbd4 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -4,6 +4,7 @@
[eq]. We build up enough lemmas about this structure to deal
nicely with proofs of equality that come up in practice in this
project. *)
+Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Isomorphism.
Require Import Crypto.Util.HProp.
@@ -142,3 +143,11 @@ Proof. destruct H; reflexivity. Defined.
Lemma eq_match_const {A P x y} (p : x = y :> A) k
: match p return P with eq_refl => k end = k.
Proof. case p; reflexivity. Defined.
+
+Lemma fg_equal {A B} (f g : A -> B) (x y : A)
+ : f = g -> x = y -> f x = g y.
+Proof. intros; subst; reflexivity. Defined.
+
+Lemma fg_equal_rel {A B R} (f g : A -> B) (x y : A)
+ : (pointwise_relation _ R) f g -> x = y -> R (f x) (g y).
+Proof. cbv [pointwise_relation]; intros; subst; trivial. Qed.