Library Fix

Fixpoint theorems : Kleene and Knaster-Tarski

Require Import Setoid.
Require Import Omega.

Order over relations

Definition leR (A:Type) (R R' : A → Prop) : Prop :=
∀ x, R x → R' x.

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

Equivalence of relations

Definition eqR (A:Type) (R R' : A → Prop) : Prop :=
∀ x , R x ↔ R' x.

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

Definitions of post-fixpoints and least-fixpoints

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

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

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

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

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

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

The leasf-fixpoint operator is defined as the intersections of the post-fixpoints

Definition lfpKT (C:Type) (F : (C → Prop) → (C→ Prop)): C → Prop :=
fun x ⇒ ∀ (X: C → Prop) , (F X) ⊆ X → X x.

Definition mono (C:Type) (F: (C → Prop) → (C → Prop)) := ∀ (e e':C-> Prop), e ⊆ e' → (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: (C → Prop) → (C → Prop)), mono C F → is_pf _ F (lfpKT C F).

lfpKT f is the least-fixpoint of f

Lemma is_lpf_lfpKT : ∀ (C:Type) (F: (C→ Prop) → (C → Prop)), mono C F → is_lfp _ F (lfpKT C F).

The *induction* principle of the fixpoint operator

Lemma lfpKT_ind : ∀ (C:Type) (F: (C→ Prop) → (C→ Prop)) (X:C->Prop), mono C F → (F X) ⊆ X → lfpKT C F ⊆ X.

Of course, the least-fixpoint is a fixpoint

Lemma lfpKT_fix : ∀ (C:Type) (F: (C → Prop) → (C → Prop)), mono C F → lfpKT C F ⊆ F (lfpKT C F).

The least-fixpoint is *also* the limit of the iterates of the function

Fixpoint iter (A:Type) (F : (A → Prop) → (A → Prop)) (n:nat) : A → Prop :=
  match n with
    | O ⇒ fun x ⇒ False
    | S n ⇒ fun x ⇒ F (iter A F n ) x
  end.

Definition lub (A:Type) (Rel : nat → A → Prop) : (A → Prop) :=
  fun x ⇒ ∃ n, Rel n x.

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

Definition chain (A:Type) (f : nat → A → Prop) :=
  ∀ n n', n ≤ n' → f n ⊆ f n'.

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

Lemma cont_morph : ∀ (C:Type) (F F': (C→ Prop) → (C → Prop)),
  (∀ x, F x ⊆ F' x) → (∀ x, F' x ⊆ F x) →
  cont C F → cont C F'.

The iterates of a monotonic function form a chain

Lemma iter_chain : ∀ (C:Type) (F : (C→ Prop) → (C → Prop)), mono C F → chain C (iter C F).

The least upper-bound of the iterates of F is a post-fixpoint

Lemma lfpK_pf : ∀ (C:Type) (F: (C → Prop) → (C → Prop)), mono C F → cont C F → is_pf _ F (lfpK _ F).

Lemma is_lpf_lfpK : ∀ (C:Type) (F: (C → Prop) → (C → Prop)), mono C F → cont C F → is_lfp _ F (lfpK _ F).

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

Lemma lfpK_ind : ∀ (C:Type) (F: (C→ Prop) → (C→ Prop)) (X:C->Prop), mono C F → cont C F → (F X) ⊆ X → lfpK C F ⊆ X.

Lemma lfpK_fix : ∀ (C:Type) (F: (C → Prop) → (C → Prop)), mono C F → cont C F → lfpK C F ⊆ F (lfpK C F).

Lemma lfpK_mono : ∀ (C:Type) (F F': (C → Prop) → (C → Prop)), mono C F → (∀ x, F x ⊆ F' x) → lfpK C F ⊆ lfpK C F'.

Require Import Max.

Lemma iter_mono : ∀ (A:Type) (F F': (A → Prop) → (A → Prop)),
  mono A F' →
  (∀ x, F x ⊆ F' x) →
  ∀ n,
  iter A F n ⊆ iter A F' n.

Lemma iter_mono_n : ∀ (A:Type) (F : (A → Prop) → (A → Prop)),
  mono A F →
  ∀ n n', n ≤ n' →
  iter A F n ⊆ iter A F n'.

Lemma lfpK_cont : ∀ (A: Type) (F : (A → Prop) → (A → Prop) → (A → Prop)),
  (∀ x, mono _ (F x)) →
  (∀ x, mono _ (fun y ⇒ F y x)) →
  (∀ y, cont _ (fun x ⇒ F x y)) →
  (∀ y, cont _ (fun x ⇒ F y x)) →
  cont _ (fun x ⇒ lfpK _ (fun y ⇒ F x y)).

Lemma cont2 : ∀ (C:Type) (F : (C → Prop) → (C → Prop) → (C → Prop)),
  (∀ x, mono _ (F x)) →
  (∀ x, mono _ (fun y ⇒ F y x)) →
  (∀ y, cont C (fun x : C → Prop ⇒ F x y)) →
  (∀ y, cont C (fun x : C → Prop ⇒ F y x)) →
  cont _ (fun x ⇒ F x x).

Definition lfpK2 (C : Type) (F : (C → Prop) → (C → Prop) → (C → Prop)) : C → Prop :=
  lfpK _ (fun x1 ⇒ lfpK _ (fun x2 ⇒ F x1 x2)).

Lemma lfpK2lfpK : ∀ (C : Type) (F : (C → Prop) → (C → Prop) → (C → Prop)),
  (∀ y, mono C (fun x ⇒ F y x)) →
  (∀ y, mono C (fun x ⇒ F x y)) →
  (∀ y, cont _ (fun x ⇒ F x y)) →
  (∀ y, cont _ (fun x ⇒ F y x)) →
  lfpK2 _ F ⊆ lfpK C (fun x ⇒ F x x).

Lemma μFusion : ∀ (C:Type) (f g h: (C → Prop) → (C → Prop)),
  mono _ f → cont _ f → mono _ h → cont _ h →
  mono _ g →
  (∀ x, f (g x) ⊆ g (h x)) →
  (lfpK _ f ⊆ g (lfpK _ h)).

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

Section AIKT.

We are now able to state basic results for abstract interpretation

  Record DomKT (D:Type) : Type := {
    F : (D → Prop ) → (D → Prop) ;
    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 : (A → Prop) → (C → Prop).
Hypothesis Gamma_mono : ∀ F F', F ⊆ F' → (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