Add global monad notation using Instances

This was mostly inspired by the std++ library.

10 files changed, 169 insertions, 104 deletions

diff --git a/src/common/Errormonad.v b/src/common/Errormonad.v
index 09c5c1c..201a101 100644
--- a/src/common/Errormonad.v
+++ b/src/common/Errormonad.v
@@ -26,13 +26,13 @@ Module ErrorMonad <: Monad.
     | Error m => Error m
     end.
 
-  Definition bind {A B : Type} (f : mon A) (g : A -> mon B) : mon B :=
+  Definition bind {A B : Type} (g : A -> mon B) (f : mon A) : mon B :=
     match f with
     | OK a => g a
     | Error m => Error m
     end.
 
-  Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> mon C) : mon C :=
+  Definition bind2 {A B C : Type} (g : A -> B -> mon C) (f : mon (A * B)) : mon C :=
     match f with
     | OK (a, b) => g a b
     | Error m => Error m
@@ -44,6 +44,11 @@ Module ErrorMonad <: Monad.
     | OK a' => a'
     end.
 
+  #[global] Instance error_ret : MRet res := @ret.
+  #[global] Instance error_bind : MBind res := @bind.
+  #[global] Instance error_join : MJoin res := @join.
+  #[global] Instance error_map : FMap res := @map.
+
 End ErrorMonad.
 
 Module ErrorMonadExtra := MonadExtra(ErrorMonad).
diff --git a/src/common/Monad.v b/src/common/Monad.v
index b7d97a1..cf3180b 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -18,6 +18,9 @@
 
 From Coq Require Import Lists.List.
 
+Declare Scope vericert_scope.
+#[local] Open Scope vericert_scope.
+
 Declare Scope monad_scope.
 
 Module Type Monad.
@@ -27,10 +30,10 @@ Module Type Monad.
   Parameter ret : forall (A : Type) (x : A), mon A.
   Arguments ret [A].
 
-  Parameter bind : forall (A B : Type) (f : mon A) (g : A -> mon B), mon B.
+  Parameter bind : forall (A B : Type) (g : A -> mon B) (f : mon A), mon B.
   Arguments bind [A B].
 
-  Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C.
+  Parameter bind2 : forall (A B C: Type) (g: A -> B -> mon C) (f: mon (A * B)), mon C.
   Arguments bind2 [A B C].
 
 End Monad.
@@ -41,10 +44,10 @@ Module MonadExtra(M : Monad).
   Module Import MonadNotation.
 
     Notation "'do' X <- A ; B" :=
-      (bind A (fun X => B))
+      (bind (fun X => B) A)
         (at level 200, X name, A at level 100, B at level 200) : monad_scope.
     Notation "'do' ( X , Y ) <- A ; B" :=
-      (bind2 A (fun X Y => B))
+      (bind2 (fun X Y => B) A)
         (at level 200, X name, Y name, A at level 100, B at level 200) : monad_scope.
 
   End MonadNotation.
@@ -70,3 +73,53 @@ Module MonadExtra(M : Monad).
     fold_left (fun a b => do a' <- a; f a' b) l s.
 
 End MonadExtra.
