Use of id function

Stream: new members

[Ayush Agrawal]

Is there some interesting use of id function used in most of the proof terms? Some below examples that I ran suggest that we are using id function where we might do away with it. Can anybody help in this regard?
#check λ (a b : ℤ) (h : a ≠ b), id (λ (hab : a - b = 0), h (int.eq_of_sub_eq_zero hab)) --∀ (a b : ℤ), a ≠ b → a - b = 0 → false
#check λ (a b : ℤ) (h : a ≠ b), λ (hab : a - b = 0), h (int.eq_of_sub_eq_zero hab) --∀ (a b : ℤ), a ≠ b → a - b = 0 → false

#check λ x, x + 1 --ℕ -> ℕ
#check λ x, id (x + 1) --ℕ -> ℕ

[Yaël Dillies]

This has to do with the typechecking algorithm. Remove them and suddenly your proof might not typecheck. I'll leave someone more knowledgeable than me explain deeper.

[Eric Wieser]

Here's an example of where id makes a difference:

abbreviation mynat := ℕ

def one : ℕ := 1

#check (one : mynat)         -- one : ℕ
#check (id one : mynat)      -- one : mynat
#check (@id mynat one)       -- one : mynat
#check (@id nat one : mynat) -- one : ℕ

[Eric Wieser]

The secret is that id one there is really @id mynat one, which means that mynat actually appears in the expression. (_ : mynat) is only a hint to the elaborator, it doesn't end up in the resulting expression.

[Ayush Agrawal]

thanks @Eric Wieser and @Yaël Dillies for the interesting points.