Tôi nghĩ rằng Lean tự động cố gắng tạo các đệ quy even.rec và odd.rec để hoạt động với Type, không phải Prop. Nhưng điều đó không hiệu quả vì Lean phân tách thế giới logic (Prop) và thế giới tính toán (Type). Nói cách khác, chúng ta có thể hủy bỏ một thuật ngữ logic (bằng chứng) chỉ để tạo ra một thuật ngữ logic. Quan sát, ví dụ của bạn sẽ hoạt động nếu bạn đã thực hiện even và odd loại ℕ → Type.
Trợ lý bằng chứng Coq, là một hệ thống liên quan, xử lý tình huống này một cách tự động bằng cách tạo ra hai nguyên tắc cảm ứng (khá yếu và không thực tế), nhưng nó không tạo ra các đệ quy chung.
Có giải pháp thay thế, được mô tả trong số Lean wiki article này. Nó liên quan đến việc viết khá nhiều bản mẫu. Hãy để tôi đưa ra một ví dụ làm thế nào nó có thể được thực hiện cho trường hợp này.
Trước hết, chúng tôi biên soạn các loại quy nạp lẫn nhau thành một gia đình quy nạp. Chúng tôi thêm một chỉ số boolean đại diện ngang nhau:
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)
Tiếp theo, chúng ta định nghĩa một số từ viết tắt để mô phỏng các loại lẫn nhau quy nạp:
-- 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
Bây giờ, chúng ta hãy tung ra những nguyên tắc cảm ứng riêng của chúng tôi:
-- 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
Sẽ tốt hơn nếu thực hiện tham số Ce : ℕ → Prop của even.induction_on ẩn, nhưng vì một số lý do mà Lean không thể suy ra nó (xem bổ đề ở cuối, e, chúng tôi phải vượt qua Ce một cách rõ ràng, nếu không thì Lean infers Ce không liên quan đến mục tiêu của chúng tôi). Tình hình là đối xứng với odd.induction_on.
Cú pháp xác định hàm đệ quy hai bên là gì?
Như đã giải thích trong lean-user thread này, hỗ trợ cho các chức năng hai bên đệ quy là rất hạn chế:
không có hỗ trợ cho các chức năng hai bên đệ quy tùy ý, nhưng có hỗ trợ cho một trường hợp rất đơn giản. Sau khi chúng tôi xác định một loại đệ quy cùng loại, chúng tôi có thể xác định các hàm đệ quy hai chiều mà "phản chiếu" cấu trúc của các loại này.
Bạn có thể tìm thấy ví dụ trong chuỗi đó.Nhưng, một lần nữa, chúng ta có thể mô phỏng các hàm đệ quy hai chiều bằng cách sử dụng cùng phương thức tham số add-a-switching-parameter. Hãy mô phỏng lẫn nhau đệ quy vị boolean evenb và 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
Dưới đây là một ví dụ về cách tất cả những điều trên có thể được sử dụng. Hãy chứng minh một bổ đề đơn giản:
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)