Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[derive.param1.trivial] Unsupported type #407

Open
eponier opened this issue Nov 24, 2022 · 9 comments · May be fixed by #408
Open

[derive.param1.trivial] Unsupported type #407

eponier opened this issue Nov 24, 2022 · 9 comments · May be fixed by #408

Comments

@eponier
Copy link
Collaborator

eponier commented Nov 24, 2022 •
edited
Loading

Inductive toto := | Toto : forall n, unit -> is_zero n = true-> toto.

and

Inductive toto := | Toto : forall n, is_zero n = true-> unit -> toto.

are supported by #[only(param1_trivial)] derive toto. while

Inductive toto := | Toto : unit -> forall n, is_zero n = true -> toto.

is not.
@gares
Copy link
Contributor

gares commented Nov 25, 2022

certainly a bug :-/
can you tell what fails with vervose?

@eponier
Copy link
Collaborator Author

eponier commented Nov 25, 2022 

derive.param1_trivial generates illtyped term: Illegal application: 
The term "is_Toto" of type
 "forall H : unit,
  is_unit H ->
  forall (n : nat) (Pn : is_nat n) (H0 : is_zero n = true),
  is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true is_true H0 ->
  is_toto (Toto H n H0)"
cannot be applied to the terms
 "u" : "unit"
 "i" : "is_unit u"
 "n" : "nat"
 "trivial_full nat is_nat is_nat_trivial n" : "is_nat n"
 "e" : "is_zero n = true"
 "trivial_full (is_zero n = true)
    (is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true is_true)
    (is_eq_trivial bool is_bool is_bool_trivial (is_zero n) (is_is_zero n Pn)
       true is_true) e"
   : "is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true is_true e"
The 6th term has type
 "is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true is_true e"
which should be coercible to
 "is_eq bool is_bool (is_zero n)
    (is_is_zero n (trivial_full nat is_nat is_nat_trivial n)) true is_true e".

@eponier
Copy link
Collaborator Author

eponier commented Nov 25, 2022

It looks like some symbolic Pn remains while it should be instantiated as (trivial_full nat is_nat is_nat_trivial n).

@gares
Copy link
Contributor

gares commented Nov 25, 2022

Right, the odd thing is that the other examples do work, so in that case it does the right substitution

@gares gares linked a pull request Nov 25, 2022 that will close this issue
param1.inhab and failure to find param1 #408
Draft
@gares
Copy link
Contributor

gares commented Nov 25, 2022

See the PR I just opened. IMO the fact we use derive makes a failure go trough. Did you derive is_zero before?

@gares
Copy link
Contributor

gares commented Nov 25, 2022

Or said otherwise, please help me reproduce the bug exactly

@gares
Copy link
Contributor

gares commented Nov 25, 2022

OK, sorry for the noise, I managed to reproduce it.

@eponier
Copy link
Collaborator Author

eponier commented Nov 25, 2022

Yes, I call derive is_zero. before.

@gares
Copy link
Contributor

gares commented Nov 25, 2022

I did put the terms in the PR as comments.
I don't have the time to dig, but I find it weird that the spine of case analysis is done right to left.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

param1.inhab and failure to find param1 LPCIC/coq-elpi
2 participants
@gares @eponier