basic handling of `def`

Stream: new members

[Moritz Firsching]

When I use def, I wonder how to replace the LHS by the RHS of the definition in a proposition. Consider this toy example:

def a := 17

lemma test: ∃ n : ℕ, n * n + 1 = a :=
begin
  use 4,
  refl,
end

Let's say instead in a more complicated proof I want to for some reason replace an occurance of a with 17. I can trivially do that like this:

def a := 17

lemma a_eq_17: a = 17 := by refl

lemma test: ∃ n : ℕ, n * n + 1 = a :=
begin
  rw [a_eq_17],
  ...
end

by just proving a lemma and then using a rewrite, but I'm pretty sure that is not how it should be done.
How should this be done?

[Patrick Massot]

unfold a

[Patrick Massot]

or dsimp [a]

[Moritz Firsching]

perfect, thanks!

[Moritz Firsching]

What about doing it in the reverse way, i.e. replace 17 by a?

def a := 17

lemma a_eq_17: a = 17 := by refl

lemma test: ∃ n : ℕ, n * n + 1 = 17 :=
begin
  rw ←a_eq_17,
  ...
end

[Johan Commelin]

tactic#generalize

[Johan Commelin]

Hmm, maybe that's not what you want...

[Johan Commelin]

What you did in the example, is called "equation lemma", and it's a useful technique.

[Johan Commelin]

But you can also use show \ex n, n * n + 1 = a.

[Moritz Firsching]

Ok, I see. So it seems to be much easier to substitute in one direction than in the other..

[Patrick Massot]

Of course it is. You could have also def b := 17 and def c := 17 in the same file, so how could Lean know what you want 17 to be replaced by, if you don't tell it?

[Moritz Firsching]

Of course I didn't expect that it should be replaced without explicitly saying which definition should be reversely substituted. I guess I was expecting something like dsimp [←a]or ununfold a to exist.