# Library LFS2

Require Import LFS.

# 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 power UA U.

Lemma power_nil U :
nil power U.

Definition rep (A U : list X) : list X :=
filter (fun xx A) U.

Lemma rep_power A U :
rep A U power U.

Lemma rep_incl A U :
rep A U A.

Lemma rep_equi A U :
A Urep A U A.

Lemma rep_mono A B U :
A Brep A U rep B U.

Lemma rep_eq' A B U :
( x, x U → (x A x B)) → rep A U = rep B U.

Lemma rep_eq A B U :
A Brep A U = rep B U.

Lemma rep_injective A B U :
A UB Urep A U = rep B UA B.

Lemma rep_idempotent A U :
rep (rep A U) U = rep A U.

Lemma dupfree_power U :
dupfree Udupfree (power U).

Lemma dupfree_in_power U A :
A power Udupfree Udupfree A.

Lemma rep_dupfree A U :
dupfree UA power Urep A U = A.

Lemma power_extensional A B U :
dupfree UA power UB power UA BA = B.

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 XXProp.
Variable step_mono : A B x, A Bstep A xstep B x.
Context {step_dec : A x, dec (step A x)}.
Variable U : list X.

Inductive lfp : XProp :=
| lfpI A x : ( a, a Alfp a) → step A xx Ulfp x.

Definition fstep (A : list X) : list X :=
filter (step A) U.

Fixpoint chain n : list X :=
match n with
| Onil
| 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 limit lfp x.

Lemma fstep_mono A B :
A Bfstep A fstep B.

Lemma chain_ascending n :
chain n chain (S n).

Lemma chain_bounded n :
chain n U.

Definition sat (A : list X) (q : XProp) : Prop :=
x, x Aq x.

Definition invariant (q : XProp) : Prop :=
A, sat A qsat (fstep A) q.

Lemma chain_invariant q n :
invariant qsat (chain n) q.

Lemma invariant_lfp :
invariant lfp.

Definition stat (n : nat) : Prop :=
chain n chain (S n).

Lemma stat_S n :
stat nstat (S n).

Lemma stat_card n :
¬ stat ncard (chain n) < card (chain (S n)).

Lemma chain_progress n :
¬ stat ncard (chain (S n)) > n.

Instance stat_dec n :
dec (stat n).

Lemma limit_fixpoint:
fstep limit limit.

Lemma lfp_limit x :
lfp x x limit.

Lemma lfp_dec x :
dec (lfp x).

End LFP.

# Quasi-maximal extensions

Lemma size_recursion X (f : Xnat) (t : XType) :
( x, ( y, f y < f xt y) → t x) → x, t x.

Section QME.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.
Variable p : list XProp.
Context {p_dec : A, dec (p A)}.
Variable U : list X.

Definition qmax (M : list X) : Prop :=
M U p M x, x Up (x::M) → x M.

Lemma qmax_or A :
A Up A{x | x U p (x::A) ¬ x A} + {qmax A}.

Lemma qmax_exists A :
A Up A{M | A M qmax M}.

End QME.

# Exercises

Section SlackRec.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.

Lemma slack_recursion U (t : list XType) :
( A, A U → ( B, B Ucard A < card Bt B) → t A) →
A, A Ut A.
End SlackRec.