From 235e58e2233a5c13a2065fdcd85073e016cad3df Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 20:04:08 -0700 Subject: Add LinearizeWf The proof of wf-preservation for inline_const isn't finished yet, though... --- src/Reflection/LinearizeWf.v | 279 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 279 insertions(+) create mode 100644 src/Reflection/LinearizeWf.v (limited to 'src') diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v new file mode 100644 index 000000000..f7860db30 --- /dev/null +++ b/src/Reflection/LinearizeWf.v @@ -0,0 +1,279 @@ +(** * Linearize: Place all and only operations in let binders *) +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.WfProofs. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. + +Local Open Scope ctype_scope. +Section language. + Context (base_type_code : Type). + Context (interp_base_type : base_type_code -> Type). + Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + + Local Notation flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + Let Tbase := @Tbase base_type_code. + Local Coercion Tbase : base_type_code >-> Syntax.flat_type. + Let interp_type := interp_type interp_base_type. + Let interp_flat_type := interp_flat_type_gen interp_base_type. + Local Notation exprf := (@exprf base_type_code interp_base_type op). + Local Notation expr := (@expr base_type_code interp_base_type op). + Local Notation Expr := (@Expr base_type_code interp_base_type op). + Local Notation wff := (@wff base_type_code interp_base_type op). + Local Notation wf := (@wf base_type_code interp_base_type op). + + Section with_var. + Context {var1 var2 : base_type_code -> Type}. + + Local Ltac t_fin_step tac := + match goal with + | _ => assumption + | _ => progress simpl in * + | _ => progress subst + | _ => progress inversion_sigma + | _ => setoid_rewrite List.in_app_iff + | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H + | _ => progress intros + | _ => solve [ eauto ] + | _ => solve [ intuition (subst; eauto) ] + | [ H : forall (x : prod _ _) (y : prod _ _), _ |- _ ] => specialize (fun x x' y y' => H (x, x') (y, y')) + | _ => rewrite !List.app_assoc + | [ H : _ \/ _ |- _ ] => destruct H + | [ H : _ |- _ ] => apply H + | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ] + | _ => progress tac + | [ |- wff _ _ _ ] => constructor + | [ |- wf _ _ _ ] => constructor + end. + Local Ltac t_fin tac := repeat t_fin_step tac. + + Lemma wff_let_bind_const G {t} v {tC} eC1 eC2 + : (forall (x1 : interp_flat_type_gen var1 t) (x2 : interp_flat_type_gen var2 t), + wff (flatten_binding_list base_type_code x1 x2 ++ G) (eC1 x1) (eC2 x2)) + -> @wff var1 var2 G tC (let_bind_const v eC1) (let_bind_const v eC2). + Proof. + revert G tC eC1 eC2; induction t; t_fin idtac. + Qed. + + Local Hint Resolve wff_let_bind_const. + Local Hint Constructors Syntax.wff. + Local Hint Resolve List.in_app_or List.in_or_app. + + Local Ltac small_inversion_helper wf G0 e2 := + let t0 := match type of wf with wff (t:=?t0) _ _ _ => t0 end in + let e1 := match goal with + | |- context[wff G0 (under_letsf ?e1 _) (under_letsf e2 _)] => e1 + | |- context[wff _ (inline_constf ?e1) (inline_constf e2)] => e1 + end in + pattern G0, t0, e1, e2; + lazymatch goal with + | [ |- ?retP _ _ _ _ ] + => first [ refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Const _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfConst _ _ _ => _ + | _ => fun _ p => p + end) + | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Var _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfVar _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Op _ _ _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfOp _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Let _ _ _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfLet _ _ _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Pair _ _ _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfPair _ _ _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) ] + end. + Fixpoint wff_under_letsf G {t} e1 e2 {tC} eC1 eC2 + (wf : @wff var1 var2 G t e1 e2) + (H : forall (x1 : interp_flat_type_gen var1 t) (x2 : interp_flat_type_gen var2 t), + wff (flatten_binding_list base_type_code x1 x2 ++ G) (eC1 x1) (eC2 x2)) + {struct e1} + : @wff var1 var2 G tC (under_letsf e1 eC1) (under_letsf e2 eC2). + Proof. + revert H. + set (e1v := e1) in *. + destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ]; + [ clear wff_under_letsf + | clear wff_under_letsf + | clear wff_under_letsf + | generalize (fun G => match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => wff_under_letsf G _ ex + | _ => I + end); + generalize (fun G => match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => fun x => wff_under_letsf G _ (eC x) + | _ => I + end); + clear wff_under_letsf + | generalize (fun G => match e1v return match e1v with Pair _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_under_letsf G _ ex + | _ => I + end); + generalize (fun G => match e1v return match e1v with Pair _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_under_letsf G _ ey + | _ => I + end); + clear wff_under_letsf ]; + revert eC1 eC2; + (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *) + small_inversion_helper wf G e2; + t_fin idtac. + Qed. + + Local Hint Resolve wff_under_letsf. + Local Hint Constructors or. + Local Hint Extern 1 => progress unfold List.In in *. + Local Hint Resolve wff_in_impl_Proper. + + Lemma wff_SmartVar {t} x1 x2 + : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2). + Proof. + unfold SmartVar. + induction t; simpl; constructor; eauto. + Qed. + + Local Hint Resolve wff_SmartVar. + + Lemma wff_linearizef G {t} e1 e2 + : @wff var1 var2 G t e1 e2 + -> @wff var1 var2 G t (linearizef e1) (linearizef e2). + Proof. + induction 1; t_fin ltac:(apply wff_under_letsf). + Qed. + + Local Hint Resolve wff_linearizef. + + Lemma wf_linearize G {t} e1 e2 + : @wf var1 var2 G t e1 e2 + -> @wf var1 var2 G t (linearize e1) (linearize e2). + Proof. + induction 1; t_fin idtac. + Qed. + + Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t) + := match e with + | Const _ v => Some v + | _ => None + end. + + Lemma wff_Const_eta G {A B} v1 v2 + : @wff var1 var2 G (Prod A B) (Const v1) (Const v2) + -> (@wff var1 var2 G A (Const (fst v1)) (Const (fst v2)) + /\ @wff var1 var2 G B (Const (snd v1)) (Const (snd v2))). + Proof. + intro wf. + assert (H : Some v1 = Some v2). + { refine match wf in @Syntax.wff _ _ _ _ _ G t e1 e2 return invert_Const e1 = invert_Const e2 with + | WfConst _ _ _ => eq_refl + | _ => eq_refl + end. } + inversion H; subst; repeat constructor. + Qed. + + Local Hint Resolve (fun G A B c1 c2 wf => proj1 (@wff_Const_eta G A B c1 c2 wf)) + (fun G A B c1 c2 wf => proj2 (@wff_Const_eta G A B c1 c2 wf)). + + Lemma wff_SmartConst G {t t'} v1 v2 x1 x2 + (Hin : List.In (existT (fun t : base_type_code => (@exprf var1 t * @exprf var2 t)%type) t (x1, x2)) + (flatten_binding_list base_type_code (SmartConst v1) (SmartConst v2))) + (Hwf : @wff var1 var2 G t' (Const v1) (Const v2)) + : @wff var1 var2 G t x1 x2. + Proof. + induction t'. simpl in *. + { intuition (inversion_sigma; inversion_prod; subst; eauto). } + { unfold SmartConst in *; simpl in *. + apply List.in_app_iff in Hin. + intuition (inversion_sigma; inversion_prod; subst; eauto). } + Qed. + + Local Hint Resolve wff_SmartConst. + + Fixpoint wff_inline_constf {t} e1 e2 G G' + (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x, x')) G' + -> wff G x x') + (wf : wff G' e1 e2) + {struct e1} + : @wff var1 var2 G t (inline_constf e1) (inline_constf e2). + Proof. + revert H. + set (e1v := e1) in *. + destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ]; + [ clear wff_inline_constf + | clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Op _ _ _ args => wff_inline_constf _ args + | _ => I + end); + clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => wff_inline_constf _ ex + | _ => I + end); + generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => fun x => wff_inline_constf _ (eC x) + | _ => I + end); + clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_inline_constf _ ex + | _ => I + end); + generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_inline_constf _ ey + | _ => I + end); + clear wff_inline_constf ]; + revert G; + (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *) + small_inversion_helper wf G' e2; + t_fin idtac; + repeat match goal with + | [ H : context[_ -> wff _ (inline_constf ?e) (inline_constf _)], e2 : exprf _ |- _ ] + => is_var e; not constr_eq e e2; specialize (H e2) + | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] + => destruct (@inline_constf A B C D E e) + | [ H : context[wff _ _ (@inline_constf ?A ?B ?C ?D ?E ?e)] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] + => destruct (@inline_constf A B C D E e) + | [ IHwf : forall x y : list _, _, H1 : forall z : _, _, H2 : wff _ _ _ |- _ ] + => solve [ specialize (IHwf _ _ H1 H2); inversion IHwf ] + | [ |- wff _ _ _ ] => constructor + end. + 3:t_fin idtac. + 4:t_fin idtac. + { match goal with + | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac + end. } + Abort. + End with_var. + + Lemma Wf_Linearize {t} (e : Expr t) : Wf e -> Wf (Linearize e). + Proof. + intros wf var1 var2; apply wf_linearize, wf. + Qed. +End language. -- cgit v1.2.3