Library Analysers

This file contains some generic analysers and their correctness proofs relative to a generic abstract semantics.

Set Implicit Arguments.
Require Export PrettyBigStep.
Require Export LibList.
Require Export Shared.
Require Export Relations otherlattices.

Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.

Ltac false_post ::=
  solve [ assumption | discriminate ].

Section General.

Variable str : structure.
Let term := term str.
Let name := name str.
Let Rule_struct := Rule_struct term.
Let left (n : name) : term := left str n.
Let rule_struct (n : name) : Rule_struct := rule_struct str n.
Let semantics := semantics str.
Variable asem : semantics.
Let ast := st asem.
Let ares := res asem.
Let acond n (sigma : ast) := cond asem n sigma.
Let arule n : Rule ast ares := rule asem n.
Let aRule := Rule ast ares.
Variable sem : semantics.
Let st := st sem.
Let res := res sem.
Let cond n (sigma : st) := cond sem n sigma.
Let rule n : Rule st res := rule sem n.
Let Rule := Rule st res.

Hypothesis term_comparable : Comparable term.

Hypothesis rule_format_correct : rule_format_correct_all sem.
Hypothesis arule_format_correct : rule_format_correct_all asem.
Hypothesis sem_semantics_full : semantics_full sem.
Hypothesis asem_semantics_full : semantics_full asem.

Hypothesis ast_lat : LatticeDec.t ast.
Hypothesis ares_lat : LatticeDec.t ares.
Hypothesis ast_top : TopDec.t ast.
Hypothesis ares_top : TopDec.t ares.

Hypothesis acond_Decidable : ∀ n sigma, Decidable (acond n sigma).
Hypothesis acond_monotone : ∀ n sigma sigma',
    sigma' ⊑♯ sigma →
    acond n sigma' →
    acond n sigma.

This function returns the list of every applicable names. In the rare cases where this function is not computable (typically because the language manipulates closures and the abstraction is not precise enough to have a finite number of rule that can be applied), it is allowed to abandon.

Variable applicable_names : term → ast → option (list name).
Hypothesis applicable_names_correct : ∀ l t sigma n,
applicable_names t sigma = Some l →
(left n = t ∧ acond n sigma) ↔ List.In n l.

Hypothesis Icr : ∀ n, arules_incr _ _ _ (arule n).

Some definitions about semantic relation properties.

Inductive eq_closure (R : term → ast → ares → Prop) : term → ast → ares → Prop :=
  | eq_closure_cons : ∀ t sigma sigma' r r',
    R t sigma r →
    sigma =♯ sigma' → r =♯ r' →
    eq_closure R t sigma' r'.

Definition rel_stable_eq (R : term → ast → ares → Prop) := ∀ t sigma sigma' r r',
  R t sigma r →
  sigma =♯ sigma' → r =♯ r' →
  R t sigma' r'.

Lemma eq_closure_stable_eq : ∀ R,
  rel_stable_eq (eq_closure R).
Proof. introv T O1 O2. inverts T as T O1' O2'. applys× eq_closure_cons T. Qed.

Lemma eq_closure_st_incr : ∀ R,
  rel_st_incr _ _ R →
  rel_st_incr _ _ (eq_closure R).
Proof.
  introv I O T. inverts T as T O1' O2'. forwards T': I T.
   eapply PosetDec.trans. exact O. apply PosetDec.refl. auto×.
   applys× eq_closure_cons T'.
Qed.

Lemma rel_stable_eq_equiv : ∀ R1 R2,
  (∀ t sigma r, R1 t sigma r ↔ R2 t sigma r) →
  rel_stable_eq R1 →
  rel_stable_eq R2.
Proof. introv E S D E1 E2. forwards*: S E E1 E2. apply E; auto¬. Qed.

Lemma aeval_stable_eq : rel_stable_eq (aeval _ _ _).
Proof.
  introv D Esigma Er. apply EquivDec.sym in Esigma.
  eapply aeval_st_pos; try apply PosetDec.refl; try eassumption.
  eapply aeval_res_pos; try apply PosetDec.refl; try eassumption.
Qed.

Definition rel_pos (R : term → ast → ares → Prop) := ∀ t sigma sigma' r r',
  R t sigma r →
  sigma' ⊑♯ sigma → r ⊑♯ r' →
  R t sigma' r'.

Lemma rel_pos_equiv : ∀ R1 R2,
  (∀ t sigma r, R1 t sigma r ↔ R2 t sigma r) →
  rel_pos R1 →
  rel_pos R2.
Proof. introv E S D E1 E2. forwards*: S E E1 E2. apply E; auto¬. Qed.

Lemma rel_pos_st_incr : ∀ R,
  rel_pos R →
  rel_st_incr _ _ R.
Proof. introv P O D. applys¬ P D O. Qed.

Definition rel_accepts_top (R : term → ast → ares → Prop) := ∀ t sigma, R t sigma (⊤♯).

Lemma hyp_in_stable_eq : ∀ R,
  rel_stable_eq R →
  rel_stable_eq (hyp_in _ _ _ R).
Proof.
  introv Re D Esigma Er.
  eapply hyp_in_st_pos; try eassumption.
    apply PosetDec.refl. applys @EquivDec.sym Esigma.
  applys hyp_in_res_pos D.
    applys @PosetDec.refl Er.
Qed.

Lemma hyp_in_st_incr : ∀ R,
  rel_st_incr _ _ R →
  rel_st_incr _ _ (hyp_in _ _ _ R).
Proof. introv Re O D. applys¬ hyp_in_st_pos O. Qed.

Lemma hyp_in_pos : ∀ R,
  rel_pos (hyp_in _ _ _ R).
Proof.
  introv D O1 O2.
  forwards D': hyp_in_st_pos acond_monotone D; try eassumption.
  applys hyp_in_res_pos O2 D'.
Qed.

Lemma hyp_in_iter_stable_eq : ∀ R,
  rel_stable_eq R →
  rel_stable_eq (hyp_in_iter _ _ _ R).
Proof.
  introv Re D Esigma Er. gen sigma' r'. induction D; introv E1 E2.
   apply hyp_in_iter_exact. auto×.
   eapply hyp_in_iter_cons. exact (fun _ _ _ D ⇒ D).
    eapply hyp_in_st_pos; try eassumption.
      apply PosetDec.refl. applys @EquivDec.sym E1.
    eapply hyp_in_res_pos; try eassumption.
      applys @PosetDec.refl E2.
    applys¬ hyp_in_impl H1.
Qed.

Lemma hyp_in_iter_st_incr : ∀ R,
  rel_st_incr _ _ R →
  rel_st_incr _ _ (hyp_in_iter _ _ _ R).
Proof.
  introv Re O D. gen sigma'. induction D; introv O.
   apply hyp_in_iter_exact. auto×.
   eapply hyp_in_iter_cons. exact (fun _ _ _ D ⇒ D).
    applys¬ hyp_in_st_pos O.
    applys¬ hyp_in_impl H1.
Qed.

Lemma hyp_in_iter_pos : ∀ R,
  rel_pos R →
  rel_pos (hyp_in_iter _ _ _ R).
Proof.
  introv Re D. gen r' sigma'. induction D; introv O1 O2.
   apply hyp_in_iter_exact. auto×.
   eapply hyp_in_iter_cons. exact (fun _ _ _ D ⇒ D).
    applys¬ hyp_in_st_pos O1.
    applys¬ hyp_in_res_pos O2.
    applys¬ hyp_in_impl H1.
Qed.

Lemma meet_closure_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  meet_closure _ _ _ R1 t sigma r →
  meet_closure _ _ _ R2 t sigma r.
Proof.
  introv I D. induction D.
   apply¬ meet_closure_exact.
   applys¬ meet_closure_meet IHD1 IHD2.
Qed.

Lemma meet_closure_aeval : meet_closure _ _ _ (aeval _ _ _) = aeval _ _ _.
Proof.
  extens. intros t sigma r. iff D.
   induction¬ D. eapply aeval_st_pos; try eassumption. eapply aeval_res_pos; try eassumption.
    apply¬ aeval_meet.
   apply¬ meet_closure_exact.
Qed.

Lemma meet_closure_stable_eq : ∀ R,
  rel_stable_eq R →
  rel_stable_eq (meet_closure _ _ _ R).
Proof.
  introv Re D Esigma Er. induction D.
   apply meet_closure_exact. applys¬ Re H.
   applys meet_closure_meet D1 D2; eapply PosetDec.trans; try eassumption; auto×.
Qed.

Lemma meet_closure_pos : ∀ R,
  rel_pos (meet_closure _ _ _ R).
Proof. introv D O1 O2. eapply meet_closure_meet; try apply D; auto×. Qed.

Definition pos_closure (R : term → ast → ares → Prop) t sigma r :=
  ∃ sigma' r',
    sigma ⊑♯ sigma' ∧ r' ⊑♯ r ∧ R t sigma' r'.

Lemma pos_closure_pos : ∀ R,
  rel_pos (pos_closure R).
Proof.
  introv (?&?&O1&O2&D) O3 O4. do 2 eexists.
  splits; try apply D; eapply PosetDec.trans; eassumption.
Qed.

Lemma pos_closure_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  pos_closure R1 t sigma r →
  pos_closure R2 t sigma r.
Proof. introv I (sigma'&r'&O2&O3&D). repeat eexists; try applys¬ I D; auto×. Qed.

Lemma pos_closure_st_incr : ∀ R,
  rel_st_incr _ _ (pos_closure R).
Proof.
  introv Re (?&?&O2&O3&D). do 2 eexists.
  splits; try apply D; try eassumption; eapply PosetDec.trans; eassumption.
Qed.

Lemma pos_closure_stable_eq : ∀ R,
  rel_stable_eq (pos_closure R).
Proof.
  introv (?&?&O2&O3&D) E1 E2. do 2 eexists.
  splits; try apply D; eapply PosetDec.trans; try eassumption;
   eapply PosetDec.refl; auto×.
Qed.

Lemma pos_closure_stable_meet : ∀ R,
  rel_stable_meet _ _ _ R →
  rel_stable_meet _ _ _ (pos_closure R).
Proof.
  introv M (?&?&O2&O3&D1) (?&?&O4&O5&D2). forwards D: M D1 D2.
  do 2 eexists. splits; try apply D; auto×.
Qed.

Lemma meet_meet_closure : ∀ R,
  meet_closure _ _ _ R = meet_closure _ _ _ (meet_closure _ _ _ R).
Proof.
  introv. extens. intros t sigma r. iff D.
   apply¬ meet_closure_exact.
   sets_eq M: (meet_closure _ _ _ R). induction D; substs¬.
    eapply meet_closure_meet; try eassumption.
Qed.

Lemma meet_pos_closure : ∀ R,
  meet_closure _ _ _ R = meet_closure _ _ _ (pos_closure R).
Proof.
  introv. extens. intros t sigma r. iff D.
   applys meet_closure_impl D. clear t sigma r D. introv D.
    do 2 eexists. splits; try eassumption; auto×.
   rewrite meet_meet_closure. applys meet_closure_impl D.
    clear t sigma r D. introv (sigma'r&r'&O1&O2&P).
    forwards P': meet_closure_exact P.
    eapply meet_closure_meet; try exact P';
     try (eapply PosetDec.trans; try eassumption; apply PosetDec.refl);
     [| apply EquivDec.sym ]; apply meet_same.
Qed.

Lemma pos_meet_closure : ∀ R,
  pos_closure (meet_closure _ _ _ R) = meet_closure _ _ _ R.
