NStrongRec.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

This file defined the strong (course-of-value, well-founded) recursion and proves its properties

Require Export NSub.

Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto).

Module NStrongRecProp (Import N : NAxiomsRecSig').
Include NSubProp N.

Section StrongRecursion.

Variable A : Type.
Variable Aeq : relation A.
Variable Aeq_equiv : Equivalence Aeq.

strong_rec allows defining a recursive function phi given by an equation phi(n) = F(phi)(n) where recursive calls to phi in F are made on strictly lower numbers than n.

For strong_rec a F n:

Parameter a:A is a default value used internally, it has no effect on the final result.
Parameter F:(N→A)->N→A is the step function: F f n should return phi(n) when f is a function that coincide with phi for numbers strictly less than n.

Definition strong_rec (a : A) (f : (N.t -> A) -> N.t -> A) (n : N.t) : A :=
 recursion (fun _ => a) (fun _ => f) (S n) n.

For convenience, we use in proofs an intermediate definition between recursion and strong_rec.

Definition strong_rec0 (a : A) (f : (N.t -> A) -> N.t -> A) : N.t -> N.t -> A :=
 recursion (fun _ => a) (fun _ => f).

Lemma strong_rec_alt : forall a f n,
 strong_rec a f n = strong_rec0 a f (S n) n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
forall (a : A) (f : (t -> A) -> t -> A) (n : t),
strong_rec a f n = strong_rec0 a f (S n) n
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
forall (a : A) (f : (t -> A) -> t -> A) (n : t),
strong_rec a f n = strong_rec0 a f (S n) n
reflexivity.
Qed.

Instance strong_rec0_wd :
 Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq)
  strong_rec0.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
Proper
  (Aeq ==>
   ((eq ==> Aeq) ==> eq ==> Aeq) ==> eq ==> eq ==> Aeq)
  strong_rec0
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
Proper
  (Aeq ==>
   ((eq ==> Aeq) ==> eq ==> Aeq) ==> eq ==> eq ==> Aeq)
  strong_rec0
unfold strong_rec0; f_equiv'.
Qed.

Instance strong_rec_wd :
 Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
Proper
  (Aeq ==>
   ((eq ==> Aeq) ==> eq ==> Aeq) ==> eq ==> Aeq)
  strong_rec
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
Proper
  (Aeq ==>
   ((eq ==> Aeq) ==> eq ==> Aeq) ==> eq ==> Aeq)
  strong_rec
