Library Theory

Correctness of the up-to techniques corresponding to the notions of (weak) monotonic functions, or controlled simulations


Require Export WeakMonotonic.

Section Global.

  Variables A X Y: Type.
  Variable TX: reduction_t A X.
  Variable TY: reduction_t A Y.

Correctness with a monotonic function

  Section MonotonicCorrect.

    Variable F: function X Y.
    Hypothesis HF: monotonic TX TY F.

    Variable R: relation2 X Y.
    Hypothesis HR: evolve TX TY R (F R).

predicate for the induction
    Let phi: forall n, evolve TX TY (UExp F R n) (UExp F R (S n)).

Proposition 1.6
    Theorem monotonic_correct: simulation TX TY (UIter F R).

  End MonotonicCorrect.

Correctness with a weakly monotonic function

  Section WeakMonotonicCorrect.

    Variable F: function X Y.
    Hypothesis HF: wmonotonic TX TY F.

    Variable R: relation2 X Y.
    Hypothesis HRt: simulation_t TX TY R.
    Hypothesis HRa: evolve_a TX TY R (F R).

first induction predicate
    Let silent: forall n, simulation_t TX TY (UExp F R n).

correction w.r.t. silent steps
    Lemma wmonotonic_correct_t: simulation_t TX TY (UIter F R).

second induction predicate
    Let visible: forall n, evolve_a TX TY (UExp F R n) (UExp F R (S n)).

Proposition 2.2
    Theorem wmonotonic_correct: simulation TX TY (UIter F R).

  End WeakMonotonicCorrect.

Correctness with a monotonic function, and a weakly monotonic function

  Section UnifiedCorrect.

    Variables F G: function X Y.
    Hypothesis HF : monotonic TX TY F.
    Hypothesis HG : wmonotonic TX TY G.

    Variable R: relation2 X Y.

    Hypothesis HFG: contains F G.

    Hypothesis HRt: evolve_t TX TY R (F R).
    Hypothesis HRa: evolve_a TX TY R (G R).

first induction predicate
    Let pre_silent: forall n, evolve_t TX TY (UExp F R n) (UExp F R (S n)).
    Let silent: simulation_t TX TY (UIter F R).

    Let HFGn: forall n, incl (UExp F R n) (UExp G R n).

second induction predicate
    Let pre_visible: forall n, evolve TX TY (UExp F R n) (UExp G R (S n)).
    Let visible: evolve_a TX TY (UIter F R) (UIter G R).

    Let HGFGn: forall n, incl (UExp (UIter G) (UIter G R) n) (UExp (UIter G) R (S n)).
    Let HGFG: eeq (UIter (UIter G) (UIter F R)) (UIter (UIter G) R).

Proposition 2.4
    Theorem unified_correct: simulation TX TY (UIter (UIter G) R).

  End UnifiedCorrect.

Correctness with a monotonic function, a weakly monotonic function, and a controlled simulation

  Section ControlledCorrect.

    Variable B: relation X.
    Hypothesis HB: controlled TX TY B.

    Variables F G: function X Y.
    Hypothesis HF : monotonic TX TY F.
    Hypothesis HG : wmonotonic TX TY G.

    Hypothesis HBF: transparent B F.
    Hypothesis HFG: contains F G.
    Hypothesis HBG: contains (chaining_l (star B)) G.

    Variable R: relation2 X Y.
    Hypothesis HRt: evolve_t TX TY R (comp (star B) (F R)).
    Hypothesis HRa: evolve_a TX TY R (G R).

first induction predicate
    Let pre_silent: forall n, evolve_t TX TY (UExp F R n) (comp (star B) (UExp F R (S n))).
    Let silent: simulation_t TX TY (comp (star B) (UIter F R)).

    Let HFGn: forall n, incl (UExp F R n) (UExp G R n).
    Let HBGGn: forall R n, incl (comp (star B) (UExp G R n)) (UExp G R (S n)).

second induction predicate
    Let pre_visible: forall n, evolve TX TY (UExp F R n) (UExp G R (2+n)).
    Let visible: evolve_a TX TY (comp (star B) (UIter F R)) (UIter G (comp (star B) (UIter F R))).

    Let HGGBF: eeq (UIter (UIter G) (comp (star B) (UIter F R))) (UIter (UIter G) R).

Proposition 3.4
    Theorem controlled_correct: simulation TX TY (UIter (UIter G) R).

  End ControlledCorrect.

End Global.