Last active
May 28, 2023 06:46
-
-
Save MarcusVoelker/3e48d7e0f85beaf8cc51a84aa5e3db18 to your computer and use it in GitHub Desktop.
Proof of Kleene Fix Point Theorem in Coq
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment