diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-18 10:47:35 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-22 10:44:07 -0400 |
| commit | fd5cba50d8743149e7ca4e386716126f2fc03e63 (patch) | |
| tree | c09dd69ea9c3dc0a77a7be0729f1a99024958a1c /src/Util/LetIn.v | |
| parent | e9fb194f228321f9477a26bf18617047722fd42a (diff) | |
Util.LetIn: fix proper instance
Diffstat (limited to 'src/Util/LetIn.v')
| -rw-r--r-- | src/Util/LetIn.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index d94674f2f..a472f4090 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -1,3 +1,4 @@ +Require Import Crypto.Util.FixCoqMistakes. Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. @@ -9,15 +10,13 @@ Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R} : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). Proof. lazy; intros; subst; auto; congruence. Qed. -(* FIXME: it adding this as a typeclass instance makes typeclass - resolution loop in ModularBaseystemOpt *) -Lemma Proper_Let_In_nd_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f} - : Proper (RA ==> RB) (fun x => Let_In x f). -Proof. intuition. Qed. +Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation B} + : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)). +Proof. cbv; intuition. Qed. Lemma app_Let_In_nd {A B C} (f:B -> C) : forall (e:A) (C:A -> B), f (Let_In e C) = Let_In e (fun v => f (C v)). -Proof. intros. cbv [Let_In]. reflexivity. Qed. +Proof. cbv; intuition. Qed. Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T. (* : forall T, gallina T -> gallina T, structurally recursive in the argument *) |