+
+(** A [Params f n] instance forces the setoid rewriting mechanism not to
+rewrite in the first [n] arguments of the function [f]. We will declare such
+instances for all operational type classes in this development. *)
+From Coq Require Export Morphisms RelationClasses.
+
+From Coq Require Setoid.
+
+Global Instance: Params (@Relation_Definitions.equiv) 2 := {}.
+
+Class MRet (M : Type -> Type) := mret: forall {A}, A -> M A.
+Global Arguments mret {_ _ _} _ : assert.
+Global Instance: Params (@mret) 3 := {}.
+Global Hint Mode MRet ! : typeclass_instances.
+
+Class MBind (M : Type -> Type) := mbind : forall {A B}, (A -> M B) -> M A -> M B.
+Global Arguments mbind {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@mbind) 4 := {}.
+Global Hint Mode MBind ! : typeclass_instances.
+
+Class MJoin (M : Type -> Type) := mjoin: forall {A}, M (M A) -> M A.
+Global Arguments mjoin {_ _ _} !_ / : assert.
+Global Instance: Params (@mjoin) 3 := {}.
+Global Hint Mode MJoin ! : typeclass_instances.
+
+Class FMap (M : Type -> Type) := fmap : forall {A B}, (A -> B) -> M A -> M B.
+Global Arguments fmap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@fmap) 4 := {}.
+Global Hint Mode FMap ! : typeclass_instances.
+
+Class OMap (M : Type -> Type) := omap: forall {A B}, (A -> option B) -> M A -> M B.
+Global Arguments omap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@omap) 4 := {}.
+Global Hint Mode OMap ! : typeclass_instances.
+
+Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : vericert_scope.
+Notation "( m ≫=.)" := (fun f => mbind f m) (only parsing) : vericert_scope.
+Notation "(.≫= f )" := (mbind f) (only parsing) : vericert_scope.
+Notation "(≫=)" := (fun m f => mbind f m) (only parsing) : vericert_scope.
+
+Notation "x ← y ; z" := (y ≫= (fun x : _ => z))
+  (at level 20, y at level 100, z at level 200, only parsing) : vericert_scope.
+
+Notation "' x ← y ; z" := (y ≫= (fun x : _ => z))
+  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : vericert_scope.
+
+Infix "<$>" := fmap (at level 61, left associativity) : vericert_scope.
+
+Notation "x ;; z" := (x ≫= fun _ => z)
+  (at level 100, z at level 200, only parsing, right associativity): vericert_scope.
diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v
index 4a80ff8..037dd83 100644
--- a/src/common/Optionmonad.v
+++ b/src/common/Optionmonad.v
@@ -43,13 +43,13 @@ Module Option <: Monad.
     | _ => None
     end.
 
-  Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
+  Definition bind {A B : Type} (g : A -> option B) (f : option A) : option B :=
     match f with
     | Some a => g a
     | _ => None
     end.
 
-  Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> option C) : option C :=
+  Definition bind2 {A B C : Type} (g : A -> B -> option C) (f : mon (A * B)) : option C :=
     match f with
     | Some (a, b) => g a b
     | _ => None
@@ -61,6 +61,12 @@ Module Option <: Monad.
     | Some a' => a'
     end.
 
+  #[global] Instance option_ret : MRet option := @ret.
+  #[global] Instance option_bind : MBind option := @bind.
+  #[global] Instance option_join : MJoin option := @join.
+  #[global] Instance option_map : FMap option := @map.
+  #[global] Instance option_omap : OMap option := @bind.
+
 End Option.
 
 Module OptionExtra.
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v
index 16dcbbf..c667fd9 100644
--- a/src/common/Statemonad.v
+++ b/src/common/Statemonad.v
@@ -42,7 +42,7 @@ Module Statemonad(S : State) <: Monad.
   Definition ret {A: Type} (x: A) : mon A :=
     fun (s : S.st) => OK x s (S.st_refl s).
 
-  Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
+  Definition bind {A B: Type} (g: A -> mon B) (f: mon A) : mon B :=
     fun (s : S.st) =>
       match f s with
       | Error msg => Error msg
@@ -53,8 +53,8 @@ Module Statemonad(S : State) <: Monad.
         end
       end.
 
-  Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
-    bind f (fun xy => g (fst xy) (snd xy)).
+  Definition bind2 {A B C: Type} (g: A -> B -> mon C) (f: mon (A * B)) : mon C :=
+    bind (fun xy => g (fst xy) (snd xy)) (f: mon (A * B)).
 
   Definition handle_error {A: Type} (f g: mon A) : mon A :=
     fun (s : S.st) =>
@@ -76,4 +76,7 @@ Module Statemonad(S : State) <: Monad.
     | Error err => Errors.Error err
     end.
 
+  #[global] Instance statemonad_ret : MRet mon := @ret.
+  #[global] Instance statemonad_bind : MBind mon := @bind.
+
 End Statemonad.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 24abece..6f602fc 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -31,8 +31,11 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Show.
+Require Export vericert.common.Monad.
 Require Export vericert.common.Optionmonad.
 
+#[global] Open Scope vericert_scope.
+
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
 
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 0ca7ead..af09ee6 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -241,10 +241,10 @@ Definition is_initial_pred (f: forest) (p: positive) :=
   | _ => None
   end.
 
