From Undecidability.Shared.Libs.DLW
Require Import utils.
Set Implicit Arguments.
Set Default Proof Using "Type".
Section recursor.
Variables (F : nat -> Prop)
(Ffun : forall n m, F n -> F m -> n = m)
(HF : ex F -> sig F)
(G : nat -> nat -> nat -> Prop)
(Gfun : forall x y n m, G x y n -> G x y m -> n = m)
(HG : forall x y, ex (G x y) -> sig (G x y)).
Fixpoint recursor n x :=
match n with
| 0 => F x
| S n => exists y, recursor n y /\ G n y x
end.
Fact recursor_fun n x y : recursor n x -> recursor n y -> x = y.
Proof using Ffun Gfun.
revert x y; induction n as [ | n IHn ]; simpl; auto.
intros x y (a & H1 & H2) (b & H3 & H4).
specialize (IHn _ _ H1 H3); subst b.
revert H2 H4; apply Gfun.
Qed.
Fixpoint recursor_coq n (Hn : ex (recursor n)) : sig (recursor n).
Proof using Ffun Gfun HF HG.
destruct n as [ | n ].
apply HF, Hn.
refine (match recursor_coq n _ with
| exist _ xn Hxn => match @HG n xn _ with
| exist _ xSn HxSn => exist _ xSn _
end
end).
* destruct Hn as (_ & y & ? & _); exists y; auto.
* destruct Hn as (x & y & H1 & H2).
exists x; revert H2; eqgoal; do 2 f_equal.
revert H1 Hxn. eapply recursor_fun.
* exists xn; auto.
Defined.
End recursor.