Library PrettyBigStep

This file contains the definition of pretty-big-step derivations, concrete and abstract, as well te predicates stating that these are related. The correctness theorem is stated and proven. An example of a concrete semantics is given in the file “ConcreteWhile.v”, as well as some derivations example. File “AbstractSign.v” gives an example of an abstract semantics.

Set Implicit Arguments.
Require Import Utf8.
Require Export Shared.
Ltac rewrite_term t :=
  fold t in *;
  repeat try match goal with
  | H : t = _ |- _ ⇒ rewrite H in ×
  | H : _ = t |- _ ⇒ rewrite <- H in ×
  end.

Section RuleStructure.

Rule Structure

Defines all things common to the concrete and abstract semantics.

Inductive Rule_struct term :=
  | Rule_struct_Ax : Rule_struct term
  | Rule_struct_R1 : term → Rule_struct term
  | Rule_struct_R2 : term → term → Rule_struct term
  .

Record structure := {

    term : Type;
    name : Type;

    left : name → term;
    rule_struct : name → Rule_struct term

  }.

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.

Inductive Rule st res :=
  | Rule_Ax : (st → option res) → Rule st res
  | Rule_R1 : (st → option st) → Rule st res
  | Rule_R2 : (st → option st) → (st → res → option st) → Rule st res
  .

Record semantics := make_semantics {

    st : Type;
    res : Type;

    cond : name → st → Prop;
    rule : name → Rule st res

  }.

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.

Inductive rule_format_correct : Rule_struct → Rule → Prop :=
  | rule_format_correct_Ax : ∀ ax,
    rule_format_correct (Rule_struct_Ax _) (Rule_Ax ax)
  | rule_format_correct_R1 : ∀ t up,
    rule_format_correct (Rule_struct_R1 t) (Rule_R1 _ up)
  | rule_format_correct_R2 : ∀ t1 t2 up next,
    rule_format_correct (Rule_struct_R2 t1 t2) (Rule_R2 up next)
  .

Definition rule_format_correct_all :=
  ∀ n, rule_format_correct (rule_struct n) (rule n).

Inductive applies : Rule → st → Prop :=
  | applies_Ax : ∀ sigma r ax,
    ax sigma = Some r →
    applies (Rule_Ax ax) sigma
  | applies_R1 : ∀ sigma sigma' up,
    up sigma = Some sigma' →
    applies (Rule_R1 _ up) sigma
  | applies_R2 : ∀ sigma sigma' up next,
    up sigma = Some sigma' →
    (∀ r, ∃ sigma', next sigma r = Some sigma') →
    applies (Rule_R2 up next) sigma
  .

Definition semantics_full :=
  ∀ n sigma,
   cond n sigma →
   applies (rule n) sigma.

Viewing the previous definition, one might ask why we do not directly define cond as being applies with the correct arguments. The reason is that most axioms, up and next functions may be more general than one might expect: most of them are structural and nothing prevent them from simply being constant or simply wrapping their argument into another structure. Furthermore, we want cond to be easily usable in proofs, which applies does not. For these reasons, we want to separate cond from applies.

End RuleStructure.

Section ConcreteWorld.

Concrete Semantics

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 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.

I've put it in Type instead of Prop as it's meaningful to have a concrete interpreter returning such an object… but apart from that, one can think of it as in Prop.

Inductive eval : term → st → res → Type :=
  | eval_cons : ∀ t sigma r n,
      t = left n →
      cond n sigma →
      apply n sigma r →
      eval t sigma r
with apply : name → st → res → Type :=
  | apply_Ax : ∀ n ax sigma r,
      rule_struct n = Rule_struct_Ax _ →
      rule n = Rule_Ax ax →
      ax sigma = Some r →
      apply n sigma r
  | apply_R1 : ∀ n t up sigma sigma' r,
      rule_struct n = Rule_struct_R1 t →
      rule n = Rule_R1 _ up →
      up sigma = Some sigma' →
      eval t sigma' r →
      apply n sigma r
  | apply_R2 : ∀ n t1 t2 up next sigma sigma1 sigma2 r r',
      rule_struct n = Rule_struct_R2 t1 t2 →
      rule n = Rule_R2 up next →
      up sigma = Some sigma1 →
      eval t1 sigma1 r →
      next sigma r = Some sigma2 →
      eval t2 sigma2 r' →
      apply n sigma r'
  .

Scheme eval_ind_2 := Induction for eval Sort Prop
  with apply_ind_2 := Induction for apply Sort Prop.
Combined Scheme eval_mutind from eval_ind_2, apply_ind_2.

End ConcreteWorld.

Section AbstractWorld.

Abstract Semantics

The abstract semantics uses similar structural data than the concrete semantics.

Require Export lattice_def.

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.

Hypothesis ast_order : PosetDec.t ast.
Hypothesis ares_order : PosetDec.t ares.

