5. 리스트 프로그램의 성질을 증명하기


리스트에 대해 계산하는 프로그램의 성질을 증명할때도 귀납적 증명을 사용할 수 있다. 귀납 인자로 리스트를 취한다. 이번에도 두 가지 목적 명제를 증명할 것이다. 처음은 비어있는 리스트의 경우이고 다음은 a::l 형태의 일반적인 리스트를 다룬다. 여기서 l은 귀납적 가정에서 사용된다.


예제 증명을 살펴보자. 앞에서 소개했던 insert와 sort 함수를 사용하는 리스트 정렬은 리스트에 나타난 원소의 수를 변경하지 않음을 증명하겠다. 리스트에 어떤 숫자가 몇번 나타나는지 그 수를 세는 함수는 다음과 같다.


Fixpoint count n l := 

   match l with

       nil => 0

    | a::tl =>

       let r := count n tl in if beq_nat n a then 1+r else r

    end.


리스트에 원소를 추가하면 이 숫자가 출현하는 빈도는 항상 증가함을 먼저 증명한다.


Lemma insert_incr : forall n l, count n (insert n l) = 1 + count n l.


intros n l; induction l.


2 subgoals

  

  n : nat

  ============================

   count n (insert n nil) = 1 + count n nil


subgoal 2 is:

 count n (insert n (a :: l)) = 1 + count n (a :: l)


simpl 전략으로 콕 시스템은 여러 함수들을 계산한다. 


simpl.


2 subgoals

  

  n : nat

  ============================

   (if beq_nat n n then 1 else 0) = 1


subgoal 2 is:

 count n (insert n (a :: l)) = 1 + count n (a :: l)


여기에서 beq_nat에 대한 정리를 찾을 필요가 있다.


SearchAbout beq_nat.

beq_nat_refl: forall n : nat, true = beq_nat n n

beq_nat_eq: forall x y : nat, true = beq_nat x y -> x = y

beq_nat_true: forall x y : nat, beq_nat x y = true -> x = y

beq_nat_false: forall x y : nat, beq_nat x y = false -> x <> y

beq_nat_true_iff: forall x y : nat, beq_nat x y = true <-> x = y

beq_nat_false_iff: forall x y : nat, beq_nat x y = false <-> x <> y

NatOrderedType.Nat_as_DT.eqb_eq:

  forall x y : nat, beq_nat x y = true <-> x = y

NatOrderedType.Nat_as_OT.eqb_eq:

  forall x y : nat, beq_nat x y = true <-> x = y

NatOrderedType.Nat_as_UBE.eqb_eq:

  forall x y : nat, beq_nat x y = true <-> x = y


이미 존재하는 beq_nat_refl 정리가 유용하다. rewrite 전술로 이 정리를 적용한다.


rewrite <- beq_nat_refl.


2 subgoals

  

  n : nat

  ============================

   1 = 1


subgoal 2 is:

 count n (insert n (a :: l)) = 1 + count n (a :: l)


현재 목적 명제의 형태는 reflexivity 전술로 쉽게 해결할 수 있다. 그 다음 목적 명제는 리스트에 대한 귀납적 증명의 귀납적인 경우이다.


reflexivity.


1 subgoal

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   count n (insert n (a :: l)) = 1 + count n (a :: l)


다시 한 번 콕 시스템에 요청해 여러 함수들을 계산한다. 


simpl. 


1 subgoal

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   count n (if leb n a then n :: a :: l else a :: insert n l) =

   S (if beq_nat n a then S (count n l) else count n l)


leb n a 식의 경우들을 먼저 각각 살펴보고, 그 다음 beq_nat n a의 경우들을 따져본다. case (leb n a) 전술을 처음 부분에 사용한다. 그 결과 두 개의 목적 명제를 만난다. 하나는 leb n a를 true로 바꾸고 다른 하나는 false로 바꾼 것이다.


case (leb n a).


2 subgoals

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   count n (n :: a :: l) =

   S (if beq_nat n a then S (count n l) else count n l)


subgoal 2 is:

 count n (a :: insert n l) =

 S (if beq_nat n a then S (count n l) else count n l)


이제 이 식을 간단하게 만들 수 있다. 그 다음 beq_nat이 다시 나타나는데 beq_nat_refl 정리를 다시 쓸 수 있다.


simpl.


2 subgoals

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   (if beq_nat n n

    then S (if beq_nat n a then S (count n l) else count n l)

    else if beq_nat n a then S (count n l) else count n l) =

   S (if beq_nat n a then S (count n l) else count n l)


subgoal 2 is:

 count n (a :: insert n l) =

 S (if beq_nat n a then S (count n l) else count n l)


rewrite <- beq_nat_refl.


2 subgoals

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   S (if beq_nat n a then S (count n l) else count n l) =

   S (if beq_nat n a then S (count n l) else count n l)


subgoal 2 is:

 count n (a :: insert n l) =

 S (if beq_nat n a then S (count n l) else count n l)


reflexivity.


1 subgoal

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   count n (a :: insert n l) =

   S (if beq_nat n a then S (count n l) else count n l)


마지막 목적 명제에서 이 식을 먼저 간단하게 변환한다.


simpl.


