(* this file is a version of veric/semax_ext.v that let external
specifications reason about the oracle. *)

Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.juicy_mem_lemmas.
Require Import VST.veric.juicy_mem_ops.
Require Import VST.sepcomp.extspec.
Require Import VST.veric.juicy_extspec.
Require Import compcert.cfrontend.Clight.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.semax.
Require Import VST.veric.semax_call.
Require Import VST.veric.semax_ext.
Require Import VST.veric.res_predicates.

(* NOTE.   ext_link: Strings.String.string -> ident
   represents the mapping from the _name_ of an external function
  (an ASCII string) to the [ident] that's used to represent it in this program module.
  That mapping can be computed from the prog_defs component of the Clight.program
  produced by clightgen.
*)

Section funspecsOracle2jspec.

Variable Z : Type.
Variable Espec : juicy_ext_spec Z.

Definition funspecOracle2pre (ext_link: Strings.String.string -> ident) (A : Type) (P : A -> Z -> environ -> mpred) (ids: list ident) (id: ident) sig (ef: external_function) x ge_s
           (tys : list typ) args z m : Prop :=
  match oi_eq_dec (Some (id, sig)) (ef_id_sig ext_link ef) as s
  return ((if s then (rmap * A)%type else ext_spec_type Espec ef) -> Prop)
  with
  | left _ =>
    fun x => exists phi0 phi1, join phi0 phi1 (m_phi m)
                       /\ P (snd x) z (make_ext_args (filter_genv (symb2genv ge_s)) ids args) phi0
                       /\ necR (fst x) phi1
  | right n => fun x' => ext_spec_pre Espec ef x' ge_s tys args z m
  end x.

Definition funspecOracle2post (ext_link: Strings.String.string -> ident) (A : Type) (Q : A -> Z -> environ -> mpred)
                        id sig ef x ge_s (tret : option typ) ret z m : Prop :=
  match oi_eq_dec (Some (id, sig)) (ef_id_sig ext_link ef) as s
  return ((if s then (rmap * A)%type else ext_spec_type Espec ef) -> Prop)
  with
  | left _ =>
    fun x => exists phi0 phi1, join phi0 phi1 (m_phi m)
                       /\ Q (snd x) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret) phi0
                       /\ necR (fst x) phi1
  | right n => fun x' => ext_spec_post Espec ef x' ge_s tret ret z m
  end x.

Inductive funspecOracle : Type :=
  mk_funspecOracle : funsig -> calling_convention -> forall A : Type,
      (A -> Z -> environ -> mpred) ->
      (A -> Z -> environ -> mpred) -> funspecOracle.

Definition funspecOracle2extspec (ext_link: Strings.String.string -> ident) (f : ident * funspecOracle)
  : external_specification juicy_mem external_function Z :=
  match f with
    | (id, mk_funspecOracle ((params, sigret) as fsig) cc A P Q) =>
      let sig := funsig2signature fsig cc in
      Build_external_specification juicy_mem external_function Z
        (fun ef => if oi_eq_dec (Some (id, sig)) (ef_id_sig ext_link ef) then (rmap * A)%type else ext_spec_type Espec ef)
        (funspecOracle2pre ext_link A P (fst (split params)) id sig)
        (funspecOracle2post ext_link A Q id sig)
        (fun rv z m => False)
  end.

Local Open Scope pred.

