Zulip Chat Archive

Stream: new members

Topic: no goals

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!

Patrick Massot (Jul 09 2020 at 19:44):

recover maybe?

Brandon Brown (Jul 09 2020 at 20:09):

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

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.

Patrick Massot (Jul 09 2020 at 20:20):

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

Ashvni Narayanan (Jul 09 2020 at 20:23):

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

Kenny Lau (Jul 09 2020 at 20:25):

#mwe

Ashvni Narayanan (Jul 09 2020 at 20:26):

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

Ashvni Narayanan (Jul 09 2020 at 20:26):

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

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''

Patrick Massot (Jul 09 2020 at 20:35):

You should probably rather leanproject get laughinggas/DVR

Kevin Buzzard (Jul 09 2020 at 20:36):

yeah I get the same horrible error

Bhavik Mehta (Jul 09 2020 at 20:52):

It seems like assoc_rw is the cause

Kevin Buzzard (Jul 09 2020 at 20:52):

Chris has just got it compiling :D

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,

Bhavik Mehta (Jul 09 2020 at 20:52):

it works

Kevin Buzzard (Jul 09 2020 at 20:54):

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

Bhavik Mehta (Jul 09 2020 at 20:54):

well val_inv should have created the nz goal

Bhavik Mehta (Jul 09 2020 at 20:55):

but assoc_rw hid it somewhere

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.

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 :)

Kevin Buzzard (Jul 09 2020 at 20:58):

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

Bhavik Mehta (Jul 09 2020 at 20:58):

I was also replying in the chat :)

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

Kevin Buzzard (Jul 09 2020 at 21:00):

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

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.

Alex J. Best (Jul 09 2020 at 21:14):

I made #3349 for this now.

Last updated: Dec 20 2023 at 11:08 UTC