Сравнение привязок have и let в Lean4

Вот как работает have

Внутренне have h : p := s; t превращается в терм (fun (h : p) => t) s. Иначе говоря, s доказывает p, а t доказывает нужное заключение при допущении h : p, после чего лямбда-абстракция и применение объединяют их.

Вот как работает let

Конструкция let предоставляет более мощное сокращение, поэтому некоторые выражения let a := t1; t2 нельзя представить в виде (fun a => t2) t1. Для упражнения разберитесь, почему определение keepType ниже проходит проверку типов, а loseType не проходит.

def keepType := let chosen := Nat; fun item : chosen => item + 4
/-
  def loseType := (fun chosen => fun item : chosen => item + 4) Nat
-/

Разница в том, что let сохраняет определение, а have его отбрасывает.

Например, в Lean 4 этот пример работает с let, но замена на have приводит к ошибке.

example : {item : Nat // item = 0} := let item := 0 ; ⟨item, rfl⟩

Обычно для доказательств используют have, а для всего остального let. В режиме тактик Lean3 с помощью dsimp [x] можно раскрыть определение let x := ..., но соответствующего способа для Lean4 я не знаю.

Рассмотрим пример с более практическим применением:

def divisibleByTwo (number : Nat) : Prop :=
  ∃ factor : Nat, number = factor * 2

theorem doubled_half (number : Nat) : divisibleByTwo (number / 2 * 2) :=
  let half := number / 2
  have : number / 2 * 2 = half * 2 := rfl
  Exists.intro half this

theorem doubled_failure (number : Nat) : divisibleByTwo (number / 2 * 2) :=
  have half := number / 2
  have : number / 2 * 2 = half * 2 := rfl -- error: type mismatch
  Exists.intro half this

Первое доказательство работает, а второе завершается ошибкой на выражении rfl. Причина в том, что let подставляет определение number / 2 вместо всех последующих вхождений half. После have компилятор, напротив, сохраняет только то, что half имеет тип Nat, и отбрасывает определение, поэтому rfl не может отождествить number / 2 * 2 с произвольным half / 2.

Поэтому промежуточные утверждения или леммы обычно вводят через have, ведь системе типов нужно свидетельство конкретного утверждения, а не сама процедура доказательства. Напротив, let вводит переменные, определения которых нужны в последующих частях доказательства.