Zulip Chat Archive

Stream: new members

Topic: Fresh variables causing trouble

view this post on Zulip Jack Crawford (Oct 24 2018 at 04:32):

I'm in a bit of a pickle right now trying to deal with one of those messy __mlocal__fresh__1234_56789 variables.

I have the following relevant lines in my tactic state:
M N __mlocal__fresh_9046_21051 : matrix (fin m) (fin n) α, r₁ : row_equivalent M __mlocal__fresh_9046_21051, r₂ : row_equivalent_step __mlocal__fresh_9046_21051 N, H₁ : row_equivalent.apply r₁ = __mlocal__fresh_9046_21051 ⊢ elementary.apply (r₂.elem) (row_equivalent.apply r₁) = N
Tantalisingly, I would love to perform some sort of rewrite or subst or simp with H₁ to rewrite the goal as ⊢ elementary.apply (r₂.elem) __mlocal__fresh_9046_21051 = N, but each of these fail.
I think I could probably perform the rewrite (just via eq.trans) if I could have myself something of the form
have H₂ : elementary.apply (r₂.elem) (row_equivalent.apply r₁) = elementary.apply (r₂.elem) __mlocal__fresh_9046_21051 (and solve this with something like congr, from H₁), but unfortunately I cannot do this as I cannot explicitly write down the __mlocal__fresh_9046_21051 (of course, the numbers change every time Lean recompiles).

Is there a way I can explicitly name my fresh variable in a less transient way?
Or am I doing something else completely stupid and in bad practice and shouldn't even have this fresh variable popping up at all?

Here's the actual code that's giving me this tactic state (you can see the fresh variable comes out of my induction over row_equivalent, which has two constructors, of the form nil : Π M, row_equivalent M M and cons : Π (r₁ : row_equivalent M N) (r₂ : row_equivalent_step N L) , row_equivalent M L)

@[simp] lemma row_equivalent.apply_implements : Π {M N : matrix (fin m) (fin n) α} (r : row_equivalent M N), r.apply = N | M N (row_equivalent.nil) := by simp[row_equivalent.apply] | M N (row_equivalent.cons r₁ r₂) := begin simp[row_equivalent.apply], have H₁, from row_equivalent.apply_implements r₁, -- Here is where I see the tactic state I provided above sorry, end

view this post on Zulip Mario Carneiro (Oct 24 2018 at 05:42):

You should use | _ _ (@row_equivalent.cons M N L r₁ r₂) in the pattern match

view this post on Zulip Jack Crawford (Oct 24 2018 at 08:24):

Ah yes, I don't know why I didn't think of this myself -- silly question!
Thanks @Mario!

Last updated: May 16 2021 at 05:21 UTC