그림으로 설명하는 펑터, 아플리커티브, 모나드

[ 원글 : http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html ]

여기 간단한 값(value)의 예가 있다:

이 값에 함수를 적용해 보자:

간단하지요. 어떤 문맥 안에 값을 놓고 반복해보자. 당분간 문맥을 값을 집어 넣을 수 있는 박스로 생각하자.:

함수를 이 값에 적용하면 그 문맥에 따라 다른 결과를 얻을 것이다. 펑터, 어플리커티브, 모나드, 애로우 등 모든 개념이 이 아이디어를 기초로 하고 있다.  Maybe 데이터 타입은 두 가지 연관된 문맥을 정의한다:

  data Maybe a = Nothing | Just a 

Just a와 Nothing일 때 함수를 적용하는 방법이 다르다는 것을 바로 알 수 있을 것다. 먼저 펑터에 대해 얘기하자!

펑터(Functors)

문맥 안에 값을 감싸두면 보통 함수를 그 값에 적용할 수 없다:

이런 상황에서 fmap이 필요하다. fmap은 문맥을 알고 있다. fmap을 통해 문맥 속의 값에 함수를 적용할 수 있다. 함수 (+3)을 Just 2에 적용한다고 가정해보자. fmap을 사용하자:

> fmap (+3) (Just 2)
Just 5

두둥!  fmap은 어떻게 하는지 가르쳐준다. 그런데 fmap은 이 함수를 적용하는 법을 어떻게 알 까?

펑터가 뭐지, 진짜?

펑터는 타입클래스다. 여기 그 정의가 있다:

Functor는 fmap을 적용하는 방법을 정의하는 데이터타입이다. 다음은 fmap의 동작 방식이다:

따라서 이렇게 할 수 있다:

> fmap (+3) (Just 2)
Just 5 

Maybe는 펑터이기 때문에 마법같이 fmap으로 이 함수를 적용한다. 이 펑터로 fmap을 Just들과 Nothing들에 어떻게 함수를 적용하는지 정한다:

  instance Functor Maybe where
    fmap func (Just val) = Just (func val)
    fmap func Nothing = Nothing 

fmap (+3) (Just 2)라고 코드의 동작을 다음과 같이 설명할 수 있다:

fmap으로 (+3)을 Nothing에 적용해볼까?

> fmap (+3) Nothing
Nothing
Bill O’Reilly being totally ignorant about the Maybe functor

빌 오라일리, Maybe 펑터에 대해 전혀 알고 있지 않은

영화 매트릭스의 모피어스처럼 fmap은 무엇을 해야할지 알고 있다. Nothing을 가지고 시작하면 Nothing으로 끝날 뿐이다! fmap은 젠(zen)이다. 이제 Maybe 데이터타입이 존재하는 이유가 있다. 예를 들어, Maybe가 없는 언어로 데이터베이스 레코드를 다룬다고 하자:

  post = Post.find_by_id(1)
if post
  return post.title
else
  return nil
end

하스켈로 옮겨보면:

  fmap (getPostTitle) (findPost 1)

