# Library Fix

Fixpoint theorems : Kleene and Knaster-Tarski
Require Import Setoid.
Require Import Omega.

Order over relations
Definition leR (A:Type) (R R' : AProp) : Prop :=
∀ x, R xR' x.

Notation "A ⊆ B" := (leR _ A B) (at level 80).

Equivalence of relations

Definition eqR (A:Type) (R R' : AProp) : Prop :=
∀ x , R xR' x.

Notation "A == B" := (eqR _ A B) (at level 80).

Definitions of post-fixpoints and least-fixpoints

Definition is_pf (A:Type) (F : (AProp) → (AProp)) (pf : AProp) :=
(F pf) ⊆ pf.

Definition is_lfp (A:Type) (F : (AProp) → (AProp)) (fx : AProp) :=
is_pf _ F fx ∧ ∀ fx', is_pf _ F fx'fxfx'.

Lemma leR_refl : ∀ (X:Type) (R :X → Prop), RR.

Lemma leR_trans : ∀ (X:Type) (A B C:X → Prop), ABBCAC.

Lemma leR_eta_l : ∀ (X:Type) (R R':X->Prop), RR' → (fun xR x) ⊆ R'.

Lemma leR_eta_r : ∀ (X:Type) (R R':X->Prop), RR'R ⊆ (fun xR' x).

The leasf-fixpoint operator is defined as the intersections of the post-fixpoints
Definition lfpKT (C:Type) (F : (CProp) → (CProp)): CProp :=
fun x ⇒ ∀ (X: CProp) , (F X) ⊆ XX x.

Definition mono (C:Type) (F: (CProp) → (CProp)) := ∀ (e e':C-> Prop), ee' → (F e) ⊆ (F e').

If F is monotonic then lfpKT f is indeed a post-fixpoint of f
Lemma is_pf_lfpKT : ∀ (C:Type) (F: (CProp) → (CProp)), mono C Fis_pf _ F (lfpKT C F).

lfpKT f is the least-fixpoint of f
Lemma is_lpf_lfpKT : ∀ (C:Type) (F: (CProp) → (CProp)), mono C Fis_lfp _ F (lfpKT C F).

The *induction* principle of the fixpoint operator
Lemma lfpKT_ind : ∀ (C:Type) (F: (CProp) → (CProp)) (X:C->Prop), mono C F → (F X) ⊆ XlfpKT C FX.

Of course, the least-fixpoint is a fixpoint
Lemma lfpKT_fix : ∀ (C:Type) (F: (CProp) → (CProp)), mono C FlfpKT C FF (lfpKT C F).

The least-fixpoint is *also* the limit of the iterates of the function
Fixpoint iter (A:Type) (F : (AProp) → (AProp)) (n:nat) : AProp :=
match n with
| Ofun xFalse
| S nfun xF (iter A F n ) x
end.

Definition lub (A:Type) (Rel : natAProp) : (AProp) :=
fun x ⇒ ∃ n, Rel n x.

Definition lfpK (C:Type) (F : (CProp) → (CProp)): CProp :=
lub C (iter C F).

Definition chain (A:Type) (f : natAProp) :=
∀ n n', nn'f nf n'.

Definition cont (C:Type) (F : (CProp) → (CProp)):=
∀ f : nat → (CProp),
chain C f
(F (lub _ f)) ⊆ (lub _ (fun nF (f n))).

Lemma cont_morph : ∀ (C:Type) (F F': (CProp) → (CProp)),
(∀ x, F xF' x) → (∀ x, F' xF x) →
cont C Fcont C F'.

The iterates of a monotonic function form a chain
Lemma iter_chain : ∀ (C:Type) (F : (CProp) → (CProp)), mono C Fchain C (iter C F).

The least upper-bound of the iterates of F is a post-fixpoint
Lemma lfpK_pf : ∀ (C:Type) (F: (CProp) → (CProp)), mono C Fcont C Fis_pf _ F (lfpK _ F).

Lemma is_lpf_lfpK : ∀ (C:Type) (F: (CProp) → (CProp)), mono C Fcont C Fis_lfp _ F (lfpK _ F).

Lemma lub_mono : ∀ (C:Type) (f f': nat → (CProp)), (∀ n, f nf' n) → lub _ flub _ f'.
Proof.
intros.
intro. intros. destruct H0. ∃ x0. eapply H ; eauto.
Qed.

Lemma lfpK_ind : ∀ (C:Type) (F: (CProp) → (CProp)) (X:C->Prop), mono C Fcont C F → (F X) ⊆ XlfpK C FX.

Lemma lfpK_fix : ∀ (C:Type) (F: (CProp) → (CProp)), mono C Fcont C FlfpK C FF (lfpK C F).

Lemma lfpK_mono : ∀ (C:Type) (F F': (CProp) → (CProp)), mono C F → (∀ x, F xF' x) → lfpK C FlfpK C F'.

Require Import Max.

Lemma iter_mono : ∀ (A:Type) (F F': (AProp) → (AProp)),
mono A F'
(∀ x, F xF' x) →
∀ n,
iter A F niter A F' n.

Lemma iter_mono_n : ∀ (A:Type) (F : (AProp) → (AProp)),
mono A F
∀ n n', nn'
iter A F niter A F n'.

Lemma lfpK_cont : ∀ (A: Type) (F : (AProp) → (AProp) → (AProp)),
(∀ x, mono _ (F x)) →
(∀ x, mono _ (fun yF y x)) →
(∀ y, cont _ (fun xF x y)) →
(∀ y, cont _ (fun xF y x)) →
cont _ (fun xlfpK _ (fun yF x y)).

Lemma cont2 : ∀ (C:Type) (F : (CProp) → (CProp) → (CProp)),
(∀ x, mono _ (F x)) →
(∀ x, mono _ (fun yF y x)) →
(∀ y, cont C (fun x : CPropF x y)) →
(∀ y, cont C (fun x : CPropF y x)) →
cont _ (fun xF x x).

Definition lfpK2 (C : Type) (F : (CProp) → (CProp) → (CProp)) : CProp :=
lfpK _ (fun x1lfpK _ (fun x2F x1 x2)).

Lemma lfpK2lfpK : ∀ (C : Type) (F : (CProp) → (CProp) → (CProp)),
(∀ y, mono C (fun xF y x)) →
(∀ y, mono C (fun xF x y)) →
(∀ y, cont _ (fun xF x y)) →
(∀ y, cont _ (fun xF y x)) →
lfpK2 _ FlfpK C (fun xF x x).

Lemma μFusion : ∀ (C:Type) (f g h: (CProp) → (CProp)),
mono _ fcont _ fmono _ hcont _ h
mono _ g
(∀ x, f (g x) ⊆ g (h x)) →
(lfpK _ fg (lfpK _ h)).

Lemma lfpKlfpK2 : ∀ (C : Type) (F : (CProp) → (CProp) → (CProp)),
(∀ y, mono C (fun xF y x)) →
(∀ y, mono C (fun xF x y)) →
(∀ y, cont _ (fun xF x y)) →
(∀ y, cont _ (fun xF y x)) →
lfpK C (fun xF x x) ⊆ lfpK2 _ F.

Section AIKT.
We are now able to state basic results for abstract interpretation

Record DomKT (D:Type) : Type := {
F : (DProp ) → (DProp) ;
Fmono : mono D F ;
Fcont : cont D F
}.

Consider a concrete domain C
Hypothesis C : Type.
Hypothesis CDom : DomKT C.

and an abstract domain A
Hypothesis A : Type.
Hypothesis ADom : DomKT A.

linked by a monotonic concretisation function
Hypothesis Gamma : (AProp) → (CProp).
Hypothesis Gamma_mono : ∀ F F', FF' → (Gamma F) ⊆ (Gamma F').

such that a one-step abstract computation correctly models a one-step concrete step
Definition Fc := (F C CDom).
Definition Fa := (F A ADom).

Hypothesis F_gamma : ∀ e, (Fc (Gamma e)) ⊆ (Gamma (Fa e)).

then, least-fixpoint commutes

Lemma lfp_corrct : (lfpK C Fc) ⊆ (Gamma (lfpK A Fa)).

Sometimes, we have a weaker property
Hypothesis F_gamma_fx : (Fc (Gamma (lfpK A Fa))) ⊆ (Gamma (Fa (lfpK A Fa))).

Lemma lfp_corrct_fx : (lfpK C Fc) ⊆ (Gamma (lfpK A Fa)).

End AIKT.

This page has been generated by coqdoc