I have some trouble with Boolean equality. It works well in the case types are properly defined. Not when they are parameters of some sections. Here is an example to illustrate this
Section Foo. Inductive fooT := A | B | C. Scheme Equality for fooT. Inductive barT := | bar1 : fooT -> barT. Scheme Boolean Equality for barT. End Foo. Section Foo_failed. Parameter fooT2 : Type. Variable fooT2_beq : fooT2 -> fooT2 -> bool. Inductive barT2 := | bar21 : fooT2 -> barT2. Scheme Boolean Equality for barT2. (* fails with Boolean equality not found for parameter fooT2. *) End Foo_failed.
I understand my definition of
fooT2_beq is not sufficient to qualify as a boolean equality for fooT2, as additional axioms might be necessary. Yet I am curious about what could be the right steps to provide the right definitions.
Any hints? Shall I add some modules (e.g. from Coq.Structures.Equalities) as parameters to have all axioms? I was thinking axioms that relates type equality to the boolean equality would help.
Thanks for your feedback
it looks like for inductives it uses the name
foo_beq but for parameters it expects
also Variable won't work, it needs a constant
no idea if this is documented anywhere
Gaëtan Gilbert said:
no idea if this is documented anywhere
There is no restriction listed here: https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:cmd.Scheme-Equality
Shall there be mention that an actual function definition is expected, and not a function passed as parameter in a section (sorry if the terminology is not accurate,) ?
This should be documented and/or fixed: it's harder to fix if there are users, but I don't understand how you can use it
I can imagine having function definitions that wrap the Variable, or maybe variants using typeclasses if the generator is flexible enough?
Using a wrapper or a typeclass would be an overkill for my use case.
Yet, I may be naive, but I do not get the issue with the variable. Is there a fundamental issue in extending Scheme Equality for this case?
The code generated for the working situation is
Arguments barT_beq X Y barT_beq = fun X Y : barT => match X with | bar1 x => match Y with | bar1 x0 => fooT_beq x x0 end end
so nothing unexpected, and especially no inlining.
fooT_beq that has been generated before. And I could write such code myself for my case.
I was hoping Scheme Equality could generate something similar for a variable. Of course, a random function
A -> A -> bool may not be a boolean equality. Hence my original question: are there any assumptions on the types?
I am not neglecting the implementation cost, and I have a work-around. But I am curious about fundamental reasons why this could not work.
@Jerome Hugues well, that's exactly why it should be properly supported!
Functions written in a section can use parameters; outside the section they just become... Function parameters!
So, doesn't seem a fundamental limitation, it's just a silly bug.
Hi @Paolo Giarrusso , I realize I used the wrongs words. My apologies, as it seems I also misled you in thinking there was an issue with parameters.
I initially thought that parameter and variable were synonym in my original message, when I wrote " and not a function passed as parameter in a section". However, my initial example used the keyword variable for the equality function, not parameter. And @Gaëtan Gilbert put me back on track with his message.
So the corrected examples are the following. Everything works when the equality function is a parameter and not when it is a variable. I initially thought these two definitions were interchangeable (like lemma vs theorem) until I read the documentation in more depth.
Section Foo_parameter. Parameter fooT2 : Type. Parameter eq_fooT2 : fooT2 -> fooT2 -> bool. Inductive barT2 := | bar21 : fooT2 -> barT2. Scheme Boolean Equality for barT2. End Foo_parameter. Section Foo_variable. Parameter fooT3 : Type. Variable eq_fooT3 : fooT3 -> fooT3 -> bool. Inductive barT3 := | bar31 : fooT3 -> barT3. Fail Scheme Boolean Equality for barT3. End Foo_variable.
That being said, I am still puzzled by the difference in treatment. https://coq.inria.fr/refman/language/core/assumptions.html?highlight=parameter#coq:cmd.Parameter indicates that a Variable is equivalent to a local parameter. And the following is accepted:
Section Foo_parameter. Parameter fooT2 : Type. #[local] Parameter eq_fooT2 : fooT2 -> fooT2 -> bool. Inductive barT2 := | bar21 : fooT2 -> barT2. Scheme Boolean Equality for barT2. End Foo_parameter.
I'll double check how I use these constructs in my dev in the future.
@Jerome Hugues Well, I apologize for the confusion on my side. I claim that it's a bug that the following doesn't work (in Coq 8.15): note I'm using . Moreover, it fails with "Boolean equality not found for _parameter_ fooT2.", which arguably is a second bug
Section Foo_failed. Variable fooT2 : Type. Variable fooT2_beq : fooT2 -> fooT2 -> bool. Unset Elimination Schemes. Inductive barT2 := | bar21 : fooT2 -> barT2. Scheme Induction for barT2 Sort Prop. Fail Scheme Equality for barT2. (* fails with "Boolean equality not found for parameter fooT2." *) End Foo_failed.
indicates that a Variable is equivalent to a local parameter.
No, it says "Outside of a section, these are equivalent to Local Parameter.". But what that means is _using_ the command outside a section is equivalent to...
I am using 8.16. Following the recommendations above, if i change
eq_fooT2 then I get a different error: Unexpected error during scheme creation: (in proof temporary_proof25): Attempt to save an incomplete proof
vernac/auto_ind_decl.ml (around line 495), you'll note that the name of the boolean equality should be
eq_x. This is confusing.
a problem is that when you write a name
x, IIUC, it could be a (local) variable, _or_ a "constant" (aka, a definition, fixpoint, axiom, ...), _or_ an inductive — those are internally different
I don't know the details, but I think that's why "Variable won't work, it needs a constant" is possible. But other schemes deal with that...
auto_ind_decl looks for a companion born of the same module as the original constant
but section variables are outcasts belonging to no module
therefore they are not a match
this could in principle be changed but I don't know if anyone wants to do the work
Last updated: Jan 27 2023 at 00:03 UTC