Quantification over Define's result

[mn200]

The following seems to be a mild regression:

val _ = Datatype`inum = inum num | infty`;
val ilt_def = Define`
  (ilt (inum x) (inum y) <=> x < y) ∧
  (ilt (inum _) infty    <=> T) ∧
  (ilt infty _           <=> F)
`;

giving as return value

Equations stored under "ilt_def".
Induction stored under "ilt_ind".
val ilt_def =
   |- ∀y x v1 v0.
     (ilt (inum x) (inum y) ⇔ x < y) ∧ (ilt (inum v0) infty ⇔ T) ∧
     (ilt infty v1 ⇔ F):
   thm

Notice how the universal quantifiers have been lifted to the top-level. Once upon a time, they used to stick with the relevant clauses. This breaks some old code (easily fixed), but is also a tad on the ugly side.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[konrad-slind]

To the best of my recall, Define wouldn't return equations
with a particular quantification format. If a definition happened
to be prim. rec. then each clause would be quantified. But if
a wf. rec. definition was needed then I don't think any effort was
made to quantify every resulting clause.

.... having done some experiments, it seems that this has changed
in the interim (or that my recall is faulty).

Konrad.

On Sun, Aug 10, 2014 at 7:47 PM, Michael Norrish notifications@github.com
wrote:

The following seems to be a mild regression:

val _ = Datatypeinum = inum num | infty;
val ilt_def = Define(ilt (inum x) (inum y) <=> x < y) ∧ (ilt (inum _) infty <=> T) ∧ (ilt infty _ <=> F);

giving as return value

Equations stored under "ilt_def".
Induction stored under "ilt_ind".
val ilt_def =
|- ∀y x v1 v0.
(ilt (inum x) (inum y) ⇔ x < y) ∧ (ilt (inum v0) infty ⇔ T) ∧
(ilt infty v1 ⇔ F):
thm

Notice how the universal quantifiers have been lifted to the top-level.
Once upon a time, they used to stick with the relevant clauses. This breaks
some old code (easily fixed), but is also a tad on the ugly side.

—
Reply to this email directly or view it on GitHub
#186.

[xrchz]

Ideally I think the specification of Define should be to return a theorem that is exactly the same as the input quotation, after a substitution of new constants for variables. Any post-processing to introduce/remove quantifiers, do alpha-renaming, or eta-conversion should be the responsibility of Define. I'm happy for this issue to be reused for this goal, or to open a new one...

[xrchz]

#58 and #59 and possibly #114 are related.