A basic question about calc without tactics

Stream: new members

[Eduardo Ochs]

Hi all... I was this person here - https://anggtwu.net/eev-lean4.html - but I stopped using Lean in setptember... I reinstalled Lean yesterday, and I saw that many things have changed, and some of the "#check"s and "#eval"s in my programs now yield errors. I am especially confused by the errors in the program below here, that I thought that would be too basic to fail. Has calc changed? How come that the first "#check" recognizes h1 but the "a = b := h1" in the first calc yields the error "Unknown identifier h1"? Where can I read about these changes? Sorry for having become a beginner again, and thanks in advance... =(

[Eduardo Ochs]

variable (h1 : a = b)
variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

#check                (h1 : a = b)
#check                (h2 : b = c + 1)
#check    (Eq.trans h1 h2 : a = c + 1)
#check                (h3 : c = d)
#check (congrArg (·+1) h3 : c + 1 = d + 1)
#check                (h4 : e = 1 + d)
#check        (Eq.symm h4 : 1 + d = e)

theorem T1 :
  a = e     := calc
  a = b     := h1
  _ = c + 1 := h2
  _ = d + 1 := congrArg Nat.succ h3
  _ = 1 + d := Nat.add_comm d 1
  _ = e     := Eq.symm h4

theorem T2 :
  a = e     := calc
  a = b     := by rw [h1]
  _ = c + 1 := by rw [h2]
  _ = d + 1 := by rw [h3]
  _ = 1 + d := by rw [Nat.add_comm]
  _ = e     := by rw [h4]

theorem T3 :
  a = e     := calc
  a = d + 1 := by rw [h1, h2, h3]
  _ = 1 + d := by rw [Nat.add_comm]
  _ = e     := by rw [h4]

theorem T4 : a = e :=
  by rw [h1, h2, h3, Nat.add_comm, h4]

theorem T5 : a = e :=
  by simp [h1, h2, h3, Nat.add_comm, h4]

[Eduardo Ochs]

sshot.png

[Yaël Dillies]

The variable inclusion behaviour has changed to be closer to what we had in Lean 3. You can now do

include h1 h2 h3 h4 in
theorem ...

to get your code working again

[Eduardo Ochs]

Aha! Thanks! =)