Stream: SerAPI

Topic: ✔ Failures when running ssreflect code

view this post on Zulip Alex Loiko (Feb 19 2023 at 21:19):

Hi, I'm working with SerAPI for Coq 8.12. I have code that is accepted by Coq 8.12 without issues but produces an error when run though SerAPI. I tested the same Coq commands both in Proof General and with coqc. I know that 8.12 is an old version, and than SerAPI is in maintenance mode, but upgrading is not something I can do easily. Here is a minified example:

(Add () "Module choice.")
(Add () "From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.")
(Add () "Set Implicit Arguments.")
(Add () "Unset Strict Implicit.")
(Add () "Unset Printing Implicit Defensive.")

(Add () "Section OtherEncodings.")
  (Add () "Variables T T1 T2 : Type.")
  (Add () "Definition tag_of_pair (p : T1 * T2) := @Tagged T1 p.1 (fun _ => T2) p.2.")
  (Add () "Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).")
  (Add () "Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag. ")
  (Add () "Admitted.")
(Add () "End OtherEncodings.")
(Add () "Prenex Implicits tag_of_pairK.")


(Exec 1)
(Exec 2)
(Exec 3)
(Exec 4)
(Exec 5)
(Exec 6)
(Exec 7)
(Exec 8)
(Exec 9)
(Exec 10)
(Exec 11)
(Exec 12)
(Exec 13)
(Exec 14)

When piping this to sertop --implicit, I get Symbol('CoqExn') and Symbol('CErrors.UserError') and the message Expected prenex implicits for tag_of_pairK'. I don't know where to start debugging this.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 21:21):

Hi @Alex Loiko , start to debug this by pasting the commands one by one, and figuring out which one is giving you the error

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 21:22):

Then, and likely the bug in Coq, do an exec after each add, and see if the problem goes away

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 21:22):

That's what coqc and coqide do, they never issue two adds without an Exec

view this post on Zulip Alex Loiko (Feb 19 2023 at 21:28):

Thanks, I did one-by-one pasting, and did rearrange the code with Exec interspersed. It's the last command that fails: the Prenex Implicits . The problem did not go away. For added context this comes from trying to feed math-comp to a tactic-predicting ML system https://github.com/UCSD-PL/proverbot9001

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 21:55):

Umm, that's a bit bizarre, do you have a paste somewhere of the full log?

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:00):

Yes, here is the last command and it's 'Exec':

*(Add () "Prenex Implicits tag_of_pairK.")*

(Answer 26 Ack)
(Answer 26
 (Added 14
  ((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
   (bol_pos_last 0) (bp 0) (ep 30))
  NewTip))
(Answer 26 Completed)

*(Exec 14)*

(Answer 27 Ack)
(Feedback
 ((doc_id 0) (span_id 14) (route 0) (contents (ProcessingIn master))))
(Feedback ((doc_id 0) (span_id 13) (route 0) (contents Processed)))
(Feedback
 ((doc_id 0) (span_id 14) (route 0)
  (contents
   (Message (level Error)
    (loc
     (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
       (bol_pos_last 0) (bp 0) (ep 30))))
    (pp
     (Pp_glue
      ((Pp_string "Expected prenex implicits for ")
       (Pp_tag constr.reference (Pp_string tag_of_pairK)))))
    (str "Expected prenex implicits for tag_of_pairK")))))
(Answer 27
 (CoqExn
  ((loc
    (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
      (bol_pos_last 0) (bp 0) (ep 30))))
   (stm_ids ((13 14))) (backtrace (Backtrace ()))
   (exn
    (CErrors.UserError
     (ssreflect "Expected prenex implicits for tag_of_pairK")))
   (pp
    (Pp_glue
     ((Pp_glue ()) (Pp_string "Expected prenex implicits for ")
      (Pp_tag constr.reference (Pp_string tag_of_pairK)))))
   (str "Expected prenex implicits for tag_of_pairK"))))
(Answer 27 Completed)

view this post on Zulip Gaëtan Gilbert (Feb 19 2023 at 22:07):

if you About tag_of_pairK after the section end, what do you get?
my hypothesis is that the correct behaviour does have the T argument and the incorrect behaviour adds it
if it's added it will be nonimplicit and followed by implicit T1 T2 and so Prenex Implicits correctly complains

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:09):

