두 Coq 유도 유형의 크기가 감소하는 것을 나타내는 방법

Question

조합 게임에 대해 유도 유형을 정의하려고합니다. 두 게임이 lessOrEq, greatOrEq, lessOrConf 또는 greatOrConf인지 비교하는 방법을 원합니다. 두 게임이 모두 lessOrEq과 greatOrEq이면 동등한 지 확인할 수 있습니다. 나는이 수표를 만들기위한 상호 재귀 적 방법을 정의 할 때

는하지만, 내가 얻을 :

Error: Cannot guess decreasing argument of fix .

나는이 생각하기 때문에 하나의 게임이나 각 재귀 호출과 크기가 다른 감소 (하지만 모두). 이것을 Coq에 어떻게 표시 할 수 있습니까?

여기 내 코드가 있습니다. 실패하는 부분은 gameCompare, innerGCompare, listGameCompare, gameListCompare의 상호 재귀 적 정의입니다.

Inductive game : Set := 
| gameCons : gamelist -> gamelist -> game 
with gamelist : Set := 
| emptylist : gamelist 
| listCons : game -> gamelist -> gamelist. 

Definition side := 
game -> gamelist. 

Definition leftSide (g : game) : gamelist := 
match g with 
    | gameCons gll glr => gll 
end. 

Definition rightSide (g : game) : gamelist := 
match g with 
    | gameCons gll glr => glr 
end. 

Inductive compare_quest : Set := 
| lessOrEq : compare_quest 
| greatOrEq : compare_quest 
| lessOrConf : compare_quest 
| greatOrConf : compare_quest. 

Definition g1side (c : compare_quest) : side := 
match c with 
    | lessOrEq => leftSide 
    | greatOrEq => rightSide 
    | lessOrConf => rightSide 
    | greatOrConf => leftSide 
end. 

Definition g2side (c : compare_quest) : side := 
match c with 
    | lessOrEq => rightSide 
    | greatOrEq => leftSide 
    | lessOrConf => leftSide 
    | greatOrConf => rightSide 
end. 

Definition combiner := 
Prop -> Prop -> Prop. 

Definition compareCombiner (c : compare_quest) : combiner := 
match c with 
    | lessOrEq => and 
    | greatOrEq => and 
    | lessOrConf => or 
    | greatOrConf => or 
end. 

Definition nextCompare (c : compare_quest) : compare_quest := 
match c with 
    | lessOrEq => lessOrConf 
    | greatOrEq => greatOrConf 
    | lessOrConf => lessOrEq 
    | greatOrConf => greatOrEq 
end. 

Definition cbn_init (cbn : combiner) : Prop := 
~ (cbn False True). 

Fixpoint gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop := 
innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) 
with innerGCompare (next_c : compare_quest) (cbn : combiner) 
     (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop := 
cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s) 
with listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop := 
match g1s with 
    | emptylist => cbn_init cbn 
    | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2) 
end 
with gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop := 
match g2s with 
    | emptylist => cbn_init cbn 
    | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr) 
end. 

Definition game_eq (g1 : game) (g2 : game) : Prop := 
(gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2). 

Answer 1

이 문제를 해결하기 위해 할 수있는 일이 몇 가지 있습니다. 나는 당신의 코드가 무엇을하려고 하는지를 정말로 이해할 수 없었다. 그래서 아마 내가 언급하려고하는 것보다 이것을 할 수있는 더 효율적인 방법이있을 것이다.

당신이 할 수있는 한 가지는 gameCompare을 함수 대신에 (아마도 상호간에) 유도 관계로 정의하는 것입니다. 나는 당신이 Coq에 얼마나 익숙하지 않은지 잘 모르겠다. 그래서 대답은 너무 커야지만 자세히 설명하지는 않겠지 만 유도적인 관계는 gameCompare과 같은 개념을 정의 할 때 함수보다 훨씬 더 큰 유연성을 준다. 유도 관계를 정의하는 방법에 대한 자세한 내용은 Benjamin Pierce의 저서 Software Foundations을 참조하십시오.

