Định nghĩa theo bất động sản trong coq

Question

Tôi gặp sự cố khi hình thức hóa các định nghĩa của biểu mẫu sau: xác định số nguyên sao cho một số thuộc tính nắm giữ.

Hãy nói rằng tôi chính thức định nghĩa về tài sản:

Definition IsGood (x : Z) : Prop := ... 

Bây giờ tôi cần một định nghĩa có dạng:

Definition Good : Z := ... 

giả định rằng tôi đã chứng minh rằng một số nguyên với tài sản tồn tại và là duy nhất:

Lemma Lemma_GoodExistsUnique : exists! (x : Z), IsGood x. 

Có cách dễ dàng để xác định Good sử dụng IsGood và Lemma_GoodExistsUnique?

Vì thuộc tính được xác định trên số nguyên, có vẻ như không cần thêm tiên đề nào. Trong mọi trường hợp, tôi không thấy làm thế nào thêm một cái gì đó giống như tiên đề của sự lựa chọn có thể giúp với định nghĩa.

Ngoài ra, tôi gặp sự cố khi hình thức hóa các định nghĩa dưới đây (tôi nghi ngờ điều này liên quan đến vấn đề tôi đã mô tả ở trên, nhưng vui lòng cho biết nếu không phải như vậy): cho mỗi x, tồn tại y và các số y khác nhau cho các số khác nhau x. Giống như, ví dụ, làm thế nào để xác định rằng có N biệt số tốt số nguyên sử dụng IsGood:

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) := ...? 

Trong toán học thực tế, định nghĩa như thế xảy ra tất cả bây giờ và một lần nữa, vì vậy đây không phải là khó khăn để chính thức hóa nếu Coq được thiết kế để phù hợp với toán học thực tế.

Answer 1

Câu trả lời ngắn cho câu hỏi đầu tiên của bạn là: nói chung, điều đó là không thể, nhưng trong trường hợp cụ thể của bạn, có.

Trong lý thuyết Coq, các mệnh đề (ví dụ: Prop s) và bằng chứng của chúng có trạng thái rất đặc biệt. Đặc biệt, nói chung không thể viết một toán tử lựa chọn để trích xuất chứng nhân của một bằng chứng tồn tại. Điều này được thực hiện để làm cho lý thuyết tương thích với các tiên đề và nguyên tắc nhất định, chẳng hạn như sự không liên quan đến bằng chứng, mà nói rằng tất cả các bằng chứng của một mệnh đề nhất định đều bằng nhau. Nếu bạn muốn có thể làm điều này, bạn cần phải thêm toán tử lựa chọn này làm tiên đề bổ sung cho lý thuyết của bạn, như trong standard library.

Tuy nhiên, trong một số trường hợp cụ thể, nó là có thể trích xuất nhân chứng ra khỏi bằng chứng tồn tại trừu tượng mà không phải định kỳ lại bất kỳ tiên đề bổ sung nào. Cụ thể, có thể thực hiện việc này cho các loại có thể đếm được (chẳng hạn như Z) khi thuộc tính được đề cập là có thể giải quyết được. Ví dụ, bạn có thể sử dụng giao diện choiceType trong thư viện Ssreflect để có được chính xác những gì bạn muốn (tìm kiếm hàm xchoose).

Điều đó đang được nói, tôi thường khuyên bạn chống lại thực hiện mọi việc theo phong cách này, bởi vì nó dẫn đến sự phức tạp không cần thiết. Có thể dễ dàng xác định trực tiếp số Good mà không cần sử dụng bằng chứng về sự tồn tại và sau đó chứng minh riêng rằng Good có thuộc tính được tìm kiếm.

Definition Good : Z := (* ... *) 
Definition IsGood (z : Z) : Prop := (* ... *) 

Lemma GoodIsGood : IsGood Good. 
Proof. (* ... *) Qed. 

Lemma GoodUnique : forall z : Z, IsGood z -> z = Good. 

Nếu bạn hoàn toàn muốn xác định Good kèm theo bằng chứng tồn tại, bạn cũng có thể thay đổi bằng chứng về Lemma_GoodExistsUnique sử dụng một liên kết trong Type thay vì Prop, vì nó cho phép bạn trích xuất các nhân chứng trực tiếp bằng cách sử dụng proj1_sig chức năng :

Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}. 
Proof. (* ... *) Qed. 

Đối với câu hỏi thứ hai của bạn, có, nó có liên quan đến điểm đầu tiên. Một lần nữa, tôi khuyên bạn nên viết một hàm y_from_x với loại Z -> Z sẽ tính y cho x và sau đó chứng minh riêng rằng hàm này liên quan đến đầu vào và đầu ra theo cách cụ thể. Sau đó, bạn có thể nói rằng các số y s khác nhau đối với các số khác nhau x s bằng cách chứng minh rằng y_from_x là dạng tiêm.

Mặt khác, tôi không chắc chắn làm thế nào ví dụ cuối cùng của bạn liên quan đến câu hỏi thứ hai này. Nếu tôi hiểu những gì bạn muốn làm một cách chính xác, bạn có thể viết một cái gì đó giống như

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) := 
    exists zs : list Z, 
    Z.of_nat (length zs) = N 
    /\ NoDup zs 
    /\ Forall IsGood zs. 

Ở đây, Z.of_nat : nat -> Z là tiêm kinh điển từ bẩm đến số nguyên, NoDup là một vị khẳng định rằng một danh sách không chứa yếu tố lặp đi lặp lại, và Forall là một vị từ bậc cao khẳng định rằng một biến vị ngữ đã cho (trong trường hợp này là IsGood) chứa tất cả các phần tử của một danh sách.

Lưu ý cuối cùng, tôi sẽ khuyên bạn không nên sử dụng Z cho những thứ chỉ có thể liên quan đến số tự nhiên. Trong ví dụ của bạn, bạn sử dụng một số nguyên để nói về cardinality của một tập hợp, và con số này luôn luôn là một số tự nhiên.