폐기됨: 택틱과 정리 증명
폐기됨: 택틱과 정리 증명 (DEPRECATED: Tactics and Theorem Proving)
경고: 여기에 문서화된 대화형 정리 증명 인터페이스는 정교화기 반영 소개(Elaborator Reflection Introduction)를 위해 폐기(deprecated)되었어요.
Idris는 대화형 정리 증명과, hole을 통한 컨텍스트 분석을 지원해요. 증명되지 않은 모든 hole을 나열하려면 :m 명령을 사용해요. 그러면 그것들의 경상 이름(qualified names)과 예상 타입이 표시돼요. hole을 대화형으로 증명하려면 :p name 명령을 사용하는데, 여기서 name은 hole이에요. 증명이 완료되면 :a 명령이 현재 모듈에 그것을 추가해요.
일단 대화형 증명기(prover)에 들어가면 다음 명령들이 사용 가능해요:
출처: 문서
본문
기본 명령 (Basic commands)
:q— 증명기를 종료해요 (현재 보조정리 증명을 포기해요).:abandon—:q와 같아요.:state— 증명의 현재 상태를 표시해요.:term— 아직 채워지지 않은 hole들과 함께 현재 증명 용어를 표시해요 (주로 디버깅에만 유용해요).:undo— 마지막 택틱을 되돌려요.:qed— 대화형 정리 증명기가 "No more goals"라고 말하면, 축하하며 이걸 입력할 수 있어요! (증명을 완료하고 증명기를 종료해요)
흔히 사용되는 택틱 (Commonly Used Tactics)
Compute
compute— 목표의 모든 용어를 정규화해요 (주의: 가정(assumptions)은 정규화하지 않아요).
---------- Goal: ----------
(Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma> compute
---------- Goal: ----------
(Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma>
Exact
exact— 목표 타입의 용어를 직접 제공해요.
---------- Goal: ----------
Nat
-lemma> exact Z
lemma: No more goals.
-lemma>
Refine
refine— 이름을 사용해 목표를 정제(refine)해요. 이름이 인자를 필요로 하면, 그것들을 새 목표로 도입해요.
Trivial
trivial— 타입과 일치하는 가정을 사용해 목표를 만족시켜요.
---------- Assumptions: ----------
value : Nat
---------- Goal: ----------
Nat
-lemma> trivial
lemma: No more goals.
-lemma>
Intro
intro— 목표가 화살표(arrow)이면, 왼쪽 용어를 가정으로 바꿔요.
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intro
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
Nat -> Nat
-lemma>
가정을 위한 자신만의 이름을 제공할 수도 있어요:
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intro number
---------- Assumptions: ----------
number : Nat
---------- Goal: ----------
Nat -> Nat
Intros
intros— 정확히intro와 같지만, 모든 왼쪽 용어에 한 번에 작동해요.
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intros
---------- Assumptions: ----------
n : Nat
m : Nat
---------- Goal: ----------
Nat
-lemma>
let
let— 새로운 가정을 도입해요; 새 것을 정의하기 위해 현재 가정들을 사용할 수 있어요.
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
BigInt
-lemma> let x = toIntegerNat n
---------- Assumptions: ----------
n : Nat
x = toIntegerNat n: BigInt
---------- Goal: ----------
BigInt
-lemma>
rewrite
rewrite— 동등 타입(x = y)을 가진 표현식을 받아, 목표에서x의 모든 인스턴스를y로 바꿔요. 종종sym과 결합해 유용해요.
---------- Assumptions: ----------
n : Nat
a : Type
value : Vect Z a
---------- Goal: ----------
Vect (mult n Z) a
-lemma> rewrite sym (multZeroRightZero n)
---------- Assumptions: ----------
n : Nat
a : Type
value : Vect Z a
---------- Goal: ----------
Vect Z a
-lemma>
sourceLocation
sourceLocation— 택틱이 호출된 소스 코드의 위치에 대한 정보로 현재 목표를 해결해요. 이것은 주로 임베디드 DSL과, 호출된 위치를 알아야 하는 assert 같은 프로그래머 도구를 위한 것이에요. 자세한 내용은Language.Reflection.SourceLocation을 참조하세요.
덜 흔하게 사용되는 택틱 (Less commonly-used tactics)
applyTactic— 사용자 정의 택틱을 적용해요. 이것은 타입List (TTName, Binder TT) -> TT -> Tactic의 함수여야 하는데, 첫 번째 인자는 증명 컨텍스트를, 두 번째는 목표를 나타내요. 택틱이 증명 용어를 직접 생성할 것이라면Tactic의Exact생성자를 사용해요.attack— ?equiv— 목표를 이전 목표와 변환 가능(convertible)한 새 목표로 바꿔요.fill— ?focus— ?mrefine— 타입에 대한 매칭으로 정제해요.reflect— ?solve— 올바른 타입으로 추측을 하고 그것으로 hole을 채워, 증명 의무를 닫아요. 이것은 대화형 증명기에서 자동으로 일어나므로,solve는 묵시적 인자 해석을 돕기 위해 사용되는 택틱 스크립트에서만 실제로 관련 있어요.try— ?