monad laws for either

rems-project · Nov 22, 2023 · 6e29ecb · 6e29ecb
1 parent bf1294e
commit 6e29ecb
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 3 deletions.
diff --git a/coq/Proofs/ProofsAux.v b/coq/Proofs/ProofsAux.v
@@ -22,6 +22,7 @@ Require Import Common.ZMap.
 
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.Monad.
+Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.Monads.EitherMonad.
 Require Import Coq.Relations.Relation_Definitions.
 
@@ -436,3 +437,11 @@ Section SimpleError.
   Qed.
 
 End SimpleError.
+
+
+#[global] Instance Monad_either_MonadLaws {T:Type}:
+  MonadLaws (Monad_either T).
+Proof.
+  split; intros;  unfold Monad_either, ret, bind;
+    repeat break_match;subst; try inl_inr_inv; try reflexivity; try inl_inr.
+Qed.
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -18,7 +18,7 @@ Require Import Lia.
 Require Import StructTact.StructTactics.
 
 From ExtLib.Data Require Import List.
-From ExtLib.Structures Require Import Monad Monads MonadExc MonadState Traversable.
+From ExtLib.Structures Require Import Monad Monads MonadLaws MonadExc MonadState Traversable.
 From ExtLib.Data.Monads Require Import EitherMonad OptionMonad.
 
 From Coq.Lists Require Import List SetoidList. (* after exltlib *)
@@ -1061,6 +1061,7 @@ Module RevocationProofs.
     (Ec : relation C)
     (m : Type -> Type)
     (M : Monad m)
+    (ML: MonadLaws M)
     (EMa : relation (m A))
     (RetProper: Proper (Ea ==> EMa) ret)
     (BindProper: Proper ((EMa) ==> (Ea ==> EMa) ==> (EMa)) (@bind m M A A))
@@ -1517,8 +1518,8 @@ Module RevocationProofs.
           eapply monadic_fold_left2_proper with
             (Ea:=repr_fold2_eq)
             (Eb:=eq)
-            (Ec:=struct_field_eq);
-            [typeclasses eauto|typeclasses eauto|reflexivity|assumption|repeat split;auto|].
+            (Ec:=struct_field_eq); try typeclasses eauto;
+            [reflexivity|assumption|repeat split;auto|].
 
           (* proper for 'f' *)
           intros a a' Ea.