연습 1.4 — 치환 결과를 직접 쓰기🔗

책 p. 23의 세 문항은 Exercises/Ch01/Ex.lean의 e14aResult, e14bResult, e14cResult에 있다. 입력 단언과 치환 사상은 주어지고, 결과 단언과 그 결과를 확인하는 증명을 함께 채운다. 앞의 치환 정리를 아직 풀지 않았어도 이 세 문항은 각각 풀 수 있다.

결과 타입 {q : Assert String // e14a /ₛ e14aSubst = q}는 두 칸짜리 묶음이다. 첫 칸은 결과 단언 q, 둘째 칸은 실제 치환 결과가 그 단언이라는 증명이다. refine ⟨⟪ … ⟫ₐ, ?_⟩로 먼저 계산한 단언을 쓰고, 남은 등식을 힌트의 정의와 이름 선택 보조정리로 확인한다. /ₛ를 그대로 첫 칸에 넣으면 계산할 구문을 다시 적은 것이므로, 이 실습에서는 양화사와 비교식으로 결과를 끝까지 써 본다.

각 양화사에서는 본문에 자유롭게 나타나는 변수만 살핀다. 그 발생에 들어올 식의 자유 변수가 결합자와 겹칠 때만 이름을 바꾼다. 치환 사상에 변수 이름이 있다고 해서 속박 발생까지 바꾸지는 않는다. 또한 동시 치환은 들어온 식에 같은 치환을 다시 적용하지 않는다.

책은 불필요한 이름 바꾸기를 금하지만 새 이름의 철자는 지정하지 않는다. 이 저장소는 안전하면 원래 이름을 유지하고, 바꿔야 할 때는 x, xx, xxx, … 중 피해야 할 집합에 없는 첫 이름을 고른다. 따라서 책에서 가능한 다른 철자의 답은 이 실습의 구문 등식과 다를 수 있다. 의미 보존은 완성 자료 e14b_meaning으로 따로 볼 수 있다.