기본적 아이디어는 보행을 함수형 언어의 리스트와 같은 재귀적인 데이터타입으로 정의한 후 구조적 귀납을 사용하는 것... 입니다만 역시 직접 해보면 말처럼 간단하지는 않네요. 일단 Coq로 첫 번째 파트만 증명해 봤습니다. 


------------------------------------------


Require Export Classical_Prop.

Require Export Nat.

Require Export List.

Import ListNotations.


Record Graph : Type :=

{ V : nat -> Prop ;

  E : forall m n : nat,

    V m -> V n -> Prop }.


Inductive Walk (G : Graph) : nat -> nat -> Prop :=

| Wrefl : forall m : nat, G.(V) m -> Walk G m m

| Wstep : forall k m n : nat, 

  forall Hk : G.(V) k, forall Hm : G.(V) m,

  G.(E) k m Hk Hm -> Walk G m n -> Walk G k n.  


Inductive Path (G : Graph) : list nat -> nat -> nat -> Prop :=

| Prefl : forall m : nat, G.(V) m -> Path G [m] m m

| Pstep : forall k m n : nat, forall l : list nat,

  forall Hk : G.(V) k, forall Hm : G.(V) m,

  G.(E) k m Hk Hm -> ~ In k l -> 

  Path G l m n -> Path G (cons k l) k n.


Theorem ShorterPath (G : Graph) : 

  forall l : list nat, forall m n : nat, Path G l m n -> 

  forall k : nat, In k l -> exists l' : list nat, Path G l' k n.

Proof.

  intros l m n H0. induction H0.

  intros k H1. inversion H1.

  exists [m]. subst. apply Prefl. 

  apply H. inversion H0.

  intros j H2. inversion H2.

  subst. exists (j :: l).

  apply (Pstep G j m n l Hk Hm H H0 H1).

  apply (IHPath j H3).

Qed.


Theorem WalkImpliesPath (G : Graph) (m n : nat) :

  Walk G m n -> exists l : list nat, Path G l m n.

Proof.

  intro H0. induction H0. 

  exists [m]. apply Prefl. apply H.

  inversion IHWalk as [l H1].

  destruct (classic (In k l)).

  apply (ShorterPath G l m n H1 k H2).

  exists (k :: l).

  apply (Pstep G k m n l Hk Hm H H2 H1).

Qed.


------------------------------------------


편의를 위해 정점의 집합은 자연수의 부분집합으로 정의했습니다. 다른 정의로 증명을 포팅하는 것도 그리 어렵지는 않을 듯.