From 68c4b1ad628b82503e674aa42435d1d4bfbcbe3f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Aug 2018 14:33:52 -0400 Subject: Add more instances for type.related --- src/Experiments/NewPipeline/LanguageWf.v | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 6c90d4ecc..9393a1ebf 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -38,17 +38,28 @@ Module Compilers. Context {base_type} {interp_base_type : base_type -> Type}. Local Notation eqv := (@type.related base_type interp_base_type (fun _ => eq)). - Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10. - Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed. + Global Instance related_Symmetric {t} {R : forall t, relation (interp_base_type t)} + {R_sym : forall t, Symmetric (R t)} + : Symmetric (@type.related base_type interp_base_type R t) | 10. + Proof. + cbv [Symmetric] in *; + induction t; cbn [type.related type.interp] in *; repeat intro; eauto. + Qed. - Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10. + Global Instance related_Transitive {t} {R : forall t, relation (interp_base_type t)} + {R_sym : forall t, Symmetric (R t)} + {R_trans : forall t, Transitive (R t)} + : Transitive (@type.related base_type interp_base_type R t) | 10. Proof. - induction t; cbn [eqv]; [ exact _ | ]. + induction t; cbn [type.related]; [ exact _ | ]. cbv [respectful]; cbn [type.interp]. intros f g h Hfg Hgh x y Hxy. etransitivity; [ eapply Hfg; eassumption | eapply Hgh ]. etransitivity; first [ eassumption | symmetry; eassumption ]. Qed. + + Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10 := _. + Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10 := _. End eqv. Section app_curried_instances. -- cgit v1.2.3