Enzo Crance (Sep 16 2022 at 14:12): 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.
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.
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).
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.
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)
Enrico Tassi (Sep 16 2022 at 14:43):You don't need sections, see the comment.
Enrico Tassi (Sep 16 2022 at 14:43):The difference is that f is not an argument of the fixpoint
Enrico Tassi (Sep 16 2022 at 14:43):(nor A and A')
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.
Enrico Tassi (Sep 16 2022 at 14:45):this trick does not work for non uniform paramters
Enrico Tassi (Sep 16 2022 at 14:45):since you need to update f while you recurse...
Enzo Crance (Sep 16 2022 at 14:45):It's what I wanted to express, thanks
Enrico Tassi (Sep 16 2022 at 14:46):I'm not aware of an equivalent trick for NUPs
Enrico Tassi (Sep 16 2022 at 14:46):Q: do you really need NUPs ?
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
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...
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
Enrico Tassi (Sep 17 2022 at 05:28):Then your f would be more quantified, but that should be it.
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)
Enrico Tassi (Sep 17 2022 at 12:20):Are you saying NUP makes the logic stronger?
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?
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
Pierre-Marie Pédrot (Sep 17 2022 at 13:38):Oh, indeed. The dreaded hidden effect of recursive types
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
Enrico Tassi (Sep 17 2022 at 19:14):Acc predates NUP, how can this be?
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
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).
Gaëtan Gilbert (Sep 19 2022 at 08:27):I guess you lose equivalence between fixpoint style and eliminator style
Matthieu Sozeau (Sep 19 2022 at 14:20):Yes
Last updated: Apr 20 2024 at 10:02 UTC