Stream: Coq users

Topic: Fixpoint termination


view this post on Zulip Enzo Crance (Sep 16 2022 at 14:12):

Hello. I have a question concerning the fixpoint termination checker in Coq. Suppose I want to write a map function for rose trees based on a map for list:

Definition listf : forall (A A' : Type), (A -> A') -> list A -> list A'.

Inductive rtree (A : Type) : Type :=
  | leaf : A -> rtree A
  | node : list (rtree A) -> rtree A.

Definition rtreef : forall (A A' : Type), (A -> A') -> rtree A -> rtree A'.

My fixpoint for rtreef does not typecheck as is, even with a struct annotation:

fix F A A' f t (* {struct t} *) :=
  match t in rtree _ return rtree A' with
  | leaf a => leaf (f a)
  | node l => node (listf (rtree A) (rtree A') (F A A' f) l)
  end

I need to bring listf into the local fixpoint.

fix listF A A' (f : A -> A') l :=
  match l in list _ return list A' with
  | nil => nil
  | cons a l => cons (f a) (listF A A' f l)
  end
with F A A' f t :=
  match t in rtree _ return rtree A' with
  | leaf a => leaf (f a)
  | node l => node (listF (rtree A) (rtree A') (F A A' f) l)
  end
for F.

Why can Coq reason more about my fixpoint if the function is defined locally? Doesn't the typechecker unfold definitions also for termination checking?
Moreover, I have cases where more than 2 fixpoints depend on each other, and it looks like this local definition trick does not work anymore. Unfortunately I haven't managed to minimise this more complex example yet.

view this post on Zulip Kazuhiko Sakaguchi (Sep 16 2022 at 14:31):

I guess that the first example (single fixpoint) works if you define listf with the first three parameters A, A', and f declared as section variables.

view this post on Zulip Enzo Crance (Sep 16 2022 at 14:34):

Unfortunately, I need the terms to quantify over these variables as I will have to write (and/or generate) the same kind of terms for more complex inductives in the future (e.g. with non-uniform parameters, indices).

view this post on Zulip Kazuhiko Sakaguchi (Sep 16 2022 at 14:40):

I maen:

Section listf.
Variables (A A' : Type) (f : A -> A').

Fixpoint listf (l : list A) :=
  match l in list _ return list A' with
  | nil => nil
  | cons a l => cons (f a) (listf l)
  end.

End listf.

(*
The above `listf` is equivalent to:
Definition listf (A A' : Type) (f : A -> A') := fix listf (l : list A) :=
  match l in list _ return list A' with
  | nil => nil
  | cons a l => cons (f a) (listf l)
  end.
*)

Inductive rtree (A : Type) : Type :=
  | leaf : A -> rtree A
  | node : list (rtree A) -> rtree A.

Fixpoint rtreef (A A' : Type) (f : A -> A') t :=
  match t in rtree _ return rtree A' with
  | leaf _ a => leaf _ (f a)
  | node _ l => node _ (listf (rtree A) (rtree A') (rtreef _ _ f) l)
  end.

view this post on Zulip Enzo Crance (Sep 16 2022 at 14:41):

I meant, how would you use your trick in a meta-language? (I will have to write these terms in the middle of another proof for example, where I cannot add section variables)

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:43):

You don't need sections, see the comment.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:43):

The difference is that f is not an argument of the fixpoint

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:43):

(nor A and A')

view this post on Zulip Kazuhiko Sakaguchi (Sep 16 2022 at 14:44):

The termination checker does unfold definitions, but reducing a fixpoint function requires a constructor application as the decreasing parameter. So, f should appear as an argument of fun, not one of fix.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:45):

this trick does not work for non uniform paramters

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:45):

since you need to update f while you recurse...

view this post on Zulip Enzo Crance (Sep 16 2022 at 14:45):

It's what I wanted to express, thanks

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:46):

I'm not aware of an equivalent trick for NUPs

view this post on Zulip Enrico Tassi (Sep 16 2022 at 14:46):

Q: do you really need NUPs ?

view this post on Zulip Enzo Crance (Sep 16 2022 at 14:47):

For now I can focus on uniform parameters only, but ideally I would like to find a pattern to make it typecheck for any inductive

view this post on Zulip Kazuhiko Sakaguchi (Sep 16 2022 at 14:55):

Aha, but does mutual fixpoint address the issue with non-uniform parameters? Then there is a problem that Coq-Elpi does not support mutual fixpoint...

view this post on Zulip Enrico Tassi (Sep 17 2022 at 05:26):

NUPs are a sort of optimization of indexes when the tgt of the type of constructors leave them syntactically unconstrained. IMO you should be able to rephrase NUPs as indexes all the times.
CC @Matthieu Sozeau

view this post on Zulip Enrico Tassi (Sep 17 2022 at 05:28):

Then your f would be more quantified, but that should be it.

view this post on Zulip Gaëtan Gilbert (Sep 17 2022 at 09:29):

IMO you should be able to rephrase NUPs as indexes all the times.

except for universe concerns
notably you can't write Acc : Prop without NUP (or you lose large elimination)

view this post on Zulip Enrico Tassi (Sep 17 2022 at 12:20):

Are you saying NUP makes the logic stronger?

view this post on Zulip Pierre-Marie Pédrot (Sep 17 2022 at 12:26):

@Gaëtan Gilbert wait, what? This is only true when -indices-matter, isn't it?

view this post on Zulip Gaëtan Gilbert (Sep 17 2022 at 13:36):

Section Well_founded.

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

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

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

argument x fails singleton elimination

view this post on Zulip Pierre-Marie Pédrot (Sep 17 2022 at 13:38):

Oh, indeed. The dreaded hidden effect of recursive types

view this post on Zulip Gaëtan Gilbert (Sep 17 2022 at 13:39):

note also https://github.com/digama0/lean-type-theory/blob/0ba178704380d2fad751f020d461b293f47e36d5/axioms.tex#L148
which basically says that lean has NUP for types in Prop

view this post on Zulip Enrico Tassi (Sep 17 2022 at 19:14):

Acc predates NUP, how can this be?

view this post on Zulip Matthieu Sozeau (Sep 19 2022 at 07:56):

You don't need singleton elimination for Acc to work, you can just use Acc_inv at each recursive call rather than destructing the Acc proof outright, I think

view this post on Zulip Matthieu Sozeau (Sep 19 2022 at 07:59):

(as long as it is ok to recurse on a Prop thing to produce a Type thing).

view this post on Zulip Gaëtan Gilbert (Sep 19 2022 at 08:27):

I guess you lose equivalence between fixpoint style and eliminator style

view this post on Zulip Matthieu Sozeau (Sep 19 2022 at 14:20):

Yes


Last updated: Feb 01 2023 at 13:03 UTC