Daniel Kuhse (Oct 31 2021 at 17:01): Daniel Kuhse (Oct 31 2021 at 17:01):(I hope this is right here, if not I'd be thankful if someone moved it to Coq users)
For a plugin I'm writing I need to generate a match statement generalized by the corresponding equality like Program does, as part of constructing a larger term. I haven't found any existing matching mechanism that I can use (at least I don't think I can use constrexpr's since I'm working with EConstr.constr terms and there doesn't seem to be a way to reference them inside constrexprs), so I'm attempting to manually compile them.
However, when generating even a small match with an inferred evars I get an error message I don't understand.
e.g. when matching on a natural number:
match ?n as H return (?n = H -> nat) with
| 0 => fun _ : ?y1 => 0
| S _ => fun _ : ?y => 0
end
If I annotate ?y1 explicitly it works, but if I let it be inferred, I get
Error: In pattern-matching on term "?n" the branch for constructor
"S" has type "nat -> ?T -> nat" which should be
"forall H : nat, ?n = S H -> nat".
Why does the inference fail here? Do I need to do something special while generating the evars? After all it works if one defines the term with these holes in Coq itself.
Gaëtan Gilbert (Oct 31 2021 at 17:13):I get "unknown existential variable" on Check (your code), do you have an actual example?
Daniel Kuhse (Oct 31 2021 at 17:32):I probably should have mentioned that I was printing the term using Printer.pr_econstr.
Do you want the ocaml code I used to generate the example term? I'm not sure how best to share it.
Maybe I'm just confused about how Coq does its type inference.
I thought this:
Check (fun n => match n as H return (n = H -> nat) with
| 0 => fun _ => 0
| S _ => fun _ => 0
end). (which works without issue)
would insert existential variables like if I generate them using Evarutil.new_evar. Is this not the case?
Daniel Kuhse (Oct 31 2021 at 19:09):I've attached both a file containing just the code to generate the failing example and a zip of it embedded into the coq plugin template so that it can be run directly with dune build
matchtest.ml matchtest.zip
Gaëtan Gilbert (Oct 31 2021 at 20:08):it seems you generate all evars in the global env, meaning they don't have access to the variables from the context. this is a problem for the S branch: as the error indirectly tells you by printing one side as an arrow and the other as a forall ?y needs access to the nat from the S
Daniel Kuhse (Oct 31 2021 at 20:53):Ah, yes, that's it, thank you very much!
Notification Bot (Oct 31 2021 at 20:53):Daniel Kuhse has marked this topic as resolved.
Last updated: Apr 19 2024 at 23:02 UTC