이 접근법의 한 가지 단점은 함수와 달리 유도 관계가 실제로 아무것도 계산하지 않는다는 것입니다. 이로 인해 때로는 사용하기가 더 어려워집니다. 특히, 함수 호출을 단순화 할 수있는 것처럼 귀납적 인 명제를 단순화 할 수 없습니다.

문제에 쉽게 적용 할 수있는 또 다른 방법은 모든 재귀 호출에 따라 감소하는 함수에 "시간"숫자 매개 변수를 추가하는 것입니다. 이로 인해 함수는 거의 종료됩니다. 그런 다음 작동 시키려면 큰 "시간"매개 변수를 사용하여 초기 호출을 수행해야합니다. 다음은이 작업을 수행 할 수있는 방법의 예

Fixpoint gameSize (g : game) : nat := 
    match g with 
    | gameCons gl1 gl2 => 1 + gameListSize gl1 + gameListSize gl2 
    end 

with gameListSize (gl : gamelist) : nat := 
    match gl with 
    | emptylist => 1 
    | listCons g gl => 1 + gameSize g + gameListSize gl 
    end. 

Definition gameCompareTime (g1 g2 : game) : nat := 
    gameSize g1 + gameSize g2. 

Fixpoint gameCompareAux (time : nat) (c : compare_quest) (g1 : game) (g2 : game) : Prop := 
    match time with 
    | O => True 
    | S time => 
     compareCombiner c 
         (listGameCompare time 
             (nextCompare c) 
             (compareCombiner c) 
             (g1side c g1) 
             g2) 
         (gameListCompare time 
             (nextCompare c) 
             (compareCombiner c) 
             g1 
             (g2side c g2)) 
    end 

with listGameCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop := 
    match time with 
    | 0 => True 
    | S time => 
     match g1s with 
     | emptylist => cbn_init cbn 
     | listCons g1s_car g1s_cdr => cbn (gameCompareAux time c g1s_car g2) (listGameCompare time c cbn g1s_cdr g2) 
     end 
    end 

with gameListCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop := 
    match time with 
    | 0 => True 
    | S time => 
     match g2s with 
     | emptylist => cbn_init cbn 
     | listCons g2s_car g2s_cdr => cbn (gameCompareAux time c g1 g2s_car) (gameListCompare time c cbn g1 g2s_cdr) 
     end 
    end. 

Definition gameCompare c g1 g2 := 
    gameCompareAux (gameCompareTime g1 g2) c g1 g2. 

Definition game_eq (g1 : game) (g2 : game) : Prop := 
(gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2). 

gameCompareTime 기능은 gameCompareAux의 호출 트리의 깊이에 합리적인 바운드처럼 보인다 두 게임의 크기의 합을 계산합니다. innerGCompare을 인라인했습니다. 경계가 좀 더 쉽게 계산되므로주의해야합니다. 시간이 끝나면 (즉, 패턴 일치에서 0 개의 브랜치) 우리는 임의의 값 (이 경우 True)을 반환합니다. 왜냐하면 우리는 함수가 그 사건에 도달하기 전에 완료 할 수있는 충분한 시간을 주었기 때문입니다.

이 접근법의 장점은 구현하기가 상대적으로 쉽다는 것입니다. 단점은 gameCompare에 대해 아무 것도 증명하지 않으면 약 gameCompareAux 및 종료 시간을 명시 적으로 추론해야한다는 것입니다. 이는 매우 까다 롭습니다.

Answer 2

함수의 감소 인수를 표시하는 한 가지 방법은 해당 함수의 도메인을 설명하는 임시 임의 술어를 사용하는 것입니다.일부 반전 보조 정리와 증명

Inductive gameCompareDom : compare_quest -> game -> game -> Prop := 
    | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2 

with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop := 
    | innerGCompareDom1 : forall next_c cbn g1 g1s g2 g2s, listGameCompareDom next_c cbn g1s g2 -> gameListCompareDom next_c cbn g1 g2s -> innerGCompareDom next_c cbn g1 g1s g2 g2s 

