diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-06 14:07:32 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-06 14:07:32 -0400 |
| commit | ae6797b2b9695ac8a8143948ba6e842a2f908052 (patch) | |
| tree | f16217d539bf13db7531f5b6decbaf9a2ca24cb9 /src | |
| parent | 3a097260dac2ca73370a493b1f25975f3394f699 (diff) | |
Add app_curried_Proper_gen as an instance
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 73ead2ae0..f59f07594 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -63,21 +63,25 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances. >> *) - Lemma app_curried_Proper {t} - : Proper (@type.related base_type base_interp (fun _ => eq) t ==> type.and_for_each_lhs_of_arrow (@type.eqv) ==> eq) - (@type.app_curried base_type base_interp t). + Global Instance app_curried_Proper_gen {base_type base_interp R t} + : Proper (@type.related base_type base_interp R t ==> type.and_for_each_lhs_of_arrow (@type.related base_type base_interp R) ==> R (type.final_codomain t)) + (@type.app_curried base_type base_interp t) | 1. Proof. - cbv [Proper respectful]; induction t; cbn [type.eqv type.app_curried]; cbv [Proper respectful]; [ intros; subst; reflexivity | ]. + cbv [Proper respectful]; induction t; cbn [type.related type.app_curried]; cbv [Proper respectful]; [ intros; assumption | ]. intros f g Hfg x y [Hxy ?]; eauto. Qed. + Lemma app_curried_Proper {t} + : Proper (@type.related base_type base_interp (fun _ => eq) t ==> type.and_for_each_lhs_of_arrow (@type.eqv) ==> eq) + (@type.app_curried base_type base_interp t). + Proof. exact _. Qed. Global Instance and_for_each_lhs_of_arrow_Reflexive {f} {R} {_ : forall t, Reflexive (R t)} {t} - : Reflexive (@type.and_for_each_lhs_of_arrow base_type f f R t). + : Reflexive (@type.and_for_each_lhs_of_arrow base_type f f R t) | 1. Proof. cbv [Reflexive] in *; induction t; cbn; repeat split; eauto. Qed. Global Instance and_for_each_lhs_of_arrow_Symmetric {f} {R} {_ : forall t, Symmetric (R t)} {t} - : Symmetric (@type.and_for_each_lhs_of_arrow base_type f f R t). + : Symmetric (@type.and_for_each_lhs_of_arrow base_type f f R t) | 1. Proof. cbv [Symmetric] in *; induction t; cbn; repeat split; intuition eauto. Qed. Global Instance and_for_each_lhs_of_arrow_Transitive {f} {R} {_ : forall t, Transitive (R t)} {t} - : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t). + : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t) | 1. Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed. End app_curried_instances. |