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 U → A ⊆ U.

  Lemma power_nil U :
    nil ∊ power U.

  Definition rep (A U : list X) : list X :=
    filter (fun x ⇒ x ∊ 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 ⊆ U → rep A U ≡ A.

  Lemma rep_mono A B U :
    A ⊆ B → rep 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 ≡ B → rep A U = rep B U.

  Lemma rep_injective A B U :
    A ⊆ U → B ⊆ U → rep A U = rep B U → A ≡ B.

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

  Lemma dupfree_power U :
    dupfree U → dupfree (power U).

  Lemma dupfree_in_power U A :
    A ∊ power U → dupfree U → dupfree A.

  Lemma rep_dupfree A U :
    dupfree U → A ∊ power U → rep A U = A.

  Lemma power_extensional A B U :
    dupfree U → A ∊ power U → B ∊ power U → A ≡ B → A = 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 X → X → Prop.
  Variable step_mono : ∀ A B x, A ⊆ B → step A x → step B x.
  Context {step_dec : ∀ A x, dec (step A x)}.
  Variable U : list X.

  Inductive lfp : X → Prop :=
  | lfpI A x : (∀ a, a ∊ A → lfp a) → step A x → x ∊ 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 ∊ limit ↔ lfp x.

  Lemma fstep_mono A B :
    A ⊆ B → fstep 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 : X → Prop) : Prop :=
    ∀ x, x ∊ A → q x.

  Definition invariant (q : X → Prop) : Prop :=
    ∀ A, sat A q → sat (fstep A) q.

  Lemma chain_invariant q n :
    invariant q → sat (chain n) q.

  Lemma invariant_lfp :
    invariant lfp.

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

  Lemma stat_S n :
    stat n → stat (S n).

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

  Lemma chain_progress n :
    ¬ stat n → card (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 : X → nat) (t : X → Type) :
  (∀ x, (∀ y, f y < f x → t y) → t x) → ∀ x, t x.

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

  Definition qmax (M : list X) : Prop :=
    M ⊆ U ∧ p M ∧ ∀ x, x ∊ U → p (x ::M) → x ∊ M.

  Lemma qmax_or A :
    A ⊆ U → p A → {x | x ∊ U ∧ p (x::A) ∧ ¬ x ∊ A } + {qmax A }.

  Lemma qmax_exists A :
    A ⊆ U → p 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 X → Type) :
    (∀ A, A ⊆ U → (∀ B, B ⊆ U → card A < card B → t B) → t A) →
    ∀ A, A ⊆ U → t A.
End SlackRec.