Proof of Kleene Fix Point Theorem in Coq

Kleene.v

Require Import Ensembles.
Require Import Setoid.

Definition map {A B : Type} (f : A -> B) (S : Ensemble A) :=
  fun b => exists a, In A S a /\ f a = b.

Section lat.

Variable A : Type.
Variable leA : A -> A -> Prop.

Definition poset :=
  (forall a, leA a a) /\
  (forall a b, (leA a b /\ leA b a) -> a = b) /\
  (forall a b c, (leA a b /\ leA b c) -> leA a c).

Hypothesis pA : poset.

Definition is_ub (S : Ensemble A) (ub : A) :=
  forall s, In A S s -> leA s ub.

Definition is_lub (S : Ensemble A) (lub : A) :=
  is_ub S lub /\ forall ub, is_ub S ub -> leA lub ub.

Definition lattice :=
  poset -> forall sA, { lub : A | is_lub sA lub }.

Definition get_lub (H : lattice) (S : Ensemble A) : A.
  unfold lattice in H. pose (H pA S). destruct s. apply x.
Defined.

Definition bottom (H : lattice) : A := get_lub H (Empty_set A).

End lat.

Arguments poset : default implicits.
Arguments is_ub : default implicits.
Arguments is_lub : default implicits.
Arguments get_lub : default implicits.
Arguments lattice : default implicits.

Lemma lub_unique : forall A (leA : A -> A -> Prop) sA luba lubb, poset leA /\ is_lub leA sA luba /\ is_lub leA sA lubb -> luba = lubb.
Proof.
  intros. destruct H as [[Href [Han Htran]] [[Haub Hal] [Hbub Hbl]]].
  apply Hal in Hbub. apply Hbl in Haub. apply Han. split;auto.
Qed.

