목록 X의 길이를 Coq의 X 생성자에 대한 인수로 사용

제목은별로 유익하지 않으므로 설명해 드리겠습니다.목록 X의 길이를 Coq의 X 생성자에 대한 인수로 사용

나는 1 차 논리에서 용어라는 것을 의미하는 것을 공식화하려하고있다. 다음은 임의의 언어 L 측면의 교과서 정의입니다 :

(1) Each variable or constant is a term. 
(2) If n ≥ 1, f is an n-ary function of L, and t1 ... tn are terms of L, then f t1 ... tn is a term of L.

는 이미 변수, 상수, 함수 및 언어 정의 var, const, func 및 lang있다. 함수의 아티 (arity)와 언어의 모든 함수의 앙상블을 각각 반환하는 함수 f_arity 및 L_funcs도 있습니다. 귀납적 인 용어 정의를주는 것은 매우 간단합니다.

그러나 작동하지 않습니다. 대신,이 오류 메시지가 나타납니다.

Error: Non strictly positive occurrence of "term" in 
"forall (f : func) (l : list (term L)), 
    length l = f_arity f -> In func (L_funcs L) f -> term L".

여기에 무슨 일이 일어나고 있는지 모호한 생각이 있습니다. 생성자 t_f에는 length l = f_arity이라는 인수가 있습니다. Coq는 화살표 왼쪽에 term L을 가지고 있기 때문에 좋지 않습니다. 하지만 Coq가 지나치게 조심스럽게 여기고 있다고 생각합니다. 유형을 조금만 조정하면 똑같은 일을 할 수 있기 때문입니다. 예를 들어, 사용자 정의 목록 유형 listN을 으로 인덱싱하여 list X n이 X이고 목록이 n 인 것으로 정의 할 수 있습니다. 그럼 난

Inductive term (L : lang) : Type := 
| t_v : var -> term L 
| t_c : const -> term L 
| t_f : forall (f : func) 
    (l : listN (term L) (f_arity f)), 
    In func (L_funcs L) f -> term L .

있을 것입니다하지만 임시, 모든 유용한 목록을 사용할 수 없게 도서관 만들기 때문에 나는이 길을 가고 싶어하지 않습니다. 그래서 나는 Coq에게 내가하려고하는 것이 완벽하게 안전하다는 것을 납득시킬 방법을 찾고있다. 그래서 생성자 인자로 length l = f_arity f을 받아 들일 것이다. 이것을 할 수있는 방법이 있습니까?

출처

2014-11-10 user287393

이것은 참으로 좋은 문제입니다. 이전에는이 형식으로 만난 적이 없었습니다.

솔직히, 불행히도, 나는 당신의 정의를 받아들이도록 Coq를 얻는 방법을 보지 못합니다. 이 문제를 완화하기위한 몇 가지 옵션은 다음과 같습니다.

용어 정형성에 대해 별도의 귀납적 술어를 사용하십시오. 용어 조작은 함수 작성시 길이 제한에 대해 걱정할 필요가 없기 때문에 훨씬 편리합니다. 반면에, 당신은 그것에 대해 아무것도 증명할 때 잘 형성에 대해 개별적으로 추론해야 할 것입니다. 따라서, 당신은
```
Inductive term L : Type := 
| t_v : var -> term L 
| t_c : const -> term L 
| t_f f (ts : list (term L)) : term L. 

Inductive wf_term L : term L -> Prop := 
| wf_v v : wf_term L (t_v v) 
| wf_c c : wf_term L (t_c c) 
| wf_f f ts : 
    In f (L_funcs L) -> 
    Forall (wf_term L) ts -> 
    length ts = f_arity f -> 
    wf_term L (t_f f ts). 
```
용어에 대한 의존적으로 입력 인코딩을 사용하여 같은 것을 할 것입니다. 예 : 당신이 당신이 조작하는 인수 목록을하지 않기 때문에 당신이 원하는 것을하지 않을 수
```
Inductive term L : nat -> Type := 
| t_v : var -> term L 0 
| t_c : const -> term L 0 
| t_f f : In f (L_funcs L) -> term L (f_arity f) 
| t_a n (t : term L (S n)) (t : term L 0) : term L n. 
```
뭔가를 줄 것 "실종"얼마나 많은 인수를 표현하는 term에 nat 매개 변수지만, 도움이 될 수 있습니다.
길이가 잘못된 목록의 "잘못된"인코딩을 사용하고 보조 유형 ("보기")과 함수를 사용하여이 "나쁜"정의를 사용하기가 더 편리하게 만듭니다.당신은 당신의 두 번째 정의처럼 term 정의,하지만 당신도 효과적으로 성가신을 숨기고, t_f'' 대신 t_f 직접 작업 사용자 정의 유도/재귀 원칙을 정의 할 수 있습니다
```
Inductive term' L : Type := 
| t_v' : var -> term' L 
| t_c' : const -> term' L 
| t_f' f (ts : list (term L)) : 
    In f (L_funcs L) -> 
    length ts = f_arity f -> 
    term' L. 

Definition term_view L (t : term L) : term' L := (* ... *) 

(* Wrapper around the original constructor *) 
Definition t_f'' L f ts : In f (L_funcs L) -> length ts = f_arity f -> term L := 
    (* ... *) 
```
처럼, 그 위에 새로운 term'을 정의 원래 정의의 세부 정보.

출처

2014-11-10 20:52:13

목록 X의 길이를 Coq의 X 생성자에 대한 인수로 사용

답변

관련 문제