coq
coq copied to clipboard
coq
unification/type inference should perhaps do more fixpoint refolding in non-performance-sensitive locations (regression over 8.5)
Note: the issue was created automatically with bugzilla2github tool
Original bug ID: BZ#5379 From: Qinxiang Cao <[email protected]> Reported version: 8.6 CC: @andrew-appel, @silene, @JasonGross
See also: BZ#4821
Comment author: Qinxiang Cao <[email protected]>
8.6 Type inference behave different with 8.5. Here is an example:
Fixpoint bool_tuple (l: nat): Type :=
match l with
| 0 => unit
| S l' => bool * bool_tuple l'
end.
Parameter P: forall l, bool_tuple (S l) -> Prop.
Goal forall l x, (fun t => P l (fst t, snd t)) x.
In Coq 8.5, the type of x is: bool * bool_tuple l in Coq 8.6, the type of x is
bool *
(fix bool_tuple (l0 : nat) : Type :=
match l0 with
| 0 => unit
| S l' => (bool * bool_tuple l')%type
end) l)
Is this a bug or a feature of Coq 8.6?
Comment author: @silene
Note that, on your example, type inference computes the exact same type in both versions. What is somewhat broken is the refolding of recursive definitions to make types look nicer. You can perform it manually by typing "fold bool_tuple".
Comment author: Qinxiang Cao <[email protected]>
(In reply to Guillaume Melquiond from comment BZ#1)
Note that, on your example, type inference computes the exact same type in both versions. What is somewhat broken is the refolding of recursive definitions to make types look nicer. You can perform it manually by typing "fold bool_tuple".
You are right. The inferred type must be equivalent w.r.t. beta-eta-delta-iota reduction, or else one of them will not type check.
I hope Coq can fix this nice refolding in type inference, or else I have to manually type a lot of definitions (which almost means type inference fails).
Comment author: @JasonGross
If I recall correctly, PMP (and/or Matthieu) found that refolding was an enormous performance bottleneck in [apply] in some cases in fiat-parsers. See bug BZ#4821.
Comment author: Qinxiang Cao <[email protected]>
(In reply to Jason Gross from comment BZ#3)
If I recall correctly, PMP (and/or Matthieu) found that refolding was an enormous performance bottleneck in [apply] in some cases in fiat-parsers. See bug BZ#4821.
I think there is two problem here. One is the type inference in a definition or a lemma. The other is the ugly print out result in proof mode.
The second problem can be fixed by manually refolding. I think this is not too bad.
However, a different type inference result of a definition will cause some proof script of its property fails (which did work in Coq 8.5).
So, if a nicer refolding will cause performance problem in some specific tactics and cannot be fixed, I am OK with that. But I still hope that at least the type inference of definitions and lemmas can be fixed.
Comment author: @andrew-appel
Let me explain why I think this is a significant bug in Coq 8.6, and it is worth fixing.
In the original example, suppose I have:
Lemma my_lemma: forall l x, (fun t => P l (fst t, snd t)) x.
Proof.
. . .
(* Oops: the type of x is very messy,
makes it hard to prove things. This is true inside
the proof . . . *)
Qed.
Lemma next_lemma: whatever.
Proof.
(* . . . but it's also true here, when I try to _use_
my_lemma in another proof. Especially, the "auto" and "rewrite"
tactics will not succeed when the types are unfolded like this. *)
Qed.
Lemma my_lemma': forall l (x: bool * bool_tuple l), (fun t => P l (fst t, snd t)) x.
Proof.
(* Here, things are not messy, either inside the proof of my_lemma',
or outside. Great! But we should not force the user to put in this
type specification for x, especially since Coq 8.5 did this correctly!
*)
Qed.
Summary: Please try to refold definitions when occurring in parameters of top-level Definitions, Lemmas, etc.
Comment author: @JasonGross
Would this suggestion fix the problem? When using a [Definition] or equivalent vernacular, add a post-processing phase that refolds fixpoints.
Comment author: Qinxiang Cao <[email protected]>
(In reply to Jason Gross from comment BZ#6)
Would this suggestion fix the problem? When using a [Definition] or equivalent vernacular, add a post-processing phase that refolds fixpoints.
I am not sure whether I understand "post-processing phase".
If this "post-processing phase" modify the type of the [Definition], then it works. If this "post-processing phase" only prints out nice proof goal, then it does not work.
In other words, if I do:
Lemma my_lemma: forall l x, (fun t => P l (fst t, snd t)) x.
Proof. ... Qed.
Check my_lemma.
Then I hope that the type of x here is folded.
I dunno what to do with this bug, it seems to me that using a type annotation or Implicit Types may be the solution.
Having to use type annotations is annoying and verbose. I think the proposed solution was roughly "sometimes we care less about performance than other times, it would be nice to be able to say that more fixpoint refolding should happen in cases where we care less about performance (such as type inference in most Definition commands)"
@JasonGross large developments such as math-comp manage to avoid these problems using a bit of typing discipline + implicit types, so I am not sure adding yet another boolean toggle to maintain and test in this case is worth the benefit.
Can you point me to examples of what math-comp does to avoid this?
In this particular example the solution is not the best:
Section Ex.
Variable l : nat.
Implicit Types (x : bool_tuple (S l)).
Goal forall x, (fun t => P l (fst t, snd t)) x.
intros.
so indeed it seems to me that there is a bit too much fighting and requires a section [which are pervasively used]
My impression is that this is hard to solve without actually modifying how fixpoints are implemented in Coq, incidentally this was one of top requests from math-comp developers years ago.
Having the flag is yet another annotation so I'm not sure how it compares to actually annotating the expected inferred types when you need it, this is some overhead but not so bad in practice.
I think the solution I'm imagining is that there's an annotation whose default value is "on for definitions and fixpoints not in proof mode, off for proof mode", so in practice, users won't need to annotate most things.
I think the solution I'm imagining is that there's an annotation whose default value is "on for definitions and fixpoints not in proof mode, off for proof mode", so in practice, users won't need to annotate most things.
This still seems a bit brittle , but I guess if someone would propose a patch it'd be OK.
Personally, I'd be tempted to make this issue a duplicate of the more general one "reimplement fixpoints in the kernel using a different reduction rule", which should solve this problems globally.
