## 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!

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.

#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,

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: May 14 2021 at 06:16 UTC