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