intros a a' Eaa' f f' Eff' n n' Enn'.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
a, a':A
Eaa':Aeq a a'
f, f':(t -> A) -> t -> A
Eff':((eq ==> Aeq) ==> eq ==> Aeq)%signature f f'
n, n':t
Enn':n == n'
Aeq (strong_rec a f n) (strong_rec a' f' n')
rewrite !strong_rec_alt; f_equiv'.
Qed.

Section FixPoint.

Variable f : (N.t -> A) -> N.t -> A.
Variable f_wd : Proper ((N.eq==>Aeq)==>N.eq==>Aeq) f.

Lemma strong_rec0_0 : forall a m,
 (strong_rec0 a f 0 m) = a.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall (a : A) (m : t), strong_rec0 a f 0 m = a
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall (a : A) (m : t), strong_rec0 a f 0 m = a
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
m:t
strong_rec0 a f 0 m = a unfold strong_rec0.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
m:t
recursion (fun _ : t => a) (fun _ : t => f) 0 m = a rewrite recursion_0; auto.
Qed.

Lemma strong_rec0_succ : forall a n m,
 Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall (a : A) (n m : t),
Aeq (strong_rec0 a f (S n) m)
  (f (strong_rec0 a f n) m)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall (a : A) (n m : t),
Aeq (strong_rec0 a f (S n) m)
  (f (strong_rec0 a f n) m)
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
n, m:t
Aeq (strong_rec0 a f (S n) m)
  (f (strong_rec0 a f n) m) unfold strong_rec0.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
n, m:t
Aeq
  (recursion (fun _ : t => a) (fun _ : t => f) (S n) m)
  (f (recursion (fun _ : t => a) (fun _ : t => f) n) m)
f_equiv.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
n, m:t
(Logic.eq ==> Aeq)%signature
  (recursion (fun _ : t => a) (fun _ : t => f) (S n))
  (f (recursion (fun _ : t => a) (fun _ : t => f) n))
rewrite recursion_succ; f_equiv'.
Qed.

Lemma strong_rec_0 : forall a,
 Aeq (strong_rec a f 0) (f (fun _ => a) 0).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall a : A,
Aeq (strong_rec a f 0) (f (fun _ : t => a) 0)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
forall a : A,
Aeq (strong_rec a f 0) (f (fun _ : t => a) 0)
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
Aeq (strong_rec a f 0) (f (fun _ : t => a) 0) rewrite strong_rec_alt, strong_rec0_succ; f_equiv'.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
x, y:t
H:x == y
Aeq (strong_rec0 a f 0 x) a
rewrite strong_rec0_0.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
a:A
x, y:t
H:x == y
Aeq a a reflexivity.
Qed.

(* We need an assumption saying that for every n, the step function (f h n)
calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
coincide on values < n, then (f h1 n) coincides with (f h2 n) *)

Hypothesis step_good :
  forall (n : N.t) (h1 h2 : N.t -> A),
    (forall m : N.t, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f h1 n) (f h2 n).

Lemma strong_rec0_more_steps : forall a k n m, m < n ->
 Aeq (strong_rec0 a f n m) (strong_rec0 a f (n+k) m).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (k n m : t),
m < n ->
Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (k n m : t),
m < n ->
Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)
 intros a k n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
forall m : t,
m < n ->
Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m) pattern n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
(fun t0 : t =>
 forall m : t,
 m < t0 ->
 Aeq (strong_rec0 a f t0 m)
   (strong_rec0 a f (t0 + k) m)) n
 apply induction; clear n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
Proper (eq ==> iff)
  (fun t0 : t =>
   forall m : t,
   m < t0 ->
   Aeq (strong_rec0 a f t0 m)
     (strong_rec0 a f (t0 + k) m))
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall m : t,
m < 0 ->
Aeq (strong_rec0 a f 0 m) (strong_rec0 a f (0 + k) m)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall n : t,
(forall m : t,
 m < n ->
 Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)) ->
forall m : t,
m < S n ->
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m)

 intros n n' Hn; setoid_rewrite Hn; auto with *.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall m : t,
m < 0 ->
Aeq (strong_rec0 a f 0 m) (strong_rec0 a f (0 + k) m)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall n : t,
(forall m : t,
 m < n ->
 Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)) ->
forall m : t,
m < S n ->
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m)

 intros m Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n) (f h2 n)
a:A
k, m:t
Hm:m < 0
Aeq (strong_rec0 a f 0 m) (strong_rec0 a f (0 + k) m)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall n : t,
(forall m : t,
 m < n ->
 Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)) ->
forall m : t,
m < S n ->
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m) destruct (nlt_0_r _ Hm).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
k:t
forall n : t,
(forall m : t,
 m < n ->
 Aeq (strong_rec0 a f n m) (strong_rec0 a f (n + k) m)) ->
forall m : t,
m < S n ->
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m)

 intros n IH m Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m < S n
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m)
 rewrite lt_succ_r in Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S n + k) m)
 rewrite add_succ_l.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
Aeq (strong_rec0 a f (S n) m)
  (strong_rec0 a f (S (n + k)) m)
 rewrite 2 strong_rec0_succ.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
Aeq (f (strong_rec0 a f n) m)
  (f (strong_rec0 a f (n + k)) m)
 apply step_good.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
forall m0 : t,
m0 < m ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
 intros m' Hm'.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
