아래 두 표현식을 보니
#eval have amount : Nat := 5 ; amount*4그리고
#eval let amount : Nat := 5 ; amount*4똑같이 동작하더군요. 정리를 증명할 때도 마찬가지예요. 서로 바꿔 써도 되나요? 차이가 뭔가요?
I've observed that these two expressions
#eval have amount : Nat := 5 ; amount*4and
#eval let amount : Nat := 5 ; amount*4behave identically. This also happens in theorem proofs. Are they interchangeable? How do they differ?
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
-/Here is how have operates
Internally, have h : p := s; t becomes the term (fun (h : p) => t) s. Put differently, s proves p, while t proves the intended conclusion under the assumption h : p, and lambda abstraction followed by application joins them together.
Here is how let operates
The let construct provides more powerful abbreviation, so some expressions let a := t1; t2 have no equivalent (fun a => t2) t1. For practice, work out why the definition called keepType below passes type checking while loseType does not.
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에서 같은 일을 어떻게 하는지는 모르겠어요.
The distinction is that let retains a definition, whereas have discards it.
For instance, this example accepts let, but substituting have fails in Lean 4.
example : {item : Nat // item = 0} := let item := 0 ; ⟨item, rfl⟩Typically, proofs use have, while other things use let. Within Lean3's tactic mode, dsimp [x] lets you unfold let x := ..., but I don't know the corresponding approach in 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는 이후에 나오는 half를 모두 정의인 number / 2로 대체하기 때문입니다. 반면 have를 쓰면 컴파일러는 half의 타입이 Nat라는 것만 기억하고 정의는 버리므로, rfl는 number / 2 * 2와 임의의 half / 2를 같다고 볼 수 없습니다.
그래서 중간 명제나 보조 정리에는 보통 have를 씁니다. 타입 시스템은 특정 명제를 증명했다는 사실만 필요하고 실제 증명 절차는 필요하지 않기 때문입니다. 반면 이후 증명에서 정의가 필요한 변수를 도입할 때는 let를 씁니다.
Consider this example with a practical use:
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 thisThe initial proof works, whereas the other one fails at its rfl expression. The reason is that let substitutes the definition number / 2 for all later uses of half. After have, however, the compiler retains only that half has type Nat and discards its definition, leaving rfl unable to identify number / 2 * 2 with an arbitrary half / 2.
Consequently, we normally introduce intermediate propositions or lemmas with have, since the type system needs evidence for the particular proposition without needing the proof's actual procedure. By contrast, let introduces variables when later parts of the proof need their definitions.
안녕하세요, 제가 코드를 바꿀 수 없는 패키지에 다음과 같은 클래스 계층이 있어요: 편하게 쓰려고 Inner를 감싸는 래퍼를 추가하려는데, Inner가 바깥 인스턴스에 의존해서 지금까지는 바깥 클래스의 서브클래스 안에 넣는…
각 항목이 문자열 배열을 담는 Map을 만들고 있어요. 타입 선언과 초기화를 한 문장으로 같이 하려면 어떻게 하나요? 제 (단순한) 시도는 이랬어요: 그랬더니 이렇게 나와요:
Typescript는 함수 정의가 인터페이스 시그니처와 다른데도 받아 주면서, 왜 그 함수를 실제로 호출할 때는 문제를 보고하나요.
