11.1. 기본 탐색과 재작성🔗

첫 번째 예제로 (a b c : Nat) : a * (b * c) = a * (c * b)를 증명해 봅시다(이 파일의 예제들은 다른 택틱으로도 즉시 끝낼 수 있으므로 다소 인위적입니다). 가장 단순하게 떠올릴 수 있는 첫 시도는 택틱 모드에 진입하여 rw [Nat.mul_comm]을 시도하는 것입니다. 그러나 이렇게 하면 항에 나타나는 맨 첫 번째 곱셈의 순서가 바뀌어 목표가 b * c * a = a * (c * b)로 변환됩니다. 이 문제를 해결하는 방법은 여러 가지가 있으며, 그중 하나는 더 정밀한 도구인 변환 모드(conversion mode)를 사용하는 것입니다. 다음 코드 블록은 각 줄 뒤의 현재 목표를 보여 줍니다.

위 코드 조각은 세 가지 탐색 명령을 보여 줍니다.

• lhs는 관계(이 경우에는 상등)의 좌변으로 이동합니다. 우변으로 이동하는 rhs도 있습니다.

• congr는 현재 헤드 함수의 (비의존적이며 명시적인) 인자 개수만큼 목표를 생성합니다(여기서 헤드 함수는 곱셈입니다).

• rfl은 반사성을 이용해 목표를 닫습니다.

해당 대상에 도달하면 일반 택틱 모드에서와 마찬가지로 rw를 사용할 수 있습니다.

변환 모드를 사용하는 두 번째 주요 이유는 바인더 아래에서 다시 쓰기를 하기 위해서입니다. (fun x : Nat => 0 + x) = (fun x => x)라는 예제를 증명하려 한다고 가정해 봅시다. 가장 단순한 첫 시도는 택틱 모드에 들어가서 rw [Nat.zero_add]를 시도하는 것입니다. 하지만 이 시도는 답답하게도 다음과 같이 실패합니다

error: tactic 'rewrite' failed, did not find instance of the pattern
       in the target expression
  0 + ?n
⊢ (fun x => 0 + x) = fun x => x

해답은 다음과 같습니다:

여기서 intro x는 fun 바인더 안으로 들어가는 탐색 명령입니다. 이 예제는 다소 인위적이며, 다음과 같이 할 수도 있다는 점에 유의하십시오:

또는 간단히

conv는 conv at h를 사용하여 로컬 컨텍스트에 있는 가설 h를 재작성할 수도 있습니다.

11.2. 패턴 매칭🔗

위의 명령들을 사용해 탐색하는 것은 번거로울 수 있습니다. 다음과 같이 패턴 매칭을 사용하면 이를 간단하게 줄일 수 있습니다:

이는 다음에 대한 구문 설탕(syntax sugar)일 뿐입니다

물론 와일드카드도 사용할 수 있습니다:

11.3. 변환 택틱 구조화하기🔗

중괄호와 .는 conv 모드에서도 택틱을 구조화하는 데 사용할 수 있습니다:

11.4. 변환 모드 안의 다른 택틱🔗

• arg i는 함수 적용의 i번째 비의존 명시적 인자로 들어갑니다.

  example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b) conv =>a:Natb:Natc:Nat| a * (b * c) = a * (c * b) lhsa:Natb:Natc:Nat| a * (b * c) arg 2a:Natb:Natc:Nat| b * c rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

• args는 congr의 다른 이름입니다.

• simp는 현재 목표에 단순화기(simplifier)를 적용합니다. 일반 택틱 모드에서 사용할 수 있는 옵션을 동일하게 지원합니다.

  def f (x : Nat) := if x > 0 then x + 1 else x + 2 example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := byx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0⊢ g x = f x conv =>x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| g x = f x rhsx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| f x simp [f, h₂]x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| x + 1 exact h₁All goals completed! 🐙

• enter [1, x, 2, y]는 주어진 인수를 사용하여 arg와 intro를 반복 적용합니다.

• 해결되지 않은 목표가 있으면 done은 실패합니다.

• trace_state는 현재 택틱 상태를 표시합니다.

• whnf는 항을 약한 머리 정규형(weak head normal form)으로 변환합니다.

• tactic => <tactic sequence>는 일반 택틱 모드로 돌아갑니다. 이는 conv 모드에서 지원하지 않는 목표를 해결하거나, 사용자 정의 합동(congruence) 보조정리 및 외연성(extensionality) 보조정리를 적용할 때 유용합니다.

  example (g : Nat → Nat → Nat) (h₁ : ∀ x, x ≠ 0 → g x x = 1) (h₂ : x ≠ 0) : g x x + x = 1 + x := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . tactic =>ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 exact h₂All goals completed! 🐙

• apply <term>은 tactic => apply <term>에 대한 구문 설탕입니다.

  example (g : Nat → Nat → Nat) (h₁ : ∀ x, x ≠ 0 → g x x = 1) (h₂ : x ≠ 0) : g x x + x = 1 + x := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . apply h₂All goals completed! 🐙