Well indeed that doesn't seem to work for me with coqc either

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:10):

@Alex Loiko are you sure you are testing properly?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:10):

tag_of_pairK has not implicits, so the Prenex Implictics can hardly work.

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:12):

Gaëtan Gilbert said:

if you About tag_of_pairK after the section end, what do you get?
my hypothesis is that the correct behaviour does have the T argument and the incorrect behaviour adds it
if it's added it will be nonimplicit and followed by implicit T1 T2 and so Prenex Implicits correctly complains

The SerAPI output is long and a bit unreadable

Add () "About tag_of_pairK.")
(Answer 31 Ack)
(Answer 31
 (Added 16
  ((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
   (bol_pos_last 0) (bp 0) (ep 19))
  NewTip))
(Answer 31 Completed)
(Exec 16)
(Answer 32 Ack)
(Feedback
 ((doc_id 0) (span_id 16) (route 0) (contents (ProcessingIn master))))
(Feedback ((doc_id 0) (span_id 13) (route 0) (contents Processed)))
(Feedback
 ((doc_id 0) (span_id 16) (route 0)
  (contents
   (Message (level Notice) (loc ())
    (pp
     (Pp_box (Pp_vbox 0)
      (Pp_glue
       ((Pp_box (Pp_hovbox 0)
         (Pp_glue
          ((Pp_string "tag_of_pairK :") (Pp_print_break 1 0)
           (Pp_box (Pp_hovbox 0)
            (Pp_glue
             ((Pp_tag constr.type (Pp_string Type))
              (Pp_tag constr.notation (Pp_string " ->")) (Pp_print_break 1 0)
              (Pp_box (Pp_hovbox 0)
               (Pp_glue
                ((Pp_box (Pp_hovbox 2)
                  (Pp_glue
                   ((Pp_tag constr.keyword (Pp_string forall))
                    (Pp_print_break 1 0)
                    (Pp_box (Pp_hovbox 1)
                     (Pp_glue
                      ((Pp_string T1) (Pp_print_break 1 0)
                       (Pp_string "T2 : ")
                       (Pp_tag constr.type (Pp_string Type))))))))
                 (Pp_string ,) (Pp_print_break 1 0)
                 (Pp_box (Pp_hovbox 2)
                  (Pp_glue
                   ((Pp_tag constr.variable (Pp_string cancel))
                    (Pp_print_break 1 0)
                    (Pp_box (Pp_hovbox 1)
                     (Pp_glue
                      ((Pp_string "(")
                       (Pp_box (Pp_hovbox 2)
                        (Pp_glue
                         ((Pp_tag constr.variable (Pp_string tag_of_pair))
                          (Pp_print_break 1 0) (Pp_string "(T2:=")
                          (Pp_tag constr.variable (Pp_string T2))
                          (Pp_string ")"))))
                       (Pp_string ")"))))
                    (Pp_print_break 1 0)
                    (Pp_box (Pp_hovbox 1)
                     (Pp_glue
                      ((Pp_string "(")
                       (Pp_box (Pp_hovbox 2)
                        (Pp_glue
                         ((Pp_tag constr.variable (Pp_string pair_of_tag))
                          (Pp_print_break 1 0) (Pp_string "(T2:=")
                          (Pp_tag constr.variable (Pp_string T2))
                          (Pp_string ")"))))
                       (Pp_string ")"))))))))))))))))
        (Pp_print_break 0 0) (Pp_print_break 0 0)
        (Pp_string "tag_of_pairK is not universe polymorphic")
        (Pp_print_break 0 0)
        (Pp_box (Pp_hovbox 2)
         (Pp_glue
          ((Pp_string Arguments) (Pp_print_break 1 0)
           (Pp_tag constr.reference (Pp_string tag_of_pairK))
           (Pp_print_break 1 0) (Pp_string _%type_scope) (Pp_print_break 1 0)
           (Pp_string [T1) (Pp_print_break 1 0) (Pp_string T2]%type_scope))))
        (Pp_print_break 0 0)
        (Pp_box (Pp_hovbox 0)
         (Pp_glue
          ((Pp_string "Expands to: Constant") (Pp_print_break 1 0)
           (Pp_string SerTop.choice.tag_of_pairK))))))))
    (str
      "tag_of_pairK :\
     \nType ->\
     \nforall T1 T2 : Type, cancel (tag_of_pair (T2:=T2)) (pair_of_tag (T2:=T2))\
     \n\
     \ntag_of_pairK is not universe polymorphic\
     \nArguments tag_of_pairK _%type_scope [T1 T2]%type_scope\
     \nExpands to: Constant SerTop.choice.tag_of_pairK")))))
(Feedback ((doc_id 0) (span_id 16) (route 0) (contents Processed)))
(Answer 32 Completed)

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:13):

