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.
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.
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).
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)
You don't need sections, see the comment.
The difference is that f
is not an argument of the fixpoint
(nor A and A')
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
.
this trick does not work for non uniform paramters
since you need to update f while you recurse...
It's what I wanted to express, thanks
I'm not aware of an equivalent trick for NUPs
Q: do you really need NUPs ?
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
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...
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
Then your f would be more quantified, but that should be it.
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)
Are you saying NUP makes the logic stronger?
@Gaëtan Gilbert wait, what? This is only true when -indices-matter, isn't it?
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
Oh, indeed. The dreaded hidden effect of recursive types
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
Acc predates NUP, how can this be?
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
(as long as it is ok to recurse on a Prop thing to produce a Type thing).
I guess you lose equivalence between fixpoint style and eliminator style
Yes
Last updated: Oct 13 2024 at 01:02 UTC