Stream: jsCoq

Topic: Funky evars?

Shachar Itzhaky (Jun 21 2021 at 19:15):

Eh, funny thing happened: I'm in a proof, right? And then I find myself, like, "wonder what's the type of fst". So I go Check fst. and then:

fst
     : ?A * ?B -> ?A
where
?A : [ST : state_typing st : state st' : state t : com
t' : com c : com s : state
H2 : state_only_values (snd (c, s))
H3 : ST ||- fst (c, s) c0 : com s0 : state
z : com * state Hstep : c / s --> c0 / s0
H4 : multi cstep (c0, s0) z
IHmulti : has_state_type (snd (c0, s0)) ST ->
state_only_values (snd (c0, s0)) ->
ST ||- fst (c0, s0) -> ~ cstuck t' st'
H1 : has_state_type s0 ST /\ (ST ||- c0) \/
(exists (i : string) (T : ty),
  ((i |-> T; ST) ||- c0) /\
  has_state_type s0 (i |-> T; ST) /\ ST i = None)
|- Type]
?B : [ST : state_typing st : state st' : state t : com
  t' : com c : com s : state
  H2 : state_only_values (snd (c, s))
  H3 : ST ||- fst (c, s) c0 : com s0 : state
  z : com * state Hstep : c / s --> c0 / s0
  H4 : multi cstep (c0, s0) z
  IHmulti : has_state_type (snd (c0, s0)) ST ->
  state_only_values (snd (c0, s0)) ->
  ST ||- fst (c0, s0) -> ~ cstuck t' st'
  H1 : has_state_type s0 ST /\ (ST ||- c0) \/
  (exists (i : string) (T : ty),
    ((i |-> T; ST) ||- c0) /\
    has_state_type s0 (i |-> T; ST) /\ ST i = None)
  |- Type]

This is waCoq 0.13.0. Have to try in native Coq (need to rebuild everything in LF+PLF for that, too lazy right now and it's late), but any idea what in the duke's name is going on here?

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:25):

Oh!

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:26):

I guess the issue is that check is creating some evars to type fst ?A ?B , however it is using the current proof context, which makes the evars context to be the one of your proof

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:27):

You could weaken them of course, or we could have Check use a different context, such as the empty one

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:27):

recall that HOL theorem provers , metavariables require to capture a context

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:28):

[as to ensure certain "freshness" conditions]

Emilio Jesús Gallego Arias (Jun 21 2021 at 19:29):

But to know what is the type of fst, you should use about, Check does something very different as you have witnessed [involving indeed the elaboration engine]

Shachar Itzhaky (Jun 21 2021 at 20:08):

oh so now Check prints the contexts of all the evars?
But it's so weird because fst is defined outside the proof, so how is my proof context in the context of ?A and ?B...

Shachar Itzhaky (Jun 21 2021 at 20:09):

But yeah I should probably change the tooltip to use About instead... had no idea

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:15):

No idea when that change happened, I think there is a printing flag you can set in init

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:15):

to avoid printing that

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:15):

but indeed for Check, you need to create the evars in the right context

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:16):

otherwise you would have problems checking proof sub-expressions

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:16):

as the evars there need the right context, so indeed that is correct behavior on the part of Check

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:16):

Check will call the type-checking engine so it is more adecuate when you need to do stuff such as Check (foo H) inside the proof

Emilio Jesús Gallego Arias (Jun 21 2021 at 21:17):

but since I already have have := foo H in math-comp, I never use check, the tactic is superior in many accounts

Pierre Courtieu (Jul 06 2021 at 14:17):

Hint: I think About is the recommended to query about identifiers. Check is for terms and may take an arbitrary time to answer due to type class resolution for instance.

Shachar Itzhaky (Jul 07 2021 at 15:26):

I have changed our contextual info UI to use About instead of Check. There are several things which we may want to filter out in the future (succ_inj_wd is not universe polymorphic etc.).
Also there's another issue: with About, if the symbol is not loaded, I do not get an error. Instead I get an info message succ_inj_wd is not defined.

Shachar Itzhaky (Jul 07 2021 at 15:26):

It was more convenient with the error status because then I could provide some more useful feedback.

Emilio Jesús Gallego Arias (Jul 07 2021 at 16:11):

About is actually quite fragile too, we should implement IMHO our own about call, similarly to what we do with goals

Shachar Itzhaky (Jul 07 2021 at 16:33):

Oh ok, I guess this can be done.

Last updated: Oct 12 2024 at 12:01 UTC