diff options
Diffstat (limited to 'src/hls/AbstrSemIdent.v')
-rw-r--r-- | src/hls/AbstrSemIdent.v | 665 |
1 files changed, 665 insertions, 0 deletions
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v new file mode 100644 index 0000000..0cc8e9d --- /dev/null +++ b/src/hls/AbstrSemIdent.v @@ -0,0 +1,665 @@ +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Linking. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePargenproofEquiv. +Require Import vericert.hls.GiblePargen. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.Abstr. +Require Import vericert.common.Monad. + +Module Import OptionExtra := MonadExtra(Option). + +#[local] Open Scope positive. +#[local] Open Scope forest. +#[local] Open Scope pred_op. + +#[local] Opaque simplify. +#[local] Opaque deep_simplify. + +#[local] Ltac destr := destruct_match; try discriminate; []. + +Inductive sem_ident {B A: Type} (c: @Abstr.ctx B) (a: A): A -> Prop := +| sem_ident_intro : sem_ident c a a. + +Section PROOF. + +Context (A B G: Type). +Context (ctx: @Abstr.ctx G). +Context (a_sem: @Abstr.ctx G -> A -> B -> Prop). + +Lemma eval_predf_negate : + forall ps p, + eval_predf ps (negate p) = negb (eval_predf ps p). +Proof. + unfold eval_predf; intros. rewrite negate_correct. auto. +Qed. + +Lemma is_truthy_negate : + forall ps p pred, + truthy ps p -> + falsy ps (combine_pred (Some (negate (Option.default T p))) pred). +Proof. + inversion 1; subst; simplify. + - destruct pred; constructor; auto. + - destruct pred; constructor. + rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto. + rewrite eval_predf_negate. rewrite H0. auto. +Qed. + +Lemma sem_pred_expr_NEapp : + forall f_p a b v, + sem_pred_expr f_p a_sem ctx a v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - inv H. constructor; auto. + - inv H. constructor; eauto. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_app_predicated_false : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx y v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = false -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v. +Proof. +Admitted. + +Lemma sem_pred_expr_prune_predicated : + forall f_p y x v, + sem_pred_expr f_p a_sem ctx x v -> + prune_predicated x = Some y -> + sem_pred_expr f_p a_sem ctx y v. +Proof. + intros * SEM PRUNE. unfold prune_predicated in *. +Admitted. + +Lemma sem_pred_expr_prune_predicated2 : + forall f_p y x v, + sem_pred_expr f_p a_sem ctx y v -> + prune_predicated x = Some y -> + sem_pred_expr f_p a_sem ctx x v. +Proof. + intros * SEM PRUNE. unfold prune_predicated in *. + Admitted. + +Lemma sem_pred_expr_app_predicated_false2 : + forall f_p y x v p ps, + sem_pred_expr f_p sem ctx (app_predicated p y x) v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = false -> + sem_pred_expr f_p sem ctx y v. +Admitted. + +Lemma sem_pred_expr_pred_ret : + forall (i: A) ps, + sem_pred_expr ps sem_ident ctx (pred_ret i) i. +Proof. intros; constructor; constructor. Qed. + +Lemma sem_pred_expr_ident_det : + forall A ps x (v v2: A), + sem_pred_expr ps sem_ident ctx x v -> + sem_pred_expr ps sem_ident ctx x v2 -> + v = v2. +Proof. + intros. + exploit (@sem_pred_expr_det G G). + apply similar_refl. + 2: { instantiate (4 := (fun x => @sem_ident x A0)). + cbn. eauto. } + intros. inv H1. inv H2. auto. + apply H. auto. +Qed. + +Lemma sem_pred_expr_NEapp2 : + forall f_p a b v ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + (forall x, NE.In x a -> eval_predf ps (fst x) = false) -> + sem_pred_expr f_p a_sem ctx b v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H0 _ IN). destruct a. + eapply sem_pred_expr_cons_false; eauto. cbn [fst] in *. + eapply sem_pexpr_eval; eauto. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H0 in H2. + destruct a. cbn [fst] in *. + eapply sem_pred_expr_cons_false. + eapply sem_pexpr_eval; eauto. eapply IHa; eauto. + intros. eapply H0. constructor; tauto. +Qed. + +Lemma sem_pred_expr_NEapp3 : + forall f_p ctx a b v, + (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> + sem_pred_expr f_p a_sem ctx b v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H _ IN). destruct a. + eapply sem_pred_expr_cons_false; eauto. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H in H1. + destruct a. cbn [fst] in *. + eapply sem_pred_expr_cons_false; auto. + eapply IHa; eauto. + intros. eapply H. constructor; tauto. +Qed. + +Lemma sem_pred_expr_NEapp4 : + forall f_p ctx a b v, + (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v -> + sem_pred_expr f_p a_sem ctx b v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H _ IN). inv H0; auto. + eapply sem_pexpr_det in H; eauto; now try apply similar_refl. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H in H1. inv H0. + eapply sem_pexpr_det in H1; eauto; now try apply similar_refl. + eapply IHa; eauto. intros. eapply H. apply NE.In_cons; auto. +Qed. + +Lemma sem_pred_expr_NEapp5 : + forall f_p ctx a b v, + (exists x, NE.In x a /\ sem_pexpr ctx (from_pred_op f_p (fst x)) true) -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v -> + sem_pred_expr f_p a_sem ctx a v. +Proof. + induction a; crush. + - inv H. inv H0. constructor; eauto. + eapply sem_pexpr_det in H2; eauto; now try apply similar_refl. + - inv H. inv H3. inv H0. constructor; auto. + eapply sem_pexpr_det in H2; eauto; now try apply similar_refl. inv H0. + constructor; auto. apply sem_pred_expr_cons_false; auto. eauto. +Qed. + +Lemma In_pexpr_eval : + forall A f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + forall (a: predicated A), + (exists x, NE.In x a /\ sem_pexpr ctx (from_pred_op f_p (fst x)) true) + \/ (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false). +Proof. + induction a; cbn in *. + - pose proof (sem_pexpr_evaluable _ _ _ _ H (fst a)); simplify. + destruct x. + + left. exists a. split; auto. constructor. + + right; intros. inv H0; auto. + - inv IHa; simplify. + + left. exists x. split; auto. apply NE.In_cons; auto. + + pose proof (sem_pexpr_evaluable _ _ _ _ H (fst a)); simplify. + destruct x. + * left. exists a; split; auto. constructor; auto. + * right; intros. inv H1. inv H4; auto. +Qed. + +Lemma sem_pred_expr_map_not : + forall A p ps y x0, + eval_predf ps p = false -> + NE.In x0 (NE.map (fun x => (p ∧ fst x, snd x)) y) -> + eval_predf ps (@fst _ A x0) = false. +Proof. + induction y; crush. + - inv H0. simplify. rewrite eval_predf_Pand. rewrite H. auto. + - inv H0. inv H2. cbn -[eval_predf]. rewrite eval_predf_Pand. + rewrite H. auto. eauto. +Qed. + +Lemma sem_pred_expr_map_Pand : + forall f_p ps x v p, + (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx x v -> + sem_pred_expr f_p a_sem ctx + (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v. +Proof. + induction x; crush. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + eapply sem_pred_expr_cons_false. cbn. + replace false with (true && false) by auto. apply sem_pexpr_Pand; auto. + eapply sem_pexpr_eval; eauto. eauto. +Qed. + +Lemma sem_pred_expr_app_predicated : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx x v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v. +Proof. + intros * SEM PS EVAL. unfold app_predicated. + eapply sem_pred_expr_NEapp2; eauto. + intros. eapply sem_pred_expr_map_not; eauto. + rewrite eval_predf_negate. rewrite EVAL. auto. + eapply sem_pred_expr_map_Pand; eauto. +Qed. + +Lemma sem_pred_expr_app_predicated2 : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx x v. +Proof. Admitted. + +Lemma sem_pred_expr_ident : + forall ps l l_, + sem_pred_expr ps sem_ident ctx l l_ -> + forall (v: B), + a_sem ctx l_ v -> + sem_pred_expr ps a_sem ctx l v. +Proof. + induction 1. + - intros. constructor; auto. inv H0. auto. + - intros. apply sem_pred_expr_cons_false; auto. + - intros. inv H0. constructor; auto. +Qed. + +Lemma sem_pred_expr_ident2 : + forall ps l v, + sem_pred_expr ps a_sem ctx l v -> + exists l_, sem_pred_expr ps sem_ident ctx l l_ /\ a_sem ctx l_ v. +Proof. + induction 1. + - exists e; split; auto. constructor; auto. constructor. + - inversion_clear IHsem_pred_expr as [x IH]. + inversion_clear IH as [SEM EVALS]. + exists x; split; auto. apply sem_pred_expr_cons_false; auto. + - exists e; split; auto; constructor; auto; constructor. +Qed. + +Fixpoint of_elist (e: expression_list): list expression := + match e with + | Econs a b => a :: of_elist b + | Enil => nil + end. + +Fixpoint to_elist (e: list expression): expression_list := + match e with + | a :: b => Econs a (to_elist b) + | nil => Enil + end. + +Lemma sem_val_list_elist : + forall l j, + sem_val_list ctx (to_elist l) j -> + Forall2 (sem_value ctx) l j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist2 : + forall l j, + Forall2 (sem_value ctx) l j -> + sem_val_list ctx (to_elist l) j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist3 : + forall l j, + sem_val_list ctx l j -> + Forall2 (sem_value ctx) (of_elist l) j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist4 : + forall l j, + Forall2 (sem_value ctx) (of_elist l) j -> + sem_val_list ctx l j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_pred_expr_predicated_map : + forall pr (f: A -> B) pred pred', + sem_pred_expr pr sem_ident ctx pred pred' -> + sem_pred_expr pr sem_ident ctx (predicated_map f pred) (f pred'). +Proof. + induction pred; unfold predicated_map; intros. + - inv H. inv H3. constructor; eauto. constructor. + - inv H. inv H5. constructor; eauto. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_predicated_map2 : + forall pr (f: A -> B) pred x, + sem_pred_expr pr sem_ident ctx (predicated_map f pred) x -> + exists pred', sem_pred_expr pr sem_ident ctx pred pred' /\ x = f pred'. +Proof. + induction pred; unfold predicated_map; intros. + - cbn in *. inv H. inv H5. destruct a. exists a. + split; auto. constructor; auto. constructor. + - cbn in *. inv H. destruct a. inv H6. cbn [fst snd] in *. + exists a; repeat constructor; auto. + exploit IHpred; eauto; simplify. + exists x0; split; auto. + destruct a. apply sem_pred_expr_cons_false; auto. +Qed. + +End PROOF. + +Section PROOF. + +Context (G: Type). +Context (ctx: @Abstr.ctx G). + +Lemma sem_pred_expr_predicated_prod : + forall A B pr (a: predicated A) (b: predicated B) a' b', + sem_pred_expr pr sem_ident ctx a a' -> + sem_pred_expr pr sem_ident ctx b b' -> + sem_pred_expr pr sem_ident ctx (predicated_prod a b) (a', b'). +Proof. + induction a; intros. + - inv H. inv H4. unfold predicated_prod. + generalize dependent b. induction b; intros. + + cbn. destruct_match. inv Heqp. inv H0. inv H6. + constructor. simplify. replace true with (true && true) by auto. + eapply sem_pexpr_Pand; eauto. constructor. + + inv H0. inv H6. cbn. constructor; cbn. + replace true with (true && true) by auto. + constructor; auto. constructor. + eapply sem_pred_expr_cons_false; eauto. cbn. + replace false with (true && false) by auto. + apply sem_pexpr_Pand; auto. + - unfold predicated_prod. simplify. + rewrite NE.app_NEmap. + inv H. eapply sem_pred_expr_NEapp. + { induction b; crush. + destruct a. inv H0. constructor. + replace true with (true && true) by auto. + eapply sem_pexpr_Pand; auto. inv H6. inv H7. + constructor. + + destruct a. inv H0. constructor. + replace true with (true && true) by auto. + constructor; auto. inv H8. inv H6. constructor. + + specialize (IHb H8). eapply sem_pred_expr_cons_false; auto. + replace false with (true && false) by auto. + apply sem_pexpr_Pand; auto. + } + { exploit IHa. eauto. eauto. intros. + unfold predicated_prod in *. + eapply sem_pred_expr_NEapp3; eauto; []. + clear H. clear H0. + induction b. + { intros. inv H. destruct a. simpl. + constructor; tauto. } + { intros. inv H. inv H1. destruct a. simpl. + constructor; tauto. eauto. } } +Qed. + +Lemma sem_pred_expr_predicated_prod2 : + forall A B f ps (a: predicated A) (b: predicated B) x, + (forall x, sem_pexpr ctx (get_forest_p' x f) (ps !! x)) -> + sem_pred_expr f sem_ident ctx (predicated_prod a b) x -> + sem_pred_expr f sem_ident ctx a (fst x) + /\ sem_pred_expr f sem_ident ctx b (snd x). +Proof. + induction a; intros. + - generalize dependent x. generalize dependent b. induction b; intros. + + cbn in *; repeat destr; destruct a, a0. inv Heqp. inv Heqp0. + inv H0. inv H6; split. + * constructor. inv H4. tauto. constructor. + * cbn in *. inv H4. constructor. tauto. constructor. + + destruct x; cbn in *. repeat destr. inv Heqp0. inv H0. + * inv H6. inv H7. repeat (constructor; auto). + * exploit IHb; eauto; intros. inv H0. cbn in *. inv H6. + inv H3. inv H1. eapply sem_pexpr_det in H0; try eassumption. discriminate. + apply similar_refl. split; auto. + apply sem_pred_expr_cons_false; auto. + - destruct x in *; cbn in *. + rewrite NE.app_NEmap in H0. + generalize dependent b; induction b; intros. + + cbn in *; repeat destr. inv Heqp0. inv H0. + * inv H6. inv H7. solve [repeat constructor; auto]. + * inv H6. inv H1. + -- exploit IHa; eauto; intros. inv H1. split; auto. + apply sem_pred_expr_cons_false; eauto. + -- exploit IHa; eauto; intros. inv H1. inv H3. + eapply sem_pexpr_det in H0; try eassumption. discriminate. + apply similar_refl. + + Admitted. + +Lemma sem_pred_expr_seq_app : + forall A B (f: predicated (A -> B)) ps l f_ l_, + sem_pred_expr ps sem_ident ctx l l_ -> + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (seq_app f l) (f_ l_). +Proof. + unfold seq_app; intros. + remember (fun x : (A -> B) * A => fst x (snd x)) as app. + replace (f_ l_) with (app (f_, l_)) by (rewrite Heqapp; auto). + eapply sem_pred_expr_predicated_map. eapply sem_pred_expr_predicated_prod; auto. +Qed. + +Lemma sem_pred_expr_seq_app2 : + forall A B (f: predicated (A -> B)) ps pr l x_, + (forall x, sem_pexpr ctx (get_forest_p' x ps) (pr !! x)) -> + sem_pred_expr ps sem_ident ctx (seq_app f l) x_ -> + exists l_ f_, + x_ = f_ l_ + /\ sem_pred_expr ps sem_ident ctx l l_ + /\ sem_pred_expr ps sem_ident ctx f f_. +Proof. + unfold seq_app; intros. + remember (fun x : (A -> B) * A => fst x (snd x)) as app. + exploit sem_pred_expr_predicated_map2; eauto; simplify. + exploit sem_pred_expr_predicated_prod2; eauto; simplify. + eauto. +Qed. + +Lemma sem_pred_expr_map : + forall A B ps (f: A -> B) y v, + sem_pred_expr ps sem_ident ctx y v -> + sem_pred_expr ps sem_ident ctx (NE.map (fun x => (fst x, f (snd x))) y) (f v). +Proof. + induction y; crush. inv H. constructor; crush. inv H3. constructor. + inv H. inv H5. constructor; eauto. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_flap : + forall A B C (f: predicated (A -> B -> C)) ps l f_, + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (flap f l) (f_ l). +Proof. + induction f. unfold flap2; intros. inv H. inv H3. + constructor; eauto. constructor. + intros. inv H. cbn. + constructor; eauto. inv H5. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_flap2 : + forall A B C (f: predicated (A -> B -> C)) ps l1 l2 f_, + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) (f_ l1 l2). +Proof. + induction f. unfold flap2; intros. inv H. inv H3. + constructor; eauto. constructor. + intros. inv H. cbn. + constructor; eauto. inv H5. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_seq_app_val : + forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) + (f: predicated (A -> B)) + ps l v f_ l_, + sem_pred_expr ps sem_ident ctx l l_ -> + sem_pred_expr ps sem_ident ctx f f_ -> + s ctx (f_ l_) v -> + sem_pred_expr ps s ctx (seq_app f l) v. +Proof. + intros. eapply sem_pred_expr_ident; [|eassumption]. + eapply sem_pred_expr_seq_app; eauto. +Qed. + +Lemma sem_pred_expr_seq_app_val2 : + forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) + (f: predicated (A -> B)) ps pr l v, + (forall x, sem_pexpr ctx (get_forest_p' x ps) (pr !! x)) -> + sem_pred_expr ps s ctx (seq_app f l) v -> + exists f_ l_, + sem_pred_expr ps sem_ident ctx l l_ + /\ sem_pred_expr ps sem_ident ctx f f_ + /\ s ctx (f_ l_) v. +Proof. + intros; exploit sem_pred_expr_ident2; eauto; simplify. + exploit sem_pred_expr_seq_app2; eauto; simplify. + eauto. +Qed. + +Fixpoint Eapp a b := + match a with + | Enil => b + | Econs ax axs => Econs ax (Eapp axs b) + end. + +Lemma Eapp_right_nil : + forall a, Eapp a Enil = a. +Proof. induction a; cbn; try rewrite IHa; auto. Qed. + +Lemma Eapp_left_nil : + forall a, Eapp Enil a = a. +Proof. auto. Qed. + +Lemma sem_pred_expr_cons_pred_expr : + forall pr s s' a e, + sem_pred_expr pr sem_ident ctx s s' -> + sem_pred_expr pr sem_ident ctx a e -> + sem_pred_expr pr sem_ident ctx (cons_pred_expr a s) (Econs e s'). +Proof. + intros. unfold cons_pred_expr. + replace (Econs e s') with ((uncurry Econs) (e, s')) by auto. + eapply sem_pred_expr_predicated_map. + eapply sem_pred_expr_predicated_prod; eauto. +Qed. + +Lemma sem_pred_expr_fold_right : + forall pr s a a' s', + sem_pred_expr pr sem_ident ctx s s' -> + Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a') -> + sem_pred_expr pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s'). +Proof. + induction a; crush. inv H0. inv H5. destruct a'; crush. destruct a'; crush. + inv H3. eapply sem_pred_expr_cons_pred_expr; eauto. + inv H0. destruct a'; crush. inv H3. + eapply sem_pred_expr_cons_pred_expr; eauto. +Qed. + +Lemma sem_pred_expr_fold_right2 : + forall A pr ctx s a a' s', + sem_pred_expr pr sem_ident ctx s s' -> + @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') -> + Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a'). +Proof. + induction a. Admitted. + +Lemma sem_pred_expr_merge : + forall G (ctx: @Abstr.ctx G) ps l args, + Forall2 (sem_pred_expr ps sem_ident ctx) args l -> + sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). +Proof. + induction l; intros. + - inv H. cbn; repeat constructor. + - inv H. cbn. unfold merge. Admitted. + +Lemma sem_pred_expr_merge2 : + forall pr l l', + sem_pred_expr pr sem_ident ctx (merge l) l' -> + Forall2 (sem_pred_expr pr sem_ident ctx) l (of_elist l'). +Proof. + induction l; crush. + - unfold merge in *; cbn in *. + inv H. inv H5. constructor. + - unfold merge in H. + pose proof (NE.of_list_exists _ l a) as Y. + inversion_clear Y as [x HNE]. rewrite HNE in H. + erewrite <- (NE.of_list_to_list _ (a :: l)) by eassumption. + apply sem_pred_expr_fold_right2 with (s := (NE.singleton (T, Enil))) (s' := Enil). + repeat constructor. + rewrite Eapp_right_nil. auto. +Qed. + +Lemma sem_merge_list : (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) + forall f rs ps m args, + sem ctx f ((mk_instr_state rs ps m), None) -> + sem_pred_expr (forest_preds f) sem_val_list ctx + (merge (list_translation args f)) (rs ## args). +Proof. + induction args; crush. cbn. constructor; constructor. + unfold merge. specialize (IHargs H). + eapply sem_pred_expr_ident2 in IHargs. + inversion_clear IHargs as [l_ [HSEM HVAL]]. + destruct_match; [|exfalso; eapply NE.of_list_contra; eauto]. + destruct args; cbn -[NE.of_list] in *. + - unfold merge in *. simplify. + inv H. inv H6. specialize (H a). + eapply sem_pred_expr_ident2 in H. + inversion_clear H as [l_2 [HSEM2 HVAL2]]. + unfold cons_pred_expr. + eapply sem_pred_expr_ident. + eapply sem_pred_expr_predicated_map. + eapply sem_pred_expr_predicated_prod; [eassumption|repeat constructor]. + repeat constructor; auto. + - pose proof (NE.of_list_exists2 _ (list_translation args f) (f #r (Reg r)) (f #r (Reg a))) as Y. + inversion_clear Y as [x [Y1 Y2]]. rewrite Heqo in Y1. inv Y1. + inversion_clear H as [? ? ? ? ? ? REG PRED MEM EXIT]. + inversion_clear REG as [? ? ? REG']. + inversion_clear PRED as [? ? ? PRED']. + pose proof (REG' a) as REGa. pose proof (REG' r) as REGr. + exploit sem_pred_expr_ident2; [exact REGa|]. + intro REGI'; inversion_clear REGI' as [a' [SEMa SEMa']]. + exploit sem_pred_expr_ident2; [exact REGr|]. + intro REGI'; inversion_clear REGI' as [r' [SEMr SEMr']]. + apply sem_pred_expr_ident with (l_ := Econs a' l_); [|constructor; auto]. + replace (Econs a' l_) with (Eapp (Econs a' l_) Enil) by (now apply Eapp_right_nil). + apply sem_pred_expr_fold_right; eauto. + repeat constructor. + constructor; eauto. + erewrite NE.of_list_to_list; eauto. + eapply sem_pred_expr_merge2; auto. +Qed. + +Lemma sem_pred_expr_list_translation : + forall args f i, + sem ctx f (i, None) -> + exists l, + Forall2 (sem_pred_expr (forest_preds f) sem_ident ctx) (list_translation args f) l + /\ sem_val_list ctx (to_elist l) ((is_rs i)##args). +Proof. + induction args; intros. + - exists nil; cbn; split; auto; constructor. + - exploit IHargs; try eassumption; intro EX. + inversion_clear EX as [l [FOR SEM]]. + destruct i as [rs' m' ps']. + inversion_clear H as [? ? ? ? ? ? REGSET PREDSET MEM EXIT]. + inversion_clear REGSET as [? ? ? REG]. + pose proof (REG a). + exploit sem_pred_expr_ident2; eauto; intro IDENT. + inversion_clear IDENT as [l_ [SEMP SV]]. + exists (l_ :: l). split. constructor; auto. + cbn; constructor; auto. +Qed. + +End PROOF. |