diff options
author | Jason Gross <jagro@google.com> | 2016-06-23 16:13:22 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-06-23 18:20:31 -0700 |
commit | 6335426c320d199bf821a0507b0e26d3ad67ff88 (patch) | |
tree | 24a7b5e38d3147b15ac32329d36f0c52e25dba91 /src/Util | |
parent | 7dcd7ef85ff1d1079e3a3378d1f241b155515598 (diff) |
Add equality on sum types
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Sum.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/Sum.v b/src/Util/Sum.v new file mode 100644 index 000000000..2f03639b2 --- /dev/null +++ b/src/Util/Sum.v @@ -0,0 +1,18 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. + +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' + | inr x', inr y' => RB x' y' + | _, _ => False + end. + +Global Instance Equivalence_sumwise {A B} {RA:relation A} {RB:relation B} + {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB} + : Equivalence (sumwise RA RB). +Proof. + split; repeat intros [?|?]; simpl; trivial; destruct RA_equiv, RB_equiv; try tauto; eauto. +Qed. + +Arguments sumwise {A B} _ _ _ _. |