The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Good morning Europe, this does not give me rest…


What we have so far is that the axiom

    Axiom deferredFix : forall {a}, a -> (a -> a) -> a.

on its own is consistent, and does not add anything to the theory.
Adding the axiom

    Axiom deferredFix_eq : forall {a} d (f : a -> a),
        (exists x, f x = x) ->
        deferredFix d f = f (deferredFix d f).

is still consistent, if Hilbert’s choice is consistent, as it is
equivalent to that, as shown with help from Gaëtan. Some might find
that too strong, and practically, proving the existence of the fixed-
point might sometimes be annoying.


So how about this axiom instead:


    Definition terminating
      {a b} (R : a -> a -> Prop) (f : (a -> b) -> (a -> b)) :=
      forall g h x, (forall y, R y x -> g y = h y) -> f g x = f h x.

    Axiom deferredFix_eq2 :
       forall {a b} d (f : (a -> b) -> (a -> b)) (R : a -> a -> Prop),
       well_founded R -> terminating R f ->
       deferredFix d f = f (deferredFix d f).

Intuitively, I would expect this to be consistent and weaker than
Hilbert’s Choice. To establish consistency, I offer the attached proof
of the axiom (again using Hilbert’s Choice and functional
extensionality).
Is this axiom weaker than those dangerously sounding axioms?



What I like about this axiom is that it allows nested recursion through
higher-order functions like map: in the proof of [terminating R f] I
can make good (even tactic-automated) use of congruence lemmas like
   
    Lemma map_cong: forall {a b} (f g : a -> b) (xs : list a)
      (forall x, In x xs -> f x = g x) -> map f xs = map g xs

which is not the case for `Program Fixpoint`, `Function` or equations,
as far as I can tell. Both the congruence lemmas and the termination
proofs are completely decoupled from the definitions, and are not
necessary before further uses of the recursive function in question.

The attachment also has an example of how I could imagine using this to
work with nested recursion.

(This is heavily inspired by Isabelle’s function package…)


Looking forward to your insights,
Joachim

-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/
Definition terminating {a b} (R : a -> a -> Prop) (f : (a -> b) -> (a -> b)) :=
    forall g h x, (forall y, R y x -> g y = h y) -> f g x = f h x.

Module deferredFixAxiom.

    Axiom deferredFix : forall {a}, a -> (a -> a) -> a.

    Axiom deferredFix_eq : forall {a} d (f : a -> a),
       (exists x, f x = x) ->
       deferredFix d f = f (deferredFix d f).

    Axiom deferredFix_eq2 : forall {a b} d (f : (a -> b) -> (a -> b)) (R : a -> a -> Prop),
       well_founded R -> terminating R f ->
       deferredFix d f = f (deferredFix d f).

End deferredFixAxiom.

Require Import Coq.Logic.ClassicalEpsilon.
Require Import Coq.Logic.FunctionalExtensionality.

Module deferredFixImplementation.


    Definition deferredFix : forall {a}, a -> (a -> a) -> a :=
      fun {a} def f => epsilon (inhabits def) (fun x => f x = x).

    Definition deferredFix_eq : forall {a} d (f : a -> a),
      (exists x, f x = x) ->
      deferredFix d f = f (deferredFix d f) :=
      fun a d f H =>
            eq_sym (epsilon_spec (inhabits d) (fun x => f x = x) H).

    Definition constructFixpoint :forall {a b} (d : a -> b) (F : (a -> b) -> (a -> b)) (R : a -> a -> Prop),
       well_founded R -> a -> b.
    Proof.
      intros ????? Hwf.
      refine (Fix Hwf _ _).
      intros x f'.
      refine (F _ x).
      intro y.
      case (excluded_middle_informative (R y x)).
      * apply f'.
      * intro. exact (d x).
    Defined.


    Definition deferredFix_eq2 : forall {a b} d (F : (a -> b) -> (a -> b)) (R : a -> a -> Prop),
       well_founded R -> terminating R F ->
       deferredFix d F = F (deferredFix d F).
    Proof.
      intros ????? Hwf Hterm .
      apply deferredFix_eq.
      exists (constructFixpoint d F R Hwf).
      unfold constructFixpoint.
      match goal with [ |- F (Fix Hwf _ ?G') = (Fix Hwf _ ?G') ] => set (G := G') end.
      extensionality x.
      rewrite (Fix_eq Hwf (fun _ : a => b) G).
      * apply Hterm.
        intros y HR.
        destruct (excluded_middle_informative (R y x)); intuition.
      * clear x.
        intros x1 f g Heq.
        apply Hterm.
        intros y HR.
        destruct (excluded_middle_informative (R y x1)); intuition.
    Qed.

End deferredFixImplementation.

Require Import Coq.Lists.List.
Require Import Omega.
Import ListNotations.

Lemma map_cong: forall {a b} (f g : a -> b) (xs : list a),
      (forall x, In x xs -> f x = g x) -> map f xs = map g xs.
Proof.
  intros. induction xs; auto; simpl; f_equal; intuition.
Qed.

Module deferredFixInAction.

Import deferredFixAxiom.

(* From https://stackoverflow.com/q/46838928/946226 *)

Inductive Tree := Node : nat -> list Tree -> Tree.

Fixpoint size (t : Tree) : nat :=
  match t with
   | Node x ts => S (fold_right Nat.add 0 (map size ts))
  end.

Definition mapTree (f : nat -> nat)  := deferredFix (fun _ => Node 0 [])
  (fun go t => match t with  Node x ts => Node (f x) (map go ts) end).

Definition Smaller t1 t2 := size t1 < size t2.

Lemma In_Smaller: forall t n ts, In t ts -> Smaller t (Node n ts).
Proof.
  intros. induction ts; inversion H; subst; unfold Smaller in *; simpl in *. 
  * omega.
  * specialize (IHts H0). omega.
Qed.

Lemma mapTree_eq f : mapTree f = 
  (fun t => match t with  Node x ts => Node (f x) (map (mapTree f) ts) end).
Proof.
  unfold mapTree.
  rewrite deferredFix_eq2 with (R := Smaller) at 1.
  * reflexivity.
  * apply Coq.Arith.Wf_nat.well_founded_lt_compat with (f := height).
    intuition.
  * intros g h x IH. 
    destruct x.
    f_equal.
    apply map_cong.
    intros x HIn.
    apply IH.
    clear f g h IH.
    (* Everything until here can easily be automated with a tactic 
       leaving one goal per recursive case with helpful assumptions.
     *)
    apply In_Smaller. assumption.
Qed.


End deferredFixInAction.

Attachment: signature.asc
Description: This is a digitally signed message part