1 subgoal


  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   (if beq_nat n a then S (count n (insert n l)) else count n (insert n l)) =

   S (if beq_nat n a then S (count n l) else count n l)


이제 beq_nat n a의 값에 대한 경우를 나누어 따져봐야 한다. 


case (beq_nat n a).


2 subgoals

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

  ============================

   S (count n (insert n l)) = S (S (count n l))


subgoal 2 is:

 count n (insert n l) = S (count n l)


그 결과로 얻은 나머지 두 목적 명제들을 보면 가정 IHl을 가지고 다시 쓰면 등식의 양쪽이 분명하게 같아질 것이다. 다음 명령어들로 이 증명을 결론짓는다. 


rewrite IHl; reflexivity.

rewrite IHl; reflexivity.

Qed.




===

번역


(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태


(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트


(3장)

Fact: 사실 명제

Theorem: 정리

Implication : 함축

Predicate : (술어) 명제

Rewriting : 다시쓰기

Equality : 등식

Goal : 목적 명제

Tactic : 전술

Hypothesis : 가정

Universal Quantification : 전칭 한정

Transitive : 추이적

Instantiation : 사례화

Associativity : 결합성


(4장)

Proof by induction : 귀납적 증명

Existential : 존재

Lemma : 보조 정리


(5장)

the step case of the proof by induction : 귀납적 증명의 귀납적 경우


저작자 표시
신고
Posted by lazyswamp Trackback 0 : Comment 0

4. 숫자 프로그램의 성질을 증명하기


자연수에 대해 계산하는 프로그램의 성질을 증명하기위해 보통 여러 계산과정이 어떤 방식으로 연관되어 있음을 보일수 있다. 주어진 함수가 재귀방식이면 대개 귀납적 방식으로  증명한다. 이때 알아야할 전술은 다음과 같다.


  • induction 전술은 자연수 n에 대한 귀납적 증명을 한다. 증명을 두 부분으로 나누어, 우선 n이 0일때 증명하고자하는 성질이 성립함을 확인한다. 그 다음 p에 대한 성질로부터 S p에 대한 성질을 증명한다. p에 대한 가정을 귀납적 가정이라 부르고 IH로 시작하는 이름을 보통 붙인다. 이 전술은 0에 대한 목적 명제와 S p에 대한 목적 명제 두 개를 만든다. 
  • simpl 전술은 복잡한 인자를 갖는 재귀함수 호출을 해당하는 값으로 대체한다. 함수의 정의에 의해 이 값을 결정한다. 
  • discriminate 전술은 0 = S ...이나 true = false와 같이 선언하는 가정이 있을때 유용하다.
  • injection 전술은 S x = S y 모양의 가정에서 x = y를 알아내는데 도움이 된다. 


4.1 귀납적 증명

증명 예제를 살펴보자. 0부터 n개의 자연수들의 합이 잘 알려진 다항식을 이룬다는 것을 증명해보자.


Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.

induction n.


2 subgoals

  

  ============================

   2 * sum_n 0 + 0 = 0 * 0


subgoal 2 is:

 2 * sum_n (S n) + S n = S n * S n


새로 생성된 두 목적 명제에서, 첫번째 것은 n을 0으로 바꾸었고, 두번째는 n을 S n으로 바꾼것이다.  두번째 목적 명제에서 n에 대해 성립한다는 가정은 표시되어 있지 않다. 


첫번째 목적 명제는 매우 쉽다. sum_n, 덧셈, 곱셈의 정의에 의하면 등식의 양쪽이 모두 0이기 때문이다. reflexivity 전술로 해결한다. 


reflexivity.


이 전술을 쓰면 두번째 목적 명제만 남았고 콕 시스템에서 전체를 보여준다. 이제 귀납적 가정을 볼 수 있다. 


1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  ============================

   2 * sum_n (S n) + S n = S n * S n


여기에서 조금 생각할 필요가 있다. S n * S n을 n * n이 나타나는 식으로 펼칠수 있다. 그 다음 IHn으로 오른편에서 왼쪽 방향으로 다시 쓸 수 있다. assert  전술을 사용해 S n * S n과 새로운 값이 같다고 임시로 선언하고, ring 전술로 이 동등 선언이 사실 성립함을 보인다. 


assert (SnSn : S n * S n = n * n + 2 * n + 1).


2 subgoals

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  ============================

   S n * S n = n * n + 2 * n + 1


subgoal 2 is:

 2 * sum_n (S n) + S n = S n * S n


ring.


1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

  ============================

   2 * sum_n (S n) + S n = S n * S n


rewrite SnSn.


1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

  ============================

   2 * sum_n (S n) + S n = n * n + 2 * n + 1


이번에는 귀납적 가정을 이용해서 n * n을 2 * sum_n n + n으로 다시 쓴다. 


rewrite <- IHn.


1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

  ============================

   2 * sum_n (S n) + S n = 2 * sum_n n + n + 2 * n + 1


다음 단계에서 sum_n (S n)을 정의에 따라 펼쳐서 그 값을 sum_n n으로 표현해본다. simpl 전술을 사용하는데, 이것은 sum_n 뿐만 아니라 곱셈도 그 정의에 따라 펼치는 것을 시도한다.


sumpl.


1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

  ============================

   n + sum_n n + (n + sum_n n + 0) + S n =

   sum_n n + (sum_n n + 0) + n + (n + (n + 0)) + 1


그 다음 단계에서 ring 전술을 사용해서 목적 명제의 등식이 덧셈의 결합성과 교환 규칙에 의해 성립함을 보인다.


ring.

Qed.


4.2 귀납에서 더 강력한 문장

재귀 함수가 몇 단계의 패턴 매칭을 사용한다면 연속적인 여러 개의 숫자들에 대해 성질을 기술하는 문장을 증명하는 것이 낫다. evenb 함수에 대한 증명의 예로 살펴보자.


Lemma evenb_p : forall n, evenb n = true -> exists x, n = 2 * x.

assert (Main: forall n, (evenb n = true -> exists x, n = 2 * x) /\

                    (evenb (S n) = true -> exists x, S n = 2 * x)).


여기에서 원래 목적 명제보다 더 강력한 문장을 증명해본다. 즉, n 뿐만 아니라 S n에 대해서도 성립함을 증명한다. 그 다음 이전처럼 귀납 방식으로 진행한다. 더 강력한 문장을 귀납 방식으로 증명하는 것은 재귀함수 증명에서 흔히 볼 수 있다.


induction n.


3 subgoals

  

  ============================

   (evenb 0 = true -> exists x : nat, 0 = 2 * x) /\

   (evenb 1 = true -> exists x : nat, 1 = 2 * x)


subgoal 2 is:

 (evenb (S n) = true -> exists x : nat, S n = 2 * x) /\

 (evenb (S (S n)) = true -> exists x : nat, S (S n) = 2 * x)

subgoal 3 is:

 forall n : nat, evenb n = true -> exists x : nat, n = 2 * x


첫번째 목적 명제는 두 부분으로 나뉜다. 처음 부분은 결론에 나타난 존재 한정이 있는 문장이다. 전술 테이블을 보면 exists 전술로 어떤 값을 주면 된다. 이 경우 x의 값을 0으로 놓으면 0 = 2 * 0이 성립함을 쉽게 알 수 있다. 두번째 부분은 다르다. x의 값으로 놓을 수 있는 것이 없다. 하지만 evenb 1 = true는 성립하지 않는다. 왜냐하면 evenb 1은 false이고 false = true는 불가능하기 때문이다. 일관성이 없는 경우는 discriminate 전술을 사용한다.


split.

   exists 0; ring.

simpl; intros H; discriminate H.


나머지 증명에 대해 자세히 설명하지 않는다. 독자 스스로 증명해볼 것을 권한다. 


  split.

    destruct IHn as [_ IHn'].

    exact IHn'.


  simpl.

  intros H.

  destruct IHn as [IHn' _].

  assert (H' : exists x, n = 2 * x).

    apply IHn'.

    exact H.

  destruct H' as [x q].

  exists (x + 1).

  rewrite q.

  ring.


가정 Main을 일단 증명하면 원래 증명하려고 했던 명제로 돌아갈수 있다. 이때 firstorder 전술로 증명을 마무리할 수 있다. 설명을 위해 다른 방법을 보여줄 것이다.


1 subgoal

  

  Main : forall n : nat,

         (evenb n = true -> exists x : nat, n = 2 * x) /\

         (evenb (S n) = true -> exists x : nat, S n = 2 * x)

  ============================

   forall n : nat, evenb n = true -> exists x : nat, n = 2 * x


intros n ev.


1 subgoal

  

  Main : forall n : nat,

         (evenb n = true -> exists x : nat, n = 2 * x) /\

         (evenb (S n) = true -> exists x : nat, S n = 2 * x)

  n : nat

  ev : evenb n = true

  ============================

   exists x : nat, n = 2 * x


여기서 지금까지 언급하지 않았던 콕 시스템의 한가지 편의 기능을 사용할 수 있다. 정리의 문장이 전칭 한정이거나 함축의 형태이면 이 정리를 마치 함수인 것 처럼 쓸 수 있다. 어떤 식에 적용하면 이것으로 사례화된 새로운 정리를 얻을 수 있다. 위의 예에서 Main 가정을 사용해서 n에 대해 사례화시킬수 있다. 


  destruct (Main n) as [H _].

  apply H.

  exact ev.


Qed.


덧셈에 다른 정의에 관한 연습문제


자연수에 대한 덧셈을 새롭게 정의할 수 있다.


Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.


다음을 증명하시오.


forall n m, add n (S m) = S (add n m)

forall n m, add (S n) m = S (add n m)

forall n m, add n m = n + m


새로운 연습문제를 증명할때 이전에 증명한 보조 정리를 사용할 수 있다.


홀수의 합에 대한 연습문제


앞에서부터 n개의 홀수를 모두 더한 합은 다음 함수로 정의한다.


Fixpoint sum_odd_n (n:nat) : nat :=

   match n with 0 => 0 | S p => 1 + 2 * p + sum_odd_n p end.


다음 문장을 증명하시오.


forall n:nat, sum_odd_n n = n * n



===

번역


(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태


(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트


(3장)

Fact: 사실 명제

Theorem: 정리

Implication : 함축

Predicate : (술어) 명제

Rewriting : 다시쓰기

Equality : 등식

Goal : 목적 명제

Tactic : 전술

Hypothesis : 가정

Universal Quantification : 전칭 한정

Transitive : 추이적

Instantiation : 사례화

Associativity : 결합성


(4장)

Proof by induction : 귀납적 증명

Existential : 존재

Lemma : 보조 정리


저작자 표시
신고
Posted by lazyswamp Trackback 0 : Comment 0

3. 명제와 증명


콕 시스템에서 t:B 표기법은 실제로 여러 목적으로 사용된다. 그 중 한가지는 t는 논리식 B의 증명임을 표현하는 것이다. 이렇게 타입을 논리 명제로 보는 것을 커리 하워드 동치(Curry-Howard Isomorphism)이라고 부른다.


식을 증명하려면 이미 만들어놓은 것을 찾아 쓸수 있다. 또한 새로운 증명을 만들어 이름을 붙일수 있다.


3.1 증명해놓은것을 찾기

(3.1절 예제를 실행하기 전에 Require Import Bool. 과 Require Import Arith.와 같은 명령으로 이미 만들어놓은 증명을 불러놓아야한다.)


사실 명제에 대해 누군가 만들어놓은 증명을 Search 명령어로 찾을 수 있다.  명령어의 인자로 이름을 준다.


Search True.

I : True


Search le.

le_S: forall n m : nat, n <= m -> n <= S m

le_n: forall n : nat, n <= n


정리 le_S는 자연수 x를 그 다음 x+1로 매핑하는 함수 S를 사용한다. 사실 3은 S (S (S 0))의 표기법일뿐이다. le_S의 문장은 이렇게 읽을 수 있다. nat 타입의 모든 n, m에 대해 n이 m보다 작거나 같다면 n은 m 다음 수보다 작거나 같다. 화살표 ->는 이전에 함수 타입을 나타냈는데, 여기서는 명제들 사이의 함축을 의미한다. 두가지 용도로 사용하는 것으로 인해 화살표 해석이 모호해지는 문제는 실제로 발생하지 않는다.


SearchPattern 명령어는 이름 대신 명제의 패턴으로 증명을 찾는다. 명제의 인자를 _으로 대체해 생략하고 패턴을 줄 수 있다.


SearchPattern (_ + _ <= _ + _).

plus_le_compat_r: forall n m p : nat, n <= m -> n + p <= m + p

plus_le_compat_l: forall n m p : nat, n <= m -> p + n <= p + m


plus_le_compat: forall n m p q : nat, n <= m -> p <= q -> n + p <= m + q



SearchRewrite 명령어도 비슷하나 다시쓰기 정리만 찾는다. 다시쓰기 정리는 등식 명제를 증명한 것이다. 명제에 패턴이 나타난 정리들을 나열한다.


SearchRewrite (_ + (_ - _)).

le_plus_minus_r: forall n m : nat, n <= m -> n + (m - n) = m


le_plus_minus: forall n m : nat, n <= m -> m = n + (m - n)



SearchAbout 명령어는 주어진 기호와 연관된 모든 정리를 찾는데 사용한다. 예를 들어, 정렬 프로그램에서 사용한 leb 함수와 연관된 정리를 찾을 수 있다. 


SearchAbout leb.

leb_correct: forall m n : nat, m <= n -> leb m n = true

leb_complete: forall m n : nat, leb m n = true -> m <= n

leb_iff: forall m n : nat, leb m n = true <-> m <= n

leb_correct_conv: forall m n : nat, m < n -> leb n m = false

leb_complete_conv: forall m n : nat, leb n m = false -> m < n

leb_iff_conv: forall m n : nat, leb n m = false <-> m < n


leb_compare: forall n m : nat, leb n m = true <-> nat_compare n m <> Gt


3.2 새롭게 증명하기

목적 지향 증명으로 알려진 접근방법으로 보통 증명한다. 다음과 같은 시나리오로 따른다. 


  1. Theorem이나 Lemma 명령으로 증명하려는 명제를 입력한다. 명령어를 사용할 때 이름도 지정해 나중에 이 정리에 대한 증명을 참조한다.
  2. 콕 시스템은 증명해야할 식으로 입력한 그 식을 보여준다. 일종의 문맥으로 증명에 사용할 수 있는 임시 사실 명제를 보여주기도한다. 수평선 ===== 위에 이 문맥을 표시하고, 그 아래에 목적 명제를 표시한다.
  3. 사용자는 명령어를 입력하고 목적 명제를 간단하게 분해한다. 
  4. 콕 시스템은 아직 남은 식들을 표시한다.
  5. 3번 단계로 돌아간다.

3번 단계에서 사용하는 명령어를 전술이라고 부른다. 어떤 전술은 목적 정리의 수를 실제로 줄인다. 목적 정리가 더이상 없으면 증명은 완성된다. Qed 명령어로 1단계에서 정한 이름으로 새로운 저이를 증명한다. 예를 살펴보자.


Lemma example2 : forall a b: Prop, a /\ b -> b /\ a.



1 subgoal

  

  ============================

   forall a b : Prop, a /\ b -> b /\ a


Proof.

   intros a b H.


1 subgoal

  

  a : Prop

  b : Prop

  H : a /\ b

  ============================

   b /\ a


  split.


2 subgoals

  

  a : Prop

  b : Prop

  H : a /\ b

  ============================

   b


subgoal 2 is:

 a


  destruct H as [H1 H2].


2 subgoals

  

  a : Prop

  b : Prop

  H1 : a

  H2 : b

  ============================

   b


subgoal 2 is:

 a


exact H2.


1 subgoal

  

  a : Prop

  b : Prop

  H : a /\ b

  ============================

   a


destruct H as [H1 H2].


1 subgoal

  

  a : Prop

  b : Prop

  H1 : a

  H2 : b

  ============================

   a


exact H1.


Proof completed.


Qed.


example2 is defined



example2 이름을 붙인 정리는 다른 전술에서 나중에 사용할 수 있다. 이 증명은 기초적인 유추 단계를 표현하는 몇가지 단계를 사용한다. 콕 시스템에는 방대한 전술이 있다. 각 전술은 목적 명제의 형태에 맞추어져있다. 각 목적 명제는 사실 문맥과 결론 두 부분으로 되어있다. 문맥은 "a : 타입"이나 "H : 식" 형태의 원소로 구성되어 있다. 이 원소들을 가정이라 부르고, 증명 과정에 임시로 사용할수 있는 사실 명제이다.


destruct H as [H1 H2]는 가정 H가 두 명제의 곱에 대한 증명이라는 형태에 맞추어 만든 전술이다. 이 전술은 새로운 두 개의 가정 H1과 H2를 문맥에 더한다.  기본적인 논리 연결자에 대한 전술을 기억해두면 유용할 것이다.


아래의 테이블에 기본 전술을 나열한다([1]의 p.130의 테이블 참고). 이 테이블을 이용하려면 다음 사항을 잘 기억해야한다. 각 논리 연결자는 문맥의 가정(편의상, H라고 하자)에 나타나거나 목적 명제의 결론에 나타날수 있다. 각각 경우마다 다른 전술을 사용한다. 가정을 다루려면 "Hypothesis"로 시작하는 줄에 나열된 전술을 사용해야한다.


예를 들어 example2 증명의 첫번째 단계에서 결론에 나타난 전칭 한정을 다루므로 intros 전술을 사용한다. intros 전술은 a, b, H 인자를 받아 세개의 논리 연결자(두 개의 전칭 한정과 한 개의 함축)를 앞에서부터 차례로 처리한다. 두번째 단계에서 결론에 나타난 곱을 다루므로 split 전술을 사용한다. 세번째 단계는 가정 H에 나타난 곱을 다룬다. 사용할 전술은 destruct H as [H1 H2]이다. 네번째 단계에서 사용한 전술은 테이블에 언급되어있지 않다. exact H2 전술은 문맥의 H2 이름이 붙은 문장을 증명하는 것이다. 전술 assumption은 콕 시스템에게 요청하여 결론에 있는 것과 동일한 문장이 가정에 나타나있는지를 찾도록하는 것이다. 다섯번째 단계는 조금더 복잡한데, intuition이라 부르는 자동 전술을 호출한다.




elim이나 case 전술을 사용하면 지정한 가정으로부터 새로운 사실 명제를 목적 명제의 전제로하는 새로운 함축을 만든다(역주 참고). intros 전술로 이 전제를 문맥의 가정으로 불러온다. 두가지 전술을 차례로 쓰는 대신 destruct 전술로 대체해서 한번에 빠르게 증명할 수 있다.


[역주]

(Lemma example2) 증명에서 intros a b H.와 split. 다음에 elim H., intros., exact H1.으로 목적 명제를 증명할 수 있고, destruct H as [H1 H2].로 동일한 증명을 할 수 있음.


2 subgoals

  

  a : Prop

  b : Prop

  H : a /\ b

  ============================

   b


subgoal 2 is:

 a


elim H.


2 subgoals

  

  a : Prop

  b : Prop

  H : a /\ b

  ============================

   a -> b -> b


subgoal 2 is:

 a


intros.


2 subgoals

  

  a : Prop

  b : Prop

  H : a /\ b

  H0 : a

  H1 : b

  ============================

   b


subgoal 2 is:

 a


exact H1


가정을 다루는 모든 전술(destruct, apply, rewrite 등)은 인자로 그 이름을 받는다. 또한 정리 이름도 인자로 받을 수 있다. 이런 식으로 증명해서 저정해놓은 정리를 나중에 다른 정리를 증명하는데 사용할 수 있다. 


3.3 전술을 사용하는 다른 증명 예제

이제까지 설명한 전술들을 사용하여 증명하는 또다른 예제를 살펴보자.


Lemma example3 : forall A B, A \/ B -> B \/ A.


논리 연결자 "합"에 대해 교환법칙이 성립함을 증명한 것이다. 말로 풀어 설명하면, 어떠한 명제 A와 B에 대해 만일 A \/ B가 성리하면 B \/ A가 성립한다이다. 증명의 첫번째 단계는 전칭 한정 명제와 가정을 문맥에 도입하는 것이다.


intros A B H.


1 subgoal

  

  A : Prop

  B : Prop

  H : A \/ B

  ============================

   B \/ A


직관적으로 설명하자면, 두 명제 A, B가 주어졌고, A \/ B가 성립한다고 가정하자. 그러면 B \/ A를 증명해야한다. 이 상황에서 문제를 어떻게 해결할지 고민해봐야한다. A \/ B를 증명하려면 결론을 다루도록 선택할 수도 있다. 즉 A를 증명할지 B를 증명할지를 선택해야할 것이다. 하지만 A \/ B가 성립한다는 것만 안다면 A를 증명할 수 없다. 왜냐하면 A가 아니라 B가 성립해서 A \/ B가 성립했었을 수도 있기 때문이다. 이렇게 결론을 직접 다루면 원하는 증명을 할 수 없다. 반면에 가정을 다루도록 선택할 수있다. A \/ B가 성립한다면 A가 성립하거나 B가 성립하는 두 가지 경우 중 하나이다. 따라서 두 경우를 각각 살펴볼 수 있다. 전술 destruct이 그러한 과정을 수행한다.


destruct H as [H1 | H1].


2 subgoals

  

  A : Prop

  B : Prop

  H1 : A

  ============================

   B \/ A


subgoal 2 is:

 B \/ A


두개의 목적 명제가 생겼고 첫번째 목적 명제에 대한 가정 H1은 A가 성립하는 경우라는 것을 말해준다. 이제는 결론을 다루어서 증명할 수 있는 상황이 되었다. 오른편 A를 증명하도록 선택하면 이 경우의 증명을 완성할 수 있다.


right; assumption.


1 subgoal

  

  A : Prop

  B : Prop

  H1 : B

  ============================

   B \/ A


세미콜론 `;'은 여러 전술을 하나로 조합할때 사용한다. 왼편의 전술을 먼저 적용해서 나온 모든 목적 명제들에 오른편 전술을 적용한다. 전술 right는 B \/ A를 A로 변환해서 합의 문장에서 오른편의 명제를 증명하겠다는 의도이다. 그 다음 전술 assumption은 가정 A(H1 이름이 붙은)를 찾아 증명한다. right; assumption 전술로 첫번째 목적 명제를 증명 완료했으므로 콕 시스템은 두번째 목적 명제를 보여준다. 이제 오직 하나만 남았다. 이번에는 합의 문장에서 왼편의 명제를 증명하되 유사하게 증명할 수 있다.


left; assumption.


Proof completed.


Qed.


3.3.1 apply를 사용하는 예제

전술 테이블에 따르면 apply 전술은 전칭 한정자나 함축 논리 연결자를 주로 사용해 표현된 가정이나 정리를 다룬다. 정리의 결론에서 전제를 분리하고, 최대한 많은 전칭 한정 변수를  추측해 현재 증명하려는 결론과 정리의 결론을 일치시키도록 하고, 전제에 대해 새로운 목적 명제를 만든다.


정리 th가 다음과 같은 형태의 문장이고,


forall x1 ... xk, A1 x1 ... xk -> A2 x1 ... xk -> ... -> An x1 ... xk -> C x1 ... xk


현재 증명하려면 결론이 C a1 ... ak 형태라고 하자. 그러면 apply 전술을 사용하면 현재 목적 명제를 n개의 목적들 즉 A1 a1 ... ak, ..., Ak a1 ... ak로 대체한다. 모든 전칭 한정 변수가 목적 명제의 결론에 나타날때 잘 적용된다. 정리의 결론과 목적 명제의 결론을 매칭시켜 콕 시스템으로 하여금 x1은 a1, x2는 a2, ... 임을 유추할 수 있도록 만든다.


정리의 결론에 나타나지 않는 변수가 있다면 콕 시스템은 이 변수가 어떤 값인지 유추할수 없다. 이런 경우 사용자가 with 지시어로 그 값을 지정할 수 있다.


두 예제를 통해 apply 전술의 쓰임새를 설명한다. 첫번째 예제에서는 apply 전술의 간단한 사용법을 설명한다. 두 자연수를 비교하는 두가지 정리를 사용한다.


Check le_n.


le_n

     : forall n : nat, n <= n


Check le_S.


le_S

     : forall n m : nat, n <= m -> n <= S m


Lemma example4 : 3 <= 5.


3은 S (S (S 0))에 대한 표기법이고, 5는 S (S (S (S (S 0))))이다. 첫번째 단계로 le_S 정리를 적용할수 있다. 이 정리의 결론 n <= S m를 목적 명제 3 <= 5와 매치되고 n과 m이 3과 4임을 알 수 있다. 이렇게 확인된 정리의 전제에 따라 새로운 목적 명제를 생성한다. 


apply le_S.


1 subgoal

  

  ============================

   3 <= 4


두번째 단계에 동일한 정리를 다시 적용한다. 이번에는 콕 시스템이 n은 3이고 m도 3이어야함을 찾아낸다.


apply le_S.


1 subgoal

  

  ============================

   3 <= 3


이제 le_n으로 증명할 수 있는 목적 명제를 얻었다. apply 전술을 다시 사용하면 더이상 새로운 목적 명제가 생기지 않고 이 증명을 저장할 수 있다.


apply le_n.

Proof completed.

Qed.


두번째 예제에서 가정이나 정리에서 전칭 한정 변수가 이 정리의 결론에 나타나지 않은 경우를 설명한다. 추이 정리에서 이런 상황이 전형적으로 발생한다. 자연수에서 작거나 같다라는 순서는 "a<=b이고 b<=c이면 a<=c" 명제가 추이 정리의 예이다. 


Check le_trans.

le_trans

     : forall n m p : nat, n <= m -> m <= p -> n <= p


Lemma example5 : forall x y, x <= 10 -> 10 <= y -> x <= y.

intros x y x10 y10.

1 subgoal

  

  x : nat

  y : nat

  x10 : x <= 10

  y10 : 10 <= y

  ============================

   x <= y


이전처럼 apply 전술로 le_trans 정리를 적용해보면 다음과 같은 에러 메시지를 보게된다.


apply le_trans

Error: Unable to find an instance for the variable m.


이 정리의 결론에 m이 나타나지 않는다. 이 정리의 결론을 목적 정리와 매칭시킬때 이 변수의 값을 찾을 수 없다. 사용자가 수작업으로 이 값을 줄 수 있다.


apply le_trans with (m := 10).


2 subgoals

  

  x : nat

  y : nat

  x10 : x <= 10

  y10 : 10 <= y

  ============================

   x <= 10


subgoal 2 is:

 10 <= y


assumption.

assumption.

Qed.


3.3.2 rewrite를 사용하는 예제

등식은 프로그램의 성질을 표현하는 가장 흔한 방법 중 하나이다. 따라서 많은 정리들이 등식으로 표현된 결론 부분을 가지고 있다. 이러한 정리들을 증명하는데 가장 유용한 전술은 rewrite이다.


대부분의 정리는 전칭 한정을 사용하고 있고, 이 정리를 사용하려면 전칭 한정 변수의 값을 추측해야 한다. rewrite 전술은 이러한 추측을 위해 사용한다. 이 전술은 목적 명제의 결론(등식 형태 가정)의 왼편의 패턴을 찾아 그 변수들의 사례화시킨다. 예를 살펴보자.


Lemma example6 : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.

intros x y.


분배 정리를 사용하기에 적절하다. SearchRewrite 명령어로 이 정리를 찾아보자.


SearchRewrite (_ * ( _ + _ )).

mult_plus_distr_l: forall n m p : nat, n * (m + p) = n * m + n * p


콕 시스템에 이 정리를 적용해 재작성하도록 요청할수 있다.


rewrite mult_plus_distr_r.



1 subgoal

  

  x : nat

  y : nat

  ============================

   (x + y) * x + (x + y) * y = x * x + 2 * x * y + y * y


콕 시스템이 전칭 한정 변수를 어떻게 사례화시켰는지 관찰할수 있다. n은 (x + y)로, m은 x로, p는 y로 놓았다. 다시 유사한 배분 정리가 필요하다 이번에는 곱셈이 오른쪽에 있는 경우에 대한 것이다. 


SearchRewrite ((_ + _) * _).

mult_plus_distr_r: forall n m p : nat, (n + m) * p = n * p + m * p


rewrite mult_plus_distr_r.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + y * x + (x + y) * y = x * x + 2 * x * y + y * y


마지막 단계에서 두가지 선택이 가능하다. p를 x로 놓거나 y로 놓을 수 있다. 콕 시스템은 x를 선택했다. 지시어를 추가해서 rewrite mult_plus_distr_r with (p := x)와 같이 더 명확하게 명령을 내릴수 있다. 다음 단계에서 등식의 왼편을 재구성하는 정리를 찾고, 그 다음에 오른편을 다룬다.


rewrite mult_plus_distr_r.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + y * x + (x * y + y * y) = x * x + 2 * x * y + y * y


SearchRewrite (_ + (_ + _)).


plus_permute_2_in_4: forall n m p q : nat, n + m + (p + q) = n + p + (m + q)

plus_permute: forall n m p : nat, n + (m + p) = m + (n + p)

plus_assoc: forall n m p : nat, n + (m + p) = n + m + p

plus_permute_2_in_4: forall n m p q : nat, n + m + (p + q) = n + p + (m + q)

plus_permute: forall n m p : nat, n + (m + p) = m + (n + p)

plus_assoc_reverse: forall n m p : nat, n + m + p = n + (m + p)


rewrite plus_assoc.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + y * x + x * y + y * y = x * x + 2 * x * y + y * y


이때 plus_assoc 정리를 오른편에서 왼편 방향으로 재작성하도록 적용하고 싶다. <-를 사용하면 된다.


rewrite <- plus_assoc with (n := x * x).


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + (y * x + x * y) + y * y = x * x + 2 * x * y + y * y


이제 곱셈에 대한 교환법칙을 사용하고 싶다. SearchPattern 명령어로 관련된 정리를 찾을 수 있다.


SearchPattern (?x * ?y = ?y * ?x).

mult_comm: forall n m : nat, n * m = m * n


rewrite mult_comm with (n := y) (m := x).


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + (x * y + x * y) + y * y = x * x + 2 * x * y + y * y


이제 x * y + x * y는 2 * x *  y임을 보여야한다. 2는 S 1의 표기법이다. 관련된 형태를 갖는 정리를 찾아본다.


SearchRewrite (S _ * _).


mult_succ_l: forall n m : nat, S n * m = n * m + m

mult_1_l: forall n : nat, 1 * n = n

...


현재 x * y가 두번 나타나는데 그 중 하나를 mult_1_l로 다시 쓰려고한다. pattern 전술은 다시쓰기를 할 대상을 제한할때 사용한다. 맨처음 나타난 것만 다시쓰려면,


pattern (x * y) at 1; rewrite <- mult_1_l.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + (1 * (x * y) + x * y) + y * y = x * x + 2 * x * y + y * y


rewrite <- mult_succ_l.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + 2 * (x * y) + y * y = x * x + 2 * x * y + y * y


이제 곱에 대한 결합성을 사용하기만 하면 된다. 


SearchRewrite (_ * (_ * _)).


mult_assoc: forall n m p : nat, n * (m * p) = n * m * p

mult_assoc_reverse: forall n m p : nat, n * m * p = n * (m * p)


rewrite mult_assoc.


1 subgoal

  

  x : nat

  y : nat

  ============================

   x * x + 2 * x * y + y * y = x * x + 2 * x * y + y * y


전략 테이블에서 나열한 reflexivity를 사용하여 마무리짓는다.


reflexivity.

Proof completed.

Qed.


다시쓰기 정리는 때때로 어떤 조건하에서만 동등함이 성립한다고 하는 전제를 가지고 있다. 이 정리를 사용해서 다시쓰기를 할때는 이 전제를 문맥에 맞게 사례화시켜 나중에 증명할 목적 명제로 추가한다.


3.4 고급 전술

증명하기 어려운 명제를 다룰때 assert 전술로 중간 단계를 참이라고 선언하는 것도 흔한 방법이다. (H : P) 형태의 인자를 주는데, 두 목적 명제를 제시한다. 하나는 P를 증명하는것이다. 두번째는 같은 문장 P를 증명하는 것이다[역주: 4장 이후에서 assert 전술을 사용한 예제 참고]. 단 이 경우 H로 명명된 가정 P를 문맥에 추가한 상황에서 증명을 진행한다.


어떤 자동 전술은 다양한 목적으로 제공된다. intutition과 tauto는 명제 논리에서 참인 사실 명제를 증명하는데 유용하다. 곱, 합, 부정만을 다루는 증명(예, example2)에서 이 전술을 한번 쓰는 것으로 해결될 수 있었다. firstorder는 술어 논리에서 참인 명제에 대해서 쓰인다. 언급한 논리 연결자외에도 존재 한정과 전칭 한정을 사용하는 명제를 증명할때 사용해보라. auto는 사용자가 미리 제공한 정리들을 적용해보는 확장가능한 전술이다. eauto는 auto와 유사하나 좀더 강력하다. 하지만 시간이 더 걸린다. ring은 합과 곱으로 이뤄진 식들의 등식을 증명할때 사용된다. omega는 선형 부등식 시스템에 대한 증명에서 사용할수 있다. omega를 사용하려면 콕 시스템이 먼저 메모리로 이 전술 라이브러리를 불러와야한다. 부등식이 선형이려면 A <= B나 A < B형태의 식이고 A와 B는 n*x 형태의 식들의 합이면 된다. 여기서 x는 변수, n은 상수이다.  omage 전술은 선형 부등식을 사례화시켜 다루는 문제에서도 사용될 수 있다. 예를 들어 f x는 선형식이 아니다. 하지만 이 부등식 시스템은 선형식을 사례화시켜 얻은 것으로 간주할 수 있다.


Require Import Omega.


Lemma omega_example :

   forall f x  y, 0 < x -> 0 < f x -> 3 * f x <= 2 * y -> f x <= y.

intros; omega.

Qed.


논리 연결자에 대한 연습문제 ([1]의 연습문제 5.6) 다음 정리를 증명하시오.


forall A B C: Prop, A /\ (B /\ C) -> (A /\ B) /\ C

forall A B C D: Prop, (A -> B) /\ (C -> D) /\ A /\ C -> B /\ D

forall A : Prop, ~(A /\ ~A)

forall A B C: Prop, A \/ (B \/ C) -> (A \/ B) \/ C

forall A B: Prop, (A \/ B) /\ ~A -> B


이 연습문제로 두가지 배울점이 있다. 전술 테이블에 나온 전술들만 사용해서 먼저 증명해야 한다. 그 다음으로 intution 전술로 바로 확인해볼수 있다.


전칭 한정에 대한 연습문제


forall A:Type, forall P Q: A -> Prop,

     (forall x, P x) \/ (forall y, Q y) -> forall x, P x \/ Q x.


===

번역


(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태


(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트


(3장)

Fact: 사실 명제

Theorem: 정리

Implication : 함축

Predicate : (술어) 명제

Rewriting : 다시쓰기

Equality : 등식

Goal : 목적 명제

Tactic : 전술

Hypothesis : 가정

Universal Quantification : 전칭 한정

Transitive : 추이적

Instantiation : 사례화

Associativity : 결합성




저작자 표시
신고
Posted by lazyswamp Trackback 0 : Comment 0


티스토리 툴바