Definition wf_funspecOracle (f : funspecOracle) :=
  match f with
    | mk_funspecOracle sig cc A P Q =>
        forall a (ge ge': genv) n args z,
          Genv.genv_symb ge = Genv.genv_symb ge' ->
          P a z (make_ext_args (filter_genv ge) n args) |-- P a z (make_ext_args (filter_genv ge') n args)
  end.

Lemma make_ext_args_symb (ge ge' : genv)
      (H: Genv.genv_symb ge = Genv.genv_symb ge') n args :
  make_ext_args (filter_genv ge) n args = make_ext_args (filter_genv ge') n args.
Proof.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n args) (make_ext_args (filter_genv ge') n args) *)
revert ge ge' n H; induction args.
* simpl; unfold filter_genv, Genv.find_symbol. intros ? ? ? ->; auto.
* intros ge ge' n H. simpl. destruct n; auto.
(* Goal: @eq environ (env_set (make_ext_args (filter_genv ge) n args) i a) (env_set (make_ext_args (filter_genv ge') n args) i a) *)
  erewrite IHargs; eauto.
(* Goal: @eq environ (env_set (make_ext_args (filter_genv ge) n args) i a) (env_set (make_ext_args (filter_genv ge') n args) i a) *)
  erewrite IHargs; eauto.
Qed.

Lemma all_funspecsOracle_wf f : wf_funspecOracle f.
Proof.
(* Goal: wf_funspecOracle f *)
destruct f; simpl; intros a ge ge' n args z H.
(* Goal: @derives rmap ag_rmap (m a z (make_ext_args (filter_genv ge) n args)) (m a z (make_ext_args (filter_genv ge') n args)) *)
erewrite make_ext_args_symb; eauto.
Qed.

Program Definition funspecOracle2jspec (ext_link: Strings.String.string -> ident) f : juicy_ext_spec Z :=
  Build_juicy_ext_spec _ (funspecOracle2extspec ext_link f) _ _ _.
Next Obligation.
destruct f; simpl; unfold funspecOracle2pre, pureat; simpl; destruct f; simpl;
  destruct f; simpl; intros e t0 ge_s typs args z.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) as s return (forall _ : if s then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (Q (@snd rmap A x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e0|e0].
* destruct e; try discriminate; injection e0 as E; subst i sg; intros a a' Hage.
(* Goal: forall _ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a)) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
intros [phi0 [phi1 [Hjoin [Hx Hy]]]].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
apply age1_juicy_mem_unpack in Hage.
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
destruct Hage as [Hage Hdry].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
destruct (age1_join2 phi0 Hjoin Hage) as [x' [y' [Hjoin' [Hage' H]]]].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
exists x', y'; split; auto.
(* Goal: and (@app_pred rmap ag_rmap (m (@snd rmap A t0) z (make_ext_args (filter_genv (symb2genv ge_s)) (@fst (list ident) (list type) (@split ident type l)) args)) x') (@necR rmap ag_rmap (@fst rmap A t0) y') *)
destruct m. split. eapply h; eauto.
(* Goal: @necR rmap ag_rmap (@fst rmap A t0) y' *)
apply (necR_trans (fst t0) phi1 y'); auto.
(* Goal: @necR rmap ag_rmap phi1 y' *)
unfold necR. constructor; auto.
* intros ? ?; auto.
(* Goal: forall (_ : @age juicy_mem juicy_mem_ageable a a') (_ : @ext_spec_pre juicy_mem external_function Z (JE_spec Z Espec) e t0 ge_s typs args z a), @ext_spec_pre juicy_mem external_function Z (JE_spec Z Espec) e t0 ge_s typs args z a' *)
destruct Espec; simpl; apply JE_pre_hered.
Qed.
Next Obligation.
destruct f; simpl; unfold funspecOracle2post, pureat; simpl; destruct f; simpl;
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
  destruct f; simpl. intros e t0 ge_s tret rv z.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) as s return (forall _ : if s then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (Q (@snd rmap A x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e0|e0].
* destruct e; try discriminate; injection e0 as E; subst i sg; intros a a' Hage; destruct m0; simpl.
(* Goal: forall _ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a)) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
intros [phi0 [phi1 [Hjoin [Hx Hy]]]].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
apply age1_juicy_mem_unpack in Hage.
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
destruct Hage as [Hage Hdry].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
destruct (age1_join2 phi0 Hjoin Hage) as [x' [y' [Hjoin' [Hage' H]]]].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi a')) (and (x phi0) (@necR rmap ag_rmap (@fst rmap A t0) phi1)))) *)
exists x', y'; split; auto.
(* Goal: and (x x') (@necR rmap ag_rmap (@fst rmap A t0) y') *)
split; [solve[eapply h; eauto]|].
(* Goal: @necR rmap ag_rmap (@fst rmap A t0) y' *)
apply (necR_trans (fst t0) phi1 y'); auto.
(* Goal: @necR rmap ag_rmap phi1 y' *)
unfold necR. constructor; auto.
* intros ? ?; auto.
(* Goal: forall (_ : @age juicy_mem juicy_mem_ageable a a') (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z Espec) e t0 ge_s tret rv z a), @ext_spec_post juicy_mem external_function Z (JE_spec Z Espec) e t0 ge_s tret rv z a' *)
destruct Espec; simpl; apply JE_post_hered.
Qed.
Next Obligation.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
intros ? ? ? ?; destruct f; destruct f; destruct f; simpl.
(* Goal: @hereditary juicy_mem (@age juicy_mem juicy_mem_ageable) (fun _ : juicy_mem => False) *)
intros a' Hage; auto.
Qed.

End funspecsOracle2jspec.
Import String.

Fixpoint add_funspecsOracle_rec (ext_link: string -> ident) Z (Espec : juicy_ext_spec Z) (fs : list (ident * funspecOracle Z)) :=
  match fs with
    | nil => Espec
    | cons (i,f) fs' => funspecOracle2jspec Z (add_funspecsOracle_rec ext_link Z Espec fs') ext_link (i,f)
  end.

Require Import Coq.Logic.JMeq.

Lemma add_funspecs_pre  (ext_link: Strings.String.string -> ident)
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
              {Z fs id sig cc A P Q x args m} Espec tys ge_s phi0 phi1 z :
  let ef := EF_external id (funsig2signature sig cc) in
  list_norepet (map fst fs) ->
  In (ext_link id, (mk_funspecOracle Z sig cc A P Q)) fs ->
  join phi0 phi1 (m_phi m) ->
  P x z (make_ext_args (filter_genv (symb2genv ge_s)) (fst (split (fst sig))) args) phi0 ->
  exists x' : ext_spec_type (JE_spec _ (add_funspecsOracle_rec ext_link Z Espec fs)) ef,
    JMeq (phi1, x) x'
    /\ ext_spec_pre (add_funspecsOracle_rec ext_link Z Espec fs) ef x' ge_s tys args z m.
Proof.
(* Goal: let ef := EF_external id (funsig2signature sig cc) in forall (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @join rmap Join_rmap phi0 phi1 (m_phi m)) (_ : @app_pred rmap ag_rmap (P x z (make_ext_args (filter_genv (symb2genv ge_s)) (@fst (list ident) (list type) (@split ident type (@fst (list (prod ident type)) type sig))) args)) phi0), @ex (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef) (fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => and (@JMeq (prod rmap A) (@pair rmap A phi1 x) (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef) x') (@ext_spec_pre juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tys args z m)) *)
induction fs; [intros; elimtype False; auto|]; intros ef H H1 H2 Hpre.
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
destruct H1 as [H1|H1].

(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{
subst a; simpl in *.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
clear IHfs H; revert x H2 Hpre; unfold funspecOracle2pre; simpl.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
destruct sig; simpl.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) as s return (forall _ : if s then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (Q (@snd rmap A x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e0|e0].
(* Goal: and (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) x h) x') (@necR rmap ag_rmap (@fst rmap A t0) y') *)
rewrite fst_split.
(* Goal: forall (x : A) (_ : @join rmap Join_rmap phi0 phi1 (m_phi m)) (_ : @app_pred rmap ag_rmap (P x z (make_ext_args (filter_genv (symb2genv ge_s)) (@map (prod ident type) ident (@fst ident type) l) args)) phi0), @ex (prod rmap A) (fun x' : prod rmap A => and (@JMeq (prod rmap A) (@pair rmap A phi1 x) (prod rmap A) x') (@ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (P (@snd rmap A x') z (make_ext_args (filter_genv (symb2genv ge_s)) (@map (prod ident type) ident (@fst ident type) l) args)) phi0) (@necR rmap ag_rmap (@fst rmap A x') phi1)))))) *)
(* Goal: forall (x : A) (_ : @join rmap Join_rmap phi0 phi1 (m_phi m)) (_ : @app_pred rmap ag_rmap (P x z (make_ext_args (filter_genv (symb2genv ge_s)) (@fst (list ident) (list type) (@split ident type l)) args)) phi0), @ex (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef) (fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => and (@JMeq (prod rmap A) (@pair rmap A phi1 x) (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef) x') (@ext_spec_pre juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tys args z m)) *)
intros x Hjoin Hp. exists (phi1,x). split; eauto.
(* Goal: forall (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x') z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x') phi1))))) (_ : forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x'0 : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x' (prod rmap A) (@pair rmap A phi1' x'0)) (@app_pred rmap ag_rmap (Q x'0 z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
elimtype False; auto.
}

(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
assert (Hin: In (ext_link id) (map fst fs)).
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{ eapply (in_map fst) in H1; apply H1. }
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
inversion H as [|? ? Ha Hb]; subst.
(* Goal: @ex (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef) (fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef => and (@JMeq (prod rmap A) (@pair rmap A phi1 x) (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef) x') (@ext_spec_pre juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef x' ge_s tys args z m)) *)
destruct (IHfs Hb H1 H2 Hpre) as [x' H3].
(* Goal: @ex (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef) (fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef => and (@JMeq (prod rmap A) (@pair rmap A phi1 x) (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef) x') (@ext_spec_pre juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) ef x' ge_s tys args z m)) *)
clear -Ha Hin H1 H3; revert x' Ha Hin H1 H3.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
destruct a; simpl; destruct f; simpl; destruct f; simpl; unfold funspecOracle2pre; simpl.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) (_ : not (@In ident i (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs))) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) as s return (forall _ : if s then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A0 => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x) (_ : forall (x0 : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc)) x0 ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) x0 (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e|e].
* injection e as E; subst i; destruct fs; [solve[simpl; intros; elimtype False; auto]|].
(* Goal: forall (x : prod rmap A0) (_ : not (@In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs)))) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x) phi1))))) (_ : forall (x0 : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x0 ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x0 (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
  intros x' Ha Hb; simpl in Ha, Hb.
(* Goal: forall (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x') z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x') phi1))))) (_ : forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x'0 : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x' (prod rmap A) (@pair rmap A phi1' x'0)) (@app_pred rmap ag_rmap (Q x'0 z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
  elimtype False; auto.
* intros; eexists; eauto.
}
Qed.

Lemma add_funspecs_post (ext_link: Strings.String.string -> ident)
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
      {Z Espec tret fs id sig cc A}
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
      {P Q : A -> Z -> environ -> mpred} {x ret z m ge_s} :
  let ef := EF_external id (funsig2signature sig cc) in
  list_norepet (map fst fs) ->
  In (ext_link id, (mk_funspecOracle Z sig cc A P Q)) fs ->
  In (ext_link id) (map fst fs) ->
  ext_spec_post (add_funspecsOracle_rec ext_link Z Espec fs) ef x ge_s tret ret z m ->
  exists (phi0 phi1 phi1' : rmap) (x' : A),
       join phi0 phi1 (m_phi m)
    /\ necR phi1' phi1
    /\ JMeq x (phi1', x')
    /\ Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret) phi0.
Proof.
(* Goal: let ef := EF_external id (funsig2signature sig cc) in forall (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
induction fs; [intros; elimtype False; auto|]; intros ef H H1 Hid Hpost.
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
destruct H1 as [H1|H1].

(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{
subst a; simpl in *.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
clear IHfs H; revert x Hpost; unfold funspecOracle2post; simpl.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
destruct sig; simpl.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) as s return (forall _ : if s then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (Q (@snd rmap A x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature (@pair (list (prod ident type)) type l t) cc))) then prod rmap A else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e0|e0].
(* Goal: forall (x : prod rmap A) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (Q (@snd rmap A x) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A x) phi1))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
(* Goal: forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
intros x [phi0 [phi1 [Hjoin [Hq Hnec]]]].
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
(* Goal: forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
exists phi0, phi1, (fst x), (snd x).
split; auto. split; auto. destruct x; simpl in *. split; auto.
(* Goal: forall (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x') z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x') phi1))))) (_ : forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x'0 : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x' (prod rmap A) (@pair rmap A phi1' x'0)) (@app_pred rmap ag_rmap (Q x'0 z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
elimtype False; auto.
}

(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
assert (Hin: In (ext_link id) (map fst fs)).
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{ apply (in_map fst) in H1; auto. }
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
inversion H as [|? ? Ha Hb]; subst.
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
clear -Ha Hin H1 Hb Hpost IHfs; revert x Ha Hin H1 Hb Hpost IHfs.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
destruct a; simpl; destruct f; simpl; unfold funspecOracle2post; simpl.
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
destruct f; simpl.
(* Goal: forall (x : if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) (_ : not (@In ident i (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs))) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) as s return (forall _ : if s then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef, Prop) then fun x0 : prod rmap A0 => @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x0) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x0) phi1)))) else fun x' : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef => @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x' ge_s tret ret z m) x) (_ : forall (x0 : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) fs) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs)) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc)) x0 ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) x0 (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (if oi_eq_dec (@Some (prod ident signature) (@pair ident signature i (funsig2signature (@pair (list (prod ident type)) type l t) c))) (@Some (prod ident signature) (@pair ident signature (ext_link id) (funsig2signature sig cc))) then prod rmap A0 else @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
if_tac [e|e].
* injection e as E; subst i; destruct fs; [solve[simpl; intros; elimtype False; auto]|].
(* Goal: forall (x : prod rmap A0) (_ : not (@In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs)))) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x) z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x) phi1))))) (_ : forall (x0 : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x0 ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x0 (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
  intros x' Ha Hb; simpl in Ha, Hb.
(* Goal: forall (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@app_pred rmap ag_rmap (m1 (@snd rmap A0 x') z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) (@necR rmap ag_rmap (@fst rmap A0 x') phi1))))) (_ : forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) (_ : @list_norepet ident (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @In (prod ident (funspecOracle Z)) (@pair ident (funspecOracle Z) (ext_link id) (mk_funspecOracle Z sig cc A P Q)) (@cons (prod ident (funspecOracle Z)) p fs)) (_ : @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) (@cons (prod ident (funspecOracle Z)) p fs))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc)) x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) p fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0)))))))), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x'0 : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (prod rmap A0) x' (prod rmap A) (@pair rmap A phi1' x'0)) (@app_pred rmap ag_rmap (Q x'0 z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
  elimtype False; auto.
* intros. apply IHfs; auto.
}
Qed.

(* for now, giving up on the previously convenient add_funspecs because it is too much dependent now
Definition add_funspecs (Espec : OracleKind) (ext_link: string -> ident) (fs : list (ident * funspecOracle Espec.(@OK_ty))) : OracleKind :=
  match Espec
        as e
        return
        match e with
          Build_OracleKind ty _ => list (ident * funspecOracle ty) -> OracleKind
        end
  with
  | Build_OracleKind ty spec =>
    fun fs => Build_OracleKind ty (add_funspecsOracle_rec ext_link ty spec fs)
  end fs.
*)

(*! Adapting semax_external to a judgment mentioning oracles *)

Definition semax_external_oracle (Espec: OracleKind) (ids: list ident) ef (A: Type) (P Q: A -> Espec.(@OK_ty) -> environ -> pred rmap):
        pred nat :=
 ALL gx: genv, ALL x: A,
 |>  ALL F: pred rmap, ALL ts: list typ, ALL args: list val, ALL z : Espec.(@OK_ty),
   juicy_mem_op (P x z (make_ext_args (filter_genv gx) ids args) * F) >=>
   EX x': ext_spec_type OK_spec ef,
    ext_spec_pre' Espec ef x' (genv_symb_injective gx) ts args z &&
     ! ALL tret: option typ, ALL ret: option val, ALL z': OK_ty,
      ext_spec_post' Espec ef x' (genv_symb_injective gx) tret ret z' >=>
          juicy_mem_op (Q x z' (make_ext_rval (filter_genv gx) ret) * F).

Section semax_ext_oracle.

Variable Espec : OracleKind.
Local Notation ty := Espec.(@OK_ty).
Local Notation spec := Espec.(@OK_spec).

Lemma semax_ext'_oracle (ext_link: Strings.String.string -> ident) id sig cc A P Q (fs : list (ident * funspecOracle ty)) :
  let f := mk_funspecOracle ty sig cc A P Q in
  In (ext_link id, f) fs ->
  list_norepet (map fst fs) ->
  (forall n, semax_external_oracle
          (Build_OracleKind _ (add_funspecsOracle_rec ext_link ty spec fs))
          (fst (split (fst sig)))
          (EF_external id (funsig2signature sig cc))
          _ P Q n).
Proof.
intros f Hin Hnorepeat.
unfold semax_external.
intros n ge x n0 Hlater F ts args z jm H jm' H2 H3.
destruct H3 as [s [t [Hjoin [Hp Hf]]]].

assert (Hp'': P x z (make_ext_args (filter_genv (symb2genv (genv_symb_injective ge)))
                                 (fst (split (fst sig))) args) s).
(* Goal: @In ident (ext_link id) (@map (prod ident (funspecOracle Z)) ident (@fst ident (funspecOracle Z)) fs) *)
(* Goal: @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec (@cons (prod ident (funspecOracle Z)) a fs))) (EF_external id (funsig2signature sig cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
{ generalize (all_funspecsOracle_wf ty f) as Hwf2; intro.
  unfold wf_funspecOracle in Hwf2.
  specialize (Hwf2 x ge (symb2genv (genv_symb_injective ge)) (fst (split (fst sig))) args z).
  spec Hwf2.
  rewrite symb2genv_ax; auto.
  apply Hwf2; auto. }
destruct (@add_funspecs_pre
            ext_link ty _ _ _ cc _ _ _ _ _ _ OK_spec ts (genv_symb_injective ge) s t z Hnorepeat Hin Hjoin Hp'')
  as [x' [Heq Hpre]].
(* Goal: @eq environ (make_ext_args (filter_genv ge) n (@cons val a args)) (make_ext_args (filter_genv ge') n (@cons val a args)) *)
simpl.
exists x'.
split; [solve[apply Hpre]|].
intros tret ret z' jm2 Hlev jm3 Hnec Hpost.

eapply add_funspecs_post in Hpost; eauto. 2:eapply (in_map fst _ _ Hin).
destruct Hpost as [phi0 [phi1 [phi1' [x'' [Hjoin' [Hnec' [Hjmeq' Hq']]]]]]].
(* Goal: and (@JMeq (prod rmap A) (@pair rmap A r a) (prod rmap A) (@pair rmap A r a)) (@app_pred rmap ag_rmap (Q a z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) *)
(* Goal: forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
exists phi0, phi1; split; auto.
assert (E : (t, x) = (phi1', x'')) by (eapply JMeq_eq, JMeq_trans; eauto).
inv E.
(* Goal: and (@JMeq (prod rmap A) (@pair rmap A r a) (prod rmap A) (@pair rmap A r a)) (@app_pred rmap ag_rmap (Q a z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0) *)
(* Goal: forall (x : @ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) (_ : @ext_spec_post juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) ef x ge_s tret ret z m), @ex rmap (fun phi0 : rmap => @ex rmap (fun phi1 : rmap => @ex rmap (fun phi1' : rmap => @ex A (fun x' : A => and (@join rmap Join_rmap phi0 phi1 (m_phi m)) (and (@necR rmap ag_rmap phi1' phi1) (and (@JMeq (@ext_spec_type juicy_mem external_function Z (JE_spec Z (add_funspecsOracle_rec ext_link Z Espec fs)) (EF_external id (funsig2signature (@pair (list (prod ident type)) type l t) cc))) x (prod rmap A) (@pair rmap A phi1' x')) (@app_pred rmap ag_rmap (Q x' z (make_ext_rval (filter_genv (symb2genv ge_s)) ret)) phi0))))))) *)
split; auto.
unfold filter_genv, Genv.find_symbol in Hq'|-*.
rewrite symb2genv_ax in Hq'; auto.
eapply pred_nec_hereditary; eauto.
Qed.

Lemma semax_ext_oracle (ext_link: Strings.String.string -> ident) id ids sig sig' cc A P Q (fs : list (ident * funspecOracle ty)) :
  let f := mk_funspecOracle ty sig cc A P Q in
  In (ext_link id,f) fs ->
  list_norepet (map fst fs) ->
  ids = fst (split (fst sig)) ->
  sig' = funsig2signature sig cc ->
  (forall n, semax_external_oracle
          (Build_OracleKind _ (add_funspecsOracle_rec ext_link ty spec fs))
          ids
          (EF_external id sig')
          _ P Q n).
Proof.
(* Goal: let f := mk_funspecOracle (@OK_ty Espec) sig cc A P Q in forall (_ : @In (prod ident (funspecOracle (@OK_ty Espec))) (@pair ident (funspecOracle (@OK_ty Espec)) (ext_link id) f) fs) (_ : @list_norepet ident (@map (prod ident (funspecOracle (@OK_ty Espec))) ident (@fst ident (funspecOracle (@OK_ty Espec))) fs)) (_ : @eq (list ident) ids (@fst (list ident) (list type) (@split ident type (@fst (list (prod ident type)) type sig)))) (_ : @eq signature sig' (funsig2signature sig cc)) (n : nat), @app_pred nat ag_nat (semax_external_oracle (Build_OracleKind (@OK_ty Espec) (add_funspecsOracle_rec ext_link (@OK_ty Espec) (@OK_spec Espec) fs)) ids (EF_external id sig') A P Q) n *)
intros; subst.
(* Goal: @app_pred nat ag_nat (semax_external_oracle (Build_OracleKind (@OK_ty Espec) (add_funspecsOracle_rec ext_link (@OK_ty Espec) (@OK_spec Espec) fs)) (@fst (list ident) (list type) (@split ident type (@fst (list (prod ident type)) type sig))) (EF_external id (funsig2signature sig cc)) A P Q) n *)
apply semax_ext'_oracle; auto.
Qed.

End semax_ext_oracle.
