From 132b663247c195a38385f8b9f473b998f2e2d37b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 2 Aug 2018 11:19:59 -0400 Subject: Generalize option_eq to support heterogenous relations --- src/Util/Option.v | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'src/Util/Option.v') diff --git a/src/Util/Option.v b/src/Util/Option.v index bccf3b6fc..2809655e4 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -34,7 +34,7 @@ End Notations. Local Open Scope option_scope. Section Relations. - Definition option_eq {A} eq (x y : option A) := + Definition option_eq {A B} eq (x : option A) (y : option B) := match x with | None => y = None | Some ax => match y with @@ -47,16 +47,26 @@ Section Relations. cbv; repeat (break_match || intro || intuition congruence || solve [ apply reflexivity | apply symmetry; eassumption - | eapply transitivity; eassumption ] ). + | eapply transitivity; eassumption + | eauto ] ). Global Instance Reflexive_option_eq {T} {R} {Reflexive_R:@Reflexive T R} - : Reflexive (option_eq R). Proof. t. Qed. + : Reflexive (option_eq R) | 1. Proof. t. Qed. + + Lemma option_eq_sym {A B} {R1 R2 : _ -> _ -> Prop} (HR : forall v1 v2, R1 v1 v2 -> R2 v2 v1) + : forall v1 v2, @option_eq A B R1 v1 v2 -> option_eq R2 v2 v1. + Proof. t. Qed. + + Lemma option_eq_trans {A B C} {R1 R2 R3 : _ -> _ -> Prop} + (HR : forall v1 v2 v3, R1 v1 v2 -> R2 v2 v3 -> R3 v1 v3) + : forall v1 v2 v3, @option_eq A B R1 v1 v2 -> @option_eq B C R2 v2 v3 -> @option_eq A C R3 v1 v3. + Proof. t. Qed. Global Instance Transitive_option_eq {T} {R} {Transitive_R:@Transitive T R} - : Transitive (option_eq R). Proof. t. Qed. + : Transitive (option_eq R) | 1 := option_eq_trans Transitive_R. Global Instance Symmetric_option_eq {T} {R} {Symmetric_R:@Symmetric T R} - : Symmetric (option_eq R). Proof. t. Qed. + : Symmetric (option_eq R) | 1 := option_eq_sym Symmetric_R. Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R} : Equivalence (option_eq R). Proof. split; exact _. Qed. -- cgit v1.2.3