We give two definitions of the abstract semantics. aeval is based on Coq's coinduction, while aeval_f is defined to be the greatest fixed point of a functionnal. Both definitions are proven equivalent.

Section Check.

Hypothesis aeval : term → ast → ares → Prop.

Inductive aapply_check_step : name → ast → ares → Prop :=
  | aapply_check_step_Ax : ∀ n ax sigma r,
      rule_struct n = Rule_struct_Ax _ →
      arule n = Rule_Ax ax →
      ax sigma = Some r →
      aapply_check_step n sigma r
  | aapply_check_step_R1 : ∀ n t up sigma sigma' r,
      rule_struct n = Rule_struct_R1 t →
      arule n = Rule_R1 _ up →
      up sigma = Some sigma' →
      aeval t sigma' r →
      aapply_check_step n sigma r
  | aapply_check_step_R2 : ∀ n t1 t2 up next sigma sigma1 sigma2 r r',
      rule_struct n = Rule_struct_R2 t1 t2 →
      arule n = Rule_R2 up next →
      up sigma = Some sigma1 →
      aeval t1 sigma1 r →
      next sigma r = Some sigma2 →
      aeval t2 sigma2 r' →
      aapply_check_step n sigma r'
  .

Inductive aapply_check : name → ast → ares → Prop :=
  | aapply_check_cons : ∀ n sigma sigma' r r',
      sigma ⊑♯ sigma' →
      r' ⊑♯ r →
      aapply_check_step n sigma' r' →
      aapply_check n sigma r
  .

Inductive hyp_in : term → ast → ares → Prop :=
  | hyp_in_cons : ∀ t sigma r,
      (∀ n,
        t = left n →
        acond n sigma →
        aapply_check n sigma r) →
      hyp_in t sigma r
  .

End Check.

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

Inductive aeval_f : term → ast → ares → Prop :=
  | aeval_f_cons : ∀ R t sigma r,
    Park R →
    R t sigma r →
    aeval_f t sigma r
  .

CoInductive aeval : term → ast → ares → Prop :=
  | aeval_cons : ∀ t sigma r,
      (∀ n,
        t = left n →
        acond n sigma →
        aapply n sigma r) →
      aeval t sigma r
with aapply : name → ast → ares → Prop :=
  | aapply_cons : ∀ n sigma sigma' r r',
      sigma ⊑♯ sigma' →
      r' ⊑♯ r →
      aapply_step n sigma' r' →
      aapply n sigma r
with aapply_step : name → ast → ares → Prop :=
  | aapply_step_Ax : ∀ n ax sigma r,
      rule_struct n = Rule_struct_Ax _ →
      arule n = Rule_Ax ax →
      ax sigma = Some r →
      aapply_step n sigma r
  | aapply_step_R1 : ∀ n t up sigma sigma' r,
      rule_struct n = Rule_struct_R1 t →
      arule n = Rule_R1 _ up →
      up sigma = Some sigma' →
      aeval t sigma' r →
      aapply_step n sigma r
  | aapply_step_R2 : ∀ n t1 t2 up next sigma sigma1 sigma2 r r',
      rule_struct n = Rule_struct_R2 t1 t2 →
      arule n = Rule_R2 up next →
      up sigma = Some sigma1 →
      aeval t1 sigma1 r →
      next sigma r = Some sigma2 →
      aeval t2 sigma2 r' →
      aapply_step n sigma r'
  .

Correction Lemmae Between aeval and aeval_f.

Lemma aapply_check_step_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  aapply_check_step R1 t sigma r →
  aapply_check_step R2 t sigma r.
Proof.
  introv I A. inverts A.
   apply× aapply_check_step_Ax.
   apply× aapply_check_step_R1.
   apply× aapply_check_step_R2.
Qed.

Lemma aapply_check_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  aapply_check R1 t sigma r →
  aapply_check R2 t sigma r.
Proof.
  introv I A. inverts A as O1 O2 D. constructors; try eassumption.
  applys aapply_check_step_impl I D.
Qed.

Lemma hyp_in_impl : ∀ (R1 R2 : term → ast → ares → Prop) t sigma r,
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  hyp_in R1 t sigma r →
  hyp_in R2 t sigma r.
Proof.
  introv I A. inverts A as Da. constructors. introv E C.
  applys× aapply_check_impl I.
Qed.

Definition Park_modulo_set (R1 R2 : term → ast → ares → Prop) :=
  ∀ t sigma r,
    R2 t sigma r →
    hyp_in (fun t sigma r ⇒ R1 t sigma r ∨ R2 t sigma r) t sigma r.

Lemma Park_modulo_complete : ∀ R1 R2,
  Park R1 →
  Park_modulo_set R1 R2 →
  Park (fun t sigma r ⇒ R1 t sigma r ∨ R2 t sigma r).
