octalgo.datalogcert.fixpoint

The DatalogCert Library CNRS & Université Paris-Sud, Université Paris-Saclay Copyright 2016-2019 : FormalData Original Authors: Véronique Benzaken Évelyne Contejean Stefania Dumbrava
Seventh part of the original file "pengine.v" with modifications


Set Implicit Arguments.

Fixed Points

Once a fixed point is reached. Any iteration gives the fixed point
Lemma fix_iter T (f : T → T) n s (s_fix : s = f s) : s = iter n f s.

If after n iteration, fixpoint is reached so is after m for m > n
Lemma iter_leq_fix T (f : T → T) x n m (i_eq: iter n f x = iter n.+1 f x) :
  n ≤ m → iter m f x = iter m.+1 f x.

note: minsetP lemma subsumes all this
Section iter_mon.

Variables (T : finType).
Implicit Types (s : {set T}) (f : {set T} → {set T}).

Increasing function
Definition monotone f := ∀ s1 s2, s1 \subset s2 → f s1 \subset f s2.

Inflating function
Definition increasing f := ∀ s, s \subset f s.
Let f be an increasing function on sets ot T
Variables (f : {set T} → {set T}) (f_mon : monotone f).

If f increasing so is f^n
Lemma iter_mon n : monotone (iter n f).

Let lb such that if s contains lb, so does f s
Variable (lb : {set T}) (f_lb : ∀ s, lb \subset s → lb \subset f s).

iterf n is |f^n(lb)]
Definition iterf n := iter n f lb.

iterf is increasing
Lemma subset_iterf m n : m ≤ n → iterf m \subset iterf n.

End iter_mon.

Section Fixpoints.

ub and s0 sets of T where T is a finite type with s0 subset of ub
Variables (T : finType) (s0 ub : {set T}).

Hypothesis (s0_bound : s0 \subset ub).

Implicit Types (s : {set T}) (f : {set T} → {set T}).

Variables (f : {set T} → {set T}).

ubound means if ub contains s, it also contains f s
Definition ubound := ∀ s, s \subset ub → f s \subset ub.

we assume that f is monotone increasing and verifies ubound
Hypothesis (f_mono : monotone f) (f_inc : increasing f) (f_ubound: ubound).

Notation iterf_incr n := (iterf f s0 n).
Notation lfp_incr := (iterf f s0 #|ub|).

f^(s0) is included in ub
Lemma iterf_incr_bound n : (iterf_incr n) \subset ub.

lfp_incr, the N iterate of f where N is the cardinal of ub is a fixpoint for f
Adapted from the lfpE lemma in http://www.ps.uni-saarland.de/extras/jaritp14/ (C) Christian Doczkal and Gert Smolka
Lemma lfpE : lfp_incr = f lfp_incr.

lfp_incr is smaller than any fixpoint that would be greater than s0 the starting point of the iterations
Lemma min_lfp_all s (hs : s0 \subset s) (sfp : s = f s) : lfp_incr \subset s.

Rephrase the existence of the LFP and its properties
Lemma has_lfp :
  { lfp : {set T} | lfp = f lfp
                  ∧ lfp = iter #|ub| f s0
                  ∧ ∀ s', s0 \subset s' → s' = f s' → lfp \subset s'}.

End Fixpoints.