diff options
Diffstat (limited to 'src/UnderLetsProofs.v')
| -rw-r--r-- | src/UnderLetsProofs.v | 1025 |
1 files changed, 1025 insertions, 0 deletions
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v new file mode 100644 index 000000000..787fdb7c4 --- /dev/null +++ b/src/UnderLetsProofs.v @@ -0,0 +1,1025 @@ +Require Import Coq.Lists.List. +Require Import Coq.Classes.Morphisms. +Require Import Coq.Lists.SetoidList. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLets. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.SpecializeBy. +Import ListNotations. Local Open Scope list_scope. + +Import EqNotations. +Module Compilers. + Import Language.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import UnderLets.Compilers. + Import ident.Notations. + Import expr.Notations. + Import invert_expr. + + Module SubstVarLike. + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + Section with_var. + Context {var1 var2 : type -> Type}. + Local Notation expr1 := (@expr.expr base_type ident var1). + Local Notation expr2 := (@expr.expr base_type ident var2). + Section with_var_like. + Context (is_var_like1 : forall t, @expr var1 t -> bool) + (is_var_like2 : forall t, @expr var2 t -> bool). + Local Notation subst_var_like1 := (@SubstVarLike.subst_var_like base_type ident var1 is_var_like1). + Local Notation subst_var_like2 := (@SubstVarLike.subst_var_like base_type ident var2 is_var_like2). + Definition is_var_like_wfT := forall G t e1 e2, expr.wf G (t:=t) e1 e2 -> is_var_like1 t e1 = is_var_like2 t e2. + Context (is_var_like_good : is_var_like_wfT). + + Lemma wf_subst_var_like G1 G2 t e1 e2 + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (subst_var_like1 e1) (subst_var_like2 e2). + Proof. + cbv [is_var_like_wfT] in *. + intro Hwf; revert dependent G2; induction Hwf; + cbn [SubstVarLike.subst_var_like]; + repeat first [ match goal with + | [ H : is_var_like1 _ ?x = _, H' : is_var_like2 _ ?y = _ |- _ ] + => assert (is_var_like1 _ x = is_var_like2 _ y) by eauto; congruence + end + | progress wf_safe_t + | progress break_innermost_match + | solve [ wf_t ] ]. + Qed. + End with_var_like. + + Section with_ident_like. + Context (ident_is_good : forall t, ident t -> bool). + + Lemma wfT_is_recursively_var_or_ident + : is_var_like_wfT (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good) + (fun t => SubstVarLike.is_recursively_var_or_ident ident_is_good). + Proof. + intros G t e1 e2 Hwf; induction Hwf; cbn [SubstVarLike.is_recursively_var_or_ident]; + congruence. + Qed. + End with_ident_like. + + Lemma wfT_is_var + : is_var_like_wfT (fun _ e => match invert_Var e with Some _ => true | None => false end) + (fun _ e => match invert_Var e with Some _ => true | None => false end). + Proof. intros G t e1 e2 Hwf; destruct Hwf; cbn [invert_Var]; reflexivity. Qed. + End with_var. + + Local Notation SubstVarLike := (@SubstVarLike.SubstVarLike base_type ident). + Local Notation SubstVar := (@SubstVarLike.SubstVar base_type ident). + Local Notation SubstVarOrIdent := (@SubstVarLike.SubstVarOrIdent base_type ident). + + Lemma Wf_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) + (is_var_like_good : forall var1 var2, is_var_like_wfT (is_var_like var1) (is_var_like var2)) + {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarLike is_var_like e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto with nocore; cbn [In]; tauto. + Qed. + + Lemma Wf_SubstVar {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVar e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_var with nocore; cbn [In]; tauto. + Qed. + + Lemma Wf_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) + {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarOrIdent should_subst_ident e). + Proof. + intros Hwf var1 var2; eapply wf_subst_var_like; eauto using wfT_is_recursively_var_or_ident with nocore; cbn [In]; tauto. + Qed. + + Section interp. + Context {base_interp : base_type -> Type} + {interp_ident : forall t, ident t -> type.interp base_interp t} + {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. + Section with_is_var_like. + Context (is_var_like : forall t, @expr (type.interp base_interp) t -> bool). + + Lemma interp_subst_var_like_gen G t (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) + (Hwf : expr.wf G e1 e2) + : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. + Proof. + induction Hwf; cbn [SubstVarLike.subst_var_like]; cbv [Proper respectful] in *; + interp_safe_t; break_innermost_match; interp_safe_t. + Qed. + + Lemma interp_subst_var_like_gen_nil t (e1 e2 : expr t) + (Hwf : expr.wf nil e1 e2) + : expr.interp interp_ident (SubstVarLike.subst_var_like is_var_like e1) == expr.interp interp_ident e2. + Proof. apply interp_subst_var_like_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + End with_is_var_like. + + Lemma Interp_SubstVarLike (is_var_like : forall var t, @expr var t -> bool) + {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVarLike is_var_like e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + + Lemma Interp_SubstVar {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVar e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + + Lemma Interp_SubstVarOrIdent (should_subst_ident : forall t, ident t -> bool) + {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (SubstVarOrIdent should_subst_ident e) == expr.Interp interp_ident e. + Proof. apply interp_subst_var_like_gen_nil, Hwf. Qed. + End interp. + End with_ident. + + Lemma Wf_SubstVarFstSndPairOppCast {t} (e : expr.Expr t) + : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOppCast e). + Proof. apply Wf_SubstVarOrIdent. Qed. + + Section with_cast. + Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}. + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation interp := (@expr.interp _ _ _ (@ident_interp)). + Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)). + + Lemma Interp_SubstVarFstSndPairOppCast {t} (e : expr.Expr t) (Hwf : expr.Wf e) + : Interp (SubstVarLike.SubstVarFstSndPairOppCast e) == Interp e. + Proof. apply Interp_SubstVarOrIdent, Hwf. Qed. + End with_cast. + End SubstVarLike. + + Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOppCast SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf. + Hint Rewrite @SubstVarLike.Interp_SubstVar @SubstVarLike.Interp_SubstVarFstSndPairOppCast @SubstVarLike.Interp_SubstVarLike @SubstVarLike.Interp_SubstVarOrIdent : interp. + + Module UnderLets. + Import UnderLets.Compilers.UnderLets. + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + Local Notation UnderLets := (@UnderLets base_type ident). + + Section with_var. + Context {var1 var2 : type -> Type}. + + Inductive wf {T1 T2} {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} + : list { t : type & var1 t * var2 t }%type -> @UnderLets var1 T1 -> @UnderLets var2 T2 -> Prop := + | Wf_Base G e1 e2 : P G e1 e2 -> wf G (Base e1) (Base e2) + | Wf_UnderLet G A x1 x2 f1 f2 + : expr.wf G x1 x2 + -> (forall v1 v2, wf (existT _ A (v1, v2) :: G) (f1 v1) (f2 v2)) + -> wf G (UnderLet x1 f1) (UnderLet x2 f2). + Global Arguments wf {T1 T2} P _ _ _. + + Lemma wf_Proper_list_impl {T1 T2} + (P1 P2 : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop) + G1 G2 + (HP : forall seg v1 v2, P1 (seg ++ G1) v1 v2 -> P2 (seg ++ G2) v1 v2) + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + e1 e2 + (Hwf : @wf T1 T2 P1 G1 e1 e2) + : @wf T1 T2 P2 G2 e1 e2. + Proof. + revert dependent G2; induction Hwf; constructor; + repeat first [ progress cbn in * + | progress intros + | solve [ eauto ] + | progress subst + | progress destruct_head'_or + | progress inversion_sigma + | progress inversion_prod + | match goal with H : _ |- _ => apply H; clear H end + | wf_unsafe_t_step + | eapply (HP nil) + | rewrite ListUtil.app_cons_app_app in * ]. + Qed. + + Lemma wf_Proper_list {T1 T2} + {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} + (HP : forall G1 G2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> forall v1 v2, P G1 v1 v2 -> P G2 v1 v2) + G1 G2 + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + e1 e2 + (Hwf : @wf T1 T2 P G1 e1 e2) + : @wf T1 T2 P G2 e1 e2. + Proof. + eapply wf_Proper_list_impl; [ intros | | eassumption ]; eauto. + eapply HP; [ | eassumption ]; intros *. + rewrite !in_app_iff; intuition eauto. + Qed. + + Lemma wf_to_expr {t} (x : @UnderLets var1 (@expr var1 t)) (y : @UnderLets var2 (@expr var2 t)) + G + : wf (fun G => expr.wf G) G x y -> expr.wf G (to_expr x) (to_expr y). + Proof. + intro Hwf; induction Hwf; cbn [to_expr]; [ assumption | constructor; auto ]. + Qed. + + Lemma wf_splice {A1 B1 A2 B2} + {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : @UnderLets var1 A1) (x2 : @UnderLets var2 A2) (Hx : @wf _ _ P G x1 x2) + (e1 : A1 -> @UnderLets var1 B1) (e2 : A2 -> @UnderLets var2 B2) + (He : forall G' a1 a2, (exists seg, G' = seg ++ G) -> P G' a1 a2 -> @wf _ _ Q G' (e1 a1) (e2 a2)) + : @wf _ _ Q G (splice x1 e1) (splice x2 e2). + Proof. + induction Hx; cbn [splice]; [ | constructor ]; + eauto using (ex_intro _ nil); intros. + match goal with H : _ |- _ => eapply H end; + intros; destruct_head'_ex; subst. + rewrite ListUtil.app_cons_app_app in *. + eauto using (ex_intro _ nil). + Qed. + + Lemma wf_splice_list {A1 B1 A2 B2} + {P_parts : nat -> list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {P : list { t : type & var1 t * var2 t }%type -> list A1 -> list A2 -> Prop} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (P_parts_Proper_list : forall n G1 G2 a1 a2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> P_parts n G1 a1 a2 -> P_parts n G2 a1 a2) + (HP : forall G' l1 l2, + (exists seg, G' = seg ++ G) -> length l1 = length x1 -> length l2 = length x2 + -> (forall n v1 v2, nth_error l1 n = Some v1 -> nth_error l2 n = Some v2 -> P_parts n G' v1 v2) + -> P G' l1 l2) + (Hx_len : length x1 = length x2) + (Hx : forall n v1 v2, nth_error x1 n = Some v1 -> nth_error x2 n = Some v2 ->@wf _ _ (P_parts n) G v1 v2) + (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2) + (He : forall G' a1 a2, (exists seg, G' = seg ++ G) -> P G' a1 a2 -> @wf _ _ Q G' (e1 a1) (e2 a2)) + : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2). + Proof. + revert dependent P; revert dependent P_parts; revert dependent G; revert dependent e1; revert dependent e2; revert dependent x2; + induction x1 as [|x1 xs1 IHx1], x2 as [|x2 xs2]; + cbn [splice_list length nth_error]; intros; try congruence. + { eapply He; [ exists nil; reflexivity | eapply HP; eauto using (ex_intro _ nil) ]. + intros []; cbn [nth_error]; intros; congruence. } + { inversion Hx_len; clear Hx_len. + pose proof (fun n => Hx (S n)) as Hxs. + specialize (Hx O). + cbn [nth_error] in *. + eapply wf_splice; [ eapply Hx; reflexivity | wf_safe_t ]. + destruct_head'_ex; subst. + lazymatch goal with + | [ |- wf _ _ (splice_list _ (fun _ => ?e1 (?a1 :: _))) (splice_list _ (fun _ => ?e2 (?a2 :: _))) ] + => eapply IHx1 with (P_parts:=fun n => P_parts (S n)) (P:=fun G' l1 l2 => P G' (a1::l1) (a2::l2)) + end; wf_safe_t; destruct_head'_ex; wf_safe_t. + { eapply wf_Proper_list; [ | | eapply Hxs ]; wf_t. } + { eapply HP; cbn [length]; rewrite ?app_assoc; eauto; []. + intros []; cbn [nth_error]; wf_safe_t; inversion_option; wf_safe_t. + { eapply P_parts_Proper_list; [ | eauto ]; wf_t. } + { eapply P_parts_Proper_list; [ | eauto ]; wf_t. } } + { eapply He; eauto; rewrite ?app_assoc; eauto. } } + Qed. + + Lemma wf_splice_list_no_order {A1 B1 A2 B2} + {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (P_Proper_list : forall G1 G2 a1 a2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> P G1 a1 a2 -> P G2 a1 a2) + (Hx_len : length x1 = length x2) + (Hx : forall n v1 v2, nth_error x1 n = Some v1 -> nth_error x2 n = Some v2 ->@wf _ _ P G v1 v2) + (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2) + (He : forall G' a1 a2, (exists seg, G' = seg ++ G) + -> length a1 = length x1 + -> length a2 = length x2 + -> (forall v1 v2, List.In (v1, v2) (combine a1 a2) -> P G' v1 v2) + -> @wf _ _ Q G' (e1 a1) (e2 a2)) + : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2). + Proof. + apply @wf_splice_list + with (P_parts := fun _ => P) + (P:=fun G' l1 l2 => length l1 = length x1 /\ length l2 = length x2 + /\ forall v1 v2, List.In (v1, v2) (combine l1 l2) -> P G' v1 v2); + repeat first [ progress wf_safe_t + | apply conj + | progress inversion_option + | progress destruct_head'_ex + | progress break_innermost_match_hyps + | match goal with + | [ H : In _ (combine _ _) |- _ ] => apply ListUtil.In_nth_error_value in H + | [ H : context[nth_error (combine _ _) _] |- _ ] + => rewrite ListUtil.nth_error_combine in H + end ]. + Qed. + End with_var. + + Section for_interp. + Context {base_interp : base_type -> Type} + (ident_interp : forall t, ident t -> type.interp base_interp t). + + Local Notation UnderLets := (@UnderLets (type.interp base_interp)). + + Fixpoint interp {T} (v : UnderLets T) : T + := match v with + | Base v => v + | UnderLet A x f => let xv := expr.interp ident_interp x in + @interp _ (f xv) + end. + + Fixpoint interp_related {T1 T2} (R : T1 -> T2 -> Prop) (e : UnderLets T1) (v2 : T2) : Prop + := match e with + | Base v1 => R v1 v2 + | UnderLet t e f (* combine the App rule with the Abs rule *) + => exists fv ev, + expr.interp_related ident_interp e ev + /\ (forall x1 x2, + x1 == x2 + -> @interp_related T1 T2 R (f x1) (fv x2)) + /\ fv ev = v2 + end. + + Lemma interp_splice {A B} (x : UnderLets A) (e : A -> UnderLets B) + : interp (splice x e) = interp (e (interp x)). + Proof. induction x; cbn [splice interp]; eauto. Qed. + + Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B) + : interp (splice_list x e) + = interp (e (map interp x)). + Proof. + revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp map]; [ reflexivity | ]. + rewrite interp_splice, IHx; reflexivity. + Qed. + + Lemma interp_to_expr {t} (x : UnderLets (expr t)) + : expr.interp ident_interp (to_expr x) = expr.interp ident_interp (interp x). + Proof. induction x; cbn [expr.interp interp to_expr]; cbv [LetIn.Let_In]; eauto. Qed. + + Lemma interp_of_expr {t} (x : expr t) + : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x. + Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed. + + Lemma to_expr_interp_related_iff {t e v} + : interp_related (expr.interp_related ident_interp (t:=t)) e v + <-> expr.interp_related ident_interp (UnderLets.to_expr e) v. + Proof using Type. + revert v; induction e; cbn [UnderLets.to_expr interp_related expr.interp_related]; try reflexivity. + setoid_rewrite H. + reflexivity. + Qed. + + Global Instance interp_related_Proper_iff {T1 T2} + : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related T1 T2) | 10. + Proof using Type. + cbv [pointwise_relation respectful Proper]. + intros R1 R2 HR x y ? x' y' H'; subst y y'. + revert x'; induction x; [ apply HR | ]; cbn [interp_related]. + setoid_rewrite H; reflexivity. + Qed. + + Lemma splice_interp_related_iff {A B T R x e} {v : T} + : interp_related R (@UnderLets.splice _ ident _ A B x e) v + <-> interp_related + (fun xv => interp_related R (e xv)) + x v. + Proof using Type. + revert v; induction x; cbn [UnderLets.splice interp_related]; [ reflexivity | ]. + match goal with H : _ |- _ => setoid_rewrite H end. + reflexivity. + Qed. + + Lemma splice_list_interp_related_iff_gen {A B T R x e1 e2 base} {v : T} + (He1e2 : forall ls', e1 ls' = e2 (base ++ ls')) + : interp_related R (@UnderLets.splice_list _ ident _ A B x e1) v + <-> list_rect + (fun _ => list _ -> _ -> Prop) + (fun ls v => interp_related R (e2 ls) v) + (fun x xs recP ls v + => interp_related + (fun x' v => recP (ls ++ [x']) v) + x + v) + x + base + v. + Proof using Type. + revert base v e1 e2 He1e2; induction x as [|? ? IHx]; cbn [UnderLets.splice_list interp_related list_rect]; intros. + { intros; rewrite He1e2, ?app_nil_r; reflexivity. } + { setoid_rewrite splice_interp_related_iff. + apply interp_related_Proper_iff; [ | reflexivity.. ]; cbv [pointwise_relation]; intros. + specialize (fun v => IHx (base ++ [v])). + setoid_rewrite IHx; [ reflexivity | ]. + intros; rewrite He1e2, <- ?app_assoc; reflexivity. } + Qed. + + Lemma splice_list_interp_related_iff {A B T R x e} {v : T} + : interp_related R (@UnderLets.splice_list _ ident _ A B x e) v + <-> list_rect + (fun _ => list _ -> _ -> Prop) + (fun ls v => interp_related R (e ls) v) + (fun x xs recP ls v + => interp_related + (fun x' v => recP (ls ++ [x']) v) + x + v) + x + nil + v. + Proof using Type. + apply splice_list_interp_related_iff_gen; reflexivity. + Qed. + + Lemma splice_interp_related_of_ex {A B T T' RA RB x e} {v : T} + : (exists ev (xv : T'), + interp_related RA x xv + /\ (forall x1 x2, + RA x1 x2 + -> interp_related RB (e x1) (ev x2)) + /\ ev xv = v) + -> interp_related RB (@UnderLets.splice _ ident _ A B x e) v. + Proof using Type. + revert e v; induction x; cbn [interp_related UnderLets.splice]; intros. + all: repeat first [ progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | reflexivity + | match goal with + | [ H : _ |- _ ] => apply H; clear H + end ]. + do 2 eexists; repeat apply conj; [ eassumption | | ]; intros. + { match goal with H : _ |- _ => apply H; clear H end. + do 2 eexists; repeat apply conj; now eauto. } + { reflexivity. } + Qed. + + Lemma splice_list_interp_related_of_ex {A B T T' RA RB x e} {v : T} + : (exists ev (xv : list T'), + List.Forall2 (interp_related RA) x xv + /\ (forall x1 x2, + List.length x2 = List.length xv + -> List.Forall2 RA x1 x2 + -> interp_related RB (e x1) (ev x2)) + /\ ev xv = v) + -> interp_related RB (@UnderLets.splice_list _ ident _ A B x e) v. + Proof using Type. + revert e v; induction x as [|x xs IHxs]; cbn [interp_related UnderLets.splice_list]; intros. + all: repeat first [ progress destruct_head'_ex + | progress destruct_head'_and + | progress cbn [List.length] in * + | progress subst + | reflexivity + | match goal with + | [ H : List.Forall2 _ nil ?x |- _ ] => is_var x; inversion H; clear H + | [ H : List.Forall2 _ (cons _ _) ?x |- _ ] => is_var x; inversion H; clear H + | [ |- List.Forall2 _ _ _ ] => constructor + | [ H : _ |- _ ] => apply H; clear H + end ]. + lazymatch goal with + | [ H : forall l1 l2, length l2 = S (length _) -> Forall2 _ l1 l2 -> _ |- _ ] + => specialize (fun l ls l' ls' (pf0 : length _ = _) pf1 pf2 => H (cons l ls) (cons l' ls') (f_equal S pf0) (Forall2_cons _ _ pf1 pf2)) + end. + eapply splice_interp_related_of_ex; do 2 eexists; repeat apply conj; + intros; [ eassumption | | ]. + { eapply IHxs. + do 2 eexists; repeat apply conj; intros; + [ eassumption | | ]. + { match goal with H : _ |- _ => eapply H; clear H end; eassumption. } + { reflexivity. } } + { reflexivity. } + Qed. + + Lemma list_rect_interp_related {A B Pnil Pcons ls B' Pnil' Pcons' ls' R} + (Hnil : interp_related R Pnil Pnil') + (Hcons : forall x x', + expr.interp_related ident_interp x x' + -> forall l l', + List.Forall2 (expr.interp_related ident_interp) l l' + -> forall rec rec', + interp_related R rec rec' + -> interp_related R (Pcons x l rec) (Pcons' x' l' rec')) + (Hls : List.Forall2 (expr.interp_related ident_interp (t:=A)) ls ls') + : interp_related + R + (list_rect + (fun _ : list _ => UnderLets B) + Pnil + Pcons + ls) + (list_rect + (fun _ : list _ => B') + Pnil' + Pcons' + ls'). + Proof using Type. induction Hls; cbn [list_rect] in *; auto. Qed. + + Lemma nat_rect_interp_related {A PO PS n A' PO' PS' n' R} + (Hnil : interp_related R PO PO') + (Hcons : forall n rec rec', + interp_related R rec rec' + -> interp_related R (PS n rec) (PS' n rec')) + (Hn : n = n') + : interp_related + R + (nat_rect (fun _ => UnderLets A) PO PS n) + (nat_rect (fun _ => A') PO' PS' n'). + Proof using Type. subst n'; induction n; cbn [nat_rect] in *; auto. Qed. + + Lemma nat_rect_arrow_interp_related {A B PO PS n x A' B' PO' PS' n' x' R} + {R' : A -> A' -> Prop} + (Hnil : forall x x', R' x x' -> interp_related R (PO x) (PO' x')) + (Hcons : forall n rec rec', + (forall x x', R' x x' -> interp_related R (rec x) (rec' x')) + -> forall x x', + R' x x' + -> interp_related R (PS n rec x) (PS' n rec' x')) + (Hn : n = n') + (Hx : R' x x') + : interp_related + R + (nat_rect (fun _ => A -> UnderLets B) PO PS n x) + (nat_rect (fun _ => A' -> B') PO' PS' n' x'). + Proof using Type. subst n'; revert x x' Hx; induction n; cbn [nat_rect] in *; auto. Qed. + + Lemma interp_related_Proper_impl_same_UnderLets {A B B' R1 R2 e v f} + (HR : forall e v, (R1 e v : Prop) -> (R2 e (f v) : Prop)) + : @interp_related A B R1 e v + -> @interp_related A B' R2 e (f v). + Proof using Type. + revert f v HR; induction e; cbn [interp_related]; [ now eauto | ]; intros F v HR H'. + destruct H' as [fv H']; exists (fun ev => F (fv ev)). + repeat first [ let x := fresh "x" in destruct H' as [x H']; exists x + | let x := fresh "x" in intro x; specialize (H' x) + | let H := fresh "H" in destruct H' as [H H']; split; [ exact H || now subst | ] + | let H := fresh "H" in destruct H' as [H' H]; split; [ | exact H || now subst ] ]. + auto. + Qed. + End for_interp. + + Section for_interp2. + Context {base_interp1 base_interp2 : base_type -> Type} + {ident_interp1 : forall t, ident t -> type.interp base_interp1 t} + {ident_interp2 : forall t, ident t -> type.interp base_interp2 t}. + + Lemma wf_interp_Proper {T1 T2} + {P : list { t : type & type.interp base_interp1 t * type.interp base_interp2 t }%type -> T1 -> T2 -> Prop} + {G v1 v2} + (Hwf : @wf _ _ T1 T2 P G v1 v2) + : exists seg, P (seg ++ G) (interp ident_interp1 v1) (interp ident_interp2 v2). + Proof using Type. + induction Hwf; [ exists nil; cbn [List.app]; assumption | ]. + let H := match goal with H : forall v1 v2, ex _ |- _ => H end in + edestruct H as [seg ?]; eexists (seg ++ [_]). + rewrite <- List.app_assoc; cbn [List.app]. + eassumption. + Qed. + End for_interp2. + End with_ident. + + Section reify. + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). + + Section with_var. + Context {var1 var2 : type -> Type}. + Local Notation expr1 := (@expr.expr base.type ident var1). + Local Notation expr2 := (@expr.expr base.type ident var2). + Local Notation UnderLets1 := (@UnderLets.UnderLets base.type ident var1). + Local Notation UnderLets2 := (@UnderLets.UnderLets base.type ident var2). + + Local Ltac wf_reify_and_let_binds_base_cps_t Hk := + repeat first [ lazymatch goal with + | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H + end + | progress subst + | progress destruct_head' False + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress expr.invert_subst + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress type.inversion_type + | progress base.type.inversion_type + | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind combine list_rect length] in * + | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * + | rewrite base.try_make_transport_cps_correct in * + | progress type_beq_to_eq + | discriminate + | congruence + | apply Hk + | exists nil; reflexivity + | eexists (cons _ nil); reflexivity + | rewrite app_assoc; eexists; reflexivity + | progress wf_safe_t + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + end + | progress inversion_option + | progress break_innermost_match_hyps + | progress expr.inversion_wf_one_constr + | progress expr.invert_match_step + | match goal with |- wf _ _ _ _ => constructor end + | match goal with + | [ H : context[wf _ _ _ _] |- wf _ _ _ _ ] => apply H; eauto with nocore + end + | progress wf_unsafe_t_step + | match goal with + | [ H : context[match Compilers.reify_list ?ls with _ => _ end] |- _ ] + => is_var ls; destruct ls; rewrite ?expr.reify_list_cons, ?expr.reify_list_nil in H + | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H + | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] + => pose proof (fun x y pf => H x y (or_introl pf)); + pose proof (fun x y pf => H x y (or_intror pf)); + clear H + end ]. + + Lemma wf_reify_and_let_binds_base_cps {t : base.type} {T1 T2} (e1 : expr1 (type.base t)) (e2 : expr2 (type.base t)) + (k1 : expr1 (type.base t) -> UnderLets1 T1) (k2 : expr2 (type.base t) -> UnderLets2 T2) + (P : _ -> _ -> _ -> Prop) G + (Hwf : expr.wf G e1 e2) + (Hk : forall G' e1 e2, (exists seg, G' = seg ++ G) -> expr.wf G' e1 e2 -> wf P G' (k1 e1) (k2 e2)) + : wf P G (reify_and_let_binds_base_cps e1 T1 k1) (reify_and_let_binds_base_cps e2 T2 k2). + Proof. + revert dependent G; induction t; cbn [reify_and_let_binds_base_cps]; intros; + try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); + break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk. + all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. + all: revert dependent k1; revert dependent k2. + all: lazymatch goal with + | [ H : length ?l1 = length ?l2 |- _ ] + => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros + end; + wf_reify_and_let_binds_base_cps_t Hk. + Qed. + + Lemma wf_let_bind_return {t} (e1 : expr1 t) (e2 : expr2 t) + G + (Hwf : expr.wf G e1 e2) + : expr.wf G (let_bind_return e1) (let_bind_return e2). + Proof. + revert dependent G; induction t; intros; cbn [let_bind_return]; cbv [invert_Abs]; + wf_safe_t; + expr.invert_match; expr.inversion_wf; try solve [ wf_t ]. + { apply wf_to_expr. + pose (P := fun t => { e1e2 : expr1 t * expr2 t | expr.wf G (fst e1e2) (snd e1e2) }). + pose ((exist _ (e1, e2) Hwf) : P _) as pkg. + change e1 with (fst (proj1_sig pkg)). + change e2 with (snd (proj1_sig pkg)). + clearbody pkg; clear Hwf e1 e2. + type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. + cbn [fst snd proj1_sig proj2_sig] in *. + repeat match goal with + | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] + => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) + end. + assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). + revert pf. + rewrite H'; clear H'. + induction Hwf; break_innermost_match; break_innermost_match_hyps; + repeat first [ progress intros + | progress type.inversion_type + | progress base.type.inversion_type + | progress wf_safe_t + | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal] in * + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) + | [ |- wf _ _ _ _ ] => constructor + end + | solve [ eauto ] + | apply wf_reify_and_let_binds_base_cps ]. } + Qed. + End with_var. + + Section with_cast. + Context (cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z). + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation interp := (@expr.interp _ _ _ (@ident_interp)). + Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)). + + Lemma interp_reify_and_let_binds_base_cps + {t e T k} + (P : T -> Prop) + (Hk : forall e', interp e' = interp e -> P (UnderLets.interp (@ident_interp) (k e'))) + : P (UnderLets.interp (@ident_interp) (@reify_and_let_binds_base_cps _ t e T k)). + Proof. + revert T k P Hk; induction t; cbn [reify_and_let_binds_base_cps]; intros; + break_innermost_match; + expr.invert_subst; cbn [type.related UnderLets.interp fst snd expr.interp ident_interp] in *; subst; eauto; + repeat first [ progress intros + | reflexivity + | progress cbn [expr.interp ident_interp List.map] + | apply (f_equal2 (@pair _ _)) + | apply (f_equal2 (@cons _)) + | match goal with + | [ H : _ |- _ ] => apply H; clear H + | [ H : SubstVarLike.is_var_fst_snd_pair_opp_cast (reify_list _) = _ |- _ ] => clear H + | [ H : context[interp (reify_list _)] |- _ ] + => rewrite expr.interp_reify_list in H + | [ |- ?Q (UnderLets.interp _ (list_rect ?P ?X ?Y ?ls ?k)) ] + => is_var ls; is_var k; + revert dependent k; induction ls; cbn [list_rect]; + [ | generalize dependent (list_rect P X Y) ]; intros + end ]. + Qed. + + Lemma interp_reify_and_let_binds_base + {t e} + : interp (UnderLets.interp (@ident_interp) (@reify_and_let_binds_base_cps _ t e _ UnderLets.Base)) + = interp e. + Proof. + eapply interp_reify_and_let_binds_base_cps; cbn [UnderLets.interp]. + trivial. + Qed. + + Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk := + repeat first [ progress subst + | progress destruct_head' False + | progress destruct_head'_and + | progress destruct_head' iff + | progress specialize_by_assumption + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress expr.invert_subst + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress type.inversion_type + | progress base.type.inversion_type + | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in * + | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in * + | rewrite base.try_make_transport_cps_correct in * + | progress type_beq_to_eq + | discriminate + | congruence + | apply Hk + | exists nil; reflexivity + | eexists (cons _ nil); reflexivity + | rewrite app_assoc; eexists; reflexivity + | rewrite expr.reify_list_cons + | rewrite expr.reify_list_nil + | progress interp_safe_t + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H' + end + | progress inversion_option + | progress break_innermost_match_hyps + | progress expr.inversion_wf_one_constr + | progress expr.invert_match_step + | match goal with + | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ] + => solve [ eapply (@expr.wf_interp_Proper _ _ _ e1 e2); eauto ] + | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H + | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ] + => pose proof (fun x y pf => H x y (or_introl pf)); + pose proof (fun x y pf => H x y (or_intror pf)); + clear H + end + | progress interp_unsafe_t_step + | match goal with + | [ H : expr.wf _ (reify_list _) ?e |- _ ] + => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst; + [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ] + | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H + | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ] + => erewrite H; clear H; + [ match goal with + | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ] + => has_evar e; + let p := fresh in + set (p := expr.interp ii e); + match v with + | context G[expr.interp ii ?e'] + => unify e e'; let v' := context G[p] in change (k p = k' v') + end; + clearbody p; reflexivity + end + | .. ] + end ]. + + Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t)) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t'))) + (k2 : base.interp t -> base.interp t') + (Hk : forall e1 v, interp e1 == v -> interp (to_expr (k1 e1)) == k2 v) + : interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (interp e2). + Proof. + revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros; + try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption); + break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk. + all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end. + all: revert dependent k1; revert dependent k2. + all: lazymatch goal with + | [ H : length ?l1 = length ?l2 |- _ ] + => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros + end; + interp_to_expr_reify_and_let_binds_base_cps_t Hk. + Qed. + + Lemma interp_let_bind_return {t} (e1 e2 : expr t) + G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2) + (Hwf : expr.wf G e1 e2) + : interp (let_bind_return e1) == interp e2. + Proof. + revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *; + repeat first [ progress wf_safe_t + | progress expr.invert_subst + | progress expr.invert_match + | progress expr.inversion_wf + | progress break_innermost_match_hyps + | progress destruct_head' False + | solve [ wf_t ] + | match goal with + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ] + | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ] + => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ] + end ]; + []. + { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }). + pose ((exist _ (e1, e2) Hwf) : P _) as pkg. + change e1 with (fst (proj1_sig pkg)). + change e2 with (snd (proj1_sig pkg)). + clearbody pkg; clear Hwf e1 e2. + type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ]. + cbn [fst snd proj1_sig proj2_sig] in *. + repeat match goal with + | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ] + => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity) + | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ] + => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity) + end. + assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity). + revert pf. + rewrite H'; clear H'. + induction Hwf; break_innermost_match; break_innermost_match_hyps; + repeat first [ progress intros + | progress type.inversion_type + | progress base.type.inversion_type + | progress wf_safe_t + | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in * + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl) + | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl) + | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl) + | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In] + | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] + => eapply H; eauto with nocore + end + | solve [ eauto ] + | solve [ eapply expr.wf_interp_Proper; eauto ] ]. + all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. } + Qed. + + Ltac recurse_interp_related_step := + let do_replace v := + ((tryif is_evar v then fail else idtac); + let v' := open_constr:(_) in + let v'' := fresh in + cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in + match goal with + | _ => progress cbv [expr.interp_related] in * + | _ => progress cbn [type.interp] + | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand + | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand + | [ |- expr.interp_related_gen ?ident_interp ?R ?f ?v ] + => do_replace v + | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1), + _ /\ _ /\ fv ev = ?x ] + => first [ do_replace x + | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ] + | _ => progress intros + | [ |- expr.interp_related_gen _ _ _ ?ev ] => is_evar ev; eassumption + | [ |- expr.interp_related_gen _ _ (?f @ ?x) ?ev ] + => is_evar ev; + let fh := fresh in + let xh := fresh in + set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; + do 2 eexists; repeat apply conj; [ | | reflexivity ] + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh + | [ |- expr.interp_related_gen _ _ (expr.Ident ?idc) ?ev ] + => is_evar ev; + cbn [expr.interp_related_gen]; apply ident.gen_interp_Proper; reflexivity + | [ H : ?x == _ |- ?x == _ ] => exact H + | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else (progress subst) + | [ |- ?x = ?x ] => tryif has_evar x then fail else reflexivity + | [ |- ?ev = _ ] => is_evar ev; reflexivity + | [ |- _ = ?ev ] => is_evar ev; reflexivity + end. + + Local Ltac do_interp_related := + repeat first [ progress cbv beta + | progress recurse_interp_related_step + | eassumption + | do 2 eexists; repeat apply conj; intros + | match goal with + | [ H : _ |- _ ] => apply H; clear H; solve [ do_interp_related ] + end ]. + + Lemma reify_and_let_binds_base_interp_related_of_ex {t e T k T' R} {v : T'} + : (exists kv xv, + expr.interp_related (@ident_interp) e xv + /\ (forall x1 x2, + expr.interp_related (@ident_interp) x1 x2 + -> interp_related (@ident_interp) R (k x1) (kv x2)) + /\ kv xv = v) + -> interp_related (@ident_interp) R (@reify_and_let_binds_base_cps _ t e T k) v. + Proof using Type. + cbv [expr.interp_related]; revert T T' k R v; induction t. + all: repeat first [ progress cbn [expr.interp_related_gen interp_related reify_and_let_binds_base_cps fst snd] in * + | progress cbv [expr.interp_related] in * + | progress intros + | assumption + | progress destruct_head'_ex + | progress destruct_head'_and + | break_innermost_match_step + | progress expr.invert_subst + | solve [ eauto ] + | solve [ do_interp_related ] + | match goal with + | [ H : expr.interp_related_gen ?ii _ (reify_list ?ls1) ?ls2 |- _ ] => change (expr.interp_related ii (reify_list ls1) ls2) in H; rewrite expr.reify_list_interp_related_iff in H + end ]. + all: match goal with + | [ H : SubstVarLike.is_var_fst_snd_pair_opp_cast _ = _ |- _ ] => clear H + end. + all: lazymatch goal with + | [ H : List.Forall2 _ ?ls1 ?ls2 + |- interp_related _ _ + (list_rect ?Pv ?Nv ?Cv ?ls1 ?k) + (?f ?ls2) ] + => let P := fresh "P" in + let N := fresh "N" in + let C := fresh "C" in + is_var k; is_var f; is_var ls1; is_var ls2; + set (P:=Pv); set (N:=Nv); set (C:=Cv); + revert dependent f; intro f; revert dependent k; intro k; revert f k; + induction H; cbn [list_rect]; intros + end. + all: repeat match goal with + | [ F := ?f |- _ ] + => match goal with + | [ |- context G[F ?x] ] + => let G' := context G[f x] in + change G'; cbv beta + end + | [ H : forall x1 x2, ?R x1 x2 -> ?R' (?f1 x1) (?f2 x2) |- ?R' (?f1 _) (?f2 _) ] + => apply H; clear H + | [ |- expr.interp_related_gen _ _ _ nil ] => reflexivity + | [ H : _ |- interp_related _ _ (reify_and_let_binds_base_cps _ _ _) _ ] => apply H + | [ |- exists kv xv, _ /\ _ /\ kv xv = ?f (?x :: ?xs) ] + => exists (fun x' => f (x' :: xs)), x; repeat apply conj; [ | | reflexivity ] + | _ => assumption + | _ => progress intros + | [ IH : (forall k k', _ -> ?R (list_rect ?P ?N ?C ?ls1 k') (k ?ls2)) + |- ?R (list_rect ?P ?N ?C ?ls1 ?k'v) ?RHS ] + => let kv := match (eval pattern ls2 in RHS) with ?kv _ => kv end in + apply (IH kv k'v); clear IH + | _ => solve [ do_interp_related ] + end. + Qed. + + Lemma reify_and_let_binds_base_interp_related {t e v} + : expr.interp_related (@ident_interp) e v + -> interp_related (@ident_interp) (expr.interp_related (@ident_interp)) (@reify_and_let_binds_base_cps _ t e _ Base) v. + Proof using Type. + intro; eapply reify_and_let_binds_base_interp_related_of_ex. + eexists id, _; eauto. + Qed. + + Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : Interp (LetBindReturn e) == Interp e. + Proof. + apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto. + Qed. + End with_cast. + + Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e). + Proof. intros ??; apply wf_let_bind_return, Hwf. Qed. + End reify. + End UnderLets. + + Hint Resolve UnderLets.Wf_LetBindReturn : wf. + Hint Rewrite @UnderLets.Interp_LetBindReturn : interp. +End Compilers. |