Cấu trúc hợp quy trong ssreflect

Question

Tôi đang cố xử lý các cấu trúc kinh điển trong ssreflect. Có 2 đoạn mã tôi lấy từ here.

Tôi sẽ mang các phần cho bool và các loại tùy chọn.

Section BoolFinType. 

    Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed. 
    Definition bool_finMixin := Eval hnf in FinMixin bool_enumP. 
    Canonical bool_finType := Eval hnf in FinType bool bool_finMixin. 
    Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed. 

End BoolFinType. 

Section OptionFinType. 

    Variable T : finType. 
    Notation some := (@Some _) (only parsing). 

    Local Notation enumF T := (Finite.enum T). 

    Definition option_enum := None :: map some (enumF T). 

    Lemma option_enumP : Finite.axiom option_enum. 
    Proof. by case => [x|]; rewrite /= count_map (count_pred0, enumP). Qed. 

    Definition option_finMixin := Eval hnf in FinMixin option_enumP. 
    Canonical option_finType := Eval hnf in FinType (option T) option_finMixin. 

    Lemma card_option : #|{: option T}| = #|T|.+1. 
    Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed. 

End OptionFinType. 

Bây giờ, giả sử tôi có một hàm f từ finType để Prop

Variable T: finType. 
Variable f: finType -> Prop. 

Goal f T. (* Ok *) 
Goal f bool. (* Not ok *) 
Goal f (option T). (* Not ok *) 

Trong hai trường hợp cuối cùng tôi nhận được lỗi sau:.

The term "bool/option T" has type "Set/Type" while it is expected to have type "finType".

Tôi đang làm gì sai ?

Answer 1

Tìm kiếm cá thể đối với cấu trúc kinh điển là bộ đếm bit trực quan trong những trường hợp này. Giả sử bạn có những thứ sau:

• loại cấu trúc S và loại T;
• một trường proj : S -> T của S;
• một phần tử x : T; và
• một phần tử st : S đã được khai báo là chuẩn, sao cho proj st được định nghĩa là x.

Trong ví dụ của bạn, chúng tôi sẽ có:

• S = finType
• T = Type
• proj = Finite.sort
• x = bool
• st = bool_finType.

tìm kiếm cấu trúc Canonical được kích hoạt chỉ trong trường hợp sau: khi các thuật toán loại kiểm tra đang cố gắng tìm một giá trị cho hợp lệ điền vào các lỗ trong phương trình proj _ = x. Sau đó, nó sẽ sử dụng st : S để điền vào lỗ này. Trong ví dụ của bạn, bạn mong đợi thuật toán hiểu rằng bool có thể được sử dụng làm finType, bằng cách chuyển đổi nó thành bool_finType, không hoàn toàn được mô tả ở trên.

Để làm cho Coq suy ra những gì bạn muốn, bạn cần sử dụng vấn đề thống nhất của biểu mẫu đó. Ví dụ:

Variable P : finType -> Prop. 
Check ((fun (T : finType) (x : T) => P T) _ true). 

Điều gì đang xảy ra ở đây? Hãy nhớ rằng Finite.sort được tuyên bố là một sự ép buộc từ finType đến Type, vì vậy x : T thực sự có nghĩa là x : Finite.sort T. Khi bạn áp dụng biểu thức fun cho true : bool, Coq phải tìm giải pháp cho Finite.sort _ = bool. Sau đó nó tìm thấy bool_finType, bởi vì nó đã được khai báo là kinh điển. Vì vậy, các yếu tố của bool là những gì kích hoạt tìm kiếm, nhưng không hoàn toàn bool chính nó.

Như ejgallego đã chỉ ra, mẫu này phổ biến đến nỗi ssreflect cung cấp cú pháp đặc biệt [finType of ...]. Nhưng nó vẫn có thể hữu ích để hiểu những gì đang xảy ra dưới mui xe.