Jerome Hugues (Sep 23 2022 at 18:11): Jerome Hugues (Sep 23 2022 at 18:11):Hi,
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
Gaëtan Gilbert (Sep 23 2022 at 18:20):it looks like for inductives it uses the name foo_beq but for parameters it expects eq_foo
also Variable won't work, it needs a constant
Gaëtan Gilbert (Sep 23 2022 at 18:20):no idea if this is documented anywhere
Jerome Hugues (Sep 23 2022 at 19:13):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,) ?
Paolo Giarrusso (Sep 23 2022 at 19:48):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
Paolo Giarrusso (Sep 23 2022 at 19:50):I can imagine having function definitions that wrap the Variable, or maybe variants using typeclasses if the generator is flexible enough?
Jerome Hugues (Sep 24 2022 at 18:52):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?
[..]
Answering myself: one difference from https://coq.inria.fr/refman/language/core/assumptions.html?highlight=parameter#coq:cmd.Parameter is that a variable exists only in the scope of a section. Whereas Scheme Equality generates functions that are globally visible.
This is enough to convince me that this cannot be properly supported.
[Marking this as solved.]
Paolo Giarrusso (Sep 24 2022 at 19:22):@Jerome Hugues well, that's exactly why it should be properly supported!
Paolo Giarrusso (Sep 24 2022 at 19:23):Functions written in a section can use parameters; outside the section they just become... Function parameters!
Paolo Giarrusso (Sep 24 2022 at 19:27):So, doesn't seem a fundamental limitation, it's just a silly bug.
Jerome Hugues (Sep 26 2022 at 03:55):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.
Paolo Giarrusso (Sep 26 2022 at 06:47):@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...
Jerome Hugues (Sep 26 2022 at 13:14):I am using 8.16. Following the recommendations above, if i change fooT2_beq to eq_fooT2 then I get a different error: Unexpected error during scheme creation: (in proof temporary_proof25): Attempt to save an incomplete proof
Looking at 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.
Paolo Giarrusso (Sep 26 2022 at 13:25):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
Paolo Giarrusso (Sep 26 2022 at 13:32):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...
Gaëtan Gilbert (Sep 26 2022 at 13:38):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: Sep 23 2023 at 13:01 UTC