with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop := 
    | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2 
    | listGameCompareDom2 : forall c cbn g1s g2 g1s_car g1s_cdr, g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2 -> listGameCompareDom c cbn g1s_cdr g2 -> listGameCompareDom c cbn g1s g2 

with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop := 
    | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s 
    | gameListCompareDom2 : forall c cbn g1 g2s g2s_car g2s_cdr, g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car -> gameListCompareDom c cbn g1 g2s_cdr -> gameListCompareDom c cbn g1 g2s. 

무장 함수는이 같은 기능을 정의 할 수 있습니다 총입니다 : 반전 보조 정리의

Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 -> 
    innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2). 

Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s, 
    innerGCompareDom next_c cbn g1 g1s g2 g2s -> 
    listGameCompareDom next_c cbn g1s g2. 

Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s, 
    innerGCompareDom next_c cbn g1 g1s g2 g2s -> 
    gameListCompareDom next_c cbn g1 g2s. 

Lemma listGameCompareDom2Inv1 : forall c cbn g1s g2 g1s_car g1s_cdr, 
    listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> 
    gameCompareDom c g1s_car g2. 

Lemma listGameCompareDom2Inv2 : forall c cbn g1s g2 g1s_car g1s_cdr, 
    listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> 
    listGameCompareDom c cbn g1s_cdr g2. 

Lemma gameListCompareDom2Inv1 : forall c cbn g1 g2s g2s_car g2s_cdr, 
    gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> 
    gameCompareDom c g1 g2s_car. 

Lemma gameListCompareDom2Inv2 : forall c cbn g1 g2s g2s_car g2s_cdr, 
    gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> 
    gameListCompareDom c cbn g1 g2s_cdr. 

Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop := 
    innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1) 

with innerGCompareAux (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) (H1 : innerGCompareDom next_c cbn g1 g1s g2 g2s) : Prop := 
    cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1)) 

with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop := 
    match g1s as gl1 return g1s = gl1 -> Prop with 
    | emptylist    => fun H2 => cbn_init cbn 
    | listCons g1s_car g1s_cdr => fun H2 => cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (listGameCompareAux c cbn g1s_cdr g2 (listGameCompareDom2Inv2 _ _ _ _ _ _ H1 H2)) 
    end eq_refl 

with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop := 
    match g2s as gl1 return g2s = gl1 -> Prop with 
    | emptylist    => fun H2 => cbn_init cbn 
    | listCons g2s_car g2s_cdr => fun H2 => cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (gameListCompareAux c cbn g1 g2s_cdr (gameListCompareDom2Inv2 _ _ _ _ _ _ H1 H2)) 
    end eq_refl. 

Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2. 

Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s, 
    innerGCompareDom next_c cbn g1 g1s g2 g2s. 

Lemma listGameCompareTot : forall g2 g1s c cbn, 
    listGameCompareDom c cbn g1s g2. 

Lemma gameListCompareTot : forall g1 g2s c cbn, 
    gameListCompareDom c cbn g1 g2s. 

Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop := 
    gameCompareAux c g1 g2 (gameCompareTot _ _ _). 

Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop := 
    innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _). 

Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop := 
    listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _). 

Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop := 
    gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _). 

교정쇄가되도록 Defined. 대신 Qed.로 끝나야를 자신의 내용은 투명하며 계산에 사용 가능합니다. 또한 불투명 한 정리를 언급하지 않아야합니다. 당신이 기대처럼 주요 기능이 볼 수 있도록

Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 = 
    innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2). 

Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s = 
    cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s). 

Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 = 
    match g1s with 
    | emptylist    => cbn_init cbn 
    | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2) 
    end. 

Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s = 
    match g2s with 
    | emptylist    => cbn_init cbn 
    | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr) 
    end. 

당신은 보조 기능에 Extraction Inline를 사용할 수 있습니다

그 후, 당신은 증거 무관의 공리에 의존하여 다음 방정식 보조 정리를 정의 할 수 있어야한다 그들을 추출 할 때까지. 그러나 함수가 bool 대신 Prop을 반환하기 때문에 여기에는 해당되지 않습니다.

전체 개발 here.