Stream: Coq users

Topic: Scheme Boolean Equality and types as parameters in a section


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Sep 23 2022 at 18:20):

no idea if this is documented anywhere

view this post on Zulip 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,) ?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

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. barT_beq reuses 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.

view this post on Zulip Paolo Giarrusso (Sep 24 2022 at 19:22):

@Jerome Hugues well, that's exactly why it should be properly supported!

view this post on Zulip Paolo Giarrusso (Sep 24 2022 at 19:23):

Functions written in a section can use parameters; outside the section they just become... Function parameters!

view this post on Zulip Paolo Giarrusso (Sep 24 2022 at 19:27):

So, doesn't seem a fundamental limitation, it's just a silly bug.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 26 2022 at 06:48):

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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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: Jan 27 2023 at 00:03 UTC