From 978ecdd839bfcdcfc4b086c5fbd6d68515e5334c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 00:51:54 -0500 Subject: Add wf_smart_Literal --- src/LanguageWf.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src') diff --git a/src/LanguageWf.v b/src/LanguageWf.v index d1083e43d..da5db2944 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -1056,6 +1056,28 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ | progress subst | solve [ eauto ] ]. Qed. + + Lemma wf_smart_Literal {t v G} + : expr.wf G (@ident.smart_Literal var1 t v) (@ident.smart_Literal var2 t v). + Proof using Type. + induction t; cbn; eta_expand; repeat constructor; auto. + all: rewrite wf_reify_list + rewrite wf_reify_option. + all: repeat first [ rewrite map_length + | progress cbv [option_map option_eq] + | apply conj + | reflexivity + | progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress inversion_prod + | progress subst + | break_innermost_match_step + | progress rewrite combine_map_map in * + | progress rewrite combine_same in * + | progress rewrite map_map in * + | progress rewrite in_map_iff in * + | solve [ auto ] ]. + Qed. End with_var2. Lemma Wf_Reify_as {t} v : expr.Wf (@GallinaReify.base.Reify_as t v). -- cgit v1.2.3