can you help me make it clear

Stream: general

[Truong Nguyen]

I read the book about lean prover. There is some code like this:

def nat.dvd (m n: ℕ ): Prop := ∃ k, n = m * k
instance : has_dvd nat := ⟨nat.dvd ⟩
theorem nat.dvd_refl (n: ℕ ) : n ∣ n := ⟨1, by simp ⟩

I don't know why this theorem can be proved by <1, simp>. What does number 1 mean?
Thank you for making it clear,

[Johan Commelin]

You see the k on the first line?

[Johan Commelin]

To prove n | n, you have to provide a k. And this proof provides 1.

[Johan Commelin]

Afterwards, you have to prove n = m * k. And in your theorem m is n, and you just provided k is 1.

[Johan Commelin]

The proof is then by simp.

[Truong Nguyen]

Ok, thanks. I see it is trivial now.

[Truong Nguyen]

By the way, is there any other way. I mean how can we write the code clearer.

[Johan Commelin]

Yes. This is called tactic mode.

[Johan Commelin]

def nat.dvd (m n: ℕ ): Prop := ∃ k, n = m * k
instance : has_dvd nat := ⟨nat.dvd ⟩
theorem nat.dvd_refl (n: ℕ ) : n ∣ n :=
begin
  existsi 1,
  simp
end

[Truong Nguyen]

Oh, ok. How can we unfold the definition of "|", to make it appear like:

\exists k, n = m * k

[Truong Nguyen]

I mean, to make it look like this:

example (n: ℕ ): ∃ k, n = n * k := _

[Reid Barton]

Do you mean you want to change what the goal looks like, inside the tactic block?

[Truong Nguyen]

Oh, yes

[Reid Barton]

Two ways. One is that you can use change to change the goal to something definitionally equivalent, like

  change ∃ k, n = n * k,

Of course, that depends on knowing what the unfolded form should be

[Truong Nguyen]

WHat is the second way

[Reid Barton]

The other way is to use unfold or dsimp or related tactics to unfold the ∣ operation, but because it is notation in this case, you need to know the actual name of the operator, which is has_dvd.dvd

[Reid Barton]

Then has_dvd is a class, so you also need to unfold the actual instance for nat. If you start with

  unfold has_dvd.dvd,

then you'll see what the actual operation is in the goal window -- it's nat.dvd

[Truong Nguyen]

I tried this:

theorem nat.dvd_refl (n: ℕ ) : n ∣ n :=
begin
unfold nat.dvd,
end

But, I got error

[Reid Barton]

So then you can unfold both at once with

  unfold has_dvd.dvd nat.dvd,

[Reid Barton]

Yep, because you have to unfold has_dvd.dvd first.
If you write set_option pp.notation false before your theorem, you can see what the notation really represents.

[Truong Nguyen]

Oh, I made it works now.
It run fine

theorem nat.dvd_refl (n: ℕ ) : n ∣ n :=
begin
unfold has_dvd.dvd nat.dvd,
end

[Mario Carneiro]

you can write dsimp [(∣)] too