11.1. 기본 탐색 및 재작성🔗

첫 번째 예시로, (a b c : Nat) : a * (b * c) = a * (c * b)라는 예제를 증명해 봅시다(이 파일의 예제들은 다른 택틱으로도 즉시 끝낼 수 있기 때문에 다소 인위적입니다). 소박한 첫 번째 시도는 택틱 모드로 들어가서 rw [Nat.mul_comm]를 시도하는 것입니다. 하지만 이는 항(term)에 나타나는 맨 처음 곱셈을 교환한 뒤, 목표를 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 모드에서 지원되지 않는 목표를 해소하거나, 사용자 정의 합동 보조정리와 확장성 보조정리를 적용할 때 유용합니다.

  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>의 문법적 설탕(syntax sugar)입니다.

  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! 🐙