From e23824e1cc026671c5928000e95c6d6927437b99 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 28 Feb 2019 20:36:00 -0500 Subject: Make [reflect] a typeclass and add a bunch of lemmas --- src/Util/Bool/Reflect.v | 242 +++++++++++++++++++++++++++++++++++++++++++++++- src/Util/Comparison.v | 1 + src/Util/Sigma.v | 122 ++++++++++++++++++++++++ src/Util/Sum.v | 2 + 4 files changed, 363 insertions(+), 4 deletions(-) create mode 100644 src/Util/Comparison.v (limited to 'src/Util') diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index 73364c3e2..d9e93fe93 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -1,5 +1,18 @@ (** * Some lemmas about [Bool.reflect] *) +Require Import Coq.Classes.CMorphisms. Require Import Coq.Bool.Bool. +Require Import Coq.Arith.Arith. +Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith_dec. +Require Import Coq.NArith.BinNat. +Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Sum. +Require Import Crypto.Util.Comparison. +Require Import Crypto.Util.Tactics.DestructHead. Lemma reflect_to_dec_iff {P b1 b2} : reflect P b1 -> (b1 = b2) <-> (if b2 then P else ~P). Proof. @@ -12,14 +25,31 @@ Proof. intro; apply reflect_to_dec_iff; assumption. Qed. Lemma reflect_of_dec {P} {b1 b2 : bool} : reflect P b1 -> (if b2 then P else ~P) -> (b1 = b2). Proof. intro; apply reflect_to_dec_iff; assumption. Qed. -Lemma reflect_of_beq {A beq} (bl : forall a a' : A, beq a a' = true -> a = a') - (lb : forall a a' : A, a = a' -> beq a a' = true) - : forall x y, reflect (x = y) (beq x y). +Lemma reflect_of_brel {A R Rb} (bl : forall a a' : A, Rb a a' = true -> (R a a' : Prop)) + (lb : forall a a' : A, R a a' -> Rb a a' = true) + : forall x y, reflect (R x y) (Rb x y). Proof. intros x y; specialize (bl x y); specialize (lb x y). - destruct (beq x y); constructor; intuition congruence. + destruct (Rb x y); constructor; intuition congruence. Qed. +Lemma reflect_to_brel {A R Rb} (H : forall x y : A, reflect (R x y) (Rb x y)) + : (forall a a' : A, Rb a a' = true -> R a a') + /\ (forall a a' : A, R a a' -> Rb a a' = true). +Proof. + split; intros x y; specialize (H x y); destruct H; intuition congruence. +Qed. + +Lemma reflect_of_beq {A beq} (bl : forall a a' : A, beq a a' = true -> a = a') + (lb : forall a a' : A, a = a' -> beq a a' = true) + : forall x y, reflect (x = y) (beq x y). +Proof. apply reflect_of_brel; assumption. Qed. + +Lemma reflect_to_beq {A beq} (H : forall x y : A, reflect (x = y) (beq x y)) + : (forall a a' : A, beq a a' = true -> a = a') + /\ (forall a a' : A, a = a' -> beq a a' = true). +Proof. apply reflect_to_brel; assumption. Qed. + Definition mark {T} (v : T) := v. Ltac beq_to_eq beq bl lb := @@ -35,3 +65,207 @@ Ltac beq_to_eq beq bl lb := intros; cbv beta delta [mark] | [ H : context[beq ?x ?x] |- _ ] => rewrite (lb x x eq_refl) in H end. + +Existing Class reflect. +Definition decb (P : Prop) {b : bool} {H : reflect P b} := b. +Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)). + +Lemma decb_true_iff P {b} {H : reflect P b} : @decb P b H = true <-> P. +Proof. symmetry; apply reflect_iff, H. Qed. +Lemma decb_bp P {b} {H : reflect P b} : @decb P b H = true -> P. +Proof. apply decb_true_iff. Qed. +Lemma decb_pb P {b} {H : reflect P b} : P -> @decb P b H = true. +Proof. apply decb_true_iff. Qed. +Lemma decb_false_iff P {b} {H : reflect P b} : @decb P b H = false <-> ~P. +Proof. generalize (decb P), (decb_true_iff P); clear; intros []; intros; intuition congruence. Qed. +Lemma decb_false_bp P {b} {H : reflect P b} : @decb P b H = false -> ~P. +Proof. apply decb_false_iff. Qed. +Lemma decb_false_pb P {b} {H : reflect P b} : ~P -> @decb P b H = false. +Proof. apply decb_false_iff. Qed. + +Global Instance dec_of_reflect P {b} {H : reflect P b} : Decidable P | 15 + := (if b as b return reflect P b -> Decidable P + then fun H => left (decb_bp P eq_refl) + else fun H => right (decb_false_bp P eq_refl)) H. + +Global Instance eq_decb_hprop {A} {x y : A} {hp : IsHProp A} : reflect (@eq A x y) true | 5. +Proof. left; auto. Qed. + +Ltac solve_reflect_step := + first [ match goal with + | [ H : reflect _ ?b |- _ ] => tryif is_var b then destruct H else (inversion H; clear H) + | [ |- reflect _ _ ] => constructor + | [ |- reflect (?R ?x ?y) (?Rb ?x ?y) ] => apply (@reflect_of_brel _ R Rb) + | [ H : forall x y, reflect (?R x y) (?Rb x y) |- _ ] => apply (@reflect_to_brel _ R Rb) in H + end + | progress destruct_head'_and + | progress intros + | progress subst + | solve [ eauto + | firstorder (auto; try discriminate) ] + (* + | [ H : + | [ H : forall x y : ?A, reflect (x = y) _, x0 : ?A, y0 : ?A |- _ ] + => no_equalities_about x0 y0; let H' := fresh in pose proof (H x0 y0) as H'; inversion H'; clear H' + | [ H : forall a0 (x y : _), reflect (x = y) _, x0 : ?A, y0 : ?A |- _ ] + => no_equalities_about x0 y0; let H' := fresh in pose proof (H _ x0 y0) as H'; inversion H'; clear H' + | [ H : true = ?x |- context[?x] ] => rewrite <- H + | [ H : false = ?x |- context[?x] ] => rewrite <- H + end + | progress intros + | split + | progress inversion_sigma + | progress inversion_prod + | progress pre_decide_destruct_sigma + | progress destruct_head'_bool + | progress destruct_head'_prod + | progress subst + | progress cbn in * + | progress hnf + | progress pre_hprop + | solve [ left; firstorder (auto; try discriminate) + | right; firstorder (auto; try discriminate) + | firstorder (auto; try discriminate) ] *) ]. + + +Ltac solve_reflect := repeat solve_reflect_step. + +Hint Constructors reflect : typeclass_instances. + +Local Hint Resolve -> Bool.eqb_true_iff : core. +Local Hint Resolve <- Bool.eqb_true_iff : core. +Local Hint Resolve internal_prod_dec_bl internal_prod_dec_lb + internal_option_dec_bl internal_option_dec_lb + internal_list_dec_bl internal_list_dec_lb + internal_sum_dec_bl internal_sum_dec_lb + sigT_dec_bl sigT_dec_lb + sigT_dec_bl_hprop sigT_dec_lb_hprop + sig_dec_bl sig_dec_lb + sig_dec_bl_hprop sig_dec_lb_hprop + internal_comparison_dec_bl internal_comparison_dec_lb + : core. + +Local Hint Extern 0 => solve [ solve_reflect ] : typeclass_instances. +Local Hint Extern 1 => progress inversion_sigma : core. + +Global Instance reflect_True : reflect True true | 10 := ReflectT _ I. +Global Instance reflect_False : reflect False false | 10 := ReflectF _ (fun x => x). +Global Instance reflect_or {A B a b} `{reflect A a, reflect B b} : reflect (A \/ B) (orb a b) | 10. exact _. Qed. +Global Instance reflect_and {A B a b} `{reflect A a, reflect B b} : reflect (A /\ B) (andb a b) | 10. exact _. Qed. +Global Instance reflect_impl_or {A B bona} `{reflect (B \/ ~A) bona} : reflect (A -> B) bona | 15. exact _. Qed. +Global Instance reflect_impl {A B a b} `{reflect A a, reflect B b} : reflect (A -> B) (implb a b) | 10. exact _. Qed. +Global Instance reflect_iff {A B a b} `{reflect A a, reflect B b} : reflect (A <-> B) (Bool.eqb a b) | 10. exact _. Qed. +Lemma reflect_not {A a} `{reflect A a} : reflect (~A) (negb a). +Proof. exact _. Qed. + +(** Disallow infinite loops of reflect_not *) +Hint Extern 0 (reflect (~?A) _) => eapply (@reflect_not A) : typeclass_instances. + +Global Instance reflect_eq_unit : reflect_rel (@eq unit) (fun _ _ => true) | 10. exact _. Qed. +Global Instance reflect_eq_bool : reflect_rel (@eq bool) Bool.eqb | 10. exact _. Qed. +Global Instance reflect_eq_Empty_set : reflect_rel (@eq Empty_set) (fun _ _ => true) | 10. exact _. Qed. +Global Instance reflect_eq_prod {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A * B)) (prod_beq A B eqA eqB) | 10. exact _. Qed. +Global Instance reflect_eq_option {A eqA} `{reflect_rel (@eq A) eqA} : reflect_rel (@eq (option A)) (option_beq eqA) | 10. exact _. Qed. +Global Instance reflect_eq_list {A eqA} `{reflect_rel (@eq A) eqA} : reflect_rel (@eq (list A)) (list_beq A eqA) | 10. exact _. Qed. +Global Instance reflect_eq_list_nil_r {A eqA} {ls} : reflect (ls = @nil A) (list_beq A eqA ls (@nil A)) | 10. +Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Qed. +Global Instance reflect_eq_list_nil_l {A eqA} {ls} : reflect (@nil A = ls) (list_beq A eqA (@nil A) ls) | 10. +Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Qed. +Global Instance reflect_eq_sum {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A + B)) (sum_beq A B eqA eqB) | 10. exact _. Qed. +Global Instance reflect_eq_sigT_hprop {A P eqA} `{reflect_rel (@eq A) eqA, forall a : A, IsHProp (P a)} : reflect_rel (@eq (@sigT A P)) (sigT_beq eqA (fun _ _ _ _ => true)) | 10. exact _. Qed. +Global Instance reflect_eq_sig_hprop {A eqA} {P : A -> Prop} `{reflect_rel (@eq A) eqA, forall a : A, IsHProp (P a)} : reflect_rel (@eq (@sig A P)) (sig_beq eqA (fun _ _ _ _ => true)) | 10. exact _. Qed. +Global Instance reflect_eq_comparison : reflect_rel (@eq comparison) comparison_beq | 10. exact _. Qed. + +Module Nat. + Definition geb_spec0 : reflect_rel ge (fun x y => Nat.leb y x) := fun _ _ => Nat.leb_spec0 _ _. + Definition gtb_spec0 : reflect_rel gt (fun x y => Nat.ltb y x) := fun _ _ => Nat.ltb_spec0 _ _. +End Nat. +Global Existing Instance Nat.eqb_spec | 10. +Global Existing Instances Nat.leb_spec0 Nat.ltb_spec0 Nat.geb_spec0 Nat.gtb_spec0. + +Module N. + Lemma geb_spec0 : reflect_rel N.ge (fun x y => N.leb y x). + Proof. intros x y; generalize (N.leb_spec0 y x); intro H; destruct H; constructor; rewrite N.ge_le_iff; assumption. Qed. + Lemma gtb_spec0 : reflect_rel N.gt (fun x y => N.ltb y x). + Proof. intros x y; generalize (N.ltb_spec0 y x); intro H; destruct H; constructor; rewrite N.gt_lt_iff; assumption. Qed. +End N. +Global Existing Instance N.eqb_spec | 10. +Global Existing Instances N.leb_spec0 N.ltb_spec0 N.geb_spec0 N.gtb_spec0. + +Module Z. + Lemma geb_spec0 : reflect_rel Z.ge Z.geb. + Proof. intros x y; generalize (Z.leb_spec0 y x); rewrite Z.geb_leb; intro H; destruct H; constructor; rewrite Z.ge_le_iff; assumption. Qed. + Lemma gtb_spec0 : reflect_rel Z.gt Z.gtb. + Proof. intros x y; generalize (Z.ltb_spec0 y x); rewrite Z.gtb_ltb; intro H; destruct H; constructor; rewrite Z.gt_lt_iff; assumption. Qed. +End Z. +Global Existing Instance Z.eqb_spec | 10. +Global Existing Instances Z.leb_spec0 Z.ltb_spec0 Z.geb_spec0 Z.gtb_spec0. + +Module Pos. + Lemma geb_spec0 : reflect_rel Pos.ge (fun x y => Pos.leb y x). + Proof. intros x y; generalize (Pos.leb_spec0 y x); intro H; destruct H; constructor; rewrite Pos.ge_le_iff; assumption. Qed. + Lemma gtb_spec0 : reflect_rel Pos.gt (fun x y => Pos.ltb y x). + Proof. intros x y; generalize (Pos.ltb_spec0 y x); intro H; destruct H; constructor; rewrite Pos.gt_lt_iff; assumption. Qed. +End Pos. +Global Existing Instance Pos.eqb_spec | 10. +Global Existing Instances Pos.leb_spec0 Pos.ltb_spec0 Pos.geb_spec0 Pos.gtb_spec0. + +Global Instance reflect_Forall {A P Pb} {HD : forall x : A, reflect (P x) (Pb x)} {ls} + : reflect (List.Forall P ls) (List.forallb Pb ls) | 10. +Proof. + induction ls as [|x xs IHxs]; cbn [List.forallb]; [ left | destruct (HD x), IHxs; [ left | right.. ] ]; + [ constructor; assumption | constructor; assumption | intro Hn.. ]; + clear HD; + try abstract (inversion Hn; subst; tauto). +Qed. +Global Instance reflect_Exists {A P Pb} {HD : forall x : A, reflect (P x) (Pb x)} {ls} + : reflect (List.Exists P ls) (List.existsb Pb ls) | 10. +Proof. + induction ls as [|x xs IHxs]; cbn [List.existsb]; [ right | destruct (HD x), IHxs; [ left.. | right ] ]; + [ intro Hn | constructor; assumption.. | intro Hn ]; + clear HD; + try abstract (inversion Hn; subst; tauto). +Qed. + +Global Instance reflect_match_pair {A B} {P : A -> B -> Prop} {Pb : A -> B -> bool} {x : A * B} + {HD : reflect (P (fst x) (snd x)) (Pb (fst x) (snd x))} + : reflect (let '(a, b) := x in P a b) (let '(a, b) := x in Pb a b) | 1. +Proof. edestruct (_ : _ * _); assumption. Qed. + +Global Instance reflect_if_bool {x : bool} {A B a b} {HA : reflect A a} {HB : reflect B b} + : reflect (if x then A else B) (if x then a else b) | 10 + := if x return reflect (if x then A else B) (if x then a else b) + then HA + else HB. + +Global Instance reflect_ex_forall_not : forall T (P:T->Prop) (exPb:bool) {d:reflect (exists b, P b) exPb}, reflect (forall b, ~ P b) (negb exPb). +Proof. + intros T P exPb d; destruct d; constructor; firstorder. +Qed. + +Global Polymorphic Instance reflect_Proper_iff + : Proper (iff ==> eq ==> iffT) reflect | 10. +Proof. + intros A B H b b' ?; subst b'; split; intro H'; destruct H, H'; constructor; auto. +Qed. + +Global Polymorphic Instance reflect_Proper_arrow + : Proper (iff ==> eq ==> arrow) reflect | 10. +Proof. + repeat intro; eapply reflect_Proper_iff; try eassumption; easy. +Qed. + +Global Polymorphic Instance reflect_Proper_flip_arrow + : Proper (iff ==> eq ==> flip arrow) reflect | 10. +Proof. + repeat intro; eapply reflect_Proper_iff; try eassumption; easy. +Qed. + +Lemma reflect_bool : forall {P b} {Preflect:reflect P b}, b = true -> P. +Proof. intros P b Preflect; destruct Preflect; solve [ auto | discriminate ]. Qed. + +Ltac vm_reflect_no_check := apply reflect_bool; vm_cast_no_check (eq_refl true). +Ltac lazy_reflect_no_check := apply reflect_bool; exact_no_check (eq_refl true). + +Ltac vm_reflect := abstract vm_reflect_no_check. +Ltac lazy_reflect := abstract lazy_reflect_no_check. diff --git a/src/Util/Comparison.v b/src/Util/Comparison.v new file mode 100644 index 000000000..28fc80d87 --- /dev/null +++ b/src/Util/Comparison.v @@ -0,0 +1 @@ +Scheme Equality for comparison. diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 222ebe89b..03a69a9be 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -101,6 +101,67 @@ Section sigT. Definition sigT_eta {A P} (p : { a : A & P a }) : p = existT _ (projT1 p) (projT2 p). Proof. destruct p; reflexivity. Defined. + + (** *** Boolean equality for [sigT] *) + Definition sigT_beq {A A' P P'} (eqA : A -> A' -> bool) (eqP : forall a a', P a -> P' a' -> bool) (p : { a : A & P a }) (q : { a' : A' & P' a' }) + : bool + := andb (eqA (projT1 p) (projT1 q)) (eqP _ _ (projT2 p) (projT2 q)). + + Lemma sigT_dec_bl {A P} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (blP : forall a p p', eqP a a p p' = true -> p = p') + {p q} + : sigT_beq eqA eqP p q = true -> p = q. + Proof. + destruct p as [a p], q as [a' q]; cbv. + specialize (blA a a'); specialize (blP a p). + destruct (eqA a a') eqn:H'; [ specialize (blA eq_refl) | discriminate ]; subst. + intro H''; specialize (blP _ H''); subst; reflexivity. + Qed. + + Lemma sigT_dec_lb {A P} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (lbA : forall a a', a = a' -> eqA a a' = true) + (lbP : forall a p p', p = p' -> eqP a a p p' = true) + {p q} + : p = q -> sigT_beq eqA eqP p q = true. + Proof. + intro; subst q; destruct p as [a p]; cbv in *. + specialize (lbA a a eq_refl); specialize (lbP a p p eq_refl). + now rewrite lbA, lbP. + Qed. + + Lemma sigT_dec_bl_hprop {A P} + (eqA : A -> A -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (P_hprop : forall (x : A) (p q : P x), p = q) + {p q} + : @sigT_beq A A P P eqA (fun _ _ _ _ => true) p q = true -> p = q. + Proof. apply sigT_dec_bl; eauto. Qed. + + Lemma sigT_dec_lb_hprop {A P} + (eqA : A -> A -> bool) + (lbA : forall a a', a = a' -> eqA a a' = true) + (P_hprop : forall (x : A) (p q : P x), p = q) + {p q} + : p = q -> @sigT_beq A A P P eqA (fun _ _ _ _ => true) p q = true. + Proof. apply sigT_dec_lb; eauto. Qed. + + Definition sigT_eq_dec {A P} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (blP : forall a p p', eqP a a p p' = true -> p = p') + (lbA : forall a a', a = a' -> eqA a a' = true) + (lbP : forall a p p', p = p' -> eqP a a p p' = true) + (p q : { a : A & P a }) + : {p = q} + {p <> q}. + Proof. + destruct (sigT_beq eqA eqP p q) eqn:H; [ left | right; intro H' ]. + { eapply sigT_dec_bl; eassumption. } + { eapply sigT_dec_lb in H'; [ | eassumption.. ]. + generalize (eq_trans (eq_sym H) H'); clear; abstract discriminate. } + Defined. End sigT. (** ** Equality for [sig] *) @@ -171,6 +232,67 @@ Section sig. Definition sig_eta {A P} (p : { a : A | P a }) : p = exist _ (proj1_sig p) (proj2_sig p). Proof. destruct p; reflexivity. Defined. + + (** *** Boolean equality for [sig] *) + Definition sig_beq {A A'} {P P' : _ -> Prop} (eqA : A -> A' -> bool) (eqP : forall a a', P a -> P' a' -> bool) (p : { a : A | P a }) (q : { a' : A' | P' a' }) + : bool + := andb (eqA (proj1_sig p) (proj1_sig q)) (eqP _ _ (proj2_sig p) (proj2_sig q)). + + Lemma sig_dec_bl {A} {P : A -> Prop} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (blP : forall a p p', eqP a a p p' = true -> p = p') + {p q} + : sig_beq eqA eqP p q = true -> p = q. + Proof. + destruct p as [a p], q as [a' q]; cbv. + specialize (blA a a'); specialize (blP a p). + destruct (eqA a a') eqn:H'; [ specialize (blA eq_refl) | discriminate ]; subst. + intro H''; specialize (blP _ H''); subst; reflexivity. + Qed. + + Lemma sig_dec_lb {A} {P : A -> Prop} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (lbA : forall a a', a = a' -> eqA a a' = true) + (lbP : forall a p p', p = p' -> eqP a a p p' = true) + {p q} + : p = q -> sig_beq eqA eqP p q = true. + Proof. + intro; subst q; destruct p as [a p]; cbv in *. + specialize (lbA a a eq_refl); specialize (lbP a p p eq_refl). + now rewrite lbA, lbP. + Qed. + + Lemma sig_dec_bl_hprop {A} {P : A -> Prop} + (eqA : A -> A -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (P_hprop : forall (x : A) (p q : P x), p = q) + {p q} + : @sig_beq A A P P eqA (fun _ _ _ _ => true) p q = true -> p = q. + Proof. apply sig_dec_bl; eauto. Qed. + + Lemma sig_dec_lb_hprop {A} {P : A -> Prop} + (eqA : A -> A -> bool) + (lbA : forall a a', a = a' -> eqA a a' = true) + (P_hprop : forall (x : A) (p q : P x), p = q) + {p q} + : p = q -> @sig_beq A A P P eqA (fun _ _ _ _ => true) p q = true. + Proof. apply sig_dec_lb; eauto. Qed. + + Definition sig_eq_dec {A} {P : A -> Prop} + (eqA : A -> A -> bool) (eqP : forall a a', P a -> P a' -> bool) + (blA : forall a a', eqA a a' = true -> a = a') + (blP : forall a p p', eqP a a p p' = true -> p = p') + (lbA : forall a a', a = a' -> eqA a a' = true) + (lbP : forall a p p', p = p' -> eqP a a p p' = true) + (p q : { a : A | P a }) + : {p = q} + {p <> q}. + Proof. + destruct (sig_beq eqA eqP p q) eqn:H; [ left | right; intro H' ]. + { eapply sig_dec_bl; eassumption. } + { eapply sig_dec_lb in H'; [ | eassumption.. ]. + generalize (eq_trans (eq_sym H) H'); clear; abstract discriminate. } + Defined. End sig. (** ** Equality for [ex] *) diff --git a/src/Util/Sum.v b/src/Util/Sum.v index 4d4fde6ac..31019d2da 100644 --- a/src/Util/Sum.v +++ b/src/Util/Sum.v @@ -3,6 +3,8 @@ Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.GlobalSettings. +Scheme Equality for sum. + Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B) := fun x y => match x, y with | inl x', inl y' => RA x' y' -- cgit v1.2.3