``` ```

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