From 29f1c8b447294b4a0a6a5127c6db23d54d43343f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 17 Aug 2018 04:08:24 -0400 Subject: Revert "Add more instances for type.related" This reverts commit 68c4b1ad628b82503e674aa42435d1d4bfbcbe3f. I think it was making things too slow. --- src/Experiments/NewPipeline/LanguageWf.v | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index b5a62687c..9c1c24a22 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -38,28 +38,17 @@ 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 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_Symmetric {t} : Symmetric (@eqv t) | 10. + Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed. - 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. + Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10. Proof. - induction t; cbn [type.related]; [ exact _ | ]. + induction t; cbn [eqv]; [ 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