diff options
Diffstat (limited to 'src/Reflection/InlineWf.v')
-rw-r--r-- | src/Reflection/InlineWf.v | 189 |
1 files changed, 158 insertions, 31 deletions
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index defd5b23e..46f4824b3 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -1,9 +1,16 @@ (** * Inline: Remove some [Let] expressions *) Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.TypeInversion. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.WfProofs. +Require Import Crypto.Reflection.WfInversion. Require Import Crypto.Reflection.Inline. Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.SplitInContext. Local Open Scope ctype_scope. Section language. @@ -19,6 +26,21 @@ Section language. Local Notation wff := (@wff base_type_code op). Local Notation wf := (@wf base_type_code op). + Local Notation wff_inline_directive G x y := + (wff G (exprf_of_inline_directive x) (exprf_of_inline_directive y) + /\ (fun x' y' + => match x', y' with + | default_inline _ _, default_inline _ _ + | no_inline _ _, no_inline _ _ + | inline _ _, inline _ _ + => True + | default_inline _ _, _ + | no_inline _ _, _ + | inline _ _, _ + => False + end) x y). + + Section with_var. Context {var1 var2 : base_type_code -> Type}. @@ -45,59 +67,164 @@ Section language. | constructor | solve [ eauto ] ]. - Lemma wff_inline_constf is_const {t} e1 e2 G G' + Local Ltac invert_inline_directive' i := + preinvert_one_type i; + intros ? i; + destruct i; + try exact I. + Local Ltac invert_inline_directive := + match goal with + | [ i : inline_directive _ |- _ ] => invert_inline_directive' i + end. + + (** XXX TODO: Clean up this proof *) + Lemma wff_inline_const_genf postprocess1 postprocess2 {t} e1 e2 G G' (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' - -> wff G x x') + -> wff G x x') (wf : wff G' e1 e2) - : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2). + (wf_postprocess : forall G t e1 e2, + wff G e1 e2 + -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2)) + : @wff var1 var2 G t (inline_const_genf postprocess1 e1) (inline_const_genf postprocess2 e2). Proof. - revert dependent G; induction wf; simpl in *; intros; auto; - specialize_by auto; unfold postprocess_for_const. + revert dependent G; induction wf; simpl in *; auto; intros; []. repeat match goal with | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H + | [ |- context[postprocess1 ?t ?e1] ] + => match goal with + | [ |- context[postprocess2 t ?e2] ] + => specialize (fun G => wf_postprocess G t e1 e2); + generalize dependent (postprocess1 t e1); + generalize dependent (postprocess2 t e2) + end + | _ => intro end. - match goal with - | [ H : _ |- _ ] - => pose proof (IHwf _ H) as IHwf' - end. - generalize dependent (inline_constf is_const e1); generalize dependent (inline_constf is_const e1'); intros. - destruct IHwf'; simpl in *; - try match goal with |- context[@is_const ?x ?y ?z] => is_var y; destruct (@is_const x y z), y end; - repeat constructor; auto; intros; - match goal with - | [ H : _ |- _ ] - => apply H; intros; progress destruct_head_hnf' or - end; - t_fin. + repeat match goal with + | [ H : forall G : list _, _ |- wff ?G' _ _ ] + => unique pose proof (H G') + | [ H : forall x y (G : list _), _ |- wff ?G' _ _ ] + => unique pose proof (fun x y => H x y G') + | [ H : forall x1 x2, (forall t x x', _ \/ List.In _ ?G -> wff ?G0 x x') -> _, + H' : forall t1 x1 x1', List.In _ ?G -> wff ?G0 x1 x1' |- _ ] + => unique pose proof (fun x1 x2 f => H x1 x2 (fun t x x' pf => match pf with or_introl pf => f t x x' pf | or_intror pf => H' t x x' pf end)) + end. + repeat match goal with + | _ => exact I + | [ H : forall x1 : unit, _ |- _ ] => specialize (H tt) + | [ H : False |- _ ] => exfalso; assumption + | _ => progress subst + | _ => progress inversion_sigma + | _ => progress inversion_prod + | _ => progress destruct_head' and + | _ => inversion_wff_step; progress subst + | _ => progress specialize_by_assumption + | _ => progress break_match + | _ => progress invert_inline_directive + | [ |- context[match ?e with _ => _ end] ] + => invert_one_expr e + | _ => progress destruct_head' or + | _ => progress simpl in * + | _ => intro + | _ => progress split_and + | [ H : wff _ TT _ |- _ ] => solve [ inversion H ] + | [ H : wff _ (Var _ _) _ |- _ ] => solve [ inversion H ] + | [ H : wff _ (Op _ _) _ |- _ ] => solve [ inversion H ] + | [ H : wff _ (LetIn _ _) _ |- _ ] => solve [ inversion H ] + | [ H : wff _ (Pair _ _) _ |- _ ] => solve [ inversion H ] + end; + repeat first [ progress specialize_by tauto + | progress specialize_by auto + | solve [ auto ] ]; + try (constructor; auto; intros). + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head' or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head or; t_fin. } Qed. - Lemma wf_inline_const is_const {t} e1 e2 G G' + Lemma wff_postprocess_for_const is_const G t + (e1 : @exprf var1 t) + (e2 : @exprf var2 t) + (Hwf : wff G e1 e2) + : wff_inline_directive G (postprocess_for_const is_const t e1) (postprocess_for_const is_const t e2). + Proof. + destruct e1; unfold postprocess_for_const; + repeat first [ progress subst + | intro + | progress destruct_head' sig + | progress destruct_head' and + | progress inversion_sigma + | progress inversion_option + | progress inversion_prod + | progress destruct_head' False + | progress simpl in * + | progress invert_expr + | progress inversion_wff + | progress break_innermost_match_step + | congruence + | solve [ auto ] ]. + Qed. + + Local Hint Resolve wff_postprocess_for_const. + + Lemma wff_inline_constf is_const {t} e1 e2 G G' + (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' + -> wff G x x') + (wf : wff G' e1 e2) + : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2). + Proof. eapply wff_inline_const_genf; eauto. Qed. + + Lemma wf_inline_const_gen postprocess1 postprocess2 {t} e1 e2 G G' (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' -> wff G x x') (Hwf : wf G' e1 e2) - : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2). + (wf_postprocess : forall G t e1 e2, + wff G e1 e2 + -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2)) + : @wf var1 var2 G t (inline_const_gen postprocess1 e1) (inline_const_gen postprocess2 e2). Proof. - revert dependent G; induction Hwf; simpl; constructor; intros; - [ eapply (wff_inline_constf is_const); [ | solve [ eauto ] ] | ]; - match goal with - | [ H : _ |- _ ] - => apply H; simpl; intros; progress destruct_head' or - end; - inversion_sigma; inversion_prod; repeat subst; simpl. - { constructor; left; reflexivity. } - { eauto. } + revert dependent G; induction Hwf; simpl; constructor; intros. + { eapply wff_inline_const_genf; eauto using wff_SmartVarVarf_nil. } + { match goal with H : _ |- _ => apply H end. + intros; destruct_head_hnf' or; t_fin. } Qed. + + Lemma wf_inline_const is_const {t} e1 e2 G G' + (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' + -> wff G x x') + (Hwf : wf G' e1 e2) + : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2). + Proof. eapply wf_inline_const_gen; eauto. Qed. End with_var. + Lemma Wf_InlineConstGen postprocess {t} (e : Expr t) + (Hwf : Wf e) + (Hpostprocess : forall var1 var2 G t e1 e2, + wff G e1 e2 + -> wff_inline_directive G (postprocess var1 t e1) (postprocess var2 t e2)) + : Wf (InlineConstGen postprocess e). + Proof. + intros var1 var2. + apply (@wf_inline_const_gen var1 var2 (postprocess _) (postprocess _) t (e _) (e _) nil nil); simpl; auto; tauto. + Qed. + Lemma Wf_InlineConst is_const {t} (e : Expr t) (Hwf : Wf e) : Wf (InlineConst is_const e). Proof. intros var1 var2. - apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; [ tauto | ]. + apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; try tauto. apply Hwf. Qed. End language. -Hint Resolve Wf_InlineConst : wf. +Hint Resolve Wf_InlineConstGen Wf_InlineConst : wf. |