-Definition update (fop : option (pred_op * forest)) (i : instr): option (pred_op * forest) :=
-  do (pred, f) <- fop;
+Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest) :=
+  let (pred, f) := fop in
   match i with
-  | RBnop => fop
+  | RBnop => Some fop
   | RBop p op rl r =>
       do pruned <-
            prune_predicated
@@ -298,7 +298,7 @@ Get a sequence from the basic block.
 |*)
 
 Definition abstract_sequence (b : list instr) : option forest :=
-  Option.map snd (fold_left update b (Some (Ptrue, empty))).
+  Option.map snd (mfold_left update b (Some (Ptrue, empty))).
 
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index eae309b..bcc3fd0 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -32,6 +32,10 @@ Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
+Require Import vericert.common.Monad.
+
+Module OptionExtra := MonadExtra(Option).
+Import OptionExtra.
 
 #[local] Open Scope positive.
 #[local] Open Scope forest.
@@ -1160,18 +1164,20 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     forall f i' i'' a sp p i p' f',
       sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') a (Iexec i'') ->
-      update (Some (p, f)) a = Some (p', f') ->
+      update (p, f) a = Some (p', f') ->
       sem (mk_ctx i sp ge) f' (i'', None).
   Proof. Admitted.
 
-  (* Lemma sem_update_instr_term : *)
-  (*   forall f i' i'' a sp i cf p p' p'' f', *)
-  (*     sem (mk_ctx i sp ge) f (i', None) -> *)
-  (*     step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> *)
-  (*     update (Some (p', f)) a = Some (p'', f') -> *)
-  (*     sem (mk_ctx i sp ge) f' (i'', Some cf) *)
-  (*          /\ eval_apred (mk_ctx i sp ge) p'' false. *)
-  (* Proof. Admitted. *)
+
+  Lemma sem_update_instr_term :
+    forall f i' i'' a sp i cf p p' p'' f',
+      sem (mk_ctx i sp ge) f (i', None) ->
+      step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) ->
+      update (p', f) a = Some (p'', f') ->
+      sem (mk_ctx i sp ge) f' (i'', Some cf)
+           /\ eval_predf (is_ps i) p'' = false.
+  Proof.
+    Admitted.
 
   (* Lemma step_instr_lessdef : *)
   (*   forall sp a i i' ti, *)
@@ -1180,12 +1186,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   (*     exists ti', step_instr ge sp (Iexec ti) a (Iexec ti') /\ state_lessdef i' ti'. *)
   (* Proof. Admitted. *)
 
-  (* Lemma step_instr_lessdef_term : *)
-  (*   forall sp a i i' ti cf, *)
-  (*     step_instr ge sp (Iexec i) a (Iterm i' cf) -> *)
-  (*     state_lessdef i ti -> *)
-  (*     exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'. *)
-  (* Proof. Admitted. *)
+  Lemma step_instr_lessdef_term :
+    forall sp a i i' ti cf,
+      step_instr ge sp (Iexec i) a (Iterm i' cf) ->
+      state_lessdef i ti ->
+      exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'.
+  Proof. Admitted.
 
 (*  Lemma app_predicated_semregset :
     forall A ctx o f res r y,
@@ -1320,75 +1326,62 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   (*   (* now apply falsy_update. *) *)
   (* (* Qed. *) Admitted. *)
 
-  (* Lemma state_lessdef_sem : *)
-  (*   forall i sp f i' ti cf, *)
-  (*     sem (mk_ctx i sp ge) f (i', cf) -> *)
-  (*     state_lessdef i ti -> *)
-  (*     exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. *)
-  (* Proof. Admitted. *)
-
-  (* Lemma update_Some : *)
-  (*   forall x n y, *)
-  (*     fold_left update x n = Some y -> *)
-  (*     exists n', n = Some n'. *)
-  (* Proof. *)
-  (*   induction x; crush. *)
-  (*   econstructor; eauto. *)
-  (*   exploit IHx; eauto; simplify. *)
-  (*   unfold update, Option.bind2, Option.bind in H1. *)
-  (*   repeat (destruct_match; try discriminate); econstructor; eauto. *)
-  (* Qed. *)
+  Lemma state_lessdef_sem :
+    forall i sp f i' ti cf,
+      sem (mk_ctx i sp ge) f (i', cf) ->
+      state_lessdef i ti ->
+      exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'.
+  Proof. Admitted.
 
   (* #[local] Opaque update. *)
 
-  (* Lemma abstr_fold_correct : *)
-  (*   forall sp x i i' i'' cf f p f', *)
-  (*     SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> *)
-  (*     sem (mk_ctx i sp ge) (snd f) (i', None) -> *)
-  (*     fold_left update x (Some f) = Some (p, f') -> *)
-  (*     forall ti, *)
-  (*       state_lessdef i ti -> *)
-  (*       exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) *)
-  (*              /\ state_lessdef i'' ti'. *)
-  (* Proof. *)
-  (*   induction x; simplify; inv H. *)
-  (*   - destruct f. exploit update_Some; eauto; intros. simplify. *)
-  (*     rewrite H3 in H1. destruct x0. *)
-  (*     exploit IHx; eauto. eapply sem_update_instr; eauto. *)
-  (*   - destruct f. *)
-  (*     exploit state_lessdef_sem; eauto; intros. simplify. *)
-  (*     exploit step_instr_lessdef_term; eauto; intros. simplify. *)
-  (*     inv H6. exploit update_Some; eauto; simplify. destruct x2. *)
-  (*     exploit sem_update_instr_term; eauto; simplify. *)
-  (*     eexists; split. *)
-  (*     eapply abstr_fold_falsy; eauto. *)
-  (*     rewrite H6 in H1. eauto. auto. *)
-  (* Qed. *)
-
-  (* Lemma sem_regset_empty : *)
-  (*   forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). *)
-  (* Proof. *)
-  (*   intros; constructor; intros. *)
-  (*   constructor; auto. constructor. *)
-  (*   constructor. *)
-  (* Qed. *)
+  Lemma abstr_fold_correct :
+    forall sp x i i' i'' cf f p f',
+      SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) ->
+      sem (mk_ctx i sp ge) (snd f) (i', None) ->
+      mfold_left update x (Some f) = Some (p, f') ->
+      forall ti,
+        state_lessdef i ti ->
+        exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf)
+               /\ state_lessdef i'' ti'.
+  Proof.
+    induction x; simplify; inv H.
+    - destruct f. (*  exploit update_Some; eauto; intros. simplify. *)
+    (*   rewrite H3 in H1. destruct x0. *)
+    (*   exploit IHx; eauto. eapply sem_update_instr; eauto. *)
+    (* - destruct f. *)
+    (*   exploit state_lessdef_sem; eauto; intros. simplify. *)
+    (*   exploit step_instr_lessdef_term; eauto; intros. simplify. *)
+    (*   inv H6. exploit update_Some; eauto; simplify. destruct x2. *)
+      (* exploit sem_update_instr_term; eauto; simplify. *)
+      (* eexists; split. *)
+      (* eapply abstr_fold_falsy; eauto. *)
+      (* rewrite H6 in H1. eauto. auto. *)
+  (* Qed. *) Admitted.
+
+  Lemma sem_regset_empty :
+    forall A ctx, @sem_regset A ctx empty (ctx_rs ctx).
+  Proof using.
+    intros; constructor; intros.
+    constructor; auto. constructor.
+    constructor.
+  Qed.
 
-  (* Lemma sem_predset_empty : *)
-  (*   forall A ctx, @sem_predset A ctx empty (ctx_ps ctx). *)
-  (* Proof. *)
-  (*   intros; constructor; intros. *)
-  (*   constructor; auto. constructor. *)
-  (*   constructor. *)
-  (* Qed. *)
+  Lemma sem_predset_empty :
+    forall A ctx, @sem_predset A ctx empty (ctx_ps ctx).
+  Proof using.
+    intros; constructor; intros.
+    constructor; auto. constructor.
+  Qed.
 
-  (* Lemma sem_empty : *)
-  (*   forall A ctx, @sem A ctx empty (ctx_is ctx, None). *)
-  (* Proof. *)
-  (*   intros. destruct ctx. destruct ctx_is. *)
-  (*   constructor; try solve [constructor; constructor; crush]. *)
-  (*   eapply sem_regset_empty. *)
-  (*   eapply sem_predset_empty. *)
-  (* Qed. *)
+  Lemma sem_empty :
+    forall A ctx, @sem A ctx empty (ctx_is ctx, None).
+  Proof using.
+    intros. destruct ctx. destruct ctx_is.
+    constructor; try solve [constructor; constructor; crush].
+    eapply sem_regset_empty.
+    eapply sem_predset_empty.
+  Qed.
 
   Lemma abstr_sequence_correct :
     forall sp x i i'' cf x',
@@ -1402,10 +1395,9 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     unfold abstract_sequence. intros. unfold Option.map in H0.
     destruct_match; try easy.
     destruct p; simplify.
-    (* eapply abstr_fold_correct; eauto. *)
-  (*   simplify. eapply sem_empty. *)
-  (* Qed. *)
-    Admitted.
+    eapply abstr_fold_correct; eauto.
+    simplify. eapply sem_empty.
+  Qed.
 
   Lemma abstr_check_correct :
     forall sp i i' a b cf ti,
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index bff68a2..6e632b8 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -385,7 +385,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Osel c AST.Tint, r1::r2::rl =>
     do tc <- translate_condition c rl;
-    ret (Vternary tc (Vvar r1) (Vvar r2))
+    mret (Vternary tc (Vvar r1) (Vvar r2))
   | Op.Olea a, _ => translate_eff_addressing a args
   | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
   end.
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 165fa91..0259be9 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -39,7 +39,7 @@ Require Import vericert.hls.FunctionalUnits.
 Remark bind_inversion:
   forall (A B: Type) (f: mon A) (g: A -> mon B)
          (y: B) (s1 s3: st) (i: st_incr s1 s3),
-    bind f g s1 = OK y s3 i ->
+    bind g f s1 = OK y s3 i ->
     exists x, exists s2, exists i1, exists i2,
             f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.
 Proof.
@@ -53,7 +53,7 @@ Qed.
 Remark bind2_inversion:
   forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
          (z: C) (s1 s3: st) (i: st_incr s1 s3),
-    bind2 f g s1 = OK z s3 i ->
+    bind2 g f s1 = OK z s3 i ->
     exists x, exists y, exists s2, exists i1, exists i2,
               f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2.
 Proof.
@@ -71,9 +71,11 @@ Ltac monadInv1 H :=
     discriminate
   | (ret _ _ = OK _ _ _) =>
     inversion H; clear H; try subst
+  | (mret _ _ = OK _ _ _) =>
+    inversion H; clear H; try subst
   | (error _ _ = OK _ _ _) =>
     discriminate
-  | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
+  | (bind ?G ?F ?S = OK ?X ?S' ?I) =>
     let x := fresh "x" in (
       let s := fresh "s" in (
         let i1 := fresh "INCR" in (
@@ -83,7 +85,7 @@ Ltac monadInv1 H :=
                 destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
                 clear H;
                 try (monadInv1 EQ2)))))))
-  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) =>
+  | (bind2 ?G ?F ?S = OK ?X ?S' ?I) =>
     let x1 := fresh "x" in (
       let x2 := fresh "x" in (
         let s := fresh "s" in (
@@ -99,6 +101,7 @@ Ltac monadInv1 H :=
 Ltac monadInv H :=
   match type of H with
   | (ret _ _ = OK _ _ _) => monadInv1 H
+  | (mret _ _ = OK _ _ _) => monadInv1 H
   | (error _ _ = OK _ _ _) => monadInv1 H
   | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
   | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 8dbd0f6..6067719 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -178,7 +178,7 @@ Proof. crush. Qed.
   { equiv := sat_equiv; }.
 
 #[global]
- Instance PandProper : Proper (equiv ==> equiv ==> equiv) Pand.
+ Instance PandProper : Proper (SetoidClass.equiv ==> SetoidClass.equiv ==> SetoidClass.equiv) Pand.
 Proof.
   unfold Proper. simplify. unfold "==>".
   intros.