diff options
author | Jason Gross <jgross@mit.edu> | 2018-08-03 19:49:47 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-08-03 19:49:47 -0400 |
commit | 022b74131203433bd21bf763e5ef8f63c6d678af (patch) | |
tree | 83e7278a96d7e4d422f27d7689524a5f2078fb62 | |
parent | ad1f0354971bdd3ae5e24f154a9fffe034af6c5e (diff) |
Add wf for DefaultValue
-rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 84aba44e7..bcf0cdf00 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -608,8 +608,36 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Ltac interp_t := repeat interp_t_step. - Import defaults. + Module DefaultValue. + Import Language.Compilers.DefaultValue. + Module expr. + Module base. + Section with_var2. + Context {var1 var2 : type -> Type}. + + Lemma wf_default G {t : base.type} : expr.wf G (@expr.base.default var1 t) (@expr.base.default var2 t). + Proof. + induction t; destruct_head' base.type.base; wf_t. + Qed. + End with_var2. + + Lemma Wf_Default {t : base.type} : Wf (@expr.base.Default t). + Proof. repeat intro; apply @wf_default. Qed. + End base. + + Section with_var2. + Context {var1 var2 : type -> Type}. + + Lemma wf_default G {t : type} : expr.wf G (@expr.default var1 t) (@expr.default var2 t). + Proof. revert G; induction t; intros; wf_t; apply base.wf_default. Qed. + End with_var2. + + Lemma Wf_Default {t : type} : Wf (@expr.Default t). + Proof. repeat intro; apply @wf_default. Qed. + End expr. + End DefaultValue. + Module GeneralizeVar. Import Language.Compilers.GeneralizeVar. Local Open Scope etype_scope. |