Lemma ord_join_is_larger : forall A (leA : A -> A -> Prop) (pA : poset leA) latA (a1 a2 : A), leA a1 a2 -> get_lub pA latA (Union A (Singleton A a1) (Singleton A a2)) = a2.
Proof.
  intros. unfold get_lub. destruct latA as [x [Hub Hless]].
  unfold is_ub in Hub. pose (Hub a2) as Ha2. assert (In A (Union A (Singleton A a1) (Singleton A a2)) a2). {
    apply Union_intror. apply In_singleton.
  }
  apply Hub in H0. assert (Ha2' := Hless a2). destruct pA as [Hs [Hp _]]. apply Hp. split. 2: auto. apply Ha2'.
  unfold is_ub. intros. inversion H1.
  - inversion H2. subst. auto.
  - inversion H2. apply Hs.
Qed.

Lemma le_lub : forall A (leA : A -> A -> Prop) (pA : poset leA) latA (a : A) (S : Ensemble A), In A S a -> leA a (get_lub pA latA S).
Proof.
  intros. unfold get_lub. destruct latA. destruct i. unfold is_ub in H0. apply H0. auto.
Qed.

Lemma lub_singleton : forall A (leA : A -> A -> Prop) (pA : poset leA) latA a, get_lub pA latA (Singleton A a) = a.
Proof.
  intros. unfold get_lub. destruct latA. destruct i. unfold is_ub in H. destruct pA as [Hr [Ha _]]. apply Ha. split.
  - apply H0. unfold is_ub. intros. inversion H1. apply Hr.
  - apply H. apply In_singleton.
Qed.

Lemma lub_union : forall A (leA : A -> A -> Prop) (pA : poset leA) latA l r, get_lub pA latA (Union A l r) = get_lub pA latA (Union A (Singleton A (get_lub pA latA l)) (Singleton A (get_lub pA latA r))).
Proof.
  intros. unfold get_lub. destruct latA. destruct latA. destruct latA. destruct latA. assert (is_lub leA (Union A l r) x0).
  2: { apply (lub_unique A leA (Union A l r)). split;auto. }
  split.
  - destruct i1 as [H1 _]. destruct i2 as [H2 _]. destruct i0 as [H0 _]. unfold is_ub in *. intros. inversion H.
  -- subst. destruct pA as [Hr [_ Ht]]. eapply Ht. split.
  --- apply H1. auto.
  --- apply H0. apply Union_introl. apply In_singleton.
  -- subst. destruct pA as [Hr [_ Ht]]. eapply Ht. split.
  --- apply H2. auto.
  --- apply H0. apply Union_intror. apply In_singleton.
  - intros. assert (x = x0). {
    destruct pA as [Hr [Ha Ht]].
    apply Ha. split.
    - destruct i0 as [H0 _]. destruct i as [_ Hx].
      apply Hx. unfold is_ub. intros. clear H. clear ub.
      unfold is_ub in H0. inversion H1.
    -- subst. apply Ht with x1. split.
    --- destruct i1. unfold is_ub in H2. apply H2. auto.
    --- apply H0. apply Union_introl. apply In_singleton.
    -- subst. apply Ht with x2. split.
    --- destruct i2. unfold is_ub in H2. apply H2. auto.
    --- apply H0. apply Union_intror. apply In_singleton.
    - clear H. clear ub. destruct i0 as [_ H0]. apply H0.
      unfold is_ub. intros. inversion H;subst.
    -- inversion H1. subst. destruct i1 as [_ Hi1].
       apply Hi1. destruct i as [Hx _]. unfold is_ub.
       intros. unfold is_ub in Hx. apply Hx.
       apply Union_introl. auto.
    -- inversion H1. subst. destruct i2 as [_ Hi2].
       apply Hi2. destruct i as [Hx _]. unfold is_ub.
       intros. unfold is_ub in Hx. apply Hx.
       apply Union_intror. auto.
  }
    subst. destruct i. apply H1. auto.
Qed.

Lemma bot_less : forall A (leA : A -> A -> Prop) (pA : poset leA) latA a, leA (bottom A leA pA latA) a.
Proof.
  intros. unfold bottom. assert (is_ub leA (Empty_set A) a).
  - unfold is_ub. intros. inversion H.
  - unfold get_lub. destruct latA. destruct i. apply H1. apply H.
Qed.

Lemma lub_bot_absorb : forall A (leA : A -> A -> Prop) (pA : poset leA) latA a, a = get_lub pA latA (Union A (Singleton A (bottom A leA pA latA)) (Singleton A a)).
Proof.
  intros. unfold get_lub. destruct latA. destruct i. destruct pA as [Hr [Ha Ht]]. eapply Ha. split.
  - unfold is_ub in H. apply H. apply Union_intror. apply In_singleton.
  - apply H0. unfold is_ub. intros. inversion H1.
  -- subst. inversion H2. subst. apply bot_less.
  -- subst. inversion H2. apply Hr.
Qed.

Section func.

Variable A : Type.
Variable B : Type.

Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.

Hypothesis pA : poset leA.
Hypothesis pB : poset leB.

Hypothesis lA : lattice leA.
Hypothesis lB : lattice leB.

Variable f : A -> B.

Definition monotonic :=
  forall a1 a2, leA a1 a2 -> leB (f a1) (f a2).

Definition scott := forall sA, f (get_lub pA lA sA) = get_lub pB lB (map f sA).

Lemma map_in : forall S a, In A S a -> In B (map f S) (f a).
Proof.
  intros. unfold map. unfold In. exists a. split;auto.
Qed.

Lemma map_union : forall l r, map f (Union A l r) = Union B (map f l) (map f r).
Proof.
  intros. apply Extensionality_Ensembles. unfold Same_set. split.
  - unfold Included. intros. destruct H. destruct H.
  subst. unfold In in H. inversion H;subst.
  -- clear H. apply Union_introl. apply map_in. auto.
  -- clear H. apply Union_intror. apply map_in. auto.
  - unfold Included. intros. destruct H.
  -- unfold In. unfold map. inversion H. destruct H0. exists x0. split;auto.
     apply Union_introl. auto.
  -- unfold In. unfold map. inversion H. destruct H0. exists x0. split;auto.
     apply Union_intror. auto.
Qed.

Lemma map_singleton : forall a, map f (Singleton A a) = Singleton B (f a).
Proof.
  intros. apply Extensionality_Ensembles. unfold Same_set. split.
  - unfold Included. intros. destruct H. destruct H. subst. inversion H. subst. apply In_singleton.
  - unfold Included. intros. destruct H. unfold map. unfold In. exists a. split. 2: auto. apply In_singleton.
Qed.

Lemma scott_is_mon : scott -> monotonic.
Proof.
  intros. unfold scott in H. unfold monotonic. intros.
  assert (Hl := ord_join_is_larger A leA pA lA a1 a2).
  apply Hl in H0. rewrite <- H0. rewrite H. rewrite map_union. repeat rewrite map_singleton. apply le_lub. apply Union_introl. apply In_singleton.
Qed.

End func.

Section fixp.

Variable A : Type.
Variable leA : A -> A -> Prop.
Variable f : A -> A.

Definition is_fp (fp : A) := f fp = fp.

Definition is_lfp (lfp : A) := is_fp lfp /\ forall fp, is_fp fp -> leA lfp fp.

Inductive rep_set (a : A) : Ensemble A :=
  | rep_set_0 : rep_set a a
  | rep_set_S x : rep_set a x -> rep_set a (f x)
  .

Fixpoint rep_app n (a : A) :=
  match n with
  | O => a
  | S k => f (rep_app k a)
  end.

Lemma rep_set_a_f_inv : forall a, rep_set a = Union A (Singleton A a) (map f (rep_set a)).
Proof.
  intros. apply Extensionality_Ensembles. split.
  - unfold Included. intros. induction H.
  -- apply Union_introl. apply In_singleton.
  -- apply Union_intror. apply map_in. apply H.
  - unfold Included. intros. induction H.
  -- inversion H. subst. apply rep_set_0.
  -- inversion H. destruct H0. subst. apply rep_set_S. apply H0.
Qed.

Lemma rep_set_n : forall a x, In A (rep_set a) x -> exists n, rep_app n a = x.
Proof.
  intros. induction H.
  - exists 0. auto.
  - destruct IHrep_set. exists (S x0). rewrite <- H0. simpl. auto.
Qed.

Lemma rep_app_com : forall x (a : A), rep_app x (f a) = f (rep_app x a).
Proof.
  intros. induction x.
  - auto.
  - simpl. rewrite IHx. auto.
Qed.

Lemma rep_set_mon : forall (pA : poset leA) a m, monotonic A A leA leA f -> is_fp m -> leA a m -> forall x, In A (rep_set a) x -> leA x m.
Proof.
  intros. apply rep_set_n in H2. destruct H2. generalize dependent a. induction x0.
  - intros. simpl in H2. subst. auto.
  - intros. simpl in H2. subst. apply IHx0 with (f a).
  2: { apply rep_app_com. }
    apply H in H1. rewrite H0 in H1. auto.
Qed.

End fixp.

Arguments is_fp : default implicits.
Arguments is_lfp : default implicits.
Arguments rep_set : default implicits.
Arguments rep_app : default implicits.


Theorem kleene : forall A (leA : A -> A -> Prop) pA (latA : lattice leA) (f : A -> A), scott A A leA leA pA pA latA latA f -> is_lfp leA f (get_lub pA latA (rep_set f (bottom A leA pA latA))).
Proof.
  intros. unfold is_lfp. split.
  - unfold is_fp. unfold scott in H. rewrite H. rewrite rep_set_a_f_inv at -1. rewrite lub_union. rewrite lub_singleton.
  apply lub_bot_absorb.
  - intros. unfold get_lub. destruct latA. assert (monotonic A A leA leA f). { apply scott_is_mon in H. auto. }
  assert (Hbl := bot_less A leA pA latA fp).
  assert (Hlefp := rep_set_mon A leA f pA (bottom A leA pA latA) fp H1 H0 Hbl).
  destruct i. apply H3. unfold is_ub. auto.
Qed.