Stream: jsCoq

Topic: Funky evars?


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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2021 at 19:25):

Oh!

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2021 at 19:27):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2021 at 19:28):

[as to ensure certain "freshness" conditions]

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

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

view this post on Zulip Shachar Itzhaky (Jun 21 2021 at 20:09):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2021 at 21:15):

to avoid printing that

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2021 at 21:16):

otherwise you would have problems checking proof sub-expressions

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

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

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

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

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

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

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

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 16:33):

Oh ok, I guess this can be done.


Last updated: Jan 31 2023 at 09:01 UTC