Zulip Chat Archive

Stream: new members

Topic: no goals


view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 19:43):

I have completed a proof, and at the end of the proof, I get this error :

tactic failed, result contains meta-variables
state:
no goals

Any help is appreciated, thank you!

view this post on Zulip Patrick Massot (Jul 09 2020 at 19:44):

recover maybe?

view this post on Zulip Brandon Brown (Jul 09 2020 at 20:09):

Did you put too many commas? I think that happened to me once

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 20:16):

I tried recover, apparently there was an unsolved goal (I went through the proof, couldn't trace where). I solved the goal, and now it gives me a very big error on the line of the statement of the lemma. The error is:

type mismatch at application
  val_inv (π ^ Inf {n :  |  (x : (val_ring K)) (H : x  S), n = v x})
(blah blah)
has type
  π_1 ^ Inf {n :  |  (x : (val_ring K)) (H : x  S_1), n = v x}  0
but is expected to have type
  π ^ Inf {n :  |  (x : (val_ring K)) (H : x  S), n = v x}  0
types contain aliased name(s): S π
remark: the tactic `dedup` can be used to rename aliases

This error was not there previously.

view this post on Zulip Patrick Massot (Jul 09 2020 at 20:20):

Having duplicate names in the local context is a very sure road to confusion.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 20:23):

I have not created any duplicates, π is a variable, and S is chosen by Lean.

view this post on Zulip Kenny Lau (Jul 09 2020 at 20:25):

#mwe

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 20:26):

https://github.com/laughinggas/DVR/blob/c163ab375a57ec17b53c1a82a2e9a6c0c35d9670/src/Test.lean#L799

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 20:26):

(Unfortunately this is not minimal, but it is working..)

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:33):

if I copy and paste that file I get an error on line 260 : unknown identifier 'add_nonneg''

view this post on Zulip Patrick Massot (Jul 09 2020 at 20:35):

You should probably rather leanproject get laughinggas/DVR

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 20:36):

yeah I get the same horrible error

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:52):

It seems like assoc_rw is the cause

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 20:52):

Chris has just got it compiling :D

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:52):

if you change the assoc_rw add_comm and line after that to:

        rw add_left_comm,
        rw val_inv _ nz,

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:52):

it works

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 20:54):

assoc_rw somehow managed to create the nz goal in some metavariably way?

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:54):

well val_inv should have created the nz goal

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:55):

but assoc_rw hid it somewhere

view this post on Zulip Alex J. Best (Jul 09 2020 at 20:57):

Too quick :wink:. I don't know how Bhavik got there, but the way I debug things like this is by sorrying out big chunks of the proof, (by changing a block { blah blah } to sorry;{ blah blah} this is easy to do / undo) doing this until you see where the error changes from the weird error message to just is_pir uses sorry you can find the section and then line of the proof where this problem occurs.

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:57):

@Alex J. Best Yup essentially the same, except on a call with kevin and chris who did most of the steps :)

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 20:58):

rofl I hadn't realised you were listening to us Bhavik :D

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 20:58):

I was also replying in the chat :)

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 20:59):

@Alex J. Best I got there by going down the huge proof and every time a new { appeared I would put a line of the form sorry, sorry}, sorry}, sorry end #exit

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 21:00):

and I just kept bisecting until I located the line where the weird metavariable goal appeared

view this post on Zulip Alex J. Best (Jul 09 2020 at 21:00):

Ah I see, somehow I always work backwards from the end sorrying out more and more for some reason, but yeah essentially the same bisection thing.

view this post on Zulip Alex J. Best (Jul 09 2020 at 21:14):

I made #3349 for this now.


Last updated: May 14 2021 at 06:16 UTC