린에서 상호 유도적 명제를 정의하는 방법은 무엇입니까?

Question

유도 식 데이터 형식에 대한 구문을 사용하려고 시도했지만 오류 메시지가 표시되었습니다. "상호 유도 형은 종속 제거가있는 기본 유도 형으로 컴파일해야합니다.". 다음은

내 시도의 예는 자연수 또한

mutual inductive even, odd 
with even: ℕ → Prop 
| z: even 0 
| n: ∀ n, odd n → even (n + 1) 
with odd: ℕ → Prop 
| z: odd 1 
| n: ∀ n, even n → odd (n + 1) 

관련 질문에 even 및 odd을 제안을 정의하는 것입니다 : 상호 재귀 함수를 정의하는 구문은 무엇입니까? 어디서나 문서화 된 것을 찾을 수없는 것 같습니다.

Answer 1

내가 린 생각이 자동으로 even.rec 및 odd.rec이 Type하지 Prop 작업 할 recursors을 만들기 위해 노력하고있다. 그러나 Lean은 논리 세계 (Prop)와 계산 세계 (Type)를 분리하기 때문에 작동하지 않습니다. 다시 말하면 논리적 용어를 생성하기 위해서만 논리적 용어 (증명)를 파기 할 수 있습니다. 예를 들어 even 및 odd이 ℕ → Type 인 경우 작동하게됩니다.

관련 시스템 인 Coq 증명 보조자는 두 가지 (약하고 비실용적 인) 유도 원리를 생성하여 자동으로 이러한 상황을 처리하지만 물론 일반적인 재귀를 생성하지는 않습니다.

해결 방법이 있습니다 (Lean wiki article에 설명되어 있음). 상당히 많은 상용구를 작성하는 것과 관련이 있습니다. 이 경우 어떻게 할 수 있는지 예를 들어 설명하겠습니다.

먼저 상호 유도 형을 유도 성 가족으로 컴파일합니다.

inductive even_odd: bool → ℕ → Prop 
| ze: even_odd tt 0 
| ne: ∀ n, even_odd ff n → even_odd tt (n + 1) 
| zo: even_odd ff 1 
| no: ∀ n, even_odd tt n → even_odd ff (n + 1) 

다음으로, 우리는 약간의 약어가 상호 유도 유형을 시뮬레이션 정의 : 우리는 부울 인덱스 나타내는 균일 추가

-- types 
def even := even_odd tt 
def odd := even_odd ff 

-- constructors 
def even.z : even 0 := even_odd.ze 
def even.n (n : ℕ) (o : odd n): even (n + 1) := even_odd.ne n o 
def odd.z : odd 1 := even_odd.zo 
def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no n e 

을 지금을,의는 우리 자신의 유도 원리를 출시하자

-- induction principles 
def even.induction_on {n : ℕ} (ev : even n) (Ce : ℕ → Prop) (Co : ℕ → Prop) 
         (ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1)) 
         (co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) : Ce n := 
    @even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce) 
       ce0 (λ n _ co, stepe n co) 
       co1 (λ n _ ce, stepo n ce) 
       tt n ev 

def odd.induction_on {n : ℕ} (od : odd n) (Co : ℕ → Prop) (Ce : ℕ → Prop) 
        (ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1)) 
        (co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) := 
    @even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce) 
       ce0 (λ n _ co, stepe n co) 
       co1 (λ n _ ce, stepo n ce) 
       ff n od 

이 even.induction_on 암시의 Ce : ℕ → Prop 매개 변수를 만들기 위해 더 나은 것, 그러나 어떤 이유로 린 (를 추론 할 수없는 말, wher에서 보조 정리를 참조 우리는 Ce을 명시 적으로 전달해야하며, 그렇지 않은 경우 기울이기는 Ce은 우리의 목표와 관련이 없습니다. 상황은 odd.induction_on과 대칭입니다.

상호 재귀 함수를 정의하는 구문은 무엇입니까?

로서이 lean-user thread 설명 상호 재귀 함수에 대한 지원이 매우 제한되어

임의 상호 재귀 함수에 대한 지원이되지 않지만, 매우 간단한 경우에 대한 지원이있다. 상호 회귀 형을 정의한 후에는이 유형의 구조를 "미러링"하는 상호 재귀 함수를 정의 할 수 있습니다.

해당 스레드에서 예제를 찾을 수 있습니다.그러나 다시, 동일한 add-a-switching-parameter 접근법을 사용하여 상호 재귀 함수를 시뮬레이션 할 수 있습니다. 의 상호 재귀 부울 조건을 evenb 및 oddb을 시뮬레이션 보자

여기

def even_oddb : bool → ℕ → bool 
| tt 0  := tt 
| tt (n + 1) := even_oddb ff n 
| ff 0  := ff 
| ff (n + 1) := even_oddb tt n 

def evenb := even_oddb tt 
def oddb := even_oddb ff 

는 모두 위의 사용 방법의 예입니다. 간단한 보조 정리를 증명해 보겠습니다.

lemma even_implies_evenb (n : ℕ) : even n -> evenb n = tt := 
    assume ev : even n, 
    even.induction_on ev (λ n, evenb n = tt) (λ n, oddb n = tt) 
    rfl 
    (λ (n : ℕ) (IH : oddb n = tt), IH) 
    rfl 
    (λ (n : ℕ) (IH : evenb n = tt), IH)