Proof.
  introv. extens. intros t sigma r. iff D.
   lets (sigma'&r'&O1&O2&D'): (rm D). eapply meet_closure_meet; try exact D';
     try (eapply PosetDec.trans; try eassumption; apply PosetDec.refl);
     [| apply EquivDec.sym ]; apply meet_same.
   do 2 eexists. splits; try (apply PosetDec.refl; auto*). auto¬.
Qed.

Lemma pos_closure_aeval : pos_closure (aeval _ _ _) = aeval _ _ _.
Proof. rewrite <- meet_closure_aeval. apply pos_meet_closure. Qed.

Definition rel_stable_hyp_in (R : term → ast → ares → Prop) := ∀ t sigma r,
  R t sigma r →
  hyp_in _ _ _ R t sigma r.

Lemma rel_stable_hyp_in_equiv : ∀ R1 R2,
  (∀ t sigma r, R1 t sigma r ↔ R2 t sigma r) →
  rel_stable_hyp_in R1 →
  rel_stable_hyp_in R2.
Proof. introv I C T. apply I in T. applys hyp_in_impl (C _ _ _ T). apply I. Qed.

Lemma rel_stable_hyp_in_stable_hyp_in : ∀ R,
  rel_stable_hyp_in R →
  rel_stable_hyp_in (hyp_in _ _ _ R).
Proof. introv S T. applys¬ hyp_in_impl T. Qed.

Lemma rel_stable_hyp_in_stable_iter : ∀ R,
  rel_stable_hyp_in R →
  rel_stable_hyp_in (hyp_in_iter _ _ _ R).
Proof.
  introv S T. inverts T as T C.
   applys¬ hyp_in_impl. apply hyp_in_iter_exact.
   applys¬ hyp_in_impl C.
Qed.

Definition rel_stable_hyp_in_inv (R : term → ast → ares → Prop) := ∀ t sigma r,
  hyp_in _ _ _ R t sigma r →
  R t sigma r.

Lemma rel_stable_hyp_in_inv_equiv : ∀ R1 R2,
  (∀ t sigma r, R1 t sigma r ↔ R2 t sigma r) →
  rel_stable_hyp_in_inv R1 →
  rel_stable_hyp_in_inv R2.
Proof. introv I C T. apply I. forwards¬ D: hyp_in_impl T; [|applys C D]. apply I. Qed.

Lemma hyp_in_iter_stable_hyp_in_inv : ∀ R,
  rel_stable_hyp_in_inv (hyp_in_iter _ _ _ R).
Proof. introv D. applys¬ hyp_in_iter_cons D. Qed.

Inductive eq_meet_iter_closure (R : term → ast → ares → Prop) : term → ast → ares → Prop :=
  | eq_meet_iter_closure_exact : ∀ t sigma r,
    R t sigma r →
    eq_meet_iter_closure R t sigma r
  | eq_meet_iter_closure_eq : ∀ t sigma sigma' r r',
    eq_meet_iter_closure R t sigma r →
    sigma =♯ sigma' → r =♯ r' →
    eq_meet_iter_closure R t sigma' r'
  | eq_meet_iter_closure_meet : ∀ t sigma sigma1 sigma2 r r1 r2,
    sigma ⊑♯ (sigma1 ⊓♯ sigma2) →
    (r1 ⊓♯ r2) ⊑♯ r →
    eq_meet_iter_closure R t sigma1 r1 →
    eq_meet_iter_closure R t sigma2 r2 →
    eq_meet_iter_closure R t sigma r
  | eq_meet_iter_closure_iter : ∀ (R' : term → ast → ares → Prop) t sigma r,
    (∀ t sigma r, R' t sigma r → eq_meet_iter_closure R t sigma r) →
    hyp_in _ _ _ R' t sigma r →
    eq_meet_iter_closure R t sigma r
  .

Lemma eq_meet_iter_closure_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  eq_meet_iter_closure R1 t sigma r →
  eq_meet_iter_closure R2 t sigma r.
Proof.
  introv I T. induction T.
   apply¬ eq_meet_iter_closure_exact.
   applys¬ eq_meet_iter_closure_eq H H0.
   applys¬ eq_meet_iter_closure_meet H H0.
   applys¬ eq_meet_iter_closure_iter R'.
Qed.

Lemma meet_closure_eq_meet_iter_closure : ∀ R t sigma r,
  meet_closure _ _ _ R t sigma r →
  eq_meet_iter_closure R t sigma r.
Proof.
  introv I. induction I.
   apply¬ eq_meet_iter_closure_exact.
   eapply eq_meet_iter_closure_meet; try eassumption.
Qed.

Lemma hyp_in_iter_eq_meet_iter_closure : ∀ R t sigma r,
  hyp_in_iter _ _ _ R t sigma r →
  eq_meet_iter_closure R t sigma r.
Proof.
  introv I. induction I.
   apply¬ eq_meet_iter_closure_exact.
   eapply eq_meet_iter_closure_iter; try eassumption.
Qed.

Lemma eq_meet_iter_closure_stable_eq : ∀ R,
  rel_stable_eq R →
  rel_stable_eq (eq_meet_iter_closure R).
Proof. introv S T O1 O2. applys¬ eq_meet_iter_closure_eq O1 O2. Qed.

Lemma eq_meet_iter_closure_stable_meet : ∀ R,
  rel_stable_meet _ _ _ (eq_meet_iter_closure R).
Proof. introv T1 T2. eapply eq_meet_iter_closure_meet; try apply PosetDec.refl; auto¬. Qed.

Lemma eq_meet_iter_closure_meet_iter_stable_meet : ∀ R,
  rel_stable_meet _ _ _ (eq_meet_iter_closure (hyp_in_iter _ _ _ R)).
Proof. introv T1 T2. eapply eq_meet_iter_closure_meet; try apply PosetDec.refl; auto¬. Qed.

Lemma eq_closure_eq_meet_iter_closure : ∀ R,
  eq_closure (eq_meet_iter_closure R) = eq_meet_iter_closure R.
Proof.
  introv. extens. intros t sigma r. iff D.
   inverts D as D. applys¬ eq_meet_iter_closure_eq D.
   constructors×.
Qed.

Lemma eq_meet_iter_closure_eq_closure : ∀ R,
  eq_meet_iter_closure (eq_closure R) = eq_meet_iter_closure R.
Proof.
  introv. extens. intros t sigma r. iff D.
   sets_eq R0: (eq_closure R). induction¬ D; substs.
    inverts H as D E1 E2. applys¬ eq_meet_iter_closure_eq E1 E2.
     apply¬ eq_meet_iter_closure_exact.
     applys eq_meet_iter_closure_eq; try eassumption.
     applys eq_meet_iter_closure_meet; try eassumption.
     applys eq_meet_iter_closure_iter; try eassumption.
   induction D.
    apply¬ eq_meet_iter_closure_exact. constructors×.
    applys eq_meet_iter_closure_eq; try eassumption.
    applys eq_meet_iter_closure_meet; try eassumption.
    applys eq_meet_iter_closure_iter; try eassumption.
Qed.

Lemma eq_meet_iter_closure_hyp_in_iter : ∀ R,
  hyp_in_iter _ _ _ (eq_meet_iter_closure R) = eq_meet_iter_closure R.
Proof.
  introv. extens. intros t sigma r. iff D.
   sets_eq R0: (eq_meet_iter_closure R). induction¬ D; substs.
    applys¬ eq_meet_iter_closure_iter H1.
   apply¬ hyp_in_iter_exact.
Qed.

Lemma eq_meet_iter_closure_meet_closure : ∀ R,
  meet_closure _ _ _ (eq_meet_iter_closure R) = eq_meet_iter_closure R.
Proof.
  introv. extens. intros t sigma r. iff D.
   sets_eq R0: (eq_meet_iter_closure R). induction¬ D; substs.
    applys¬ eq_meet_iter_closure_meet H H0.
   apply¬ meet_closure_exact.
Qed.

Lemma eq_meet_iter_closure_stable_hyp_in_inv : ∀ R,
  rel_stable_hyp_in_inv (eq_meet_iter_closure R).
Proof. introv D. applys× eq_meet_iter_closure_iter D. Qed.

Lemma meet_closure_trans : ∀ (R1 R2 : _ → ast → ares → Prop) t sigma sigma' r r',
  (∀ t sigma sigma' r r',
    sigma' ⊑♯ sigma → r ⊑♯ r' →
    R1 t sigma r → R2 t sigma' r') →
  sigma' ⊑♯ sigma → r ⊑♯ r' →
  meet_closure _ _ _ R1 t sigma r →
  meet_closure _ _ _ R2 t sigma' r'.
Proof.
  introv I O1 O2 D. gen sigma' r'. induction D; introv O1 O2.
   apply meet_closure_exact. applys¬ I O1 O2.
   eapply meet_closure_meet; try (eapply PosetDec.trans; eassumption); auto×.
Qed.

Lemma hyp_in_iter_trans : ∀ (R1 R2 : _ → ast → ares → Prop) t sigma sigma' r r',
  (∀ t sigma sigma' r r',
    sigma' ⊑♯ sigma → r ⊑♯ r' →
    R1 t sigma r → R2 t sigma' r') →
  sigma' ⊑♯ sigma → r ⊑♯ r' →
  hyp_in_iter _ _ _ R1 t sigma r →
  hyp_in_iter _ _ _ R2 t sigma' r'.
Proof.
  introv I O1 O2 D. gen sigma' r'. induction D; introv O1 O2.
   apply hyp_in_iter_exact. applys¬ I O1 O2.
   forwards¬ D: hyp_in_pos R' t O1 O2.
    eapply hyp_in_iter_cons. exact (fun _ _ _ D ⇒ D).
    applys× hyp_in_impl D.
Qed.

Lemma eq_meet_iter_closure_trans : ∀ (R1 R2 : _ → ast → ares → Prop) t sigma sigma' r r',
  (∀ t sigma sigma' r r',
    sigma' ⊑♯ sigma → r ⊑♯ r' →
    R1 t sigma r → R2 t sigma' r') →
  sigma' ⊑♯ sigma → r ⊑♯ r' →
  eq_meet_iter_closure R1 t sigma r →
  eq_meet_iter_closure R2 t sigma' r'.
Proof.
  introv I O1 O2 D. gen sigma' r'. induction D; introv O1 O2.
   apply eq_meet_iter_closure_exact. applys¬ I O1 O2.
   apply¬ IHD; eapply PosetDec.trans; try eassumption; auto×.
   forwards D: eq_meet_iter_closure_meet IHD1 IHD2;
     try (eapply PosetDec.trans; eassumption); try (apply PosetDec.refl; auto*); auto¬.
   eapply eq_meet_iter_closure_iter. exact (fun _ _ _ D ⇒ D).
    eapply hyp_in_pos; try eassumption. applys× hyp_in_impl H1.
Qed.

Lemma eq_meet_iter_closure_trans_st : ∀ (R1 R2 : _ → ast → ares → Prop) t sigma sigma' r r',
  (∀ t sigma sigma' r r',
    sigma' ⊑♯ sigma → r =♯ r' →
    R1 t sigma r → R2 t sigma' r') →
  sigma' ⊑♯ sigma → r =♯ r' →
  eq_meet_iter_closure R1 t sigma r →
  eq_meet_iter_closure R2 t sigma' r'.
Proof.
  introv I O1 O2 D. gen sigma' r'. induction D; introv O1 O2.
   apply eq_meet_iter_closure_exact. applys¬ I O1 O2.
   apply¬ IHD; try eapply PosetDec.trans; try eassumption; auto×.
   forwards D: eq_meet_iter_closure_meet IHD1 IHD2; try apply D;
     try (eapply PosetDec.trans; try eassumption; apply PosetDec.refl; eassumption);
     try apply PosetDec.refl; apply EquivDec.refl.
   eapply eq_meet_iter_closure_iter. exact (fun _ _ _ D ⇒ D).
    eapply hyp_in_pos; try eassumption; try (apply PosetDec.refl; eassumption).
    applys× hyp_in_impl H1.
Qed.

Lemma eq_meet_iter_closure_pos : ∀ R,
  rel_pos R →
  rel_pos (eq_meet_iter_closure R).
Proof.
  introv Re T. gen sigma' r'. induction T; introv O1 O2.
   apply eq_meet_iter_closure_exact. applys¬ Re O1 O2.
   apply¬ IHT.
    eapply PosetDec.trans; try eassumption; auto×.
    eapply PosetDec.trans; try eassumption; auto×.
   applys¬ eq_meet_iter_closure_meet T1 T2; eapply PosetDec.trans; eassumption.
   forwards D: eq_meet_iter_closure_trans; try eassumption;
     [| applys× eq_meet_iter_closure_iter H1 ]. auto×.
Qed.

Lemma eq_meet_iter_closure_st_incr : ∀ R,
  rel_st_incr _ _ R →
  rel_st_incr _ _ (eq_meet_iter_closure R).
Proof.
  asserts L: (∀ R,
      rel_stable_eq R →
      rel_st_incr _ _ R →
      rel_st_incr _ _ (eq_meet_iter_closure R)).
    introv S Re O T. sets_eq r': r. asserts E: (r =♯ r').
      substs. apply EquivDec.refl.
    rewrite EQr' in T. clear EQr'. gen sigma' r'. induction T; introv O E.
     eapply eq_meet_iter_closure_eq; try eassumption; auto×.
      apply eq_meet_iter_closure_exact. applys¬ Re O.
     apply¬ IHT.
      eapply PosetDec.trans; try eassumption; auto×.
      eapply EquivDec.trans; eassumption.
     applys¬ eq_meet_iter_closure_meet T1 T2; eapply PosetDec.trans; try eassumption; auto×.
     forwards D: eq_meet_iter_closure_trans_st; try eassumption;
       [| applys× eq_meet_iter_closure_iter H1 ].
      clear - S Re. introv O E D. applys¬ S E. applys¬ Re D.
  introv Re. rewrite <- eq_meet_iter_closure_eq_closure. apply L.
   apply eq_closure_stable_eq.
   applys eq_closure_st_incr Re.
Qed.

Lemma eq_meet_iter_closure_constr : ∀ R t sigma r,
  rel_stable_eq R →
  rel_stable_meet _ _ _ R →
  rel_stable_hyp_in_inv R →
  rel_pos R →
  eq_meet_iter_closure R t sigma r →
  R t sigma r.
Proof.
  introv Re M SC pos D. induction D.
   auto×.
   auto×.
   applys× pos H H0.
   apply SC. apply¬ hyp_in_impl; auto×.
Qed.

Analysers

This is the result of an analyser: it can either respond by a result (separately proven correct) or by the list of terms and contexts it fails to evaluate, with an eventual list of oracle's hints.

Inductive analyser_result :=
  | analyser_found : ares → analyser_result
  | analyser_failed : list (term × ast) → list (term × ast × ares) → analyser_result
  .

Coercion analyser_found : ares >-> analyser_result.

Inductive correct_analyser_result_modulo (R : term → ast → ares → Prop) t sigma
    : analyser_result → Prop :=
  | correct_analyser_result_aeval : ∀ r : ares,
    R t sigma r →
    correct_analyser_result_modulo R t sigma r
  | correct_analyser_result_fail : ∀ lf lo,
    correct_analyser_result_modulo R t sigma (analyser_failed lf lo)
  .

Definition analyser_correct_modulo (R : term → ast → ares → Prop)
    (analyser : term → ast → analyser_result) :=
  ∀ t sigma r,
    analyser t sigma = r →
    correct_analyser_result_modulo R t sigma r.

Definition correct_analyser_result :=
  correct_analyser_result_modulo (aeval asem _ _).

Definition analyser_correct :=
  analyser_correct_modulo (aeval asem _ _).

Lemma correct_analyser_result_modulo_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma ar,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  correct_analyser_result_modulo R1 t sigma ar →
  correct_analyser_result_modulo R2 t sigma ar.
Proof. introv I Cc. inverts Cc as Rel; substs; constructors×. Qed.

Lemma correct_analyser_result_modulo_iter : ∀ R t sigma ar,
  correct_analyser_result_modulo R t sigma ar →
  correct_analyser_result_modulo (hyp_in_iter _ _ _ R) t sigma ar.
Proof. introv. apply correct_analyser_result_modulo_impl. apply¬ hyp_in_iter_exact. Qed.

Lemma analyser_correct_modulo_impl : ∀ (R1 R2 : term → ast → ares → Prop) analyser,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  analyser_correct_modulo R1 analyser →
  analyser_correct_modulo R2 analyser.
Proof. introv I C E. forwards Cc: C E. applys× correct_analyser_result_modulo_impl I. Qed.

Lemma analyser_correct_modulo_iter : ∀ R analyser,
  analyser_correct_modulo R analyser →
  analyser_correct_modulo (hyp_in_iter _ _ _ R) analyser.
Proof. introv. apply¬ analyser_correct_modulo_impl. apply¬ hyp_in_iter_exact. Qed.

Here follows some monads to manipulate this type.

Definition is_res r cont :=
  match r with
  | analyser_found ar ⇒ cont ar
  | analyser_failed _ _ ⇒ r
  end.

Lemma is_res_out : ∀ a cont r,
  is_res a cont = analyser_found r →
  ∃ (r0 : ares), a = r0 ∧ cont r0 = analyser_found r.
Proof. introv E. destruct× a. inverts E. Qed.

Lemma is_env_correct : ∀ t sigma t' sigma' ar cont,
  correct_analyser_result t sigma ar →
  (∀ r : ares, ar = r → correct_analyser_result t' sigma' (cont r)) →
  correct_analyser_result t' sigma' (is_res ar cont).
Proof.
  introv Cr Ccont. inverts Cr.
   forwards~: Ccont.
   constructors.
Qed.

Definition merge_res r1 r2 :=
  match r1, r2 with
  | analyser_found ar1, analyser_found ar2 ⇒
    analyser_found (ar1 ⊔♯ ar2)
  | analyser_failed lf1 lo1, analyser_failed lf2 lo2 ⇒
    analyser_failed (lf1 ++ lf2) (lo1 ++ lo2)
  | analyser_failed _ _, _ ⇒ r1
  | _, analyser_failed _ _ ⇒ r2
  end.

Lemma merge_res_out : ∀ a1 a2 r,
  merge_res a1 a2 = analyser_found r →
  ∃ (r1 r2 : ares), a1 = r1 ∧ a2 = r2 ∧ (r = r1 ⊔♯ r2).
Proof. introv E. destruct a1; destruct× a2; inverts E. repeat eexists. Qed.

Section Failing.

The Failing Analyser

Definition failing_analyser t sigma := analyser_failed ([ (t, sigma) ]) nil.

Lemma failing_analyser_correct : analyser_correct failing_analyser.
Proof. introv E. inverts E. constructors. Qed.

End Failing.

Section Trivial.

The Trivial Analyser

This analyser always returns ⊤♯.

Definition trivial_analyser (t : term) (sigma : ast) : analyser_result :=
⊤♯ : ares.

Note that this proof is completely independant on the current semantics. It only requests its fullness.

Lemma aeval_accepts_top : rel_accepts_top (aeval _ _ _).
Proof.
  cofix D. introv. constructors.
  introv Eq C. lets RT: arule_format_correct n. lets SF: asem_semantics_full n sigma C.
  simpl in SF. inverts RT as Eq1 Eq2; rewrite <- Eq2 in SF; inverts SF as Eq3 Eq4;
    symmetry in Eq1; symmetry in Eq2;
    (constructors; [ apply PosetDec.refl; auto× | apply TopDec.prop |]).
   apply¬ aapply_step_Ax; eassumption.
   eapply aapply_step_R1; try eassumption; apply D.
   lets (sigma''&Eq5): Eq4 (⊤♯ : ares). eapply aapply_step_R2; try eassumption; apply D.
Qed.

Lemma trivial_analyser_correct : analyser_correct trivial_analyser.
Proof. introv E. unfolds in E. inverts E. constructors¬. apply× aeval_accepts_top. Qed.

End Trivial.

Section Step.

Step Analyser

Variable analyse : term → ast → analyser_result.
Hypothesis analyse_correct : analyser_correct analyse.

This function applies the given rule n to its semantic context. Note that this function is independant of the example.

Definition analyse_apply_rule (n : name) (sigma : ast) : analyser_result :=
  match rule_struct n, arule n with
  | Rule_struct_Ax, Rule_Ax ax ⇒
    unsome_default (⊥♯) (ax sigma)
  | Rule_struct_R1 t, Rule_R1 up ⇒
    analyse t (unsome_default (⊥♯) (up sigma))
  | Rule_struct_R2 t1 t2, Rule_R2 up next ⇒
    is_res (analyse t1 (unsome_default (⊥♯) (up sigma))) (fun r1 ⇒
      analyse t2 (unsome_default (⊥♯) (next sigma r1)))
  | _, _ ⇒ (⊥♯ : ares)
  end.

Lemma analyse_apply_rule_correct_modulo : ∀ R n sigma r,
  analyser_correct_modulo R analyse →
  acond n sigma →
  analyse_apply_rule n sigma = analyser_found r →
  aapply_check_step asem R n sigma r.
Proof.
  clear analyse_correct. introv analyse_correct C E. lets RT: arule_format_correct n. unfolds in E.
  lets SF: asem_semantics_full n sigma C. inverts RT as Eq1 Eq2; inverts SF as Eq3 Eq4 Eq5;
    symmetry in Eq1, Eq2; unfolds rule_struct, arule; rewrite Eq1 in *; rewrite Eq2 in *;
    (inverts Eq4 || inverts Eq5); rewrite Eq3 in *; simpls; inverts E as E; substs.
   eapply aapply_check_step_Ax; auto×.
   forwards¬ CE: analyse_correct E. inverts CE as D.
    eapply aapply_check_step_R1; auto×.
   forwards (r0&eq&E'): is_res_out (rm E).
    forwards¬ CE1: analyse_correct eq. inverts CE1 as D1.
    forwards¬ CE2: analyse_correct E'. inverts CE2 as D2.
    eapply aapply_check_step_R2; auto×. forwards (sigma2&Eq): Eq4. rewrite Eq at 2. simpls¬.
Qed.

Lemma analyse_apply_rule_correct : ∀ n sigma r,
  acond n sigma →
  analyse_apply_rule n sigma = analyser_found r →
  aapply_step asem _ _ n sigma r.
Proof.
  introv C E. rewrite aapply_step_check.
  apply¬ analyse_apply_rule_correct_modulo.
Qed.

This function performs one step of analyse and call another analyser for every subcalls.

Definition analyse_step (t : term) (sigma : ast) : analyser_result :=
  'let rules := applicable_names t sigma in
  match rules with
  | Some l ⇒
    fold_left (fun n ⇒
        merge_res (analyse_apply_rule n sigma))
      (analyser_found (⊥♯)) l
  | None ⇒ analyser_failed ([(t, sigma)]) nil
  end.

Lemma analyse_step_f_correct : ∀ R,
  analyser_correct_modulo R analyse →
  analyser_correct_modulo (hyp_in _ _ _ R) analyse_step.
Proof.
  clear analyse_correct. introv analyse_correct Eq. unfolds in Eq.
  let_name. destruct rules as [rules|]; try solve [ substs; constructors¬ ].
  destruct r as [r|l]; constructors. apply hyp_in_cons. introv Et C.
  sets_eq ra: (analyser_found r). gen r.
  applys (fold_left_ex_ind (fun n' : name ⇒ n = n') (fun ra : analyser_result ⇒
    ∀ r : ares, ra = r → aapply_check asem _ _ R n sigma r)) Eq.
   introv [A|IH] Eqc; substs.
    simpl in C. unfolds acond.
     lets (r1&r2&n1&n2&n3): (merge_res_out _ _ (rm Eqc)). substs.
     apply aapply_check_res_pos with (r := r1); auto×.
     constructors; try (apply PosetDec.refl; apply EquivDec.refl).
     apply¬ analyse_apply_rule_correct_modulo.
    lets (r1&r2&n1&n2&n3): (merge_res_out _ _ (rm Eqc)). substs.
      forwards¬ n2: (rm IH). inverts n2 as O1 O2 n2.
      constructors; try apply n2; auto×.
   eexists. splits¬. symmetry in EQrules. applys¬ applicable_names_correct EQrules.
Qed.

Lemma analyse_step_correct : analyser_correct analyse_step.
Proof. introv Eq. rewrite aeval_hyp_in. apply¬ analyse_step_f_correct. Qed.

End Step.

Section Fuel.

A Finite Analyser

Variable fallback_analyser : term → ast → analyser_result.
Hypothesis fallback_analyser_correct : analyser_correct fallback_analyser.

There are more than one possiblity to use the previous step analyser. This one is just calling it a given number of time before abandonning to a fallback analyser.

Fixpoint analyse_fuel fuel :=
  match fuel with
    | O ⇒ fallback_analyser
    | S fuel' ⇒ analyse_step (analyse_fuel fuel')
  end.

Lemma analyse_fuel_correct : ∀ fuel,
  analyser_correct (analyse_fuel fuel).
Proof.
  induction fuel; introv D.
   apply¬ fallback_analyser_correct.
   simpls. applys¬ analyse_step_correct D.
Qed.

Lemma analyse_fuel_f_correct : ∀ R fuel,
  analyser_correct_modulo R fallback_analyser →
  analyser_correct_modulo (applyn fuel (hyp_in _ _ _) R) (analyse_fuel fuel).
Proof.
  introv analyser_correct. induction¬ fuel.
  simpl. applys analyse_step_f_correct IHfuel.
Qed.

End Fuel.

Section DeepUnfold.

An Analyser With Fuel Only Decrementing It When It Really Need To

Here is the definition of looping branchs. We only need to get one step in each loops: it's not a problem if stat_while_1 is not considered as a looping term as every loops in which it is involved also involves stat_while_2, which is considered as a looping term.

Variable is_looping_branch : term → term → Prop.
Hypothesis is_looping_branch_Decidable : ∀ p1 p2,
  Decidable (is_looping_branch p1 p2).

Inductive prev_term : term → term → Prop :=
  | prev_term_R1 : ∀ n t1 t2,
    left n = t1 →
    rule_struct n = Rule_struct_R1 t2 →
    prev_term t2 t1
  | prev_term_R2_up : ∀ n t1 t2 t3,
    left n = t1 →
    rule_struct n = Rule_struct_R2 t2 t3 →
    prev_term t2 t1
  | prev_term_R2_next : ∀ n t1 t2 t3,
    left n = t1 →
    rule_struct n = Rule_struct_R2 t2 t3 →
    prev_term t3 t1
  .

Definition prev_term_not_looping t1 t2 :=
  prev_term t1 t2 ∧ ¬ is_looping_branch t1 t2.

The following lemma basically states that we can iterate on these terms.

Hypothesis prev_term_not_looping_wf : well_founded prev_term_not_looping.

The order relation we need is however a little more complex than this as we will actually iterate two times on looping terms: the first time is the call to the oracle and the second one is the verification that the oracle's predication is actually correct. We thus need to be able to mark the various looping terms to avoid them to be passed more than one time.

Inductive prev_term_loops : relation (term × nat) :=
  | prev_term_loops_term : ∀ k1 k2 t1 t2,
    k1 ≤ k2 →
    prev_term_not_looping t1 t2 →
    prev_term_loops (t1, k1) (t2, k2)
  | prev_term_loops_incr : ∀ k1 k2 t1 t2,
    k1 < k2 →
    prev_term t1 t2 →
    prev_term_loops (t1, k1) (t2, k2)
  .

Lemma prev_term_loops_wf : well_founded prev_term_loops.
Proof.
  intros (t&k). asserts SI: (k ≤ k). math.
  gen SI. generalize k at 1 3. gen t. induction k.
   introv Pk. gen t. asserts: (k = 0). math. substs.
    apply (well_founded_ind prev_term_not_looping_wf). intros t IHp.
    constructors. intros (t'&k') R.
    asserts (P&NL&Ek): (prev_term t' t ∧ ¬ is_looping_branch t' t ∧ k' = 0).
      inverts R as N R; try lets (P&NL): (rm R); splits~; math.
    substs. apply IHp. splits¬.
   refine (well_founded_ind prev_term_not_looping_wf _ _). intros t IHp k' Hk'.
    constructors. intros (t'&k'') R. tests Dk: (k'' ≤ k).
     apply IHk. math.
     asserts (P&NL&Ik): (prev_term t' t ∧ ¬ is_looping_branch t' t ∧ k'' = S k).
        inverts R as N R; try lets (P&NL): (rm R); splits~; math.
      substs. apply IHp; try math. splits¬.
Qed.

An enhanced version of analyse_apply_rule, but with a proof that it effectively decreases prev_term.

Definition analyse_apply_rule_prev_term t
    (following : ∀ t', prev_term t' t → ast → analyser_result)
    (n : name) (L : left n = t) (sigma : ast) : analyser_result.
  refine (
    match rule_struct n as s, arule n as r return rule_struct n = s → analyser_result with
    | Rule_struct_Ax, Rule_Ax ax ⇒ fun _ ⇒
      unsome_default (⊥♯) (ax sigma)
    | Rule_struct_R1 t, Rule_R1 up ⇒ fun _ ⇒
      let sigma' := unsome_default (⊥♯) (up sigma) in _
    | Rule_struct_R2 t1 t2, Rule_R2 up next ⇒ fun _ ⇒
      let sigma1 := unsome_default (⊥♯) (up sigma) in
      is_res _ (fun r1 ⇒
        let sigma2 := unsome_default (⊥♯) (next sigma r1) in _)
    | _, _ ⇒ fun _ ⇒ (⊥♯ : ares)
    end eq_refl).
  applys following sigma'. applys× prev_term_R1 L.
  applys following sigma1. applys× prev_term_R2_up L.
  applys following sigma2. applys× prev_term_R2_next L.
Defined.

As the previous term was defined through tactics, we like to have an “equivalence” with the usual corresponding term.

Lemma analyse_apply_rule_prev_term_analyse_apply_rule : ∀ t simple_analyser n L sigma r r',
  analyse_apply_rule simple_analyser n sigma = r →
  analyse_apply_rule_prev_term (t := t) (fun t' _ ⇒ simple_analyser t') n L sigma = r' →
  r = r'.
Proof.
  introv E1 E2. unfolds in E1. unfolds in E2.
  destruct (rule_struct n); destruct (arule n); substs¬.
Qed.

Lemma analyse_apply_rule_prev_term_correct_modulo : ∀ R t analyser n L sigma r,
  (∀ t' P sigma' ar',
     analyser t' P sigma' = ar' →
     correct_analyser_result_modulo R t' sigma' ar') →
  acond n sigma →
  analyse_apply_rule_prev_term (t := t) analyser n L sigma = analyser_found r →
  aapply_check_step asem R n sigma r.
Proof.
  asserts dep_destr_match: (∀ (S1 S2 : Rule_struct) (E : S1 = S2) B (b : B) fax fr1 fr2,
      match S1 as s return S1 = s → B with
      | Rule_struct_Ax ⇒ fax S1
      | Rule_struct_R1 t ⇒ fr1 S1 t
      | Rule_struct_R2 t1 t2 ⇒ fr2 S1 t1 t2
      end eq_refl = b →
      match S2 as s return S1 = s → B with
      | Rule_struct_Ax ⇒ fax S2
      | Rule_struct_R1 t ⇒ fr1 S2 t
      | Rule_struct_R2 t1 t2 ⇒ fr2 S2 t1 t2
      end E = b).
    introv ?. substs¬.
  introv analyse_correct C E. lets RT: arule_format_correct n. unfolds in E.
  lets SF: asem_semantics_full n sigma C. inverts RT as Eq1 Eq2; inverts SF as Eq3 Eq4 Eq5;
    unfolds arule; symmetry in Eq1, Eq2; rewrite Eq2 in *;
    set (E':= dep_destr_match _ _ Eq1 _ _ (fun x e ⇒ _) (fun x1 x2 e ⇒ _) (fun x1 x2 x3 e ⇒ _) E);
    clearbody E'; clear E; try rewrite Eq1 in *; simpl in E';
    (inverts Eq4 || inverts Eq5); rewrite Eq3 in E'; simpls; substs.
   inverts E'. eapply aapply_check_step_Ax; auto×.
   forwards CA: analyse_correct E'. inverts CA.
    eapply aapply_check_step_R1; auto×.
   forwards (r0&eq&E): is_res_out (rm E').
    forwards¬ CE1: analyse_correct eq. inverts CE1 as D1.
    forwards¬ CE2: analyse_correct E. inverts CE2 as D2.
    eapply aapply_check_step_R2; auto×.
    forwards (sigma2&Eq): Eq4. rewrite Eq at 2. simpls¬.
Qed.

Lemma analyse_apply_rule_prev_term_correct : ∀ t analyser n L sigma r,
  (∀ t' P sigma' ar',
     analyser t' P sigma' = ar' →
     correct_analyser_result t' sigma' ar') →
  acond n sigma →
  analyse_apply_rule_prev_term (t := t) analyser n L sigma = analyser_found r →
  aapply_step asem _ _ n sigma r.
Proof.
  clear rule_format_correct sem_semantics_full asem_semantics_full acond_monotone Icr.
  introv analyser_correct C E. rewrite aapply_step_check.
  applys¬ analyse_apply_rule_prev_term_correct_modulo analyser_correct E.
Qed.

Definition fold_applicable_names t (sigma : ast) (A : Type)
    (f : A → ∀ n, left n = t → A) (i : A) (fail : A) : A.
  set_eq lo: (applicable_names t sigma).
  destruct lo as [l|]; [| apply fail ].
  asserts F: (Forall (fun n ⇒ left n = t) l).
    asserts P: (∀ n : name, List.In n l → left n = t).
      clear - EQlo applicable_names_correct. introv I. symmetry in EQlo.
      applys¬ applicable_names_correct EQlo.
    apply Forall_forall. intros n I. apply¬ P.
  clear - i f F. gen i. induction l; intro i.
   exact i.
   forwards E: Forall_inv F. forwards IH: Forall_inv_prop F.
    exact (IHl IH (f i _ E)).
Defined.

Lemma dep_equals : ∀
    (A B : Type) (a : A) (f : ∀ b : A, Some b = Some a → B) (b c : A)
    (E1 : Some b = Some a) (E2 : Some c = Some a),
  f b E1 = f c E2.
Proof.
  introv.
  asserts M1: (a = b). inverts¬ E1.
  asserts M2: (a = c). inverts¬ E2.
  substs. pi_rewrite¬ E1.
Qed.

Lemma fold_applicable_names_rew_applicables_names : ∀ t sigma A
    rules following (i fail : A)
    (Eq : Some rules = applicable_names t sigma),
  fold_applicable_names (t := t) sigma following i fail =
    list_rect (λ l : list name, Forall (λ n : name, left n = t) l → A → A)
         (λ (_ : Forall (λ n : name, left n = t) nil) (i : A), i)
         (λ (a : name) (l : list name)
          (IHl : Forall (λ n : name, left n = t) l → A → A)
          (F : Forall (λ n : name, left n = t) (a :: l))
          (i : A), IHl (Forall_inv_prop F) (following i a (Forall_inv F))) rules
         (match Forall_forall (λ n : name, left n = t) rules with
          | conj _ x0 ⇒ x0
          end
            (λ (n : name) (I : List.In n rules),
             match
               match applicable_names_correct n (Logic.eq_sym Eq) with
               | conj _ x0 ⇒ x0
               end I
             with
             | conj x _ ⇒ x
             end)) i.
Proof.
  introv. unfolds. match goal with |- ?a = ?b ⇒ sets_eq <- r: a end.
  asserts S: (∀ C,
     match applicable_names t sigma as o return o = _ → A with
     | Some l ⇒ fun EQlo ⇒ C l EQlo
     | None ⇒ fun _ ⇒ fail
     end eq_refl = r →
     ∀ EQlo, C rules EQlo = r).
   clear - Eq. introv E; introv. destruct (applicable_names t sigma); tryfalse.
    rewrite <- E. apply¬ dep_equals.
  lets¬ E': S EQr.
Qed.

Lemma fold_applicable_names_fold_left : ∀ t sigma A rules
    simple_following (i r r' fail : A),
  applicable_names t sigma = Some rules →
  fold_left simple_following i rules = r →
  fold_applicable_names (t := t) sigma (fun n a _ ⇒ simple_following a n) i fail = r' →
  r = r'.
Proof.
  introv Def E1 E2. unfolds in E2.
  asserts S: (∀ C,
     match applicable_names t sigma as o return o = _ → A with
     | Some l ⇒ fun EQlo ⇒ C l EQlo
     | None ⇒ fun _ ⇒ fail
     end eq_refl = r' →
     ∀ EQlo, C rules EQlo = r').
   clear E1 E2 Def. introv E1; introv. destruct (applicable_names t sigma); tryfalse.
    rewrite <- E1. apply¬ dep_equals.
  symmetry in Def. lets E2': (rm S) (rm E2). set (E2 := E2' Def). clearbody E2. clear E2'.
  sets_eq Cl: (λ (n : name) (I : List.In n rules),
    match
      match applicable_names_correct n (Logic.eq_sym Def) with
      | conj _ x0 ⇒ x0
      end I
    with
    | conj x _ ⇒ x
    end).   clear EQCl. clear Def. gen r r' i Cl. induction rules; simpl; introv E1 E2.
   substs¬.
   asserts Cl': (∀ n : name, List.In n rules → left n = t).
     introv I. apply Cl. right¬.
    apply (IHrules _ _ _ E1 Cl'). rewrite <- E2. fequals.
Qed.

Lemma fold_applicable_names_ind : ∀ t sigma A P Q f (i fail : A) r,
  (∀ (a : A) n (eq : left n = t), acond n sigma → Q a ∨ P n eq → Q (f a n eq)) →
  (∃ n, ∃ (eq : left n = t), acond n sigma ∧ P n eq) →
  fold_applicable_names (t := t) sigma f i fail = r →
  Q fail →
  Q r.
Proof.
  introv R E F QF. unfolds in F.
  set_eq <- o: (applicable_names t sigma). destruct o as [rules|].
   asserts S: (∀ C,
      match applicable_names t sigma as o return o = _ → A with
      | Some l ⇒ fun EQlo ⇒ C l EQlo
      | None ⇒ fun _ ⇒ fail
      end eq_refl = r →
      ∀ EQlo, C rules EQlo = r).
     clear - EQo. rewrite EQo. introv E; introv. substs. apply¬ dep_equals.
   symmetry in EQo. lets F': (rm S) (rm F). set (F := F' EQo). clearbody F. clear F'.
   asserts EQ: (Q i ∨ ∃ n, ∃ (eq : left n = t),
       acond n sigma ∧ (List.In n rules ∧ P n eq)).
     right. lets (n&eq&C&Pn): (rm E). repeat eexists; auto×.
     rewrite× <- applicable_names_correct.
   clear E. gen i. unfolds fold_applicable_names.
   set (pi := fun n ⇒
     match applicable_names_correct n (Logic.eq_sym EQo) with
     | conj _ x0 ⇒ x0
     end).
   change (λ (n : name) (I : List.In n rules),
       match
         match applicable_names_correct n (Logic.eq_sym EQo) with
         | conj _ x0 ⇒ x0
         end I
       with
       | conj x _ ⇒ x
       end) with (λ (n : name) (I : List.In n rules),
       match pi n I
       with
       | conj x _ ⇒ x
       end). clearbody pi.
   gen pi. clear EQo. induction rules; simpl.
    introv II E [?|(n&eq&C&Pn)]; substs¬. false×.
    introv E H. asserts pi': (∀ n : name, List.In n rules → left n = t ∧ acond n sigma).
       clear - pi. introv I. apply pi. right¬.
      apply IHrules with (pi := pi') (i :=
          (f i a (Forall_inv
            (match Forall_forall (λ n : name, left n = t) (a :: rules) with
             | conj _ x0 ⇒ x0
             end (λ (n : name) (I : a = n ∨ List.In n rules),
               match pi n (@Logic.eq_ind_r _ (a :: rules) _
                 (fun I0 : (a = n) ∨ (List.In n rules) ⇒ I0)
                 _ eq_refl I) with
               | conj x _ ⇒ x
               end))))); auto¬.
         substs¬. clear. fequals.
       destruct H as [?|(n&eq&C&[?|I]&Pn)].
        left. apply¬ R. apply¬ pi.
        subst a. left. apply¬ R. right. pi_rewrite eq in Pn. apply× Pn.
        right. repeat eexists; try apply Pn; auto¬.
   asserts: (r = fail); [|clear F; substs~].
    asserts S: (∀ C,
       match applicable_names t sigma as o return o = _ → A with
       | Some l ⇒ fun EQlo ⇒ C l EQlo
       | None ⇒ fun _ ⇒ fail
       end eq_refl = r →
       r = fail). clear - EQo. rewrite¬ EQo.
    applys S F.
Qed.

An enhanced version of analyse_step.

Definition analyse_step_prev_term_loops t following sigma : analyser_result :=
  fold_applicable_names (t := t) sigma (fun r n Eq ⇒
      merge_res r (analyse_apply_rule_prev_term following n Eq sigma))
    (analyser_found (⊥♯))
    (analyser_failed ([(t, sigma)]) nil).

Lemma analyse_step_prev_term_loops_correct_modulo : ∀ R t following sigma ra,
  (∀ t' (P : prev_term t' t) sigma' ra',
    following _ P sigma' = ra' →
    correct_analyser_result_modulo R t' sigma' ra') →
  analyse_step_prev_term_loops following sigma = ra →
  correct_analyser_result_modulo (hyp_in _ _ _ R) t sigma ra.
Proof.
  clear rule_format_correct sem_semantics_full asem_semantics_full acond_monotone Icr.
  introv following_correct Eq. unfolds in Eq.
  destruct ra as [r|l]; constructors. apply hyp_in_cons. introv Et C.
  sets_eq ra: (analyser_found r). gen r.
  applys (fold_applicable_names_ind sigma (fun (n' : name) (_ : _ = t) ⇒ n = n') (fun ra : analyser_result ⇒
    ∀ r : ares, ra = r → aapply_check asem _ _ R n sigma r)) Eq.
   introv [IH|A] Eqc; substs.
    lets (r1&r2&n1&n2&n3): (merge_res_out _ _ (rm Eqc)). substs.
     forwards¬ n3: (rm IH). inverts n3 as O1 O2 n3.
     constructors; try apply n3; auto×.
    simpl in C.
     lets (r1&r2&n1&n2&n3): (merge_res_out _ _ (rm Eqc)). substs.
     apply aapply_check_res_pos with (r := r2); auto×.
     constructors; try (apply PosetDec.refl; apply EquivDec.refl).
     eapply analyse_apply_rule_prev_term_correct_modulo with (L := eq_refl).
      apply× following_correct.
      auto×.
      apply n2.
   repeat eexists. rewrite¬ Et. exact C.
   introv E. inverts E.
Qed.

Lemma analyse_step_prev_term_loops_correct : ∀ t following sigma ra,
  (∀ t' (P : prev_term t' t) sigma' ra',
    following _ P sigma' = ra' →
    correct_analyser_result t' sigma' ra') →
  analyse_step_prev_term_loops following sigma = ra →
  correct_analyser_result t sigma ra.
Proof.
  clear rule_format_correct sem_semantics_full asem_semantics_full acond_monotone Icr.
  introv following_correct Eq. unfolds. rewrite aeval_hyp_in.
  applys¬ analyse_step_prev_term_loops_correct_modulo following_correct.
Qed.

Variable fallback_analyser : term → ast → analyser_result.
Hypothesis fallback_analyser_correct : analyser_correct fallback_analyser.

An enhanced version of analyse_fuel that only decrease its counter when traversing a looping step.

Definition analyse_deep_fuel (fuel : nat) (t : term) (sigma : ast) : analyser_result.
  refine (Fix prev_term_loops_wf (fun _ ⇒ ast → analyser_result)
            (fun tf deep_fuel ⇒ _) (t, fuel) sigma).
  clear t sigma fuel. intro sigma. destruct tf as (t&fuel).
  refine (analyse_step_prev_term_loops (fun t' (P : _ t) ⇒ _) sigma).
  destruct (decide (is_looping_branch t' t)) eqn:L; fold_bool; rew_refl in L.
   destruct fuel as [|fuel'].
     exact (fallback_analyser t').
     refine (deep_fuel _ _).
      applys prev_term_loops_incr fuel' P. math.
   refine (deep_fuel _ _).
    applys prev_term_loops_term fuel. math. splits. apply P. apply L.
Defined.

Definition analyse_deep_fuel_rel R fuel :=
  applyn fuel (fun R ⇒ hyp_in_iter asem _ _ (hyp_in _ _ _ R))
    (hyp_in_iter asem _ _ R).

Lemma analyse_deep_fuel_rel_one : ∀ R fuel t sigma r,
  analyse_deep_fuel_rel R fuel t sigma r →
  hyp_in_iter asem _ _ R t sigma r.
Proof.
  introv D. gen t sigma r. induction¬ fuel; introv D.
  simpl in D. rewrite <- hyp_in_iter_iter. applys hyp_in_iter_impl D.
  clear - IHfuel. introv D. applys× hyp_in_iter_cons D.
Qed.

Lemma analyse_deep_fuel_correct_modulo : ∀ R fuel,
  analyser_correct_modulo R fallback_analyser →
  analyser_correct_modulo (hyp_in _ _ _ (analyse_deep_fuel_rel R fuel))
    (analyse_deep_fuel fuel).
Proof.
  clear fallback_analyser_correct rule_format_correct sem_semantics_full
        asem_semantics_full acond_monotone Icr.
  cuts R: (∀ (tf : term × nat) R sigma ar,
     analyser_correct_modulo (hyp_in_iter asem _ _ R) fallback_analyser →
     let (t, fuel) := tf in
     analyse_deep_fuel fuel t sigma = ar →
     correct_analyser_result_modulo
       (hyp_in _ _ _ (applyn fuel
         (fun R ⇒ hyp_in_iter asem _ _ (hyp_in _ _ _ R))
         (hyp_in_iter asem _ _ R)))
       t sigma ar).
    introv C E. applys× R (t, fuel). applys analyser_correct_modulo_iter C.
  refine (well_founded_induction_type prev_term_loops_wf _ _).
  intros (t&fuel) IH. introv analyser_correct E.
  unfolds in E. rewrite Fix_eq in E.
   applys¬ analyse_step_prev_term_loops_correct_modulo E.
    clear E. introv E. simpls. cases_if as LB; fold_bool; rew_refl in LB.
     destruct fuel as [|fuel'].
      applys analyser_correct E.
      simpl. apply correct_analyser_result_modulo_iter.
       apply¬ (IH (t', fuel')).
       applys prev_term_loops_incr fuel' P. math.
     applys¬ correct_analyser_result_modulo_impl (IH (t', fuel)).
      clear E IH LB sigma P. clears. introv A.
       rewrite applyn_altern in A. forwards× A': hyp_in_iter_cons A.
       rewrite× <- applyn_altern in A'.
      applys prev_term_loops_term fuel. math. splits¬.
      apply analyser_correct.
   clear E. introv Efg. asserts~: (f = g).
     clear - Efg. applys func_ext_dep_2 Efg.
   substs¬.
Qed.

Lemma analyse_deep_fuel_correct : ∀ fuel,
  analyser_correct (analyse_deep_fuel fuel).
Proof.
  clear rule_format_correct sem_semantics_full
        asem_semantics_full acond_monotone Icr.
  introv. unfolds. rewrite aeval_hyp_in.
  eapply analyser_correct_modulo_impl; [|
    applys analyse_deep_fuel_correct_modulo fallback_analyser_correct ].
  clear. introv A. applys hyp_in_impl A.
  clear. introv A. unfolds in A. rewrite hyp_in_iter_aeval in A.
  forwards¬ E: applyn_ind (fun R ⇒ R = aeval _ _ _); [| rewrite¬ E in A ].
  clear. introv E. substs.
  rewrite hyp_in_aeval. rewrite¬ hyp_in_iter_aeval.
Qed.

End DeepUnfold.

Section WithOracle.

An Analyser Using an Oracle.

Definition of the Verifier

We assume that we have an oracle, that is a set of triples (t, sigma, r) that we will check coherent (thus correct). For efficiency and clarity reason, these triples will be implemented using the following structure.

Variable oracle : heap term (list (ast × ares)).

This function returns the oracle on a more readable form.

Definition flatten_oracle :=
  flat_map
    (fun triple : term × list (ast × ares) ⇒
      let (t, srl) := triple in
      LibList.map (fun sr : ast × ares ⇒
        let (sigma, r) := sr in (t, sigma, r)) srl)
    (to_list oracle).

This predicate states whether a triple is accepted by the oracle. Note that we will define two ways of reading in the oracle (see the functions read_oracle and read_oracle_meet below). We thus define two corresponding predicates.

Definition oracle_triple_direct t sigma r :=
  ∃ l, List.In (sigma, r) l ∧ binds oracle t l.

Definition oracle_triple := pos_closure oracle_triple_direct.

Definition oracle_triple_meet := meet_closure _ _ _ oracle_triple.

Lemma oracle_triple_st_incr : rel_st_incr _ _ oracle_triple.
Proof. apply pos_closure_st_incr. Qed.

Lemma oracle_triple_meet_st_incr : rel_st_incr _ _ oracle_triple_meet.
Proof. apply meet_closure_st_incr. apply oracle_triple_st_incr. Qed.

Lemma oracle_triple_stable_eq : rel_stable_eq oracle_triple.
Proof. apply pos_closure_stable_eq. Qed.

Lemma oracle_triple_pos : rel_pos oracle_triple.
Proof. apply pos_closure_pos. Qed.

Lemma oracle_triple_meet_stable_eq : rel_stable_eq oracle_triple_meet.
Proof. apply meet_closure_stable_eq. apply oracle_triple_stable_eq. Qed.

Lemma oracle_triple_meet_stable_meet : rel_stable_meet _ _ _ oracle_triple_meet.
Proof. apply meet_closure_stable_meet. Qed.

Lemma oracle_triple_meet_pos : rel_pos oracle_triple_meet.
Proof. apply meet_closure_pos. Qed.

Lemma oracle_binds : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l → R t sigma r) →
  ∀ t sigma r, oracle_triple t sigma r → pos_closure R t sigma r.
Proof. introv BR (l&sigma'&r'&O1&O2&I&B). forwards: BR I B. repeat eexists; eassumption. Qed.

Lemma oracle_binds_hyp_in_iter : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l → hyp_in_iter _ _ _ R t sigma r) →
  ∀ t sigma r, oracle_triple t sigma r → hyp_in_iter _ _ _ (pos_closure R) t sigma r.
Proof.
  introv BR (sigma'&r'&O1&O2&l&I&B). forwards T: BR I B.
  applys hyp_in_iter_pos (pos_closure R) O1 O2.
    apply pos_closure_pos.
  clear sigma r O1 O2 l I B. applys hyp_in_iter_impl T.
  clear. introv D. repeat eexists; try apply PosetDec.refl; auto×.
Qed.

Lemma oracle_meet_binds : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l → R t sigma r) →
  ∀ t sigma r, oracle_triple_meet t sigma r →
    meet_closure _ _ _ R t sigma r.
Proof.
  introv BR T. induction T.
   rewrite <- pos_meet_closure. apply¬ oracle_binds. constructors×.
   forwards D: meet_closure_meet IHT1 IHT2; try eassumption.
Qed.

Section OracleDefs.

Variable normalise : (term → ast → ares → Prop) → (term → ast → ares → Prop).

Definition oracle_indom t sigma :=
  ∃ r, normalise oracle_triple t sigma r.

Definition oracle_correct := ∀ t sigma r,
  oracle_triple_direct t sigma r →
  aeval asem _ _ t sigma r.

Definition oracle_correct_modulo (R : term → ast → ares → Prop) := ∀ t sigma r,
  oracle_triple_direct t sigma r →
  R t sigma r.

Lemma oracle_correct_modulo_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  oracle_correct_modulo R1 →
  oracle_correct_modulo R2.
Proof. introv I C T. auto×. Qed.

Hypothesis normalise_exact : ∀ (R : term → ast → ares → Prop) t sigma r,
  R t sigma r →
  normalise R t sigma r.
Hypothesis normalise_idem : ∀ R,
  normalise (normalise R) = normalise R.
Hypothesis normalise_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) → ∀ t sigma r,
  normalise R1 t sigma r →
  normalise R2 t sigma r.

Inductive normalise_hyp_in_iter : (term → ast → ares → Prop) → term → ast → ares → Prop :=
  | normalise_hyp_in_iter_exact : ∀ (R : term → ast → ares → Prop) t sigma r,
    R t sigma r →
    normalise_hyp_in_iter R t sigma r
  | normalise_hyp_in_iter_normalise : ∀ (R R' : term → ast → ares → Prop) t sigma r,
    (∀ t sigma r, R' t sigma r → normalise_hyp_in_iter R t sigma r) →
    normalise R' t sigma r →
    normalise_hyp_in_iter R t sigma r
  | normalise_hyp_in_iter_cons : ∀ (R R' : term → ast → ares → Prop) t sigma r,
    (∀ t sigma r, R' t sigma r → normalise_hyp_in_iter R t sigma r) →
    hyp_in_iter _ _ _ R' t sigma r →
    normalise_hyp_in_iter R t sigma r
  .

Lemma normalise_hyp_in_iter_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  ∀ t sigma r,
    normalise_hyp_in_iter R1 t sigma r →
    normalise_hyp_in_iter R2 t sigma r.
Proof.
  introv I D. induction D.
   apply¬ normalise_hyp_in_iter_exact.
   eapply normalise_hyp_in_iter_normalise; try eassumption. auto×.
   eapply normalise_hyp_in_iter_cons; try eassumption. auto×.
Qed.

Lemma normalise_normalise_hyp_in_iter : ∀ R,
  normalise (normalise_hyp_in_iter R) = normalise_hyp_in_iter R.
Proof.
  introv. extens. intros t sigma r. iff D.
   applys¬ normalise_hyp_in_iter_normalise D.
   apply¬ normalise_exact.
Qed.

Lemma normalise_hyp_in_iter_normalise_hyp_in_iter : ∀ R,
  normalise_hyp_in_iter (normalise_hyp_in_iter R) = normalise_hyp_in_iter R.
Proof.
  introv. extens. intros t sigma r. iff D.
   sets_eq R0: (normalise_hyp_in_iter R). induction D; substs.
     auto×.
     eapply normalise_hyp_in_iter_normalise; try eassumption. auto×.
     eapply normalise_hyp_in_iter_cons; try eassumption. auto×.
   apply¬ normalise_hyp_in_iter_exact.
Qed.

Lemma normalise_hyp_in_iter_normalise_eq_normalise_hyp_in_iter : ∀ R,
  normalise_hyp_in_iter (normalise R) = normalise_hyp_in_iter R.
Proof.
  introv. extens. intros t sigma r. iff D.
   rewrite <- normalise_hyp_in_iter_normalise_hyp_in_iter. applys normalise_hyp_in_iter_impl D.
    introv D'. applys normalise_hyp_in_iter_normalise D'. apply¬ normalise_hyp_in_iter_exact.
   applys normalise_hyp_in_iter_impl D. apply¬ normalise_exact.
Qed.

Lemma normalise_hyp_in_iter_pos : ∀ R,
  (∀ R, rel_pos (normalise R)) →
  rel_pos (normalise_hyp_in_iter R).
Proof.
  introv Re D O1 O2. eapply normalise_hyp_in_iter_normalise.
    exact (fun _ _ _ D ⇒ D).
  applys Re O1 O2. apply¬ normalise_exact.
Qed.

Definition Park_normalise (R : term → ast → ares → Prop) :=
  ∀ t sigma r,
    R t sigma r →
    hyp_in _ _ _ (normalise_hyp_in_iter R) t sigma r.

End OracleDefs.

Lemma normalise_hyp_in_iter_impl_norm : ∀ (norm1 norm2 : _ → term → ast → ares → Prop) R,
  (∀ R t sigma r, norm1 R t sigma r → norm2 R t sigma r) →
  ∀ t sigma r,
    normalise_hyp_in_iter norm1 R t sigma r →
    normalise_hyp_in_iter norm2 R t sigma r.
Proof.
  introv I D. induction D.
   apply¬ normalise_hyp_in_iter_exact.
   eapply normalise_hyp_in_iter_normalise; try eassumption. auto×.
   eapply normalise_hyp_in_iter_cons; try eassumption.
Qed.

Lemma oracle_binds_normalise_hyp_in_iter : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l →
    normalise_hyp_in_iter pos_closure R t sigma r) →
  ∀ t sigma r, oracle_triple t sigma r →
    normalise_hyp_in_iter pos_closure R t sigma r.
Proof.
  introv BR (sigma'&r'&O1&O2&l&I&B). forwards T: BR I B.
  applys normalise_hyp_in_iter_pos pos_closure R O1 O2.
   clear. introv D. repeat eexists; try eassumption; auto×.
   apply pos_closure_pos.
  clear sigma r O1 O2 l I B. applys normalise_hyp_in_iter_impl T.
  clear. introv D. repeat eexists; try apply PosetDec.refl; auto×.
Qed.

Lemma oracle_meet_binds_normalise_hyp_in_iter : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l →
    normalise_hyp_in_iter (meet_closure _ _ _) R t sigma r) →
  ∀ t sigma r, oracle_triple_meet t sigma r →
    normalise_hyp_in_iter (meet_closure _ _ _) R t sigma r.
Proof.
  introv BR T. induction T.
   lets (sigma'&r'&O1&O2&l&I&B): (rm H). forwards T: BR I B.
    eapply normalise_hyp_in_iter_normalise. exact (fun _ _ _ D ⇒ D).
    rewrite <- pos_meet_closure. repeat eexists; try eassumption.
    applys meet_closure_exact T.
   eapply normalise_hyp_in_iter_normalise. exact (fun _ _ _ D ⇒ D).
    eapply meet_closure_meet; try eassumption; constructors×.
Qed.

Lemma Park_normalise_Park_pos_closure : ∀ R,
  Park_normalise pos_closure R →
  Park _ _ _ (normalise_hyp_in_iter pos_closure R).
Proof.
  introv PN D. induction D.
   apply¬ PN.
   lets (sigma'&r'&O1&O2&D): (rm H1). applys¬ hyp_in_pos O1 O2.
   forwards D: hyp_in_iter_impl H1.
     introv D. applys H0 D PN.
    forwards D': hyp_in_iter_check D. applys hyp_in_impl D'.
    clear. introv D. applys¬ normalise_hyp_in_iter_cons D.
Qed.

Lemma Park_normalise_Park_meet_closure : ∀ R,
  Park_normalise (meet_closure _ _ _) R →
  Park _ _ _ (normalise_hyp_in_iter (meet_closure _ _ _) R).
Proof.
  introv PN D. induction D.
   apply¬ PN.
   induction H1.
    applys¬ H0.
    asserts P: (rel_pos (normalise_hyp_in_iter (meet_closure _ _ _) R)).
      apply normalise_hyp_in_iter_pos.
       apply meet_closure_exact.
       apply meet_closure_pos.
     forwards¬ M: hyp_in_meet IHmeet_closure1 IHmeet_closure2.
      apply¬ rel_pos_st_incr.
      clear. introv D1 D2. apply¬ normalise_hyp_in_iter_normalise.
       exact (fun _ _ _ D ⇒ D).
       eapply meet_closure_meet; try (apply PosetDec.refl; auto*);
        apply¬ meet_closure_exact.
     applys¬ hyp_in_pos M.
   forwards D: hyp_in_iter_impl H1.
     introv D. applys H0 D PN.
    forwards D': hyp_in_iter_check D. applys hyp_in_impl D'.
    clear. introv D. applys¬ normalise_hyp_in_iter_cons D.
Qed.

The following functions get the least result we can get from the oracle.

Definition read_oracle (t : term) (sigma : ast) : option ares :=
  'let l := unsome_default nil (read_option oracle t) in
  'let sr :=
    list_take_first (fun (sr : ast × ares) ⇒
      let (sigma', r') := sr in
      decide (sigma ⊑♯ sigma')) l in
  option_map snd sr.

Definition read_oracle_meet (t : term) (sigma : ast) : option ares :=
  'let l := unsome_default nil (read_option oracle t) in
  LibList.fold_left (fun (sr : ast × ares) ro ⇒
    let (sigma', r') := sr in
    ifb sigma ⊑♯ sigma' then Some ((unsome_default (⊤♯) ro) ⊓♯ r')
    else ro) None l.

Lemma read_oracle_triple : ∀ t sigma r,
  read_oracle t sigma = Some r →
  oracle_triple t sigma r.
Proof.
  introv E. unfolds in E. rewrite read_option_def in E. let_name.
  cases_if as I; unfolds unsome_default.
   let_name. destruct sr as [sr|]; inverts E. forwards× (Il&Inf): list_take_first_prop.
    destruct sr as [s r]. rew_refl in Inf.
    forwards× B: @read_binds I. eexists. ∃ r.
    splits; [eassumption | auto× | eexists ]. splits; try exact B.
    rewrite¬ <- EQl.
   substs. rewrite list_take_first_nil in E. false×.
Qed.

Lemma read_oracle_correct_modulo (R : term → ast → ares → Prop) : ∀ t sigma r,
  oracle_correct_modulo R →
  read_oracle t sigma = Some r →
  pos_closure R t sigma r.
Proof. introv C E. forwards T: read_oracle_triple E. applys pos_closure_impl C T. Qed.

Lemma read_oracle_correct : ∀ t sigma r,
  oracle_correct →
  read_oracle t sigma = Some r →
  aeval asem _ _ t sigma r.
Proof. introv. rewrite <- pos_closure_aeval. applys× read_oracle_correct_modulo. Qed.

Lemma read_oracle_meet_triple : ∀ t sigma r,
  read_oracle_meet t sigma = Some r →
  oracle_triple_meet t sigma r.
Proof.
  introv E. unfolds in E. rewrite read_option_def in E. let_name.
  cases_if as I; tryfalse; unfolds unsome_default.
   asserts Cl: (∀ sigma r,
       (∃ sigma' r', sigma ⊑♯ sigma' ∧ r' ⊑♯ r ∧ List.In (sigma', r') l) →
         oracle_triple_meet t sigma r).
     introv (sigma'&r'&Isigma&Ir&Il). apply¬ meet_closure_exact.
     do 2 eexists. splits; try eassumption.
     eexists. splits; try eassumption. apply¬ @read_binds.
    sets_eq T: (None : option ares).
    asserts CT: (∀ r, T = Some r → oracle_triple_meet t sigma r).
      substs. introv A. inverts A.
    clear - E Cl CT. gen T. induction l; introv E CT.
     auto×.
     simpls. forwards~: IHl E.
      introv (sigma'&r'&Isigma&Ir&I). apply Cl. repeat eexists; try eassumption. right¬.
      destruct a as [sigma' r']. cases_if¬.
       forwards Cr': Cl.
        repeat eexists; try (left; reflexivity); try eassumption. apply PosetDec.refl; auto×.
       destruct T as [r0|]; introv Eq; inverts Eq.
        forwards D: meet_closure_meet CT Cr'; try apply PosetDec.refl;
          [apply meet_same| | |]; auto¬.
        applys¬ oracle_triple_meet_stable_eq Cr'.
         apply EquivDec.sym. apply meet_top.
   substs. inverts¬ E.
Qed.

Lemma read_oracle_meet_correct_modulo (R : term → ast → ares → Prop) : ∀ t sigma r,
  oracle_correct_modulo R →
  read_oracle_meet t sigma = Some r →
  meet_closure _ _ _ R t sigma r.
Proof.
  introv C E. forwards T: read_oracle_meet_triple E.
  applys meet_closure_impl C. rewrite¬ meet_pos_closure.
Qed.

Lemma read_oracle_meet_correct : ∀ t sigma r,
  oracle_correct →
  read_oracle_meet t sigma = Some r →
  aeval asem _ _ t sigma r.
Proof. introv. rewrite <- meet_closure_aeval. applys read_oracle_meet_correct_modulo. Qed.

Section GuessStep.

Variable read_oracle : term → ast → option ares.

Variable normalise : (term → ast → ares → Prop) → term → ast → ares → Prop.

Hypothesis normalise_exact : ∀ (R : term → ast → ares → Prop) t sigma r,
  R t sigma r →
  normalise R t sigma r.
Hypothesis normalise_idem : ∀ R,
  normalise (normalise R) = normalise R.
Hypothesis normalise_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) → ∀ t sigma r,
  normalise R1 t sigma r →
  normalise R2 t sigma r.

Hypothesis Park_normalise_Park : ∀ R,
  Park_normalise normalise R → Park _ _ _ (normalise_hyp_in_iter normalise R).

Hypothesis oracle_binds : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l → R t sigma r) →
  ∀ t sigma r, normalise oracle_triple t sigma r → normalise R t sigma r.
Hypothesis oracle_binds_normalise_hyp_in_iter : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l →
    normalise_hyp_in_iter normalise R t sigma r) →
  ∀ t sigma r, oracle_triple_meet t sigma r →
    normalise_hyp_in_iter normalise R t sigma r.

Hypothesis read_oracle_correct_modulo : ∀ (R : term → ast → ares → Prop) t sigma r,
  oracle_correct_modulo R →
  read_oracle t sigma = Some r →
  normalise R t sigma r.
Hypothesis read_oracle_correct : ∀ t sigma r,
  oracle_correct →
  read_oracle t sigma = Some r →
  aeval asem _ _ t sigma r.

This analyser returns a result using the oracle.

Definition guess_step analyser :=
  analyse_step (fun t sigma ⇒
    match read_oracle t sigma return analyser_result with
    | Some r ⇒ r
    | None ⇒ analyser t sigma
    end).

Lemma guess_step_correct_modulo : ∀ (R : term → ast → ares → Prop) analyser,
  oracle_correct_modulo R →
  analyser_correct_modulo (hyp_in_iter _ _ _ (normalise R)) analyser →
  analyser_correct_modulo
    (hyp_in asem _ _ (hyp_in_iter _ _ _ (normalise R)))
    (guess_step analyser).
Proof.
  introv OC analyse_correct E.
  applys analyse_step_f_correct E.
  clear t sigma r E. introv E. simpls. destruct (read_oracle t sigma) eqn:E'.
   substs. constructors. apply¬ hyp_in_iter_exact.
   apply¬ correct_analyser_result_modulo_impl. auto×.
Qed.

Lemma guess_step_correct : ∀ analyser,
  oracle_correct →
  analyser_correct analyser →
  analyser_correct (guess_step analyser).
Proof.
  introv OC analyse_correct.
  applys analyse_step_correct.
  introv E. simpls. destruct (read_oracle t sigma) eqn:E'.
   substs. constructors¬.
   apply¬ analyse_correct.
Qed.

Variable is_looping_branch : term → term → Prop.
Hypothesis is_looping_branch_Decidable : ∀ p1 p2,
  Decidable (is_looping_branch p1 p2).

Hypothesis prev_term_not_looping_wf :
  well_founded (prev_term_not_looping is_looping_branch).

A better one that unfolds until it reached a looping point (where we really want the oracle to intervene). Note that every point of the oracle that deal about non-such terms won't be considered.

Variable deep : nat.
Definition deep_guess_step analyser :=
  analyse_deep_fuel _ prev_term_not_looping_wf (fun t sigma ⇒
    match read_oracle t sigma return analyser_result with
    | Some r ⇒ r
    | None ⇒ analyser t sigma
    end) deep.

Lemma deep_guess_step_correct_modulo : ∀ (R : term → ast → ares → Prop) analyser,
  oracle_correct_modulo R →
  analyser_correct_modulo (hyp_in_iter _ _ _ (normalise R)) analyser →
  analyser_correct_modulo
    (hyp_in _ _ _ (hyp_in_iter _ _ _ (normalise R)))
    (deep_guess_step analyser).
Proof.
  introv OC analyse_correct E. unfolds in E.
  forwards¬ C: analyse_deep_fuel_correct_modulo E.
   clear t sigma r E. introv E. simpls. destruct (read_oracle t sigma) eqn:E'.
    substs. constructors¬. apply¬ hyp_in_iter_exact.
     applys read_oracle_correct_modulo OC E'.
    apply¬ correct_analyser_result_modulo_impl. auto×.
   applys correct_analyser_result_modulo_impl C. introv D. applys hyp_in_impl D.
    clear D. introv D. forwards T: analyse_deep_fuel_rel_one D.
    rewrite¬ hyp_in_iter_iter in T.
Qed.

Lemma deep_guess_step_correct : ∀ analyser,
  oracle_correct →
  analyser_correct analyser →
  analyser_correct (deep_guess_step analyser).
Proof.
  introv OC analyse_correct.
  applys analyse_deep_fuel_correct.
  introv E. simpls. destruct (read_oracle t sigma) eqn:E'.
   substs. constructors¬.
   apply¬ analyse_correct.
Qed.

Section GuessFuel.

Variable guess_step : (term → ast → analyser_result) → term → ast → analyser_result.

Hypothesis guess_step_correct_modulo : ∀ (R : term → ast → ares → Prop) analyser,
  oracle_correct_modulo R →
  analyser_correct_modulo (hyp_in_iter _ _ _ (normalise R)) analyser →
  analyser_correct_modulo
    (hyp_in asem _ _ (hyp_in_iter _ _ _ (normalise R)))
    (guess_step analyser).
Hypothesis guess_step_correct : ∀ analyser,
  oracle_correct →
  analyser_correct analyser →
  analyser_correct (guess_step analyser).

Fixpoint guess_fuel fuel :=
  match fuel with
    | O ⇒ fun t sigma ⇒ analyser_failed ([(t, sigma)]) flatten_oracle
    | S fuel' ⇒ guess_step (guess_fuel fuel')
  end.

Lemma guess_fuel_correct_modulo R : ∀ fuel,
  oracle_correct_modulo R →
  analyser_correct_modulo
    (hyp_in _ _ _ (hyp_in_iter _ _ _ (normalise R)))
    (guess_fuel fuel).
Proof.
  induction fuel; introv C.
   introv E. substs. constructors.
   simpl. forwards¬ IH: analyser_correct_modulo_impl IHfuel.
     introv T. applys hyp_in_iter_cons T. exact (fun _ _ _ D ⇒ D).
    forwards¬ C': guess_step_correct_modulo IH.
Qed.

Lemma guess_fuel_correct : ∀ fuel,
  oracle_correct →
  analyser_correct (guess_fuel fuel).
Proof.
  introv C. induction fuel.
   introv E. substs. constructors.
   apply¬ guess_step_correct.
Qed.

We can now check whether the oracle is coherent.

Definition result_coherent_fuel fuel t sigma r :=
  match guess_fuel fuel t sigma with
  | analyser_found r0 ⇒ decide (r0 ⊑♯ r)
  | analyser_failed _ _ ⇒ false
  end.

Definition results_coherent_fuel fuel :=
  filter_heap (fun t l ⇒
    decide (~ Forall (fun (sr : ast × ares) ⇒
      istrue (let (sigma, r) := sr in
      result_coherent_fuel fuel t sigma r)) l)) oracle.

Lemma result_coherent_fuel_correct_modulo : ∀ R fuel t sigma r,
  oracle_correct_modulo R →
  result_coherent_fuel fuel t sigma r →
  hyp_in _ _ _ (hyp_in_iter _ _ _ (normalise R)) t sigma r.
Proof.
  introv O D. unfolds in D. sets_eq <- r0: (guess_fuel fuel t sigma).
  forwards¬ C: guess_fuel_correct_modulo O EQr0. clear EQr0.
  inverts C as T; rew_refl in D; tryfalse.
  applys¬ hyp_in_res_pos D.
Qed.

Lemma results_coherent_fuel_result_coherent : ∀ fuel,
  results_coherent_fuel fuel = nil → ∀ t sigma r,
  oracle_triple_direct t sigma r →
  result_coherent_fuel fuel t sigma r.
Proof.
  introv C (l&I&B).
  asserts L: (∀ A B C : Prop, ¬A → B → (A ↔ B ∧ C) → ¬C). clear. auto×.
  unfolds in C. match type of C with
                | filter_heap ?T _ = _ ⇒ sets_eq P: T end.
  refine (let NF := L _ _ _ _ B (filter_heap_spec P _ _ _) in _). rewrite× C.
  clear C. substs. rew_refl in NF. rew_logic in NF.
  applys¬ Forall_in NF I.
Qed.

Lemma results_coherent_fuel_correct_Park : ∀ fuel,
  results_coherent_fuel fuel = nil →
  Park_normalise normalise oracle_triple_direct.
Proof.
  introv C. lets CB: results_coherent_fuel_result_coherent C. clear C.
  introv T. apply CB in T.
  forwards¬ D: result_coherent_fuel_correct_modulo T.
    exact (fun _ _ _ D ⇒ D).
  applys hyp_in_impl D. clear - normalise_impl. introv D.
  eapply normalise_hyp_in_iter_cons. exact (fun _ _ _ D ⇒ D).
  applys hyp_in_iter_impl D. clear - normalise_impl. introv D.
  eapply normalise_hyp_in_iter_normalise. exact (fun _ _ _ D ⇒ D).
  applys normalise_impl D. clear. introv D.
  apply¬ normalise_hyp_in_iter_exact.
Qed.

Lemma results_coherent_fuel_correct : ∀ fuel,
  results_coherent_fuel fuel = nil →
  oracle_correct.
Proof.
  introv E. forwards P: results_coherent_fuel_correct_Park E.
  introv T. eapply Park_aeval. applys Park_normalise_Park P.
  apply¬ normalise_hyp_in_iter_exact.
Qed.

End GuessFuel.

End GuessStep.

End WithOracle.

Section OracleFinal.

Variable read_oracle : term → ast → option ares.

Variable normalise : (term → ast → ares → Prop) → term → ast → ares → Prop.

Hypothesis normalise_exact : ∀ (R : term → ast → ares → Prop) t sigma r,
  R t sigma r →
  normalise R t sigma r.
Hypothesis normalise_idem : ∀ R,
  normalise (normalise R) = normalise R.
Hypothesis normalise_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) → ∀ t sigma r,
  normalise R1 t sigma r →
  normalise R2 t sigma r.

Hypothesis Park_normalise_Park : ∀ R,
  Park_normalise normalise R → Park _ _ _ (normalise_hyp_in_iter normalise R).

Hypothesis oracle_binds : ∀ oracle (R : term → ast → ares → Prop),
  (∀ t sigma r l,
    List.In (sigma, r) l → binds oracle t l → R t sigma r) →
  ∀ t sigma r, normalise (oracle_triple oracle) t sigma r → normalise R t sigma r.

Hypothesis read_oracle_correct_modulo : ∀ oracle (R : term → ast → ares → Prop) t sigma r,
  oracle_correct_modulo oracle R →
  read_oracle t sigma = Some r →
  normalise R t sigma r.
Hypothesis read_oracle_correct : ∀ oracle t sigma r,
  oracle_correct oracle →
  read_oracle t sigma = Some r →
  aeval asem _ _ t sigma r.

Variable guess_step : heap term (list (ast × ares)) →
                      (term → ast → analyser_result) → term → ast → analyser_result.

Hypothesis guess_step_correct_modulo : ∀ (R : term → ast → ares → Prop) oracle analyser,
  oracle_correct_modulo oracle R →
  analyser_correct_modulo (hyp_in_iter _ _ _ (normalise R)) analyser →
  analyser_correct_modulo
    (hyp_in asem _ _ (hyp_in_iter _ _ _ (normalise R)))
    (guess_step oracle analyser).
Hypothesis guess_step_correct : ∀ oracle analyser,
  oracle_correct oracle →
  analyser_correct analyser →
  analyser_correct (guess_step oracle analyser).

The final analyser

Definition analyser_oracle_fuel fuel oracle : term → ast → _ :=
  'let l := results_coherent_fuel oracle (guess_step oracle) fuel in
  ifb l = nil then
    guess_fuel oracle (guess_step oracle) fuel
  else fun _ _ ⇒
    analyser_failed
      (flat_map (fun tl : term × _ ⇒
        let (t, l) := tl in
        LibList.map (fun sr : ast × ares ⇒
          let (sigma, r) := sr in (t, sigma)) l) l)
      (flatten_oracle oracle).

Lemma analyser_oracle_fuel_correct : ∀ oracle fuel,
  analyser_correct (analyser_oracle_fuel fuel oracle).
Proof.
  introv. unfolds analyser_oracle_fuel. let_name. cases_if.
   substs. forwards× OC: results_coherent_fuel_correct.
    applys¬ guess_fuel_correct OC.
   introv E. simpls. substs. constructors.
Qed.

End OracleFinal.

Section Oracles.

An Analyser Iterating the Construction of Oracles

Let's take as argument one analyser using an oracle defined above.

Variable analyser_oracle : heap term (list (ast × ares)) → term → ast → analyser_result.
Hypothesis analyser_oracle_correct : ∀ oracle, analyser_correct (analyser_oracle oracle).

Let's also use a function guessing new results on which the previous analyser failed.

Variable hint_oracle : heap term (list (ast × ares)) → term → ast
→ heap term (list (ast × ares)).

As every analyse returns when they fail a list of terms and contexts that they need to continue the computation, we can go back and forth to complete their lists of invariants.

Fixpoint analyser_back_and_forth (fuel : nat) oracle (t : term) (sigma : ast) :=
  match fuel with
  | O ⇒ analyser_oracle oracle t sigma
  | S fuel' ⇒
    match analyser_oracle oracle t sigma return analyser_result with
    | analyser_found r ⇒ r
    | analyser_failed lf lo ⇒
      let oracle' :=
        fold_left (fun (ts : term × ast) h ⇒
          let (t, sigma) := ts in
          hint_oracle h t sigma) oracle lf in
      analyser_back_and_forth fuel' oracle' t sigma
    end
  end.

Lemma analyser_back_and_forth_correct : ∀ fuel oracle,
  analyser_correct (analyser_back_and_forth fuel oracle).
Proof.
  induction fuel; introv.
   introv. simpl. apply analyser_oracle_correct.
   introv I. simpls. substs.
    sets_eq <- ar E': (analyser_oracle oracle t sigma). destruct ar.
     applys¬ analyser_oracle_correct E'.
     apply¬ IHfuel.
Qed.

Some Simple Oracles

Fixpoint add_list_oracle sigma r l :=
  match l : list (ast × ares) with
  | nil ⇒ [ (sigma, r) ]
  | sr0 :: l' ⇒
    ifb snd sr0 ⊑♯ r then
      ifb sigma ⊑♯ fst sr0 then l
      else sr0 :: add_list_oracle sigma r l'
    else
      (sigma, r) :: l
  end.

Definition add_oracle (h : heap term (list (ast × ares))) t sigma r :=
  let l := unsome_default nil (read_option h t) in
  write h t (add_list_oracle sigma r l).

Variable is_looping_branch : term → term → Prop.
Hypothesis is_looping_branch_Decidable : ∀ p1 p2,
  Decidable (is_looping_branch p1 p2).

Hypothesis prev_term_not_looping_wf : well_founded (prev_term_not_looping is_looping_branch).

Here is an example of an oracle for a given term, parametrised by an integer. It unfolds this number of time the semantics, before returning ⊥♯, hoping that this ⊥♯ will be joined with more correct results.

Definition oracle_unfold fuel (h : heap term (list (ast × ares))) t sigma :=
  let check_oracle t sigma :=
    unsome_default ((⊥♯ : ares) : analyser_result)
      (option_map analyser_found (read_oracle h t sigma)) in
  match analyse_deep_fuel is_looping_branch_Decidable prev_term_not_looping_wf
          check_oracle fuel t sigma with
  | analyser_found r ⇒ add_oracle h t sigma r
  | analyser_failed _ _ ⇒ h
  end.

Here is another example that adds results specific for the looping terms.

Definition oracle_loop_unfold fuel (h : heap term (list (ast × ares))) t sigma :=
  let check_oracle t sigma :=
    unsome_default ((⊥♯ : ares) : analyser_result)
      (option_map analyser_found (read_oracle h t sigma)) in
  match analyse_deep_fuel is_looping_branch_Decidable prev_term_not_looping_wf
          check_oracle fuel t sigma with
  | analyser_found r ⇒
    add_oracle h t sigma r
  | analyser_failed _ _ ⇒ h
  end.

End Oracles.

End General.