generalize equiv relations in Util.Option and EdDSARepChange

2 files changed, 47 insertions, 21 deletions

diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v
index 48845b08e..2e745ffea 100644
--- a/src/EdDSARepChange.v
+++ b/src/EdDSARepChange.v
@@ -48,7 +48,7 @@ Section EdDSA.
   Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref).
   Proof. intros ? ? Hx; rewrite Hx; reflexivity. Qed.
 
-  Context {Edec:word b-> option E}   {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> Edec P_ = Some P}.
+  Context {Edec:word b-> option E}   {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}.
   Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.
 
   Local Infix "++" := combine.
@@ -66,9 +66,11 @@ Section EdDSA.
     setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a,
         Sdec (split2 b b sig) = Some a /\
         Eenc (_ * B + wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message)) mod _ * Eopp A)
-        = split1 b b sig)); setoid_rewrite (eq_enc_E_iff pk).
+        = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk).
     setoid_rewrite <-weqb_true_iff.
-    repeat setoid_rewrite <-option_rect_false_returns_true_iff.
+    setoid_rewrite <-option_rect_false_returns_true_iff_eq.
+    rewrite <-option_rect_false_returns_true_iff by
+     (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity).
 
     subst_evars.
     (* TODO: generalize this higher order reflexivity *)
diff --git a/src/Util/Option.v b/src/Util/Option.v
index 03fd77988..591a285ad 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -3,22 +3,34 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.Logic.
 
-Definition option_eq {A} eq (x y : option A) :=
-  match x with
-  | None    => y = None
-  | Some ax => match y with
-               | None => False
-               | Some ay => eq ax ay
-               end
-  end.
-
-Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R}
-  : Equivalence (option_eq R).
-Proof.
-  split; cbv; repeat (break_match || intro || intuition congruence ||
-                      solve [ apply reflexivity | apply symmetry; eassumption | eapply transitivity; eassumption ] ).
-Qed.
-
+Section Relations.
+  Definition option_eq {A} eq (x y : option A) :=
+    match x with
+    | None    => y = None
+    | Some ax => match y with
+                 | None => False
+                 | Some ay => eq ax ay
+                 end
+    end.
+  
+  Local Ltac t :=
+    cbv; repeat (break_match || intro || intuition congruence ||
+                 solve [ apply reflexivity
+                       | apply symmetry; eassumption
+                       | eapply transitivity; eassumption ] ).
+  
+  Global Instance Reflexive_option_eq {T} {R} {Reflexive_R:@Reflexive T R}
+    : Reflexive (option_eq R). Proof. t. Qed.
+  
+  Global Instance Transitive_option_eq {T} {R} {Transitive_R:@Transitive T R}
+    : Transitive (option_eq R). Proof. t. Qed.
+  
+  Global Instance Symmetric_option_eq {T} {R} {Symmetric_R:@Symmetric T R}
+    : Symmetric (option_eq R). Proof. t. Qed.
+  
+  Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R}
+    : Equivalence (option_eq R). Proof. split; exact _. Qed.
+End Relations.
 
 Global Instance Proper_option_rect_nd_changebody
       {A B:Type} {RB:relation B} {a:option A}
@@ -34,8 +46,20 @@ Global Instance Proper_option_rect_nd_changevalue
   : Proper (RB ==> option_eq RA ==> RB) (@option_rect A (fun _ => B) some).
 Proof. cbv; repeat (intro || break_match || f_equiv || intuition congruence). Qed.
 
-Lemma option_rect_false_returns_true_iff {T} (f:T->bool) (o:option T) :
-  option_rect (fun _ => bool) f false o = true <-> exists s:T, o = Some s /\ f s = true.
+Lemma option_rect_false_returns_true_iff
+      {T} {R} {reflexiveR:Reflexive R}
+      (f:T->bool) {Proper_f:Proper(R==>eq)f} (o:option T) :
+  option_rect (fun _ => bool) f false o = true <-> exists s:T, option_eq R o (Some s) /\ f s = true.
+Proof.
+  unfold option_rect; break_match; logic; [ | | congruence .. ].
+  { repeat esplit; easy. }
+  { match goal with [H : f _ = true |- f _ = true ] =>
+                    solve [rewrite <- H; eauto] end. }
+Qed.
+
+Lemma option_rect_false_returns_true_iff_eq
+      {T} (f:T->bool) (o:option T) :
+  option_rect (fun _ => bool) f false o = true <-> exists s:T, Logic.eq o (Some s) /\ f s = true.
 Proof. unfold option_rect; break_match; logic; congruence. Qed.
 
 Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,