The Coq mailing list

[roconnor AT theorem.ca]

I forgot to include WfType_nat.v and WfType.v which are required.  They
are exactly the same as the standard library except they use Type instead
Set.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Set Implicit Arguments.

(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)

(** This module proves the validity of
    - well-founded recursion (also called course of values)
    - well-founded induction

   from a well-founded ordering on a given set *)

Require Import Notations.
Require Import Logic.
Require Import Datatypes.

(** Well-founded induction principle on Prop *)

Section Well_founded.

 Variable A : Type.
 Variable R : A -> A -> Prop.

 (** The accessibility predicate is defined to be non-informative *)

 Inductive Acc : A -> Prop :=
     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.

 Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
  destruct 1; trivial.
 Defined.

  (** the informative elimination :
     [let Acc_rec F = let rec wf x = F x wf in wf] *)

 Section AccRecType.
  Variable P : A -> Type.
  Variable
    F :
      forall x:A,
        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.

  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).

 End AccRecType.

 Definition Acc_rec (P:A -> Type) := Acc_rect P.

 (** A simplified version of Acc_rec(t) *)

 Section AccIter.
  Variable P : A -> Type. 
  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.

  Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).

 End AccIter.

 (** A relation is well-founded if every element is accessible *)

 Definition well_founded := forall a:A, Acc a.

 (** well-founded induction on Type and Prop *)

 Hypothesis Rwf : well_founded.

 Theorem well_founded_induction_type :
  forall P:A -> Type,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  intros; apply (Acc_iter P); auto.
 Defined.

 Theorem well_founded_induction :
  forall P:A -> Type,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  exact (fun P:A -> Type => well_founded_induction_type P).
 Defined.

 Theorem well_founded_ind :
  forall P:A -> Prop,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  exact (fun P:A -> Prop => well_founded_induction_type P).
 Defined.

(** Building fixpoints  *) 

Section FixPoint.

Variable P : A -> Type.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.

Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).

Definition Fix (x:A) := Fix_F (Rwf x).

(** Proof that [well_founded_induction] satisfies the fixpoint equation. 
    It requires an extra property of the functional *)

Hypothesis
  F_ext :
    forall (x:A) (f g:forall y:A, R y x -> P y),
      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.

Scheme Acc_inv_dep := Induction for Acc Sort Prop.

Lemma Fix_F_eq :
 forall (x:A) (r:Acc x),
   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
destruct r using Acc_inv_dep; auto.
Qed.

Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
intro x; induction (Rwf x); intros.
rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
apply F_ext; auto.
Qed.


Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
intro x; unfold Fix in |- *.
rewrite <- (Fix_F_eq (x:=x)).
apply F_ext; intros.
apply Fix_F_inv.
Qed.

End FixPoint.

End Well_founded. (************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)

(** Well-founded relations and natural numbers *)

Require Import Lt.
Require Export WfType.

Open Local Scope nat_scope.

Implicit Types m n p : nat.

Section Well_founded_Nat.

Variable A : Type.

Variable f : A -> nat.
Definition ltof (a b:A) := f a < f b.
Definition gtof (a b:A) := f b > f a.

Theorem well_founded_ltof : well_founded ltof.
Proof.
red in |- *.
cut (forall n (a:A), f a < n -> Acc ltof a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
unfold ltof in |- *; intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Qed.

Theorem well_founded_gtof : well_founded gtof.
Proof well_founded_ltof.

(** It is possible to directly prove the induction principle going
   back to primitive recursion on natural numbers ([induction_ltof1])
   or to use the previous lemmas to extract a program with a fixpoint
   ([induction_ltof2]) 

the ML-like program for [induction_ltof1] is : [[
   let induction_ltof1 F a = indrec ((f a)+1) a 
   where rec indrec = 
        function 0    -> (function a -> error)
               |(S m) -> (function a -> (F a (function y -> indrec y m)));;
]]

the ML-like program for [induction_ltof2] is : [[
   let induction_ltof2 F a = indrec a
   where rec indrec a = F a indrec;;
]] *)

Theorem induction_ltof1 :
 forall P:A -> Type,
   (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
intros P F; cut (forall n (a:A), f a < n -> P a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply F.
unfold ltof in |- *; intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Defined. 

Theorem induction_gtof1 :
 forall P:A -> Type,
   (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact induction_ltof1.
Defined.

Theorem induction_ltof2 :
 forall P:A -> Type,
   (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact (well_founded_induction well_founded_ltof).
Defined.

Theorem induction_gtof2 :
 forall P:A -> Type,
   (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
exact induction_ltof2.
Defined.

(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
    then [R] is well-founded. *)

Variable R : A -> A -> Prop.

Hypothesis H_compat : forall x y:A, R x y -> f x < f y.

Theorem well_founded_lt_compat : well_founded R.
Proof.
red in |- *.
cut (forall n (a:A), f a < n -> Acc R a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Qed.

End Well_founded_Nat.

Lemma lt_wf : well_founded lt.
Proof well_founded_ltof nat (fun m => m).

Lemma lt_wf_rec1 :
 forall n (P:nat -> Type), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
exact
 (fun p (P:nat -> Type) (F:forall n, (forall m, m < n -> P m) -> P n) =>
    induction_ltof1 nat (fun m => m) P F p).
Defined.

Lemma lt_wf_rec :
 forall n (P:nat -> Type), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
exact
 (fun p (P:nat -> Type) (F:forall n, (forall m, m < n -> P m) -> P n) =>
    induction_ltof2 nat (fun m => m) P F p).
Defined.

Lemma lt_wf_ind :
 forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
intro p; intros; elim (lt_wf p); auto with arith.
Qed.

Lemma gt_wf_rec :
 forall n (P:nat -> Type), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof.
exact lt_wf_rec.
Defined.

Lemma gt_wf_ind :
 forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof lt_wf_ind.

Lemma lt_wf_double_rec :
 forall P:nat -> nat -> Type,
   (forall n m,
      (forall p (q:nat), p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
Defined.

Lemma lt_wf_double_ind :
 forall P:nat -> nat -> Prop,
   (forall n m,
      (forall p (q:nat), p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
Qed.

Hint Resolve lt_wf: arith.
Hint Resolve well_founded_lt_compat: arith.

Section LT_WF_REL.
Variable A : Type.
Variable R : A -> A -> Prop.

(* Relational form of inversion *)
Variable F : A -> nat -> Prop.
Definition inv_lt_rel x y :=
   exists2 n : _, F x n & (forall m, F y m -> n < m).

Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
Remark acc_lt_rel : forall x:A, (exists n : _, F x n) -> Acc R x.
intros x [n fxn]; generalize x fxn; clear x fxn.
pattern n in |- *; apply lt_wf_ind; intros.
constructor; intros.
case (F_compat y x); trivial; intros.
apply (H x0); auto.
Qed.

Theorem well_founded_inv_lt_rel_compat : well_founded R.
constructor; intros.
case (F_compat y a); trivial; intros.
apply acc_lt_rel; trivial.
exists x; trivial.
Qed.


End LT_WF_REL.

Lemma well_founded_inv_rel_inv_lt_rel :
 forall (A:Type) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
Qed.