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')

  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')

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.


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.