diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 9c1c24a22..55c763dc1 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -38,18 +38,33 @@ 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. + Local 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) | 100. + 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. + Local 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) | 100. 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. + Hint Extern 100 (Symmetric (@type.related ?base_type ?interp_base_type ?R ?t)) + => (tryif has_evar R then fail else simple apply (@related_Symmetric base_type interp_base_type t R)) : typeclass_instances. + Hint Extern 100 (Transitive (@type.related ?base_type ?interp_base_type ?R ?t)) + => (tryif has_evar R then fail else simple apply (@related_Transitive base_type interp_base_type t R)) : typeclass_instances. Section app_curried_instances. Context {base_type} {base_interp : base_type -> Type}. |