Coq를 이용한 퀵소트 증명

나는 Coq 시스템을 이용한 퀵 소트 알고리즘의 프로그램 검증에 대한 논문을 쓰고있다. 나는 Coq에서 quicksort를 정의했다. 그러나 나의 상사와 나 자신은 전술을 사용하여 실제 증거를 쓰는 것을 매우 편안하게 생각하지 않는다. coq 증명의 해당 부분을 도울 수있는 사람이 있습니까? 다음은 우리가 지금까지 함께 온 것입니다 : 내가 증명 알고Coq를 이용한 퀵소트 증명

Inductive nat : Type := 
    | O : nat 
    | S : nat -> nat. 

Check (S (S (S (S O)))). 

Definition isZero (n:nat) : bool := 
    match n with 
    O => true 
    |S p => false 
    end. 

Inductive List: Set := 
| nil: List 
| cons: nat -> List -> List. 

Fixpoint Concat (L R: List) : List := 
match L with 
| nil => R 
| cons l ls => cons l (Concat ls R) 
end. 

Fixpoint Less (n m:nat) := 
    match m with 
    O => false 
    |S q => match n with 
      O => true 
     |S p => Less p q 
     end 
    end.  

Fixpoint Lesseq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => false 
      |S q => Lesseq p q 
      end 
    end. 

Fixpoint Greatereq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => true 
      |S q => Greatereq p q 
      end 
    end. 


Fixpoint Allless (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Less n m with 
       false => Allless ls n 
       |true => cons m (Allless ls n) 
       end 
end.    

Fixpoint Allgeq (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Greatereq n m with 
       false => Allgeq ls n 
       |true => cons m (Allgeq ls n) 
       end 
end. 

Fixpoint qaux (n:nat) (l:List) : List := 
    match n with 
    O => nil 
|S p => match l with 
     nil => nil 
     |cons m ls => let low := Allless ls m in 
        (let high := Allgeq ls m in 
        Concat (qaux p low) (cons m (qaux p high))) 
     end 
end. 

Fixpoint length (l:List) : nat := 
match l with 
    nil => O 
|cons m ls => S (length ls) 
end. 

Fixpoint Quicksort (l:List) : List := qaux (length l) l.

우리가 보조 정리하거나 정리를 필요로하지만 나는 그 후 어디서부터 시작 모르겠습니다 일. 도움을 주셔서 감사합니다 :)

출처

2012-04-07 user1319321

당신이 코드에 대해 증명할 수있는 많은 훌륭한 theorems 있습니다.

숫자와 목록을 목록의 숫자 색인에 매핑하는 pos 함수를 정의하십시오.
목 1
: S에서 B 모두 나열 S의 경우, 및, (a < = b) < -> (a (정렬 S를 POS)) < = (포스 B (정렬 S)). 이것은 정렬 함수에 대한 정확성 정리 일 것입니다.
토륨 2 (정렬 (정렬들)) = 정렬 S
토륨 3 최소리스트의 최대 요소 S.을 찾는 기능 최소 및 최대 정의 다음 분류 된리스트의 최소한의 소자의 POS 0
토륨 4 : 정렬 된리스트의 역방향의 최대 요소의 POS는 0

이다,

요약 정렬 루틴에서 술어를 추출하여 인수로 전달할 수 있습니다.

목 5 : 그 (일종의 < = S)를보기 =이 무한히 계속 될 수

등 ((종류> = S) 역). 그것은 많은 재미입니다. :-)

출처

2012-04-10 16:46:15

"기호 테스트"의 문제점으로 문제점을보십시오. 출력이 정확한지 테스트 한 다음 초기 코드와 테스트 함수의 모든 조합이 의도 한대로 작동 함을 보여주는 함수를 작성하십시오.

다음은 데이터 유형의 정렬 알고리즘에 대한 필자가 가장 좋아하는 테스트 기능입니다.

Lemma Quicksort_sorted : forall l, sorted (Quicksort l) = true.

을하지만 당신은 주를 증명에 도착하기 전에 많은 중간 보조 정리를 증명해야합니다 :

Fixpoint sorted (l : List) : bool := 
    match l with cons a l' => 
    match l' with cons b l'' => 
     if Lesseq a b then sorted l' else false 
    | nil => true 
    end 
    | nil => true 
    end.

당신은 다음과 같은 방법으로 증거를 시작할 수 있습니다. 따라서 공식적인 증명은 테스트의 전체 범위를 보장한다는 점을 제외하고는 테스트와 정말 같습니다.

출처

2012-11-09 09:17:19 Yves

Coq를 이용한 퀵소트 증명

답변

관련 문제