(** In this file you will discover a classic inductive predicate: [acc].
Through this example we will learn that induction can be performed over
predicates and not only things that you think of as term/data.
Some (relatively independent) bonuses explore coinduction and
transfinite trees. *)
(** * Accessibility
Given a binary relation [R] over an arbitrary type [A],
the accessible elements of [R] are those [a:A] from which there is
no infinite chain [a R a_1 R a_2 R a_3], etc.
The set of accessible elements can also be defined as the least set [S]
such that,
for any [a:A],
if [S] contains all [b] such that [a R b],
then [S] must also contain [a].
In Coq, we don't use sets and relations. A type is an [A:Type], a binary
relation over it is some [R:A->A->Prop], and a set is given via a predicate
[S:A->Prop]. The least fixed point definition is directly obtained via the
primitive notion of inductive definition. *)
Inductive acc (A:Type) (R:A->A->Prop) : A->Prop :=
| mk_acc : forall a:A, (forall b:A, R a b -> acc A R b) -> acc A R a.
(** If [x : acc A R a] then [x] must be of the form [mk_acc A R a F] where
[F] gives, for any [b] for which there is a proof [P] of [R a b],
a subtree [F b P : acc A R b].
Thus [x : acc A R a] can be seen as a derivation tree
obtained using a single inference rule:
(acc b1) (acc b2) ... (acc bN) ...
---------------------------------- [mk_acc]
acc a
where the [bI] form a complete enumeration of the elements [b]
such that [a R b].
The rule has an arbitrary arity: it may be infinite, finite, and even zero
(in which case the node is a leaf and the derivation is completed).
This tree can be infinitely branching, but it cannot have an infinite
branch -- this comes from the least fixed point / inductive nature of [acc].
This aspect will be explored later; for now, let us start with
simple examples. *)
(** We say that a relation is well-founded when all elements of its domain are
accessible. *)
Definition wf (A:Type) (R:A->A->Prop) := forall x, acc A R x.
(** ** Accessibility for the predecessor relation over natural numbers.
Can you picture the shape of [acc] trees for that relation ?
Prove that [2] is accessible, then generalize to all natural numbers. *)
Require Import Arith.
Definition R_pred (x:nat) (y:nat) : Prop := x = S y.
Goal acc nat R_pred 2.
Proof.
Admitted.
Theorem wf_pred : wf nat R_pred.
Proof.
Admitted.
(** When a relation is well-founded, we have [H : acc _ R x] for any [x] and
we can induct on [H]. Formally this relies on the induction principle generated
by Coq for each inductive definition, called [acc_ind] for [acc].
To understand this induction principle, it may be useful to think of [H]
as a derivation tree, as explained above. *)
Check acc_ind.
(** In the particular case when we induct over [acc nat R_pred _] this yields an
induction principle over natural numbers that is essentially the usual one,
as illustrated in the next example. *)
Goal forall x, x = x+0.
Proof.
intros.
assert (acc nat R_pred x); [apply wf_pred|].
induction H.
destruct a.
+ reflexivity.
+ simpl.
rewrite<- H0.
reflexivity.
unfold R_pred; auto.
Qed.
(** ** Accessibility over the usual strict order on [nat]
Let us consider acc on (the converse of) [lt].
It is a well-founded relation but, unlike [pred], its branching is
unbounded:
given [x:nat], there are [x-1] natural numbers [y] such that [yA->Prop) : A -> nat -> Prop :=
| height_step : forall a n, (forall b, R a b -> height A R b n) -> height A R a (S n).
(** Show that all [acc]-trees have a height when taking [R := R_lt]. *)
Lemma lt_tran_S : forall n m p, n < m -> m < S p -> n < p.
Admitted.
Goal forall n, height nat R_lt n (S n).
Admitted.
(** Now define some [A] and [R] such that [wf A R] but [acc]-trees
do not have a height: they are transfinite trees. *)
Definition A : Type.
Admitted.
Definition R : A->A->Prop.
Admitted.
Goal wf A R.
Admitted.
Goal exists a:A, forall n:nat, ~ height A R a (S n).
Admitted.
End Bonus_height.
(** * Bonus 2: coinductives *)
Module Bonus_coinduction.
(** We shall use least and greatest fixed points to understand inductive
and coinductive definitions.
Consider the lattice of subsets of some type [A], ordered by inclusion.
This corresponds to predicates over [A], ordered by implication.
Consider the following two operators over this lattice, the second one
being for [A := nat]. *)
Variable A : Type.
Definition F_id (P:A->Prop) := fun x => P x.
Definition F_N (P:nat->Prop) := fun n => n = 0 \/ exists m, n = S m /\ P m.
(** ** Inductive predicates, aka least fixed points *)
(** We define two predicates that intuitively correspond to the least fixed
points of the previous two operators. To make this connection formal
we would have to write [mk_LFP : forall x, F LFP x -> LFP x]
but Coq won't allow this. So we inline [F] and, in the case of [LFP_N],
also translate the existential and disjunction connectives of [F_N]
into a simpler form using two constructors; in this way, Coq allows
us to work better on [LFP_N]. *)
Inductive LFP_id : A -> Prop :=
| mk_LFP_id : forall x, LFP_id x -> LFP_id x.
Inductive LFP_N : nat -> Prop :=
| LFP_N_0 : LFP_N 0
| LFP_N_S : forall n, LFP_N n -> LFP_N (S n).
(** We can now show that we have least pre-fixed points. *)
Goal forall x, F_N LFP_N x -> LFP_N x.
Admitted.
Goal forall (P:nat->Prop),
(forall x, F_N P x -> P x) -> (forall x, LFP_N x -> P x).
Admitted.
(** Observe finally that our two least fixed points are the extremal
predicates of their respective lattices. *)
Goal forall n, LFP_N n.
Admitted.
Goal forall n, ~ LFP_id n.
Admitted.
(** ** Coinductive predicates, aka greatest fixed points
We follow the same approach as before,
but using coinductive rather than inductive definitions.
Intuitively, we are forming greatest fixed points. *)
CoInductive GFP_id : A -> Prop :=
| mk_GFP_id : forall x, GFP_id x -> GFP_id x.
CoInductive GFP_N : nat -> Prop :=
| GFP_N_0 : GFP_N 0
| GFP_N_S : forall x, GFP_N x -> GFP_N (S x).
(** Show that [GFP_N] is a post-fixed point of [F_N]. *)
Goal forall x, GFP_N x -> F_N GFP_N x.
Admitted.
(** To show that it is the greatest post-fixed point, we use [coinduction]
rather than [induction].
In the terminology of the lattice of predicates, we would be proving
that the predicate [P] is less than [GFP_N].
This would be obtained by showing that [P] is a post-fixed point of
[F_N], i.e. showing that, for any [x] such that if [P x],
we have [F_N P x], which is easy.
Coq's coinduction principle is similar, with a difference that comes in
part from the fact that [F_N] is not explicit in the definition of
[GFP_N]. We launch coinduction using [cofix HC] which introduces an
assumption [HC : forall x, P x -> GFP_N x] and (shockingly) keeps the
same goal [forall x, P x -> GFP_N x]. The assumption [HC] can only be
used after that the goal has been constructor using some constructor
of the coinductive type -- this corresponds to introducing the missing
[F_N] step.
Improper uses of [HC] will lead to a failure upon [Qed]. *)
Goal forall (P:nat->Prop),
(forall x, P x -> F_N P x) -> (forall x, P x -> GFP_N x).
Proof.
intros P HP.
cofix HC.
intros x Hx.
destruct (HP x Hx) as [H|(y,(H,Hy))]; rewrite H; clear H.
+ apply GFP_N_0.
+ apply GFP_N_S. apply HC; assumption.
Qed.
(** Both greatest fixed point examples are the true predicates.
Prove it for [GFP_id], using coinduction. *)
Goal forall n, GFP_id n.
Admitted.
(** Fixed points and complete lattices may be familiar objects,
but they do not provide the simplest intuitions for everybody.
We outline next a more computational intuition.
Induction on some type [T] (whose parameters are omitted for
simplicity) corresponds to the definition of a recursive function
of type [T -> A], where each recursive call is performed on a
(syntactically) strictly decreased argument.
In other words, at every new iteration something is consumed.
Coinduction on [T] corresponds to the definition of a recursive
computation of type [A -> T] that produces a possibly infinite object,
but in a productive manner: it calls itself recursively only to build
subterms of the result, which has first been partially constructed
using a constructor of the coinductive type.
In other words, at every new iteration something is produced.
Overall, this means that any finite prefix of the (possibly infinite)
object can be obtained in finite time. *)
End Bonus_coinduction.
(** * Bonus 3: infinite chains *)
Module Bonus_chains.
(** We define [infch] as a coinductive predicate.
As would be the case for an inductive definition, [H : infch A R a] is
necessarily constructed from one of its constructors; in that case
there is a single constructor [mk_infch].
However, coinductives correspond to greatest fixed points while
inductives correspond to least fixed points. For now, this just
means that you cannot induct on a coinductive;
but you can still use [inversion]. *)
CoInductive infch (A:Type) (R:A->A->Prop) : A->Prop :=
| mk_infch : forall x y, R x y -> infch A R y -> infch A R x.
(** You don't need anything new to show that, if there is an infinite
chain from some [x], then [x] cannot be accessible. *)
Goal forall A R x, infch A R x -> ~ acc A R x.
Admitted.
(** To prove that for any inaccessible element [x], there is an infinite
chain starting from [x], you need to reason by coinduction,
cf. previous bonus. You will need some classical reasoning step:
you can choose the axiom that suits you best. *)
Goal forall A R x, ~ acc A R x -> infch A R x.
Admitted.
(** We now define the existence of an infinite chain in a more usual
way. Can you show that it is equivalent to the previous coinductive
definition? You may take further axioms from set theory: consider
for instance the axiom of choice. *)
Definition infch_f (A:Type) (R:A->A->Prop) (x:A) : Prop :=
exists (f:nat->A), f 0 = x /\ forall n, R (f n) (f (S n)).
End Bonus_chains.