만일  findPost에서 포스트를 반환하면 getPostTitle로 그 제목을 얻을 수 있다. 만일 findPost에서 아무것도 반환하지 않으면 (Nothing을 반환하면Nothing을 반환할 것이다. 꽤 깔끔하죠? <$>은 fmap의 인픽스(infix) 버전으로, 위 코드 대신 다음과 같이 작성할 수 있다:

  getPostTitle <$> (findPost 1)

다른 예를 보자: 함수를 리스트에 적용하면 어떻게 되나?

리스트도 펑터다! 여기 그 정의가 있다:

  instance Functor [] where
    fmap = map

오케이, 마지막 예: 함수에 다른 함수를 적용하면 어떨까? 

  fmap (+3) (+1)

여기 함수가 있다:

여기 다른 함수에 적용할 함수가 있다:

그 결과는 단지 또다른 함수다!

> import Control.Applicative
> let foo = fmap (+3) (+2)
> foo 10
15

따라서 함수도 펑터다!

  instance Functor ((->) r) where
    fmap f g = f . g 

fmap을 함수에 사용하면 그 결과는 함수 조합이 된다!

어플리커티브(Applicatives)

어플리커티브는 그 다음 레벨로 데려다준다. 어플리커티브를 사용하면, 펑터처럼, 값을 어떤 문맥 안에 감쌀 수 있다:

그러나 함수도 문맥 안에 감쌀 수 있다!

자, 이해해보자. Control.Applicative에서 <*>를 두어 어떤 문맥에 감싸져 있는 함수를 관련된 문맥 속에 있는 값에 적용하는 방법을 지정한다:

예컨데:

  Just (+3) <*> Just 2 == Just 5

<*>를 사용하면 재미있는 상황이 벌어질 수 있다. 예를 들어:

  > [(*2), (+3)] <*> [1, 2, 3]
[2, 4, 6, 4, 5, 6]

펑터로는 할 수 없지만 어플리커티브로 할 수 있는 것이 있다. 두 개의 인자를 받는 함수를 문맥에 감싸져 있는 두 개의 값에 어떻게 적용할 수 있을까?

> (+) <$> (Just 5)
Just (+5)
> Just (+5) <$> (Just 4)
ERROR ??? WHAT DOES THIS EVEN MEAN WHY IS THE FUNCTION WRAPPED IN A JUST

어플리커티브:

> (+) <$> (Just 5)
Just (+5)
> Just (+5) <*> (Just 3)
Just 8 

Applicative는 Functor보다 유연하다. "다 큰 남자는 인자를 몇 개 받든 상관없이 어떠한 함수라도 사용할 수 있어야 한다."라고 마치 말하는 것 같다. "<$>와 <*>를 가지고 임의 개수의 값을 받는 어떤 함수에 포장된 값들을 전달하고 그 결과로 포장된 값을 반환 받을 수 있다!"

> (*) <$> Just 5 <*> Just 3
Just 15

이러한 똑같은 일을 하는 liftA2라 부르는 함수가 있다:

> liftA2 (*) (Just 5) (Just 3)
Just 15

모나드(Monads)

모나드를 배우는 방법:

  1. 컴퓨터 과학 분야의 박사학위를 얻은 다음,
  2. 그것을 던져 버린다. 왜냐하면 여기 설명에서는 그 학위가 필요하지 않기 때문에!

모나드는 새로운 방법을 추가한다.

펑터는 함수를 포장된 값에 적용한다:

어플리커티브는 포장된 함수를 포장된 값에 적용한다:

모나드는 포장된 값을 반환하는 함수에 포장된 값을 적용한다.모나드는 바인드라고 읽는 함수로 이것을 한다.

예를 살펴보자. Maybe는 모나드다: 

Just a monad hanging out

half는 짝수에 대해 동작하는 함수라 가정하자:

  half x = if even x
           then Just (x `div` 2)
           else Nothing

포장된 값을 전달하면 무슨 일이 벌어질까?

함수 >>=를 사용해서 포장된 값을 함수로 밀어낼 수 있다. 함수 >>=의 사진이 여기 있다:

동작 방식을 설명한다:

> Just 3 >>= half
Nothing
> Just 4 >>= half
Just 2
> Nothing >>= half
Nothing

내부에서 어떤 일이 벌어지고 있나? Monad는 타입클래스다. 부분적으로 아래와 같이 정의한다: 

  class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b

바인드 함수 >>=는:

따라서 Maybe는 Monad다:

  instance Monad Maybe where
    Nothing >>= func = Nothing
    Just val >>= func  = func val

아래에서 Just 3에 대한 동작을 설명한다!

Nothing을 주는 경우는 더 간단하다:

이런 함수 호출들을 차례로 묶을 수 있다:

> Just 20 >>= half >>= half >>= half
Nothing

쿨! 이제 Maybe는 펑터, 어플리커티브, 모나드라는 것을 알았다. 

이제 다른 예를 반복해서 살펴보자: IO 모나드:

특히 3가지 함수들. getLine은 특별한 인자 없이 사용자 입력을 받는다:

  getLine :: IO String

readFile은 파일 이름 문자열을 인자로 받고 그 파일 내용을 반환한다:

  readFile :: FilePath -> IO String

putStrLn은 문자열을 받아 출력한다:

  putStrLn :: String -> IO ()

세가지 모든 함수들은 일반 값을 받아(또는 받지 않고) 포장된 값을 반환한다. 이 함수들을 바인드 함수  >>=를 사용하여 차례대로 묶을 수 있다!

  getLine >>= readFile >>= putStrLn

하스켈 언어는 모나드를 사용하는데 편리한 구문, do 표기법을 제공한다:

  foo = do
    filename <- getLine
    contents <- readFile filename
    putStrLn contents

결론

  1. 펑터는 Functor 타입클래스를 구현하는 데이터 타입이다.
  2. 어플리커티브는 Applicative 타입클래스를 구현하는 데이터 타입이다.
  3. 모나드는 Monad 타입클래스를 구현하는 데이터 타입이다.
  4. Maybe는 이 세가지를 모두 구현한다. 따라서 펑터이고, 어플리커티브이며, 모나드이다.

이 세가지의 차이점은 무엇인가?

  • 펑터:  fmap이나 <$>를 사용하여 함수를 포장된 값에 적용한다.
  • 어플리커티브: <*>나 liftA를 사용하여 포장된 함수를 포장된 값에 적용한다.
  • 모나드: >>=나 liftM을 사용하여 포장된 값을 리턴하는 함수를 포장된 값에 적용한다.

자, 여기까지 설명을 들었다면 모나드가 쉽고 SMART IDEA(tm)라는 점에 우리 모두 동의할 것이라 생각한다.  이 가이드로 여러분의 궁금증을 일부 해소했다면 이제 더 심화된 내용을 살펴볼 차례다. LYAH의 모나드 섹션을 살펴보라. 이 가이드에서 넘어갔던 많은 것이 있다. Miran은 자세한 설명을 해줄 것이다.



'Haskell' 카테고리의 다른 글

하스켈 프로그래밍 스터디 계획  (0) 2015.08.31
하스켈 프로그래밍(Haskell) 커뮤니티  (0) 2015.08.31
Posted by lazyswamp :

아담 칠리파라(Adam Chlipala)의 책 9.2절 Heterogeneous Lists 참고. 


ML이나 Haskell에서 리스트는 매우 빈번하게 사용한다. [1,2,3,4,5]는 1부터 5까지 정수를 포함하는 리스트로 그 타입은 Haskell에서 [Int]이다. ML이나 Haskell에서의 리스트는 타입이 동일한 원소들의 리스트를 얘기한다. 따라서, [1, true]와 같은 식은 허용하지 않는다. Haskell에서 타입 클래스(type class)를 사용하면 타입이 다른 원소들의 리스트를 표현할 수는 있지만 복잡하다. 콕 시스템은 ML이나 Haskell보다 더 복잡한 타입 시스템을 갖추고 있어 상대적으로 간단하게 이러한 리스트를 표현할 수 있다.


콕 시스템에서 타입이 다른 원소들의 리스트를 만드는 방법을 살펴본다. 기본적인 아이디어는 리스트 타입을 타입 수준의 리스트로 색인을 달아 각 원소의 타입이 무엇인지 설명하는 것이다. 간단한 생각이지만 콕으로 표현했을때 간단한 리스트도 꽤 복잡해진다. 


Inductive hlist (A:Type) (B:A ->Type) : list A -> Type :=

   HNil : hlist A B nil

| HCons : forall (x:A) (ls:list A), B x -> hlist A B ls -> hlist A B (x::ls).


예를 들어 hlist의 쓰임새를 살펴보자. 먼저, HCons의 타입은 선언된 바와 같다. 전칭 한정 변수가 네 개이다.


Check HCons.


HCons

     : forall (A : Type) (B : A -> Type) (x : A) (ls : list A),

       B x -> hlist A B ls -> hlist A B (x :: ls)



첫번째 전칭 한정 변수 A를 Set으로 대체한다. 


Check HCons Set.


HCons Set

     : forall (B : Set -> Type) (x : Set) (ls : list Set),

       B x -> hlist Set B ls -> hlist Set B (x :: ls)


두번째 전칭 한정 변수 B를 (fun T: Set => T)로 대체한다. 사실 이 함수는 Set -> Set 타입을 갖는다. 서브 타입 관계에 의해 Set -> Type으로 간주한다. 


Check HCons Set (fun T:Set => T).


HCons Set (fun T : Set => T)

     : forall (x : Set) (ls : list Set),

       (fun T : Set => T) x ->

       hlist Set (fun T : Set => T) ls ->

       hlist Set (fun T : Set => T) (x :: ls)


그 다음 전칭 한정 변수 x에 bool을 넘긴다. bool의 타입은 Set이다.


Check HCons Set (fun T:Set => T) bool.


HCons Set (fun T : Set => T) bool

     : forall ls : list Set,

       (fun T : Set => T) bool ->

       hlist Set (fun T : Set => T) ls ->

       hlist Set (fun T : Set => T) (bool :: ls)


마지막 전칭 한정 변수 ls에 nil을 준다. nil은 list Set 타입이므로 타입 리스트이다.


Check HCons Set (fun T:Set => T) bool nil.


HCons Set (fun T : Set => T) bool nil

     : (fun T : Set => T) bool ->

       hlist Set (fun T : Set => T) nil ->

       hlist Set (fun T : Set => T) (bool :: nil)


(fun T : Set => T) bool을 베타 환원(beta redunction)으로 계산하면 bool이 된다. 따라서 HCons Set (fun T : Set => T) bool nil의 타입은 bool -> ... 형태이다. 그래서 이 함수의 부울 인자로 true를 지정한다.


Check HCons Set (fun T:Set => T) bool nil true.


HCons Set (fun T : Set => T) bool nil true

     : hlist Set (fun T : Set => T) nil ->

       hlist Set (fun T : Set => T) (bool :: nil)


HNil Set (fun T : Set => T)는 hlist의 정의에 의해 hlist Set (fun T : Set => T) nil 타입을 갖는다.


Check HNil Set (fun T : Set => T)


HNil Set (fun T : Set => T)

     : hlist Set (fun T : Set => T) nil


다시 원래 식으로 돌아가서 마지막 인자로 HNil Set (fun T : Set => T)를 넘기면 hlist 타입의 타입이 다른 원소들의 리스트가 된다.


Check HCons Set (fun T:Set => T) bool nil true (HNil Set (fun T:Set => T)).


HCons Set (fun T : Set => T) bool nil true (HNil Set (fun T : Set => T))

     : hlist Set (fun T : Set => T) (bool :: nil)


조금 간단하게 hlist를 사용하기 위해 다음 세 가지 정의를 도입하자.


Definition HList := hlist Set (fun T:Set => T).

Definition hcons := HCons Set (fun T:Set => T).

Definition hnil := HNil Set (fun T:Set => T).


list Set은 타입 리스트로, 타입이 다른 원소들의 리스트를 표현하는 아이디어가 HList의 타입에 그대로 표현되어 있다. 


Check HList.


HList

      : list Set -> Type


리스트 [1, true]를 다음과 같이 작성할 수 있다.


Check hcons nat (bool::nil) 1 (hcons bool nil true hnil).


hcons nat (bool :: nil) 1 (hcons bool nil true hnil)

     : hlist Set (fun T : Set => T) (nat :: bool :: nil)




Posted by lazyswamp :

8. 귀납적 성질


귀납적 정의로 새로운 술어를 기술할 수도 있다. 타입 A에 대한 술어는 A 타입의 원소를 입력 받아 명제 타입 Prop의 원소를 반환하는 함수로 간단히 기술할 수 있다. 귀납적 명제의 컨스트럭터는 술어로 규정하는 정리들이다. 이 술어에 기반한 문장에 대한 증명은 오직 이 컨스트럭터의 조합으로만 얻을 수 있다.


8.1 귀납적 술어 정의하기

짝수 자연수 집합을 뜻하는 술어를 다음과 같이 귀납적 정의를 쓸 수 있다.


Inductive even : nat -> Prop :=

   even0 : even 0

| evenS : forall x:nat, even x -> even (S (S x)).



x가 자연수라면 even x는 명제이다. 정리 even0는 even 0 명제를 증명할 때 사용하고, 정리 evenS는 명제 even 0로 부터 명제 even 2를 추론할 때 쓸 수 있다. evenS를 반복해서 사용하면 나머지 숫자들도 even 술어를 만족함을 증명하는데 이용할 수 있다.


귀납 타입처럼 case, elim, destruct 전술들을 사용해서 귀납 명제에 관련된 가정에 대해 추론할 수 있다. 이 전술들을 쓰면 귀납 정의의 각 컨스트럭터 별로 하나씩 목적 명제를 다시 만들어 낼 것이다. 덧붙이자면 컨스트럭터가 전제로 귀납 명제를 사용하면 elim과 induction 전술은 귀납 가정을 만든다.


8.2 귀납적 술어에 대한 귀납 증명

변수 x가 귀납적 성질을 만족한다면 그 변수 자체에 대한 귀납을 사용하는 것 보다 귀납적 성질에 대한 귀납을 사용해서 그 변수에 대한 성질을 증명하는 것이 종종 더 효율적이다. 다음 증명의 예를 보자.


Lemma even_mult : forall x, even x -> exists y, x = 2 * y.

intros x H; elim H.


2 subgoals

  

  x : nat

  H : even x

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

   exists y : nat, 0 = 2 * y


subgoal 2 is:

 forall x0 : nat,

 even x0 -> (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y


첫번째 목적 명제는 even의 첫번째 컨스트럭터를 사용해주 even x를 증명하는 경우이다. 이때 변수 x는 0으로 바꾸어 이 목적 명제를 표시한다. y를 0으로 놓고 증명할 수 있다.


exists 0; ring.


1 subgoal

  

  x : nat

  H : even x

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

   forall x0 : nat,

   even x0 ->

   (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y


그 다음 목적 명제는 even의 두번째 컨스트럭터를 가지고 even x를 증명하는 경우에 대한 것이다. 이때 x가 S (S x0)인 변수 x0가 반드시 존재해야 한다. 그리고 elim 전술은 even x0에 대한 귀납 가정을 도입한다. 이렇게 x0는 S (S x0)에 대해 증명할 성질을 만족할 것으로 가정한다. 이런 점에서 elim 전술은 귀납 가정을 생성한다. 이는 마치 induction 전술에서와 정확히 같다. 사실 elim대신 induction 전술을 쓸 수 있다. 두 전술은 거의 똑같다. 


intros x0 Hevenx0 IHx.


1 subgoal

  

  x : nat

  H : even x

  x0 : nat

  Hevenx0 : even x0

  IHx : exists y : nat, x0 = 2 * y

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

   exists y : nat, S (S x0) = 2 * y


이제 IHx는 귀납 가정이다. x가 x0의 다음 다음이라면 x0의 반이되는 값 y가 존재함을 이미 알고 있음을 뜻한다. 이 값을 S (S x0)의 반을 구하기 위해 이용한다. 다음의 전술을 사용해서 증명을 완료한다.


destruct IHx as [y Heq].

rewrite Heq.

exists (S y).

ring.


destruct 전술을 이전과 다르게 사용했다. 이 전술로 원소를 새로 만들어 이름을 붙이고, 이 이름을 문맥에 도입한다. 


8.3 inversion 전술

inversion 전술은 귀납적 명제에 관한 문장을 증명하는 다양한 방법에서 쓰일 수 있다. 이 전술은 귀납적 명제의 모든 컨스트럭터를 분석하고, 적용할 수 없는 것은 버리며, 적용가능한 컨스트럭터에 대해서 새로운 목적 명제를 만들고 이 컨스트럭터의 전제들을 문맥에 불러들인다. 예를 들어, 1이 짝수가 아님을 증명하는데 매우 적합하다. 왜냐하면 어떤한 컨스트럭터도 명제 even 1로 결론짓지 않기 때문이다. evenS는1 = S (S x)를 증명해야하고, even0는 1=0을 증명해야하는데 모두 거짓이다.


Lemma not_even_1 : ~even 1.

intros even1.


1 subgoal

  

  even1 : even 1

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

   False


inversion even1.

Qed.


inversion 전술을 사용하는 다른 예로, 짝수의 이전 이전 수는 짝수임을 증명해보자. 이 문장에서 주어진 수를 S (S x)로 놓고 이전 이전 수를 x로 놓자.


Lemma even_inv : forall x, even (S (S x)) -> even x.


intros x H.


1 subgoal

  

  x : nat

  H : even (S (S x))

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

   even x


이 전술에서 even 술어의 컨스트럭터들을 분석하면 even0를 사용해서 가정 H를 증명할 수 없음을 인식한다. 오직 evenS만 사용될 수 있다. 그러므로 even x0와 S (S x) = S (S x0)가 성립하는 x0가 반드시 존재해야 한다. 즉, even x가 성립한다.


inversion H.


1 subgoal

  

  x : nat

  H : even (S (S x))

  x0 : nat

  H1 : even x

  H0 : x0 = x

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

   even x


assumption.

Qed.


even_inv의 문장은 evenS 문장의 반대임을 참고하시오. 이 전술의 이름을 이렇게 붙이 이유이다. 


귀납적 성질은 매우 복잡한 개념을 표현하는데 사용할 수 있다. 프로그래밍 언어의 의미를 귀납적 정의로 정의할 수 있다. 기본적인 계산 단계에 각각 해당하는 컨스트럭터들을 도입할 수 있다. 



===

번역


(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 : 귀납적 증명의 귀납적 경우


(6장)

datatype : 타입, 데이터 타입

Binary tree : 이진 트리

Internal Node : 내부 노드

Leaf : 끝 노드

Proof by Cases : 경우를 나누어 증명

Constructor : 컨스트럭터

Injective : 단사적


(7장)

Well-founded : 기초가 튼튼한(?)

Iterator : 반복자


(8장)


Predicate : 술어



Posted by lazyswamp :

7. 콕 시스템의 숫자


콕 시스템에서 대부분의 데이터 타입을 귀납 타입으로 표현한다. 콕 패키지는 이 데이터 타입에 대한 다양한 성질, 함수, 정리를 제공한다. Arith 패키지는 자연수(0부터 무한대)에 대한 많은 정리들을 포함하고 있다. 자연수는 O(0을 표현하는)과 S를 컨스트럭터로 하는 귀납 타입으로 기술한다.


Print nat.


Inductive nat : Set :=  O : nat | S : nat -> nat


덧셈, 곱셈, 뺄셈 (x - y에서 x가 y보다 작으면 0)도 제공한다. 이 패키지는 ring 전술을 제공하는데, 덧셈과 곱셈의 결합 규칙과 교환 법칙과 배분 법칙 하에 자연수 식들 간의 등식이 성립하는지 증명한다. 이 전술은 뺄셈은 처리하지 않는다. 그 이유는 자연수에 대한 뺄셈의 특별한 정의(역주: 위의 괄호 내용) 때문이다. 앞에서 이미 설명한바와 같이 자연수 구문에 대한 편리 기능이 있다. 예를 들어, 3은 S (S (S O))이다.


자연수를 귀납 타입으로 정의하면 자연수를 받는 재귀 함수를 정의할 수 있다. 재귀 함수 호출에 대한 제약이 있다. 주어진 인자의 바로 앞 숫자를 재귀함수 호출의 인자로 사용하는 그러한 함수를 쉽게 정의할 수 있을 것이다. 예를 들어, 팩토리얼 함수이다.


Fixpoint nat_fact (n:nat) : nat :=

    match n with O => 1 | S p => S p * nat_fact p end.


피보나치 함수의 정의다.


Fixpoint fib (n:nat) : nat :=

    match n with

       O => 0

    | S q => 

       match q with 

           O => 1

       |   S p => fib p + fib q

       end

    end.


ZArith 패키지는 정수를 표현하는 두 가지 데이터 타입을 제공한다. 양의 정수 (1부터 무한대)를 모델하는 이진 표현의 positive 귀납 타입과 세 개의 컨스트럭터(양의 정수, 음의 정수, 0을 구분하는)를 갖는 타입 Z이다. 이 패키지는 순서 개념과 덧셈, 뺄셈, 곱셈, 나눗셈, 루트와 같은 기본 연산을 제공한다. ring 전술은 정수에 대해서도 적용할 수 있다. 이번에는 뺄셈도 잘 지원한다. omega 전술은 nat 타입에 대한 선형식과 Z 타입의 선형식에 대해서도 잘 적용된다.


자연수가 아니라 정수를 가지고 작업하려면, 콕 시스템에게 모든 수에 관한 표기법을 정수에 관련된 표기법으로 해석하도록 요청하는 것이 편리하다. 다음 명령어를 사용한다.


Open Scope Z_scope.


타입 Z는 구조적 재귀에 적합하지 않다. 그래서 입력으로 양의 정수나 음의 정수를 받는 재귀 함수를 정의하는 것은 쉽지 않다. 이 문제를 해결하는 주요 방법은 [1]에서 설명한 기초가 튼튼한 재귀를 사용하는 것이다. 또다른 해결 방법은 반복자에 의존하는 것이다. 반복자는 동일한 연산을 주어진 횟수만큼 반복하는 연산이다. 횟수는 정수로 지정한다. 이 방법은 앞의 방법에 비해 강력하지는 않지만 이해하기 쉬운 장점이 있다. 이 반복자를 iter라 한다.


Check iter.

iter : Z -> forall A : Type, (A -> A) -> A -> A    


예를 들어, 팩토리얼 함수를 다시 정의해서 테스트해보자. 입력으로 한 쌍의 숫자를 받아 다시 한 쌍의 숫자를 반환하는 보조 함수를 사용한다. n과 n!을 입력하면 출력은 n+1과 (n+1)!이다. 이 함수를 iter의 입력으로 준다.


Definition fact_aux (n:Z) :=

  iter n (Z*Z) (fun p => (fst p + 1, snd p * (fst p + 1))) (0, 1).


Definition Z_fact (n:Z) := snd (fact_aux n).


Eval vm_compute in Z_fact 100.

93326...


iter로 정의한 함수의 성질을 증명하기 위해서 이 튜토리얼에서 설명한 내용으로 부족하다. 튜토리얼의 마지막에 관련 연습문제와 해를 제공한다.


이제부터 다시 자연수만 다루도록 돌아간다. 콕 시스템에게 다음 명령어를 주어 정수 표기법에 대한 규정을 해제한다.


Close Scope Z_scope.




===

번역


(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 : 귀납적 증명의 귀납적 경우


(6장)

datatype : 타입, 데이터 타입

Binary tree : 이진 트리

Internal Node : 내부 노드

Leaf : 끝 노드

Proof by Cases : 경우를 나누어 증명

Constructor : 컨스트럭터

Injective : 단사적


(7장)

Well-founded : 기초가 튼튼한(?)

Iterator : 반복자



Posted by lazyswamp :

6. 새로운 데이터 타입 정의하기


숫자, 부울값, 리스트는 모두 데이터 타입의 예이다. 프로그래밍할때 종종 새로운 데이터 타입이 필요하다. 그 데이터는 어떤 경우들을 모아놓은 것이고 각각의 경우에 해당하는 필드들을 가지고 있음을 표현한다.  콕 시스템은 이런 방식의 데이터 구성을 표현하는데 편리한 방법을 제공한다.


6.1 귀납 타입을 정의하기

여기에 귀납 타입을 정의하는 예가 있다.


Inductive bin : Type :=

   L : bin

| N : bin -> bin -> bin.


이것은 새로운 타입 bin을 만든다. bin의 타입은 Type이다. 이 bin 타입으로 두 가지 경우를 따르는 데이터를 표현한다. 첫번째 경우는 L로 표기하고 필드가 없다. 두번째 경우는 N t1 t2와 같이 쓰고 bin 타입의 두 개의 필드가 있다. 즉, bin 타입의 원소는 상수 L을 취하거나 N을 bin 타입의 두 객체에 적용하는 두가지 다른 방법으로 만들수 있다.


Check N L (N L L)

N L (N L L)

     : bin


이 bin 타입은 내부 노드나 끝 노드에 별도의 정보를 가지고 있지 않는 이진 트리를 포함한다.


데이터 타입 정의에 대한 연습문제


세 가지 경우를 표현하는 데이터 타입을 정의하시오.  상수, 세개의 필드(숫자, 지금 정의하고 있는 데이터 타입의 값 두 개)를 갖는 경우, 네개의 필드(부울값, 지금 정의하는 데이터 타입의 값 세 개)를 갖는 경우를 표현해야한다.


6.2 패턴 매칭

귀납 타입의 원소는 패턴 매칭을 하는 함수로 처리할 수 있다. 예를 들어 인자로 N L L이면 false를 그 외의 형태를 받으면 true를 반환하는 함수를 작성할 수 있다.


Definition example7 (t : bin): bool :=

   match t with N L L => false | _ => true end.


6.3 재귀함수 정의

귀납 데이터 타입이라면 어떠한 것에 대해서도 Fixpoint 명령어를 사용하여 재귀 함수를 정의할 수 있다. 하지만 자연수와 리스트에서 처럼 동일한 구조적 재귀 규칙을 반드시 따라야 한다. 즉, 오직 변수에 대해서만 재귀함수 호출을 할 수 있고 이 변수는 처음 주어진 인자에서 패턴 매칭을 통해 얻는 것이어야 한다. 다음은 우리가 새로 정의한 데이터 타입에 대한 재귀함수의 예제이다.


Fixpoint flatten_aux (t1 t2:bin) : bin :=

   match t1 with

       L => N L t2

   | N t'1 t'2 => flatten_aux t'1 (flatten_aux t'2 t2)

   end.


Fixpoint flatten (t:bin) : bin :=

   match t with

       L => L 

   | N t1 t2 => flatten_aux t1 (flatten t2))

   end.


Fixpoint size (t:bin) : nat :=

   match t with

       L => 1 | N t1 t2 => 1 + size t1 + size t2

   end.


사용자가 정의한 데이터 타입에 대한 구조적 재귀함수를 가지고 계산하는 것은 숫자와 리스트의 경우처럼 비슷하다.


6.4 경우를 나누어 증명

지금까지 우리가 도입한 귀납 타입에 대해 함수들을 정의해보았고, 이제 이 함수들의 성질을 증명할 수 있다. 첫번째 예제에서 bin 타입의 원소에 대한 경우 분석을 한다.


Lemma example7_size :

      forall t, example7 t = false -> size t = 3.


intros t; destruct t.


2 subgoals

  

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

   example7 L = false -> size L = 3


subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3


전술 destruct t는 t에 대한 귀납 타입의 정의에 따라 다양한 경우를 따져본다. 식 t는 L로 만든 것일 수도 있고, N을 다른 트리 t1과 t2에 적용한 결과일 가능성도 있다. 따라서 이 전술을 쓰면 두 가지 목적 명제가 나온다. 


트리 L에 대해서 example7과 size의 결과 값을 알고 있다. 콕 시스템에게 요청해서 그것을 계산한다. 


simpl.


2 subgoals

  

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

   true = false -> 1 = 3


subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3


이 계산을 하면 example7 L이 true이므로 false이기를 기대하는 것과 다름을 발견한다. 아래의 전술로 이런 비일관성을 다룬다. 


intros H.


2 subgoals

  

  H : true = false

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

   1 = 3


subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3



discriminate H.


1 subgoal

  

  t1 : bin

  t2 : bin

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

   example7 (N t1 t2) = false -> size (N t1 t2) = 3


그 결과 첫번째 목적 명제를 증명했다. discriminate H 전술은, 가정 H가 귀납 타입에서 두 개의 다른 컨스트럭터[역주: bin 타입의 컨스트럭터는 L과 N이다.]가 같은 값을 반환한다고 선언할 때 사용할 수 있다. 그런 가정은 일관성이 없고, 이 전술은 이 일관성을 직접 이용해서 이러한 경우는 결코 일어날 수 없음을 표현한다. 


귀납 타입의 컨스트럭터는 단사적이다는 또다른 중요한 성질이 있다. 이것에 대해서는 나중에 6.6절에서 설명한다. 


두번째 목적 명제에 대해서도 t1과 t2의 값에 대해 경우 분석을 해야 한다. 자세한 증명은 생략한다. 다음에 나열한 전술들을 사용하여 완료할 수 있다. 


destruct t1.


2 subgoals

  

  t2 : bin

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

   example7 (N L t2) = false -> size (N L t2) = 3


subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3


destruct t2.


3 subgoals

  

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

   example7 (N L L) = false -> size (N L L) = 3


subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3


첫번째 목적 명제에 있는 함수를 계산하도록 콕 시스템에 요청한다.


simpl.


3 subgoals

  

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

   false = false -> 3 = 3


subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3


함축의 오른편이 참이므로 콕 시스템은 자동으로 이것을 증명할 수 있다. 전술 테이블을 참조해서 더 기초적인 방법으로 증명하려면 intro와 reflexivity 전술을 차례로 사용할 수 있다.


auto.


2 subgoals

  

  t2_1 : bin

  t2_2 : bin

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

   example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3


subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3


intros H; discriminate H.

intros H; discriminate H.

Qed.


6.5 귀납적 증명

귀납 타입에 대한 가장 일반적인 증명이 귀납적 증명이다. 이 방법으로 귀납 타입 원소에 대한 성질을 증명할때 사실 우리는 각 컨스트럭터로 분류되는 경우를 따지고 있는 것이다. 마치 경우 분석에서 했던 것 처럼 말이다. 물론 변형된 부분도 있다. 귀납 타입의 인자를 갖는 컨스트럭터를 다룰때 이러한 인자에 대해서 증명하려고 하는 성질이 성립한다고 가정할 수 있다.


목적 지향적인 증명을 할때 elim 전술로 귀납 원리를 사용한다. 이 전술을 설명하기 위해 flatten_aux와 size 함수에 대한 간단한 사실 명제를 증명할 것이다.


Lemma flatten_aux_size : 

   forall t1 t2, size (flatten_aux t1 t2) = size t1 + size t2 + 1.


induction t1.


2 subgoals

  

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

   forall t2 : bin, size (flatten_aux L t2) = size L + size t2 + 1


subgoal 2 is:

 forall t2 : bin,

 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1


두 개의 목적 명제가 생기는데, 첫번째는 flatten_aux의 첫번째 인자가 L일때, 두번째는 N t1_1 t1_2일때 보조 정리의 명제를 증명하는 것이다. 두 함수의 정의를 사용하면 증명을 쉽게 진행할 수 있다. 콕 시스템에서 simple 전술을 사용한다. 얻은 결과는 ring 전술로 해결한다.


intros t2.

simpl.


2 subgoals

  

  t2 : bin

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

   S (S (size t2)) = S (size t2 + 1)


subgoal 2 is:

 forall t2 : bin,

 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1


ring.


1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

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

   forall t2 : bin,

   size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1


두번째 목적 명제를 증명할때, t1_1과 t1_2에 대한 귀납 가정을 사용할 수 있다. 다시 한번 size와 flatten_aux 함수를 호출한 결과 값을 콕 시스템으로 하여금 계산하도록 명령을 내릴 수 있다. 그 다음 귀납 가정을 사용할 수 있다.


intros t2; simpl.


1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size (flatten_aux t1_1 (flatten_aux t1_2 t2)) =

   S (size t1_1 + size t1_2 + size t2 + 1)


rewrite IHt1_1


1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size t1_1 + size (flatten_aux t1_2 t2) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)



rewrite IHt1_2


1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size t1_1 + (size t1_2 + size t2 + 1) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)


ring.

Proof completed.

Qed.



flatten과 size에 대한 연습문제


Lemma flatten_size : forall t, size (flatten t) = size t.


flatten_aux_size 보조 정리를 사용하되 apply 전술이나 rewrite 전술을 함께 고려해야 한다.


6.6 injection 전술을 사용하는 예제

이번에는 injection 전술을 사용하는 증명의 예를 설명한다. 어떠한 트리도 자신의 부분을 구성할 수 없음을 증명한다.


Lemma not_subterm_self_l : forall x y, ~ x = N x y.


1 subgoal

  

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

   forall x y : bin, x <> N x y


이 목적 명제에 등식의 부정을 _ <> _로 표시함을 볼 수 있다. x에 대한 귀납적 증명을 한다.


induction x.


2 subgoals

  

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

   forall y : bin, L <> N L y


subgoal 2 is:

 forall y : bin, N x1 x2 <> N (N x1 x2) y


첫번째 목적 명제는 이 귀납 타입의 두 컨스트럭터가 다르다는 것이다. discriminate 전술을 사용한다. 첫번째를 해결하고 두번째 목적 명제를 보자.


intros y; discriminate.


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

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

   forall y : bin, N x1 x2 <> N (N x1 x2) y


이 목적 명제의 결론이 부정 형태이므로 전술 테이블을 참고해서 해당하는 전술을 선택할 수 있다. 이 예에서, 사실 명제의 부정은 이 사실 명제는 False를 함축한다라는 함수로 표현할 수도 있음을 보여준다. 


intros y abs.


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

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

   False


가정 abs는 N x1 x2와 N (N x1 x2) y가 동등함을 표현한다. 컨스트럭터 N은 두 인자에 대해 단사적이어서 x1이 N x1 x2와 같다는 것을 함축한다. 이러한 유추 과정을 injection 전술로 표현한다.


injection abs.


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

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

   x2 = y -> x1 = N x1 x2 -> False


그 결과 두 개의 등식이 함축의 전제로 이 목적 명제의 결론에 도입되었다. 이 등식들을 새로운 가정으로 도입할 수 있다. 


intros h2 h1.


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

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

   False


가정 h1과 IHx1(을 사례화 시킨 명제)는 서로 모순이다. 다음 전술로 이것을 표현한다.


assert (IHx1' : x1 <> N x1 x2).


2 subgoals

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

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

   x1 <> N x1 x2


subgoal 2 is:

 False


   apply IHx1.


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

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

   False


case IHx1'.


[역주: IHx1'이 true와 false 경우 분석. true 경우는 False 결론을 낼 수없으므로 쉽게 배제. 남은 경우는 IHx1' = false.] 


1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

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

   x1 = N x1 x2


exact h1.


Proof completed.


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 : 귀납적 증명의 귀납적 경우


(6장)

datatype : 타입, 데이터 타입

Binary tree : 이진 트리

Internal Node : 내부 노드

Leaf : 끝 노드

Proof by Cases : 경우를 나누어 증명

Constructor : 컨스트럭터

Injective : 단사적





Posted by lazyswamp :

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 :

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 :

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 :

2. 콕으로 프로그래밍하기


콕 시스템에서 프로그램은 보통 함수로 표현한다. 프로그램이 간단하면 이 시스템 자체에서 실행할 수 있고, 더 복잡하다면 일반적인 프로그래밍언어로된 프로그램으로 변환하여 시스템 밖에서 실행할 수도 있다.


2.1 상수 정의


키워드 Definition으로 상수를 새로 정의할 수 있다. 예를 보자.


Definition example := fun x : nat => x*x + 2*x + 1.


동일하지만 이렇게도 정의할 수 있다.


Definition example1 ( x : nat) := x*x + 2*x + 1.


이 명령어들을 실행한다음 다른 명령어로 이 함수를 다뤄볼수 있다.


Check example1.

example1 : nat -> nat


Eval compute in example1 1.

= 4 : nat


어떤 경우에는 이전에 만들었던 정의를 없애고 싶을수가 있다. Reset 명령어로 정의한 이름을 주면 가능하다. 정의한 내용을 보고싶으면 Print 명령어를 사용한다. Coqide나 Proof-General 같은 특별한 환경을 사용하고 있다면 작업창 상단의 화살표로 문서의 이곳 저곳으로 실행 포인트를 이동할수 있다.


2.2 부울 조건식

콕에 미리 정의되어있는 타입으로 부울값의 타입이 있다. true와 false 두가지 값을 갖는다. 부울식을 제대로 사용하려면 Bool 라이브러리를 불러야한다. 부울 곱, 합, 부정 등의 정의를 사용할수 있다.


Require Import Bool.


부울값은 if...then...else... 구문으로 검사할수 잇다.


Eval compute in if true then 3 else 5.

= 3 : nat


이 타입과 연관되어 사용할 수 있는 함수로 무엇이 있는지 알고 싶다면 Search나 SearchAbout 명령어를 사용할수 잇다. Search 명령어를 사용한 예를 보자.


Search bool.

false: bool

true: bool

xorb: bool -> bool -> bool

orb: bool -> bool -> bool

negb: bool -> bool

implb: bool -> bool -> bool

ifb: bool -> bool -> bool -> bool

eqb: bool -> bool -> bool

andb: bool -> bool -> bool



2.3 자연수로 계산하기

자연수의 타입도 콕에 준비되어있다. 이 타입을 제대로 사용하려면 역시 Arith 라이브러리를 불러야한다.


Require Import Arith.


자연수는 0부터 무한대까지의 숫자들이다. 자연수 나름의 조건식을 구성하는 방법이 있다. 모든 자연수를 0 또는 어떤 자연수 p의 그 다음 S p로 표현하는 아이디어를 이용한다. 즉, 1은 S 0, 2는 S (S 0)가 된다.


이런 방식에서는 모든 자연수가 0이거나 다른 수의 다음으로 두가지 경우로 나눌수 있다. 이런 구분 방식으로 함수로 작성하면 다음과 같다. 이 함수는 인자가 오직 0인 경우에만 true를 반환한다.


Definition is_zero (n : nat) := 

   match n with

     0 => true

   | S p => false

   end.


match ... with ... end 식을 패턴매칭 구문이라고 부른다. 이 식을 계산한 결과는 n의 패턴에 달려있다. 0의 패턴이면 true이고, S p 패턴에 맞으면 false가 된다. S p 패턴에서 기호 S는 무엇의 다음이라는 개념을 뜻하는데 만일 n이 S p 패턴과 일치하면 다음과 같이 직관적으로 해석할 수 있다. n은 어떤 수의 다음에 위치한 수다. 패턴에 나타난 p는 일종의 지역변수로 그 "어떤 수"를 받는다. 화살표 => 오른편의 식에 p를 자유롭게 사용할 수 있다.


패턴매칭은 자연수로 계산할때 자주 사용한다. 예를 들어, 콕 시스템에서 제공하는 pred 함수는 0보다 큰 자연수를 그 전에 위치하는 수로, 0은 0으로 매핑한다.


Print pred.

pred = fun n : nat =>

   match n with | 0 => n | S u => u end

        : nat -> nat


Argument scope is [nat_scope]


pred 함수는 패턴매칭 구문을 사용해서 S u 형태의 수는 u로, 0은 0으로 매핑하는 것을 표현한다.


자연수로 계산할때 재귀 형태가 흔히 나타난다. 패턴매칭을 사용하는 함수를 정의할때 이 함수에 인자의 이전 숫자를 주어 사용하는 것이 가능하다. 콕은 재귀 방식으로 정의된 것을 매우 조심스럽게 다루기 때문에 특별한 키워드를 함께 사용해야한다. Fixpoint 키워드이다. 두 자연수를 더하는 재귀함수의 예를 보자.


Fixpoint sum_n n :=

   match n with

       0 => 0

   | S p => p + sum_n p

   end.


재귀함수를 정의할때 구조적 재귀라는 제약을 고려해야한다. 재귀함수를 호출하려면 원래 인자의 부분식만을 인자로 취할수 있다. 더 정확히 말하자면, 재귀함수의 인자는 반드시 변수이고 패턴매칭을 통해서 원래 인자로부터 얻은 것이어야 한다. 이런 제약을 지키면 모든 계산이, 설사 재귀함수를 쓰더라도, 종료함을 보장할 수 있다. sum_n의 정의는 제대로된 형태를 갖추고 있다. 왜냐하면 원래 인자 n과 매치되는 S p 패턴의 변수 p만 사용하기 때문이다.


예를 들어, 구조적 재귀 제약을 지키지 않은 다음 정의는 사용할수 없다.


Fixpoint rec_bad n :=

   match n with 0 => 0 | S p => rec_bad (S p) end.

Error:

Recursive definition of rec_bad is ill-formed.

In environment

rec_bad : nat -> nat

n : nat

p : nat

Recursive call to rec_bad has principal argument equal to "S p" instead of

"p".

Recursive definition is:

"fun n : nat => match n with

                | 0 => 0

                | S p => rec_bad (S p)

                end".


여러개의 인자를 받는 재귀함수를 정의할수 있다. 이런 경우 이 인자들중 하나는 구조적 재귀 제약을 따라야 한다. 예를 들어 아래 함수는 합의 중간결과를 인자로 받아 첫번째 인자인 자연수를 누적해서 더한다. 첫번째 인자에 대해서 구조적 재귀 제약을 만족한다. 왜냐하면 재귀함수를 호출할 때 첫번째 인자 p는 원래 첫번째 인자 n을 패턴매칭해서 얻은 것이기 때문이다.


Fixpoint sum_n2 n s :=

   match n with

       0 => s

   | S p => sum_n2 p (p + s)

   end.


재귀함수를 정의할 때 부울 타입과 같이 다른 타입의 값을 반환하도록 정의할수도 있다. 자연수로 주어진 인자가 짝수인지 검사하는 함수가 그러한 예이다.


Fixpoint evenb n :=

   match n with

      0 => true

    | 1 => false

    | S (S p) => evenb p

   end.


이 예제에서 깊은 패턴매칭을 사용했고, 두가지 이상의 경우를 나열했다. 콕 시스템은 모든 경우를 커버하는지 검사하고 재귀함수호출에서 패턴매칭을 통해서 얻은 변수들을 인자를 사용하는지를 검사할 것이다.


2.4 리스트로 계산하기

같은 타입의 데이터를 리스트로 모아 다룰 수 있다. 물론 리스트를 사용하기 위해 필요한 라이브러리를 불러야한다.


Require Import List.


여러 원소를 모아 하나의 리스트를 만드려면 두개의 콜론 ::으로 구분해서 차례로 나열하고 맨끝에 ::nil을 둔다.


Check 1::2::3::nil.

1 :: 2 :: 3 :: nil

      : list nat


:: 표기법은 어떤 리스트 앞에 요소를 추가함을 뜻한다. nil은 원소가 없는 리스트이고, 3::nil은 원소가 오직 3을 가지고 있고, 2::3::nil은 3만 포함하는 리스트 앞에 2를 붙인 리스트다.


nil은 콕 시스템에서 특별하게 사용된다. 왜냐하면 사용되는 문맥에 따라 다르게 사용될 수 있기 때문이다. 요소를 포함하는 리스트에서는 이 원소와 동일한 타입에 대한 비어있는 리스트를 표현한다. 하지만 nil을 그 자체로만 쓰면 콕 시스템은 문맥을 판단하지 못해 적절히 해석하는데 어려움에 처하게 된다(콕 시스템의 버전에 따라 다름).


Check nil.

Error: Cannot infer the implicit parameter A of nil.


또는

nil

      : list ?1


이런 문제가 발생하면 nil을 사용할때 의도하는 문맥을 타입으로 콕 시스템에게 알려주어 해결할 수 있다.


Check (nil : list nat).

nil:list nat

    : list nat


리스트를 다루는 몇가지 함수들을 콕 시스템에서 제공한다. 리스트 붙이기 함수 app (보통 ++로 사용), 함수를 받아 리스트의 각각의 원소에 적용하는 함수 map 등이 있다.


Eval compute in map (fun x => x + 3) (1::3::2::nil).

= 4 :: 6 :: 5 :: nil : list nat


Eval compute in map S (1::22::3::nil).

= 2 :: 23 :: 4 :: nil : list nat


Eval compute in

   let l := (1::2::3::nil) in l ++ map (fun x => x + 3) l.

= 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: nil : list nat


리스트, map, app에 대한 연습문제

숫자 n을 입력받아 0부터 n-1까지 n개의 원소로 된 리스트를 반환하는 함수를 정의하시오.


리스트의 원소를 다룰때 패턴매칭 식을 사용한다. 자연수에 대한 패턴매칭과 유사하다. 리스트는 비어있거나 다른 리스트 앞에 원소를 갖는 두가지 경우로 분류할 수 있다. 두번째의 경우에 패턴매칭 식으로 리스트의 첫번째 원소와 나머지 리스트에 이름을 붙일 수 있다. 다음 예를 살펴보자. 인자로 주어진 리스트가 적어도 원소를 하나 포함하고 있고 첫번째 원소가 짝수이면 true를 반환하는 함수이다.


Definition head_evb l :=

   match l with nil => false | a::tl => evenb a end.


리스트에 대한 재귀함수를 정의할 수도 있다. 자연수를 다룰때와 동일하게 구조적 재귀 제약을 따라야 한다. 재귀함수 호출은 인자 리스트에서 직접적으로 얻은 부분리스트만 인자로 취할 수 있다. 리스트의 원소를 모두 더하는 예를 보자.


Fixpoint sum_list l :=

   match l with nil => 0 | n::tl => n + sum_list tl end.


마지막 예로, 자연수 리스트를 정렬하는 함수를 작성해보자. 두 자연수를 비교해서 부울값을 반환하는 함수 leb를 사용한다. 콕 시스템에서 제공한다.


Fixpoint insert n l :=

   match l with

       nil => n :: nil

   | a::tl => if leb n a then n::l else a ::insert n tl

   end.


Fixpoint sort l :=

   match l with

       nil => nil

   | a::tl => insert a (sort tl)

   end.


간단하게 테스트해보자.


Eval compute in sort (1::4::3::22::5::16::7::nil).

= 1 :: 3 :: 4 :: 5 :: 7 :: 16 :: 22 :: nil

     : list nat



정렬에 대한 연습문제

리스트를 인자로 받아 원소의 수가 2미만이거나 첫번째 원소가 두번째 원소보다 작을 때 true를 반환하는 함수를 작성하시오. 그 다음 역시 리스트를 인자로 받아 정렬되었는지 검사해서 true를 반환하는 함수를 작성하시오.


카운팅에 대한 연습문제

콕 시스템에서 제공하는 함수 beq_nat으로 두 자연수를 비교할수 있다. 이 함수를 이용하여 count_list를 작성하시오. 인자로 자연수와 리스트를 받아 이 자연수가 리스트 원소로 몇번 나타나는지 세어 그 횟수를 반환한다.


===

번역


(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 : 부분리스트

Posted by lazyswamp :

Coq 증명기(http://coq.inria.fr/)는 수학과 알고리즘을 형식화해서 표현하고 여러 성질을 증명하는 도구입니다. 


Coq 증명기가 무엇인지 궁금하거나 배워보고 싶은 분들이 참고 할 수 있는 Yves Bertot의 "Coq in a Hurry"를 번역했습니다. 1장~8장까지 별도의 글로 나누어 올려놓았고, 9장과 10장은 연습문제와 해답으로 번역에서 제외했습니다.


특히, 프로그래밍언어, 정형기법, 논리, 컴파일러를 전공하거나 관심을 두신 분들이 이 글의 독자가 될 수 있을 것으로 생각합니다.


새로운 프로그래밍언어를 배울때 가장 좋은 방법은 자신만의 문제를 하나 선택해서 스스로 풀어보는 것이지요. 저도 이 글을 읽고 번역한 다음, 텍스트 패턴 매칭에 대한 어떤 성질을 증명해보고 있습니다. 좌충우돌... 그럼에도 불구하고 Coq에 조금씩 적응하고 있구나 하는 생각이 듭니다. Coq을 처음 배운다면 구문이 생각나지 않을 수 있고, 증명하는데 적절한 전술이 무었일까 답답할 수도 있습니다. 이런 경우 1장~8장을 뒤적이면 유용한 답을 찾을 수 있을 것입니다. 특히 초보자에게 가장 도움이 되는 부분은 3장이 아닐까 생각합니다.


마지막으로, 글쓰기도 어렵지만 번역은 더 어렵네요. 글을 읽으시다 잘 이해가 가지 않는 문장이 있으면 틀림없이 번역에 문제가 있을 것으로 추측됩니다. 잘못된 번역, 더 매끄러운 번역이 생각나시면 언제든지 댓글을 달아주세요. 


2014년 7월, 최광훈.



[원문]

Coq in a Hurry (Yves Bertot, April 2010)

 - http://cel.archives-ouvertes.fr/docs/00/47/58/07/PDF/coq-hurry.pdf




콕, 빨리 빨리 - 이브 베르토


이 글에서 콕 시스템을 간단히 소개하고 논리적 개념과 함수를 정의하고 추론하는 법을 일러준다. 일종의 튜토리얼이고, 독자들은 이 시스템의 몇가지만을 배워 하고싶은 것을 빨리 실험해볼 수 있다. 더욱 자세히 배우고 싶다면 참고문헌 [1]을 보면 된다. 특히 방대한 연습문제가 있어 훈련하기에 좋다.



 참고 문헌



[1] Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Devel- opment, Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.


[2] The Coq development team. The Coq proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2004. http://coq.inria.fr/doc/ main.html 


목차

 1. 식과 논리식

 2. 콕으로 프로그래밍하기

 3. 명제와 증명

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

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

 6. 새로운 데이터 타입 정의하기

 7. 콕 시스템의 숫자

 8. 귀납적 성질

 9. 연습문제 (원문 참고)

 10. 해답 (원문 참고)



1. (계산?)식과 논리식


콕 시스템은 일종의 언어를 제공한다. 이 언어로 논리식을 다루고, 구문 형태를 살피고, 증명하기도 한다. 논리식은 함수를 사용하여 구성하기도 하고, 제한된 형태지만 이 함수들을 가지고 계산도 한다.


1.1 바른 식 쓰기


먼저 식이 제대로 된 형태인지 검사하는 법을 배울 필요가 있다. 이 명령어는 Check이다. 몇가지 예를 들어보자. 이 시스템의 기초적인 객체와 타입을 두세가지 사용한다. 명령어는 항상 점으로 끝난다. 이제부터 사용자가 콕 시스템에 보내는 글은 이런 스타일이고, 이 시스템에서 응답하는 내용은 이런 스타일이다. 


Check True.

True : Prop


Check False.

False : Prop


Check 3.

3 : nat


Check (3+4).

3 + 4 : nat


Check (3=5).

3=5 : Prop


Check (3,4).

(3,4) : nat * nat


Check ((3=5)/\True).

3 = 5 /\ True : Prop


Check nat -> Prop

nat -> Prop : Type


Check (3 <= 6).

3 <= 6 : Prop


두가지 목적으로 A : B 표기법을 사용한다. 식 A의 타입이 식 B이다거나 A는 B의 증명임을 나타낸다. 우리가 입력하는 식에서도 이 표기법을 사용할 수 있다. 보통 어떤 식의 타입을 분명히 드러내고자할때 그렇다. 


Check (3,3=5):nat*Prop

(3,3=5):nat * Prop

       : nat * Prop


이 식들 중 어떤 것은 논리 명제로 읽고 (즉  Prop 타입을 가지고) 또 어떤 것은 숫자로 읽고(nat 타입을 갖고), 다른 것은 더 복잡한 자료구조의 원소로 읽기도 한다. 물론 제대로 형태를 갖추지 못한 식도도 검사해볼수 있다. 이 경우 콕 시스템은 에러문을 출력해 문제점을 설명해줄것이다.


복잡한 식을 구성하려면 명제들을 논리 연결자들로 조합하거나 덧셈, 곱셈, 쌍만들기 등으로 식들을 구성하면된다. 키워드 fun을 사용해서 새로운 함수도 만들수 있다. 람다계산법과 같은데에서 lambda 기호대신 쓴다. Check 명령어로 함수를 검사하면 nat 타입의 숫자 x를 입력으로 받아 x가 3과 같다는 명제를 리턴한다고 설명해준다. 그 다음 Check 명령어에서 검사하는 논리명제는 모든 자연수 x에 대해 x는 3보다 작거나 또는 자연수 y가 존재해서 x=y+3이다.


Check (fun x:nat => x=3).

fun x : nat => x = 3 : nat -> Prop


Check (forall x:nat, x<3 \/ (exists y:nat, x=y+3)).

forall x:nat, x<3 \/ (exists y:nat, x=y+3) : Prop


이번에는 let을 사용하는 식을 살펴보자. 식에 임시 이름을 부여할 때 유용하다. 예제에서 let으로 이름을 붙인 식은 숫자를 입력받아 숫자의 쌍을 반환하는 함수다. 함수 f를 어떤 값, 예를 들어 3에 적용하는 표기 방법도 보여준다. 단순히 함수 이름 f와 인자 3을 나란히 쓰면된다. 보통 수학에서 하던것과 달리 인자를 감싸는 괄호를 항상 쓰지 않아도 된다. 


Check (let f := fun x => (x * 3, x) in f 3).

let f := fun x : nat => (x * 3, x) in f 3 : nat * nat 


어떤 표기법은 다용도로 사용된다. 예를 들어, * 기호는 곱셈을 표시하기도 하고 타입에서 곱을 표시하기도 한다. Locate 명령어로 표기법이 의미하는 함수를 찾을 수 있다.


Locate "_ <= _".

Notation Scope

"x <= y" := le x y : nat_scope

                    (default interpretation)


텀의 형태가 제대로 되려면 두가지 조건을 갖춰야한다. 정해진 구문을 따라야한다. 예를 들어, 열린괄호와 닫힌괄호의 쌍이 맞아야 하고 두개의 피연산자를 요구하는 연산자에게는 그렇게 인자가 주어져야한다. 두번째 조건은 타입에 맞게 식을 구성해야한다. Check 명령어는 식이 제대로 구성되었는지 검사도 하고 식의 타입을 알려주기도한다. 예를 들어 어떤 식이 제대로 되었는지 차근차근 단계별로 확인할 수 있다.


Check True.

True : Prop


Check False.

False : Prop


Check and.

and : Prop -> Prop -> Prop


Check (and True False).

True /\ False : Prop


마지막 예에서 and는 Prop 타입의 인자를 받아 Prop -> Prop 타입의 함수를 반환하는 함수다. 따라서 Prop 타입의 True에 적용할 수 있다. 그 결과 반환되는 함수는 또다른 Prop 타입의 인자를 기대하고 False에 적용할 수 있다. 표기법 a -> b -> c는 사실

a -> (b -> c)이다. 표기법 f a b는 사실 (f a) b 이다.


그리고 /\는 피연산자들 가운데에 연산자를 배치하는 인픽스 표기법을 따른다. Locate 명령어로 확인할 수 있다.



2. 식을 계산하기


콕 시스템으로 식을 계산할 수도 있다. 기호 계산 방식을 사용하는데, 여러가지 전략이 있다. compute라고 부르는 전략은 다음과 같이 사용한다.


Eval compute in 

   let f := fun x => (x * 3, x) in f 3.

= (9, 3) : nat * nat


이 명령어를 실행한 뒤에는 함수 f가 사라진다. 이 식을 계산할 때 임시로 정의되고 f 3을 계산할 때 사용될 뿐이다.


함수에 관한 연습문제 (참고문헌 [1]의 연습문제 2.5) 다섯개의 인자를 받아 그 합을 반환하는 함수를 작성하고, Check 명령어로 제대로된 형태로 작성했는지 확인한 다음, Eval 명령어로 샘플 값들을 주어 계산해보시오.  연습문제에 대한 답은 모두 이 글의 마지막에 제공한다.




===

번역


Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태



Posted by lazyswamp :