m':t
Hm':m' < m
Aeq (strong_rec0 a f n m')
  (strong_rec0 a f (n + k) m')
 apply IH.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
k, n:t
IH:forall m0 : t,
m0 < n ->
Aeq (strong_rec0 a f n m0)
  (strong_rec0 a f (n + k) m0)
m:t
Hm:m <= n
m':t
Hm':m' < m
m' < n
 apply lt_le_trans with m; auto.
Qed.

Lemma strong_rec0_fixpoint : forall (a : A) (n : N.t),
 Aeq (strong_rec0 a f (S n) n) (f (fun n => strong_rec0 a f (S n) n) n).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (n : t),
Aeq (strong_rec0 a f (S n) n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (n : t),
Aeq (strong_rec0 a f (S n) n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (strong_rec0 a f (S n) n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
rewrite strong_rec0_succ.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (f (strong_rec0 a f n) n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
apply step_good.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
forall m : t,
m < n ->
Aeq (strong_rec0 a f n m) (strong_rec0 a f (S m) m)
intros m Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
Aeq (strong_rec0 a f n m) (strong_rec0 a f (S m) m)
symmetry.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
Aeq (strong_rec0 a f (S m) m) (strong_rec0 a f n m)
setoid_replace n with (S m + (n - S m)).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
Aeq (strong_rec0 a f (S m) m)
  (strong_rec0 a f (S m + (n - S m)) m)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
n == S m + (n - S m)
apply strong_rec0_more_steps.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
m < S m
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
n == S m + (n - S m)
apply lt_succ_diag_r.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
n == S m + (n - S m)
rewrite add_comm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
n == n - S m + S m
symmetry.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
n - S m + S m == n
apply sub_add.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n, m:t
Hm:m < n
S m <= n
rewrite le_succ_l; auto.
Qed.

Theorem strong_rec_fixpoint : forall (a : A) (n : N.t),
 Aeq (strong_rec a f n) (f (strong_rec a f) n).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (n : t),
Aeq (strong_rec a f n) (f (strong_rec a f) n)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (n : t),
Aeq (strong_rec a f n) (f (strong_rec a f) n)
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (strong_rec a f n) (f (strong_rec a f) n)
transitivity (f (fun n => strong_rec0 a f (S n) n) n).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (strong_rec a f n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
  (f (strong_rec a f) n)
rewrite strong_rec_alt.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (strong_rec0 a f (S n) n)
  (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
  (f (strong_rec a f) n)
apply strong_rec0_fixpoint.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
Aeq (f (fun n0 : t => strong_rec0 a f (S n0) n0) n)
  (f (strong_rec a f) n)
f_equiv.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a:A
n:t
(eq ==> Aeq)%signature
  (fun n0 : t => strong_rec0 a f (S n0) n0)
  (strong_rec a f)
intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *.
Qed.

NB: without the step_good hypothesis, we have proved that strong_rec a f 0 is f (fun _ ⇒ a) 0. Now we can prove that the first argument of f is arbitrary in this case...

Theorem strong_rec_0_any : forall (a : A)(any : N.t->A),
 Aeq (strong_rec a f 0) (f any 0).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (any : t -> A),
Aeq (strong_rec a f 0) (f any 0)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a : A) (any : t -> A),
Aeq (strong_rec a f 0) (f any 0)
intros.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
any:t -> A
Aeq (strong_rec a f 0) (f any 0)
rewrite strong_rec_fixpoint.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
any:t -> A
Aeq (f (strong_rec a f) 0) (f any 0)
apply step_good.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a:A
any:t -> A
forall m : t, m < 0 -> Aeq (strong_rec a f m) (any m)
intros m Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n) (f h2 n)
a:A
any:t -> A
m:t
Hm:m < 0
Aeq (strong_rec a f m) (any m) destruct (nlt_0_r _ Hm).
Qed.

... and that first argument of strong_rec is always arbitrary.

Lemma strong_rec_any_fst_arg : forall a a' n,
 Aeq (strong_rec a f n) (strong_rec a' f n).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a a' : A) (n : t),
Aeq (strong_rec a f n) (strong_rec a' f n)
Proof.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
forall (a a' : A) (n : t),
Aeq (strong_rec a f n) (strong_rec a' f n)
intros a a' n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
Aeq (strong_rec a f n) (strong_rec a' f n)
generalize (le_refl n).A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
n <= n -> Aeq (strong_rec a f n) (strong_rec a' f n)
set (k:=n) at -2.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
k:=n:t
k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k) clearbody k.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n, k:t
k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k) revert k.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
forall k : t,
k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k) pattern n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
(fun t0 : t =>
 forall k : t,
 k <= t0 -> Aeq (strong_rec a f k) (strong_rec a' f k))
  n
apply induction; clear n.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
Proper (eq ==> iff)
  (fun t0 : t =>
   forall k : t,
   k <= t0 ->
   Aeq (strong_rec a f k) (strong_rec a' f k))
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall k : t,
k <= 0 -> Aeq (strong_rec a f k) (strong_rec a' f k)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k)
(* compat *)
intros n n' Hn.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n, n':t
Hn:n == n'
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) <->
(forall k : t,
 k <= n' -> Aeq (strong_rec a f k) (strong_rec a' f k))
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall k : t,
k <= 0 -> Aeq (strong_rec a f k) (strong_rec a' f k)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k) setoid_rewrite Hn; auto with *.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall k : t,
k <= 0 -> Aeq (strong_rec a f k) (strong_rec a' f k)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k)
(* 0 *)
intros k Hk.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
k:t
Hk:k <= 0
Aeq (strong_rec a f k) (strong_rec a' f k)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k) rewrite le_0_r in Hk.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
k:t
Hk:k == 0
Aeq (strong_rec a f k) (strong_rec a' f k)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k)
rewrite Hk, strong_rec_0.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
k:t
Hk:k == 0
Aeq (f (fun _ : t => a) 0) (strong_rec a' f 0)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k) symmetry.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
k:t
Hk:k == 0
Aeq (strong_rec a' f 0) (f (fun _ : t => a) 0)
A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k) apply strong_rec_0_any.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n : t) (h1 h2 : t -> A),
(forall m : t, m < n -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n) (f h2 n)
a, a':A
forall n : t,
(forall k : t,
 k <= n -> Aeq (strong_rec a f k) (strong_rec a' f k)) ->
forall k : t,
k <= S n -> Aeq (strong_rec a f k) (strong_rec a' f k)
(* S *)
intros n IH k Hk.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
Aeq (strong_rec a f k) (strong_rec a' f k)
rewrite 2 strong_rec_fixpoint.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
Aeq (f (strong_rec a f) k) (f (strong_rec a' f) k)
apply step_good.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m : t, m < n0 -> Aeq (h1 m) (h2 m)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
forall m : t,
m < k -> Aeq (strong_rec a f m) (strong_rec a' f m)
intros m Hm.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
m:t
Hm:m < k
Aeq (strong_rec a f m) (strong_rec a' f m)
apply IH.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
m:t
Hm:m < k
m <= n
rewrite succ_le_mono.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
m:t
Hm:m < k
S m <= S n
apply le_trans with k; auto.A:Type
Aeq:relation A
Aeq_equiv:Equivalence Aeq
f:(t -> A) -> t -> A
f_wd:Proper ((eq ==> Aeq) ==> eq ==> Aeq) f
step_good:forall (n0 : t) (h1 h2 : t -> A),
(forall m0 : t,
 m0 < n0 -> Aeq (h1 m0) (h2 m0)) ->
Aeq (f h1 n0) (f h2 n0)
a, a':A
n:t
IH:forall k0 : t,
k0 <= n ->
Aeq (strong_rec a f k0) (strong_rec a' f k0)
k:t
Hk:k <= S n
m:t
Hm:m < k
S m <= k
rewrite le_succ_l; auto.
Qed.

End FixPoint.
End StrongRecursion.

Arguments strong_rec [A] a f n.

End NStrongRecProp.