Emilio Jesús Gallego Arias said:

Alex Loiko are you sure you are testing properly?

I'm not at all sure at what I am doing. My example comes from choice.v https://github.com/math-comp/math-comp/blob/2e593391f3ae5019135eeb9a73f866231d1edad3/mathcomp/ssreflect/choice.v#L145 which I have scaled down to the minimum that reproduces the error.

view this post on Zulip Gaëtan Gilbert (Feb 19 2023 at 22:13):

      "tag_of_pairK :\
     \nType ->\
     \nforall T1 T2 : Type, cancel (tag_of_pair (T2:=T2)) (pair_of_tag (T2:=T2))\

I think that Type -> is the problem

@Emilio Jesús Gallego Arias lack of implicits should produce expected some implicits not expected prenex implicits lookng at the code

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:15):

Yes in this case it is the section parameter

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:17):

But my point is that 8.16 coqc can't check this:

Module choice.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section OtherEncodings.
  Variables T T1 T2 : Type.
  Definition tag_of_pair (p : T1 * T2) := @Tagged T1 p.1 (fun _ => T2) p.2.
  Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).
  Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag.
  Admitted.
End OtherEncodings.
Prenex Implicits tag_of_pairK.

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:17):

image.png Sorry I did not know what I was doing. I get the same error in PG. I do get that error in the ML system though, and I thought I had something that compiles in coq and fails with SerAPI.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:18):

Aha

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:18):

Nope, I'm afraid that snippet is not legal Coq code

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:19):

Systems that can continue checking such as coq-lsp won't care (they will just skip this command), but otherwise yes, you are stuck

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:21):

Can you see at a glance why the math-comp code is valid? https://github.com/math-comp/math-comp/blob/2e593391f3ae5019135eeb9a73f866231d1edad3/mathcomp/ssreflect/choice.v#L124-L145

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:23):

yes, it is valid because that is its type at the Prenex Implicit time:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:23):

tag_of_pairK :
forall [T1 T2 : Type], cancel (tag_of_pair (T2:=T2)) (pair_of_tag (T2:=T2))

tag_of_pairK is not universe polymorphic
Arguments tag_of_pairK [T1 T2]%type_scope x
tag_of_pairK is opaque
Expands to: Constant b.tag_of_pairK

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:25):

You have removed the proof from tag_of_pariK

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:25):

Emilio Jesús Gallego Arias said:

yes, it is valid because that is its type at the Prenex Implicit time:

Huh, when I replace the proofs with 'Admitted', the Prenex line fails, but when I leave them in it passes. Does that mean the type of tag_of_pairK depend on the proofs? Does coq check that the proof term doesn't reference T or something?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:25):

so the section mechanism fails to properly recreate the type outside of the section

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:25):

Yes, exactly @Alex Loiko , you found the problem.

view this post on Zulip Alex Loiko (Feb 19 2023 at 22:26):

Thanks @Emilio Jesús Gallego Arias and @Gaëtan Gilbert !

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:26):

This would fix your example:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:26):

  Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag.
  Proof using T1 T2.
  Admitted.
End OtherEncodings.

Prenex Implicits tag_of_pairK.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:26):

but that kind of annotation doesn't scale

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2023 at 22:26):

Proof using will tell Coq what variables the proof is allowed to use

view this post on Zulip Notification Bot (Feb 19 2023 at 22:32):

Alex Loiko has marked this topic as resolved.

Last updated: Jun 10 2023 at 23:01 UTC