Require Import LFS. (** printing el #∊# *) (** printing <<= #⊆# *) (** printing === #≡# *) (** * Power Set Representation We define a function [power : list X -> list (list X)] such that [power U] contains a list representation of every subset of [U]. If [U] is duplicate-free, then [power U] is duplicate-free and every subset of U is represented by exactly one element of [U]. We also define a function [rep : list X -> list X] such that [rep A U] yields an element of [power U]. If [A <<= U], then [rep A U === A]. *) Section PowerRep. Variable X : Type. Context {eq_X_dec : eq_dec X}. Fixpoint power (U : list X ) : list (list X) := match U with | nil => [nil] | x :: U' => power U' ++ map (cons x) (power U') end. Lemma power_incl A U : A el power U -> A <<= U. Proof. revert A ; induction U as [|x U] ; simpl ; intros A D. - destruct D as [[]|[]] ; auto. - apply in_app_iff in D as [E|E]. now auto. apply in_map_iff in E as [A' [E F]]. subst A. apply incl_shift. auto. Qed. Lemma power_nil U : nil el power U. Proof. induction U ; simpl ; auto using in_or_app. Qed. Definition rep (A U : list X) : list X := filter (fun x => x el A) U. Lemma rep_power A U : rep A U el power U. Proof. revert A ; induction U as [|x U] ; intros A. - simpl ; auto. - simpl. decide (x el A) as [D|D] ; auto using in_or_app, in_map. Qed. Lemma rep_incl A U : rep A U <<= A. Proof. unfold rep. intros x D. apply in_filter in D. apply D. Qed. Lemma rep_equi A U : A <<= U -> rep A U === A. Proof. intros D. split. now apply rep_incl. unfold rep. intros x E. apply in_filter. auto. Qed. Lemma rep_mono A B U : A <<= B -> rep A U <<= rep B U. Proof. intros D. apply filter_pq_incl. auto. Qed. Lemma rep_eq' A B U : (forall x, x el U -> (x el A <-> x el B)) -> rep A U = rep B U. Proof. intros D. apply filter_pq_eq. auto. Qed. Lemma rep_eq A B U : A === B -> rep A U = rep B U. Proof. intros D. apply filter_pq_eq. firstorder. Qed. Lemma rep_injective A B U : A <<= U -> B <<= U -> rep A U = rep B U -> A === B. Proof. intros D E F. transitivity (rep A U). - symmetry. apply rep_equi, D. - rewrite F. apply rep_equi, E. Qed. Lemma rep_idempotent A U : rep (rep A U) U = rep A U. Proof. unfold rep at 1 3. apply filter_pq_eq. intros x D. split. + apply rep_incl. + intros E. apply in_filter. auto. Qed. Lemma dupfree_power U : dupfree U -> dupfree (power U). Proof. intros D. induction D as [|x U E D] ; simpl. - constructor. now auto. constructor. - apply dupfree_app. + intros [A [F G]]. apply in_map_iff in G as [A' [G G']]. subst A. apply E. apply (power_incl F). auto. + exact IHD. + apply dupfree_map ; congruence. Qed. Lemma dupfree_in_power U A : A el power U -> dupfree U -> dupfree A. Proof. intros E D. revert A E. induction D as [|x U D D'] ; simpl ; intros A E. - destruct E as [[]|[]]. constructor. - apply in_app_iff in E as [E|E]. + auto. + apply in_map_iff in E as [A' [E E']]. subst A. constructor. * intros F ; apply D. apply (power_incl E'), F. * auto. Qed. Lemma rep_dupfree A U : dupfree U -> A el power U -> rep A U = A. Proof. intros D ; revert A. induction D as [|x U E F] ; intros A G. - destruct G as [[]|[]] ; reflexivity. - simpl in G. apply in_app_iff in G as [G|G]. + simpl. decide (x el A) as [H|H]. * exfalso. apply E. apply (power_incl G), H. * auto. + apply in_map_iff in G as [A' [G H]]. subst A. simpl. decide (x=x \/ x el A') as [G|G]. * f_equal. rewrite <- (IHF A' H) at 2. apply filter_pq_eq. apply power_incl in H. intros z K. split ; [|now auto]. intros [L|L] ; subst ; tauto. * exfalso ; auto. Qed. Lemma power_extensional A B U : dupfree U -> A el power U -> B el power U -> A === B -> A = B. Proof. intros D E F G. rewrite <- (rep_dupfree D E). rewrite <- (rep_dupfree D F). apply rep_eq, G. Qed. End PowerRep. (** * Decidability of finite least fixpoints We fix a monotone and decidable step predicate and a finite universe [U]. We define the predicate [lfp] inductively as the least set closed under the step predicate restricted to [U]. We show that [lfp] is decidable. *) Section LFP. Variable X : Type. Context {eq_X_dec : eq_dec X}. Variable step : list X -> X -> Prop. Variable step_mono : forall A B x, A <<= B -> step A x -> step B x. Context {step_dec : forall A x, dec (step A x)}. Variable U : list X. Inductive lfp : X -> Prop := | lfpI A x : (forall a, a el A -> lfp a) -> step A x -> x el U -> lfp x. Definition fstep (A : list X) : list X := filter (step A) U. Fixpoint chain n : list X := match n with | O => nil | S n' => fstep (chain n') end. (** NB: Defining chain with nat_iter would require many manual unfolds. *) Definition limit := chain (card U). (** We will show: [x el limit <-> lfp x]. *) Lemma fstep_mono A B : A <<= B -> fstep A <<= fstep B. Proof. unfold fstep. intros D. apply filter_pq_incl. intros x E. apply step_mono, D. Qed. Lemma chain_ascending n : chain n <<= chain (S n). Proof. induction n ; simpl ; auto using fstep_mono. Qed. Lemma chain_bounded n : chain n <<= U. Proof. destruct n ; simpl. - auto. - apply filter_incl. Qed. Definition sat (A : list X) (q : X -> Prop) : Prop := forall x, x el A -> q x. Definition invariant (q : X -> Prop) : Prop := forall A, sat A q -> sat (fstep A) q. Lemma chain_invariant q n : invariant q -> sat (chain n) q. Proof. intros A ; induction n ; simpl. now intros x []. auto. Qed. Lemma invariant_lfp : invariant lfp. Proof. intros A B x C. apply lfpI with (A:=A). - exact B. - unfold fstep in C. apply in_filter in C. tauto. - apply (filter_incl C). Qed. Definition stat (n : nat) : Prop := chain n === chain (S n). Lemma stat_S n : stat n -> stat (S n). Proof. unfold stat ; simpl. intros D ; split ; apply fstep_mono, D. Qed. Lemma stat_card n : ~ stat n -> card (chain n) < card (chain (S n)). Proof. intros D. destruct (card_or (chain_ascending (n:=n))) as [E|E]. - exfalso. apply D. exact E. - exact E. Qed. Lemma chain_progress n : ~ stat n -> card (chain (S n)) > n. Proof. intros A ; assert (B := stat_card A). induction n. - omega. - assert (C: ~stat n). + intros C ; apply A, stat_S, C. + assert (D:= stat_card C). apply IHn in C ; omega. Qed. Instance stat_dec n : dec (stat n). Proof. unfold stat. decide claim. Qed. Lemma limit_fixpoint: fstep limit === limit. Proof. decide (stat (card U)) as [A|A]. - symmetry ; exact A. - exfalso. apply chain_progress in A. assert (B := chain_bounded (n:=S (card U))). apply (card_le (eq_X_dec:= eq_X_dec)) in B. simpl in *. omega. Qed. Lemma lfp_limit x : lfp x <-> x el limit. Proof. split. - intros H ; induction H as [A x B C IHH D]. rewrite <- limit_fixpoint. apply in_filter ; split. + exact D. + apply (step_mono C IHH). - apply chain_invariant, invariant_lfp. Qed. Lemma lfp_dec x : dec (lfp x). Proof. assert (D:= lfp_limit x). symmetry in D. apply (dec_prop_iff D). decide claim. Qed. End LFP. (** * Quasi-maximal extensions *) Lemma size_recursion X (f : X -> nat) (t : X -> Type) : (forall x, (forall y, f y < f x -> t y) -> t x) -> forall x, t x. Proof. intros step x. apply step. assert (G: forall n y, f y < n -> t y). { intros n. induction n. - intros y B. exfalso. omega. - intros y B. apply step. intros z C. apply IHn. omega. } apply G. Qed. Section QME. Variable X : Type. Context {eq_X_dec : eq_dec X}. Variable p : list X -> Prop. Context {p_dec : forall A, dec (p A)}. Variable U : list X. Definition qmax (M : list X) : Prop := M <<= U /\ p M /\ forall x, x el U -> p (x::M) -> x el M. Lemma qmax_or A : A <<= U -> p A -> {x | x el U /\ p (x::A) /\ ~ x el A} + {qmax A}. Proof. intros D E. destruct (sigma_forall_list U (fun x => p(x::A) -> x el A)) as [[x [F G]]|F]. - left. exists x. apply dec_DM_impl in G ; auto. - unfold qmax. auto. Qed. Lemma qmax_exists A : A <<= U -> p A -> {M | A <<= M /\ qmax M}. Proof. revert A. refine (size_recursion (f:= fun A => card U - card A) _). intros A IH E F. destruct (qmax_or E F) as [[x [G [H K]]]|G]. - destruct (IH (x::A)) as [M [L Q]]. + assert (L: card A < card (x::A)). { apply card_lt with (x:=x) ; auto. } assert (M: card A < card U). { apply card_lt with (x:=x) ; auto. } omega. + apply incl_cons ; assumption. + exact H. + exists M. split. apply incl_lcons with (x:=x), L. exact Q. - exists A. unfold qmax. auto. Qed. End QME. (** * Exercises *) Section SlackRec. Variable X : Type. Context {eq_X_dec : eq_dec X}. Lemma slack_recursion U (t : list X -> Type) : (forall A, A <<= U -> (forall B, B <<= U -> card A < card B -> t B) -> t A) -> forall A, A <<= U -> t A. Proof. intros D. refine (size_recursion (f:= fun A => card U - card A) _). intros A IH E. apply (D A E). intros B F G. apply IH ; [|exact F]. generalize (card_le E), (card_le F). omega. Qed. End SlackRec.