Proof.
  introv P1 P2 [D|D].
   applys× hyp_in_impl P1.
   apply¬ P2.
Qed.

Lemma aapply_step_check : aapply_step = aapply_check_step aeval.
Proof.
  extens. intros t sigma r. iff A.
    inverts A.
     apply× aapply_check_step_Ax.
     apply× aapply_check_step_R1.
     apply× aapply_check_step_R2.
    inverts A.
     apply× aapply_step_Ax.
     apply× aapply_step_R1.
     apply× aapply_step_R2.
Qed.

Theorem aevals_equiv : ∀ t sigma r,
  aeval t sigma r ↔ aeval_f t sigma r.
Proof.
  introv. iff D.
   constructors×. clear D t sigma r. introv D. inverts D as Ac.
    constructors. introv E C. forwards Aac: Ac E C. inverts Aac as O1 O2 D.
    constructors; try eassumption. rewrite¬ <- aapply_step_check.
   inverts D as R_check Rc. gen t sigma r. cofix Dv. introv Rc.
    forwards Dc: R_check Rc. inverts Dc as Ac.
    constructors. introv E C. forwards Aac: Ac E C. inverts Aac as O1 O2 D.
    constructors; try eassumption. inverts D.
     apply× aapply_step_Ax.
     apply× aapply_step_R1.
     apply× aapply_step_R2.
Qed.

Corollary aevals_same : aeval = aeval_f.
Proof. extens. exact aevals_equiv. Qed.

Corollary Park_aeval : ∀ R,
  Park R →
  ∀ t sigma r, R t sigma r → aeval t sigma r.
Proof. introv P D. rewrite aevals_same. apply× aeval_f_cons. Qed.

Lemma aeval_hyp_in_impl : ∀ t sigma r,
  aeval t sigma r → hyp_in aeval t sigma r.
Proof.
  introv D. rewrite aevals_same in ×. inverts D as I D.
  forwards D': I D. applys¬ hyp_in_impl D'.
  clear - I. introv D. constructors×.
Qed.

Lemma check_fix_aeval : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r, R t sigma r → hyp_in R t sigma r) →
  ∀ t sigma r, R t sigma r → aeval t sigma r.
Proof. introv ER. introv D. rewrite aevals_same. constructors×. Qed.

Lemma aeval_hyp_in : aeval = hyp_in aeval.
Proof.
  extens. intros t sigma r. iff D.
   inverts D as Dec. constructors. introv E C. forwards A: Dec E C.
    inverts A as O1 O2 A. constructors; try eassumption.
    rewrite¬ <- aapply_step_check.
   inverts D as Dec. constructors. introv E C. forwards A: Dec E C.
    inverts A as O1 O2 A. constructors; try eassumption.
    rewrite¬ aapply_step_check.
Qed.

Inductive hyp_in_iter : (term → ast → ares → Prop) → term → ast → ares → Prop :=
  | hyp_in_iter_exact : ∀ (R : term → ast → ares → Prop) t sigma r,
    R t sigma r →
    hyp_in_iter R t sigma r
  | hyp_in_iter_cons : ∀ (R R' : term → ast → ares → Prop) t sigma r,
    (∀ t sigma r, R' t sigma r → hyp_in_iter R t sigma r) →
    hyp_in R' t sigma r →
    hyp_in_iter R t sigma r
  .

Lemma hyp_in_iter_applyn : ∀ n R t sigma r,
  applyn n hyp_in R t sigma r →
  hyp_in_iter R t sigma r.
Proof.
  induction n; introv D.
   apply× hyp_in_iter_exact.
   apply hyp_in_iter_cons with (R' := applyn n hyp_in R); auto×.
Qed.

Lemma hyp_in_iter_impl : ∀ (R1 R2 : term → ast → ares → Prop),
  (∀ t sigma r, R1 t sigma r → R2 t sigma r) →
  (∀ t sigma r, hyp_in_iter R1 t sigma r → hyp_in_iter R2 t sigma r).
Proof.
  introv I D. gen I. induction D; introv I.
   apply× hyp_in_iter_exact.
   apply hyp_in_iter_cons with (R' := hyp_in_iter R2); trivial.
    applys hyp_in_impl H1. introv D. apply× H0.
Qed.

Lemma hyp_in_iter_iter : ∀ (R : term → ast → ares → Prop),
   hyp_in_iter (hyp_in_iter R) = hyp_in_iter R.
Proof.
  extens. intros t sigma r. iff D; [| apply¬ hyp_in_iter_exact ].
  sets_eq R': (hyp_in_iter R). rewrite EQR'.
  asserts I: (∀ t sigma r, R' t sigma r → hyp_in_iter R t sigma r). substs×.
  clear EQR'. gen R. induction¬ D; introv I.
   apply hyp_in_iter_cons with (R' := hyp_in_iter R0); trivial.
    applys hyp_in_impl H1. introv D. apply× H0.
Qed.

Lemma hyp_in_iter_check : ∀ (R : term → ast → ares → Prop) t sigma r,
  hyp_in_iter (hyp_in R) t sigma r →
  hyp_in (hyp_in_iter R) t sigma r.
Proof.
  introv D. sets_eq R': (hyp_in R).
  asserts I: (∀ t sigma r, R' t sigma r → hyp_in (hyp_in_iter R) t sigma r).
   rewrite EQR'. clear. introv D. applys hyp_in_impl D.
    apply hyp_in_iter_exact.
  clear EQR'. induction× D.
  applys hyp_in_impl H1. introv D.
   apply hyp_in_iter_cons with (R' := hyp_in_iter R); trivial.
  applys H0 D I.
Qed.

Lemma check_fix_aeval_iter_cons : ∀ (R : term → ast → ares → Prop),
  (∀ t sigma r, R t sigma r → hyp_in (hyp_in_iter R) t sigma r) →
  ∀ t sigma r, R t sigma r → aeval t sigma r.
Proof.
  introv ER D. rewrite aevals_same.
  apply aeval_f_cons with (R := hyp_in_iter R); try solve [ constructors× ].
  clear t sigma r D. introv D. inverts× D. apply× hyp_in_impl.
Qed.

Lemma hyp_in_aeval : hyp_in aeval = aeval.
Proof.
  extens. intros t sigma r. iff D; [| apply¬ aeval_hyp_in_impl ].
  rewrite aevals_same in ×. applys aeval_f_cons D.
  clear t sigma r D. introv D. applys hyp_in_impl D.
  clear t sigma r D. introv D. rewrite <- aevals_same in ×. apply× aeval_hyp_in_impl.
Qed.

Lemma hyp_in_iter_aeval : hyp_in_iter aeval = aeval.
Proof.
  extens. intros t sigma r. iff D.
   sets_eq R: aeval. induction¬ D; substs¬.
    rewrite <- hyp_in_aeval. applys× hyp_in_impl H1.
   applys hyp_in_iter_exact D.
Qed.

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

Lemma Park_weak_hyp_in_iter : ∀ R,
  Park_weak R →
  Park_weak (hyp_in_iter R).
Proof.
  introv Pw D. induction D.
   forwards× D: Pw. rewrite¬ <- hyp_in_iter_iter in D.
   applys hyp_in_impl H1. introv D. forwards¬ D': H0 D.
   applys¬ hyp_in_iter_cons D'.
Qed.

Lemma Park_weak_aeval : ∀ R,
  Park_weak R →
  ∀ t sigma r, R t sigma r → aeval t sigma r.
Proof.
  introv Pw D. forwards D': hyp_in_iter_exact (rm D).
  forwards P: Park_weak_hyp_in_iter Pw.
  rewrite aevals_same. apply× aeval_f_cons.
  introv D. rewrite <- hyp_in_iter_iter. apply¬ P.
Qed.

Miscellanous Properties About aeval.

Hypothesis acond_monotone : ∀ n sigma sigma',
  sigma' ⊑♯ sigma →
  acond n sigma' →
  acond n sigma.

Lemma aapply_st_pos : ∀ n sigma sigma' r,
  sigma' ⊑♯ sigma →
  aapply n sigma r →
  aapply n sigma' r.
Proof.
  introv O DA. inverts DA as Ost Ores D. constructors.
   applys @PosetDec.trans O Ost.
   apply Ores.
   apply D.
Qed.

Lemma aapply_check_st_pos : ∀ R n sigma sigma' r,
  sigma' ⊑♯ sigma →
  aapply_check R n sigma r →
  aapply_check R n sigma' r.
Proof.
  introv O DA. inverts DA as Ost Ores D. constructors.
   applys @PosetDec.trans O Ost.
   apply Ores.
   apply D.
Qed.

Lemma hyp_in_st_pos : ∀ R t sigma sigma' r,
  sigma' ⊑♯ sigma →
  hyp_in R t sigma r →
  hyp_in R t sigma' r.
Proof.
  introv O D. inverts D as app. constructors.
  introv E C. forwards C': acond_monotone O C. forwards DA: app E C'.
  applys¬ aapply_check_st_pos DA.
Qed.

Lemma aeval_st_pos : ∀ t sigma sigma' r,
  sigma' ⊑♯ sigma →
  aeval t sigma r →
  aeval t sigma' r.
Proof. rewrite aeval_hyp_in. apply hyp_in_st_pos. Qed.

Lemma aapply_res_pos : ∀ n sigma r r',
  r ⊑♯ r' →
  aapply n sigma r →
  aapply n sigma r'.
Proof.
  introv O DA. inverts DA as Ost Ores D. constructors.
   apply Ost.
   applys @PosetDec.trans Ores O.
   apply D.
Qed.

Lemma aapply_check_res_pos : ∀ R n sigma r r',
  r ⊑♯ r' →
  aapply_check R n sigma r →
  aapply_check R n sigma r'.
Proof.
  introv O DA. inverts DA as Ost Ores D. constructors.
   apply Ost.
   applys @PosetDec.trans Ores O.
   apply D.
Qed.

Lemma hyp_in_res_pos : ∀ R t sigma r r',
  r ⊑♯ r' →
  hyp_in R t sigma r →
  hyp_in R t sigma r'.
Proof.
  introv O D. inverts D as app. constructors.
  introv E C. forwards DA: app E C.
  applys¬ aapply_check_res_pos DA.
Qed.

Lemma aeval_res_pos : ∀ t sigma r r',
  r ⊑♯ r' →
  aeval t sigma r →
  aeval t sigma r'.
Proof. rewrite aeval_hyp_in. apply hyp_in_res_pos. Qed.

Hypothesis ares_meet : MeetDec.t ares.
Hypothesis ast_join : JoinDec.t ast.
Hypothesis ast_meet : MeetDec.t ast.

Lemma acond_join : ∀ n sigma sigma',
  acond n sigma →
  acond n sigma' →
  acond n (sigma ⊔♯ sigma').
Proof. introv C1 C2. applys× acond_monotone C1. Qed.

Inductive arules_incr : aRule → Prop :=
  | arules_incr_Ax : ∀ aax,
      (∀ asigma asigma' ar ar',
        aax asigma = Some ar →
        aax asigma' = Some ar' →
        asigma' ⊑♯ asigma →
        ar' ⊑♯ ar) →
      arules_incr (Rule_Ax aax)
  | arules_incr_R1 : ∀ aup,
      (∀ asigma asigma' asigma0 asigma0',
        aup asigma = Some asigma0 →
        aup asigma' = Some asigma0' →
        asigma' ⊑♯ asigma →
        asigma0' ⊑♯ asigma0) →
      arules_incr (Rule_R1 _ aup)
  | arules_incr_R2 : ∀ aup anext,
      (∀ asigma asigma' asigma0 asigma0',
        aup asigma = Some asigma0 →
        aup asigma' = Some asigma0' →
        asigma' ⊑♯ asigma →
        asigma0' ⊑♯ asigma0) →
      (∀ asigma asigma' ar ar' asigma0 asigma0',
        anext asigma ar = Some asigma0 →
        anext asigma' ar' = Some asigma0' →
        asigma' ⊑♯ asigma →
        ar' ⊑♯ ar →
        asigma0' ⊑♯ asigma0) →
      arules_incr (Rule_R2 aup anext)
  .

Hypothesis Icr : ∀ n, arules_incr (arule n).
Hypothesis Fsem : semantics_full asem.

Definition rel_stable_meet (R : term → ast → ares → Prop) :=
  ∀ t sigma1 sigma2 r r',
  R t sigma1 r → R t sigma2 r' →
  R t (sigma1 ⊓♯ sigma2) (r ⊓♯ r').

Lemma rel_stable_meet_equiv : ∀ R1 R2,
  (∀ t sigma r, R1 t sigma r ↔ R2 t sigma r) →
  rel_stable_meet R1 →
  rel_stable_meet R2.
Proof. introv E M D1 D2. forwards: M; try apply E; [apply D1|apply D2|auto~]. Qed.

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

Lemma rel_stable_meet_altern : ∀ (R : term → ast → ares → Prop),
  rel_st_incr R →
  rel_stable_meet R ↔ ∀ t sigma sigma1 sigma2,
    sigma ⊑♯ (sigma1 ⊓♯ sigma2) → ∀ r r',
    R t sigma1 r →
    R t sigma2 r' →
    R t sigma (r ⊓♯ r').
Proof. introv pos. iff Re. auto×. introv D1 D2. applys¬ Re D1 D2. Qed.

Lemma hyp_in_meet : ∀ (R : term → ast → ares → Prop),
  rel_st_incr R →
  rel_stable_meet R →
  rel_stable_meet (hyp_in R).
Proof.
  introv pos M. apply rel_stable_meet_altern. unfolds. apply hyp_in_st_pos.
  set (M' := proj1 (rel_stable_meet_altern pos) M). clearbody M'. clear M.
  introv O D1 D2. inverts D1 as app1. inverts D2 as app2. constructors.
  introv E C. forwards Icn: Icr n.
  forwards C1: acond_monotone C; [ applys @PosetDec.trans O; apply MeetDec.bound1 |].
  forwards C2: acond_monotone C; [ applys @PosetDec.trans O; apply MeetDec.bound2 |].
  forwards DA1: app1 E C1. forwards DA2: app2 E C2.
  inverts DA1 as Ost1 Ores1 D1. inverts DA2 as Ost2 Ores2 D2.
  asserts Ir: ((r'0 ⊓♯ r'1) ⊑♯ (r ⊓♯ r')). clear - Ores1 Ores2. auto×.
  asserts Is: ((sigma1 ⊓♯ sigma2) ⊑♯ (sigma' ⊓♯ sigma'0)). clear - Ost1 Ost2. auto×.
  asserts CM: (acond n (sigma' ⊓♯ sigma'0)).
    applys¬ acond_monotone C. applys¬ @PosetDec.trans O.
  forwards App: Fsem CM. fold (arule n) in App.
  clear - O App Icn Is Ir C1 C2 D1 D2 M'.
  destruct (rule_struct n) eqn: S;
    inverts D1 as E11 E12 E13 I11 N1 I12; rewrite S in *; inverts E11;
    inverts D2 as E21 E22 E23 I21 N2 I22; rewrite S in *; inverts E21;
    rewrite E22 in *; inverts E12; inverts Icn as I1 I2; inverts App as App1 App2.
   asserts Ir': (r0 ⊑♯ (r ⊓♯ r')).
      forwards~: I1 E13 App1. forwards~: I1 E23 App1.
      applys× PosetDec.trans Ir.
    constructors; [ applys¬ @PosetDec.trans O Is | exact Ir' |].
    eapply aapply_check_step_Ax; try eassumption.
   constructors; [ applys¬ @PosetDec.trans O Is | exact Ir |].
    eapply aapply_check_step_R1; try eassumption. applys M' I11 I21.
    forwards~: I1 E13 App1. forwards~: I1 E23 App1.
   constructors; [ applys¬ @PosetDec.trans O Is | exact Ir |].
    lets (sigma_next&Esigma_next): (App2 (r0 ⊓♯ r1)).
    eapply aapply_check_step_R2; try eassumption.
     applys M' I11 I21.
      forwards~: I1 E13 App1. forwards~: I1 E23 App1.
     applys M' I12 I22.
      forwards~: I2 N1 Esigma_next. forwards~: I2 N2 Esigma_next.
Qed.

Inductive transfert_fun_meet : Rule ast ares → Prop :=
  | transfert_fun_meet_ax : ∀ ax,
    transfert_fun_meet (Rule_Ax ax)
  | transfert_fun_meet_R1 : ∀ up,
    (∀ sigma1 sigma1' sigma2 sigma2',
      up sigma1 = Some sigma1' →
      up sigma2 = Some sigma2' →
      up (sigma1 ⊓♯ sigma2) = Some (sigma1' ⊓♯ sigma2')) →
    transfert_fun_meet (Rule_R1 _ up)
  | transfert_fun_meet_R2 : ∀ up next,
    (∀ sigma1 sigma1' sigma2 sigma2',
      up sigma1 = Some sigma1' →
      up sigma2 = Some sigma2' →
      up (sigma1 ⊓♯ sigma2) = Some (sigma1' ⊓♯ sigma2')) →
    (∀ sigma1 r1 sigma1' sigma2 r2 sigma2',
      next sigma1 r1 = Some sigma1' →
      next sigma2 r2 = Some sigma2' →
      next (sigma1 ⊓♯ sigma2) (r1 ⊓♯ r2) = Some (sigma1' ⊓♯ sigma2')) →
    transfert_fun_meet (Rule_R2 up next)
  .

Lemma hyp_in_meet_transert_fun : ∀ (R : term → ast → ares → Prop),
  (∀ n, transfert_fun_meet (arule n)) →
  rel_stable_meet R →
  rel_stable_meet (hyp_in R).
Proof.
  introv T M. cuts P: (∀ t sigma sigma1 sigma2 r r',
      hyp_in R t sigma1 r →
      hyp_in R t sigma2 r' →
      sigma = (sigma1 ⊓♯ sigma2) →
      hyp_in R t sigma (r ⊓♯ r')).
    introv D1 D2. applys¬ P D1 D2.
  introv D1 D2 O. inverts D1 as app1. inverts D2 as app2. constructors.
  introv E C. forwards Icn: Icr n.
  forwards C1: acond_monotone C.
    rewrite O. apply MeetDec.bound1.
  forwards C2: acond_monotone C.
    rewrite O. apply MeetDec.bound2.
  forwards DA1: app1 E C1. forwards DA2: app2 E C2.
  inverts DA1 as Ost1 Ores1 D1. inverts DA2 as Ost2 Ores2 D2.
  asserts Ir: ((r'0 ⊓♯ r'1) ⊑♯ (r ⊓♯ r')). clear - Ores1 Ores2. auto×.
  asserts Is: ((sigma1 ⊓♯ sigma2) ⊑♯ (sigma' ⊓♯ sigma'0)). clear - Ost1 Ost2. auto×.
  asserts CM: (acond n (sigma' ⊓♯ sigma'0)).
    applys¬ acond_monotone C. rewrite¬ O.
  forwards App: Fsem CM. fold (arule n) in App. forwards Tr: T n.
  clear - O App Icn Is Ir C1 C2 D1 D2 M Tr.
  destruct (rule_struct n) eqn: S;
    inverts D1 as E11 E12 E13 I11 N1 I12; rewrite S in *; inverts E11;
    inverts D2 as E21 E22 E23 I21 N2 I22; rewrite S in *; inverts E21;
    rewrite E22 in *; inverts E12; inverts Icn as I1 I2; inverts App as App1 App2.
   asserts Ir': (r0 ⊑♯ (r ⊓♯ r')).
      forwards~: I1 E13 App1. forwards~: I1 E23 App1.
      applys× PosetDec.trans Ir.
    constructors; [ rewrite O; exact Is | exact Ir' |].
    eapply aapply_check_step_Ax; try eassumption.
   constructors; [ rewrite O; exact Is | exact Ir |].
    forwards D: M I11 I21. applys aapply_check_step_R1 D; try eassumption.
    inverts Tr as T. apply× T.
   constructors; [ rewrite O; exact Is | exact Ir |].
    lets (sigma_next&Esigma_next): (App2 (r0 ⊓♯ r1)).
    inverts Tr as Tup Tnext. forwards¬ T: Tup E13 E23. rewrite App1 in T. inverts T.
    forwards¬ T: Tnext N1 N2. rewrite Esigma_next in T. inverts T.
    eapply aapply_check_step_R2; try eassumption.
     forwards¬ D: M I11 I21.
     forwards¬ D: M I12 I22.
Qed.

Inductive meet_closure (R : term → ast → ares → Prop) : term → ast → ares → Prop :=
  | meet_closure_exact : ∀ t sigma r,
      R t sigma r →
      meet_closure R t sigma r
  | meet_closure_meet : ∀ t sigma sigma1 sigma2 r r1 r2,
      sigma ⊑♯ (sigma1 ⊓♯ sigma2) →
      (r1 ⊓♯ r2) ⊑♯ r →
      meet_closure R t sigma1 r1 →
      meet_closure R t sigma2 r2 →
      meet_closure R t sigma r
  .

Lemma meet_closure_stable_meet : ∀ R,
  rel_stable_meet (meet_closure R).
Proof. introv D1 D2. applys¬ meet_closure_meet D1 D2. Qed.

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

Lemma hyp_in_meet_rel : ∀ t sigma r,
  meet_closure aeval t sigma r →
  hyp_in (meet_closure aeval) t sigma r.
Proof.
  introv D. induction D.
   applys¬ hyp_in_impl.
    apply meet_closure_exact.
    apply¬ aeval_hyp_in_impl.
   applys hyp_in_st_pos H. applys hyp_in_res_pos H0.
    apply¬ hyp_in_meet.
     clear. introv O D. inverts D as O1 O2 D1 D2.
      apply meet_closure_exact. applys¬ aeval_st_pos O1.
      applys meet_closure_meet D1 D2; try eassumption.
       applys¬ @PosetDec.trans O.
     clear. introv D1 D2. applys× meet_closure_meet D1 D2.
Qed.

Lemma aeval_meet : rel_stable_meet aeval.
Proof.
  introv D1 D2. rewrite aevals_same.
  apply aeval_f_cons with (R := meet_closure aeval).
   clear t sigma1 sigma2 r r' D1 D2. introv D.
    forwards M: hyp_in_meet (meet_closure aeval).
     clear. introv O D. inverts D as O1 O2 D1 D2.
      apply meet_closure_exact. applys¬ aeval_st_pos O.
      applys¬ meet_closure_meet D1 D2. applys¬ @PosetDec.trans O.
     clear. introv D1 D2. applys× meet_closure_meet D1 D2.
     inverts D as O1 O2 D1 D2.
      eapply hyp_in_impl.
       apply meet_closure_exact.
       apply¬ aeval_hyp_in_impl.
     applys hyp_in_st_pos O1. applys hyp_in_res_pos O2.
      apply¬ M; apply¬ hyp_in_meet_rel.
   eapply meet_closure_meet; try apply× @PosetDec.refl; apply¬ meet_closure_exact.
Qed.

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

Lemma Park_meet_Park : ∀ R,
  (∀ n, transfert_fun_meet (arule n)) →
  Park_meet R →
  Park (meet_closure R).
Proof.
  introv T P D. induction D.
   forwards~: R.
   eapply hyp_in_st_pos; try eassumption.
    eapply hyp_in_res_pos; try eassumption.
    applys¬ hyp_in_meet_transert_fun T meet_closure_stable_meet.
Qed.

Lemma Park_meet_Park_st_incr : ∀ R,
  rel_st_incr R →
  Park_meet R →
  Park (meet_closure R).
Proof.
  introv T P D. induction D.
   forwards~: R.
   eapply hyp_in_st_pos; try eassumption.
    eapply hyp_in_res_pos; try eassumption.
    applys¬ hyp_in_meet meet_closure_stable_meet. apply¬ meet_closure_st_incr.
Qed.

End AbstractWorld.

Section Correctness.

Correctness

Require Export lat_prop.
Require Export CompleteLattice.

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 TC : rule_format_correct_all sem.

Hypothesis Lst : LatticeDec.t ast.
Hypothesis Lr : LatticeDec.t ares.

Variable gst : ast → st → Prop.
Hypothesis Gst : Gamma.t _ _ gst.
Variable gres : ares → res → Prop.
Hypothesis Gres : Gamma.t _ _ gres.

We could add as hypothesis for every condition underneath that cond is respected, but I don't think that it would really be necessary in practise: abstract transfert functions are usually more or less close to the concrete ones. Thus would further more complexify the definition of this predicate.

Inductive propagates : aRule → Rule → Prop :=
  | propagates_Ax : ∀ ax aax,
      (∀ sigma asigma r ar,
        gst asigma sigma →
        ax sigma = Some r →
        aax asigma = Some ar →
        gres ar r) →
      propagates (Rule_Ax aax) (Rule_Ax ax)
  | propagates_R1 : ∀ up aup,
      (∀ sigma asigma sigma' asigma',
        gst asigma sigma →
        up sigma = Some sigma' →
        aup asigma = Some asigma' →
        gst asigma' sigma') →
      propagates (Rule_R1 _ aup) (Rule_R1 _ up)
  | propagates_R2 : ∀ up aup next anext,
      (∀ sigma asigma sigma' asigma',
        gst asigma sigma →
        up sigma = Some sigma' →
        aup asigma = Some asigma' →
        gst asigma' sigma') →
      (∀ sigma asigma r ar sigma' asigma',
        gst asigma sigma →
        gres ar r →
        next sigma r = Some sigma' →
        anext asigma ar = Some asigma' →
        gst asigma' sigma') →
      propagates (Rule_R2 aup anext) (Rule_R2 up next)
  .

Hypothesis Pr : ∀ n, propagates (arule n) (rule n).

Lemma format_correct_conserved : rule_format_correct_all asem.
Proof.
  intro n. lets P: Pr n. lets T: TC n.
  fold (rule_struct n) in ×. fold (arule n). fold (rule n) in T.
  inverts T; rewrite_term (rule n); inverts P; constructors.
Qed.

Hypothesis acond_correct : ∀ n asigma sigma,
  gst asigma sigma →
  cond n sigma →
  acond n asigma
  .

Theorem correctness : ∀ t asigma ar,
  aeval _ _ _ t asigma ar →
  ∀ sigma r,
    gst asigma sigma →
    eval _ t sigma r →
    gres ar r.
Proof.
  cuts (IHE&IHA): ((∀ t sigma r,
      eval _ t sigma r →
      ∀ asigma ar,
      aeval _ _ _ t asigma ar →
      gst asigma sigma →
      gres ar r)
    ∧ ∀ n sigma r,
      apply _ n sigma r →
      ∀ asigma ar,
      aapply_step _ _ _ n asigma ar →
      gst asigma sigma →
      gres ar r).
    introv aE G E. forwards*: IHE.
  apply eval_mutind.
  introv Et C A IHA aE G. inverts aE as allBranches.
  forwards aA: allBranches Et.
    apply× acond_correct.
  inverts aA as Ssigma Sr aA. forwards G': IHA aA.
    forwards~: @Gamma.monotone Ssigma G.
  forwards~: Gamma.monotone Sr G'.
  introv Estr ER Eax aA G. inverts aA; rewrite_term (rule_struct n); inverts Estr.
  forwards P: Pr n. rewrite_term (rule n). rewrite_term (arule n). inverts P as Hyp.
  apply× Hyp.
  introv Estr ER Eup E IH aA G.
  inverts aA as Estr' ER' Eup' aE'; rewrite_term (rule_struct n); inverts Estr.
  forwards P: Pr n. rewrite_term (rule n). rewrite_term (arule n). inverts P as Hyp.
  forwards*: Hyp.
  introv Estr ER Eup E1 IH1 Enext Ae2 IH2 aA G.
  inverts aA as Estr1 ER1 Eup1 aE1 Enext1 aE2; rewrite_term (rule_struct n); inverts Estr.
  forwards P: Pr n. rewrite_term (rule n). rewrite_term (arule n). inverts P as Hyp1 Hyp2.
  forwards*: Hyp1.
Qed.

End Correctness.