The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

hi coq-users,

Recently I realized that one can define a fixpoint of a (semantically
monotonic) function on relations using "Inductive" by means
of Mendler-style fixpoint.

I know that the idea of Mendler-style fixpoint is known.
I wonder whether this trick has been used in Coq.
Anyway, to me, it is quite interesting, so I post it here to share the trick.

The problem is to define the least fixpoint of a monotonic function f
of type (A1 -> A2 -> .. -> An -> Prop) -> (A1 -> A2 -> ... -> An -> Prop).

For simiplicity, just consider it for n = 1.

=====================================
Set Implicit Arguments.

Definition mypred (A : Type) := A -> Prop.
Hint Unfold mypred.

Definition mypred_le A (f g : mypred A) : Prop :=
  forall a (IN: f a), g a.
Hint Unfold mypred_le.

Definition mypred_monotone A (f : mypred A -> mypred A) : Prop :=
  forall (Q Q' : mypred A) a (IN: f Q a) (LE: mypred_le Q Q'), f Q' a.
Hint Unfold mypred_monotone.
=====================================

If you try to define the least fixpoint 'fixp f' of a function f :
mypred A -> mypred A
naively from the equation 'f (fixp f) = fixp f', then of course you will fail.

=====================================
(* A naive approach does not work !!! *)
Inductive fixp A (f : mypred A -> mypred A) (a : A) : Prop :=
| wfixp_fold (IN: f (fixp f) a).

Error: Non strictly positive occurrence of "fixp" in
 "f (fixp A f MON) a -> fixp A f MON a".
=====================================

The usual way, I think, is to construct it following Knaster–Tarski
fixpoint theorem.

=====================================
(* Note that 'ktfixp' is a not recursive definition. *)
Definition ktfixp A (f : mypred A -> mypred A) (a : A) : Prop :=
  exists P, (forall Q, mypred_le (f Q) Q -> mypred_le P Q) /\ P a.
=====================================

Then we can show that 'ktfixp f' is a fixpoint of and the least such
*if* f is monotone.

=====================================
Lemma ktfixp_induction :
  forall A (a : A) (f : mypred A -> mypred A) (P : mypred A)
    (IH: ktfixp f a)
    (MON: mypred_monotone f)
    (IP: mypred_le (f P) P),
  P a.
Proof. firstorder. Qed.

Lemma le_ktfixp :
  forall A (f : mypred A -> mypred A)
    (MON: mypred_monotone f),
  mypred_le (f (ktfixp f)) (ktfixp f).
Proof. eexists; split; eauto; red; intros; eapply H, MON; eauto;
firstorder. Qed.

Lemma ktfixp_le :
  forall A (f : mypred A -> mypred A)
    (MON: mypred_monotone f),
  mypred_le (ktfixp f) (f (ktfixp f)).
Proof. red; intros; eapply (ktfixp_induction IN); eauto using le_ktfixp. Qed.
=====================================

However, I realized that following Mendler's fixpoint theorem,
one can define the least robust fixpoint of f using "Inductive"
regardless of whether f is monotone or not.

=====================================
(* Note that 'mfixp' is recursively defined. *)
Inductive mfixp A (f : mypred A -> mypred A) (a : A) : Prop :=
| mfixp_fold (P : mypred A) (IN: f P a) (LE: mypred_le P (mfixp f)).
Hint Constructors mfixp.
=====================================

Then Coq gives us a right form of induction principle, and ways of
folding and unfolding.
The folding lemma is 'mfixp_fold' and unfolding can be done just by
destruct "mfixp f".

So, just defining 'mfixp' is enough.
We don't need any lemmas like mfixp_induction, mfixp_le, le_mfixp.

Just to see how it works, let's try to prove some properties of mfixp
as examples.
The proofs are all trivial.

First, let's prove the same properties above.

=====================================
Lemma mfixp_induction :
  forall A (a : A) (f : mypred A -> mypred A) (P : mypred A)
    (IH: mfixp f a)
    (MON: mypred_monotone f)
    (IP: mypred_le (f P) P),
  P a.
Proof. intros; induction IH; eauto. Qed.

Lemma le_mfixp :
  forall A (f : mypred A -> mypred A)
    (MON: mypred_monotone f),
  mypred_le (f (mfixp f)) (mfixp f).
Proof. eauto. Qed.

Lemma mfixp_le :
  forall A (f : mypred A -> mypred A)
    (MON: mypred_monotone f),
  mypred_le (mfixp f) (f (mfixp f)).
Proof. red; intros; induction IN; eauto. Qed.
=====================================

Unlike ktfixp, Mendler fixpoint has similar induction principle,
folding and unfolding
even when f is not monotone.

=====================================
Lemma mfixp_induction_gen :
  forall A (a : A) (f : mypred A -> mypred A) (P : mypred A)
    (IH: mfixp f a)
    (IP: forall (Q: mypred A) b (IH: f Q b) (LE: mypred_le Q P), P b),
  P a.
Proof. intros; induction IH; eauto. Qed.

Lemma le_mfixp_gen :
  forall A (f : mypred A -> mypred A) Q a
    (IN: f Q a)
    (LE: mypred_le Q (mfixp f)),
  mfixp f a.
Proof. eauto. Qed.

Lemma mfixp_le_gen :
  forall A (f : mypred A -> mypred A) a
    (MON: mypred_monotone f)
    (IN: mfixp f a),
  exists Q, f Q a /\ mypred_le Q (mfixp f).
Proof. intros; induction IN; eauto. Qed.
=====================================

Indeed, I used this trick in the Coq formalization of my recent work
and it worked very well and simplified the proofs.

I hope this helps.

Best regards,
Gil