Tôi khá mới ở Coq và cố gắng phát triển một khuôn khổ dựa trên nghiên cứu của tôi. Công việc của tôi khá nặng và tôi đang gặp sự cố khi mã hóa nó vì Coq dường như coi bộ xử lý như thế nào.Công thức phù hợp của các bộ trong Coq?
Có Type và Set, mà họ gọi là 'loại', và tôi có thể sử dụng chúng để xác định một tập hợp mới:
Variable X: Type.
Và sau đó có một mã hóa thư viện (phụ) đặt là 'Ensembles', là các hàm từ một số Type đến Prop. Nói cách khác, họ là các vị từ trên Type:
Variable Y: Ensemble X.
Ensemble s cảm thấy giống như bộ toán học thích hợp. Ngoài ra, chúng được xây dựng dựa trên nhiều thư viện khác. Tôi đã thử tập trung vào chúng: xác định một bộ phổ quát U: Set, và sau đó giới hạn bản thân mình (phụ) Ensemble s trên U. Nhưng không. Ensemble s không thể được sử dụng như các loại cho các biến khác, cũng không phải để xác định các tập con mới:
Variable y: Y. (* Error *)
Variable Z: Ensemble Y. (* Error *)
Bây giờ, tôi biết có một số cách để có được xung quanh đó. Câu hỏi "Subset parameter" cung cấp hai câu hỏi. Cả hai đều sử dụng các cưỡng chế. Các gậy đầu tiên để Set s. Thứ hai về cơ bản sử dụng Ensemble s (mặc dù không theo tên). Nhưng cả hai yêu cầu khá một số máy móc để thực hiện một cái gì đó rất đơn giản.
Câu hỏi: Cách đề xuất các bộ xử lý nhất quán (và thanh lịch) là gì?
Ví dụ: Đây là ví dụ về những gì tôi muốn làm: Giả sử một tập hợp DD. Xác định một cặp dm = (D, <) nơi D là một tập hợp con hữu hạn của DD và < là một trật tự một phần nghiêm ngặt về D.
Tôi chắc chắn rằng với đủ tinkering với các sự ép buộc hoặc các cấu trúc khác, tôi có thể hoàn thành nó; nhưng không phải theo cách đặc biệt có thể đọc được; và không có trực giác tốt về cách thao tác cấu trúc thêm nữa. Ví dụ: các loại kiểm tra sau:
Record OrderedSet {DD: Set} : Type := {
D : (Ensemble DD);
order : (relation {d | In _ D d});
is_finite : (Finite _ D);
is_strict_partial : (is_strict_partial_order order)
}.
Nhưng tôi không chắc đó là điều tôi muốn; và nó chắc chắn trông không đẹp lắm. Lưu ý rằng tôi sẽ chuyển tiếp và chuyển tiếp giữa Set và Ensemble theo cách có vẻ tùy ý.
Có rất nhiều thư viện ở đó sử dụng Ensemble s, vì vậy phải có cách tốt để xử lý chúng, nhưng những thư viện đó dường như không được ghi lại rất rõ (hoặc ... tất cả).
Cập nhật: Để làm phức tạp hơn nữa, cũng có một số triển khai tập hợp khác, như MSets. Điều này dường như hoàn toàn tách biệt và không tương thích với Ensemble. Nó cũng sử dụng bool thay vì Prop vì một số lý do. Ngoài ra còn có FSets, nhưng nó có vẻ là một phiên bản MSO lỗi thời.
Xin chào Adam! Tôi chia sẻ quan điểm chung của bạn về 'Set' và' Ensemble'. Nhưng điều này không cho tôi một cách tốt để (ví dụ) sử dụng một Ensemble như một loại cho một biến mới mà sau đó hoạt động như một tập hợp con. Vâng, không phải không có sự ép buộc. Có lẽ không có cách nào xung quanh điều đó? – mhelvens
Bạn có nghĩa là đối với phần tập hợp con trong * Câu hỏi * của bạn? Vâng, đơn đặt hàng của bạn là một phần anyway, do đó, có bất cứ điều gì ngăn cản bạn từ xác định đơn đặt hàng của bạn trên toàn bộ vũ trụ _DD_ thay thế? Tôi nghĩ rằng đó sẽ là một cách làm theo cách thông thường hơn, trừ khi có một số ràng buộc bổ sung mà bạn không đề cập đến? – akoprowski
Vâng, tất cả các phần của câu hỏi của tôi, thực sự. Ví dụ chỉ là: một ví dụ. Tôi muốn một cách để liên tục chuyển đổi giữa các tập (phụ) và (phụ) mà không phải tính toán theo từng trường hợp cụ thể. --- Nhưng về thứ tự từng phần đó: đó là một thứ tự một phần hữu hạn được chỉ định bằng tay (để đi với tập hợp hữu hạn). Nếu tôi gõ nó như là một thứ tự trên DD nó có thể đặt hàng các yếu tố bên ngoài tập * D *. Tôi không chắc liệu điều đó có gây rối với bất kỳ bằng chứng nào trong tương lai hay không ... nhưng nó không đặc biệt thanh lịch. – mhelvens