使用 ssreflect 进行子类型化

Question

我一直在尝试学习如何使用 ssreflect http://ssr.msr-inria.inria.fr/~jenkins/current/mathcomp.ssreflect.eqtype.html 作为我的主要参考来进行子类型化，但是运行遇到了问题。我想要做的是从具有三个术语的类型 T，创建一个具有两个术语 a,b 的子类型 T'。 (1) {x:T | P x}和subType P有什么区别？ (2) 从我下面的代码中，我有 Sub a Pa 是 T' 的项，是否可以有一个适用于 a, b 的通用证明？我在这里感到困惑，因为从 eqType.v 开始感觉好像 insub 是用来从一个类型投射到它的子类型的。

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Inductive T : Set := a | b | c.

Definition P := fun (x:T) =>
 match x with
 | a => true
 | b => true
 | c => false
 end.

 Definition T' := {x:T | P x}.
 Definition T'' := subType P.

 Definition cast (x: T) : option T'.
 destruct (P x) eqn:prf.
 - exact (Some (exist _ x prf)).
 - exact None.
 Defined.


 Definition Pa : is_true (P a).
   destruct (P a) eqn:prf.
   exact. simpl in prf. unfold is_true. symmetry. apply prf. Defined.

 Check (Sub a Pa) : T'.

 Check val (Sub a Pa) : T.

 Check insub (val (Sub a Pa)) : option T'.

 Definition Px :forall x : T, is_true (P x).
  intros x. destruct (P x) eqn:prf.
  - unfold is_true. reflexivity.
  - unfold is_true.
  Abort.

Answer 1

(1) what is the difference between {x:T | P x} and subType P?

subType P是一条记录，包含P建立某些类型val : U -> T.

的子类型的所有相关证明

{x : T | P x} 是常规 sigma 类型，如果 P 是布尔谓词，math-comp 已声明为该类型构建 subType P 记录的规范方法。

(2) From my code below, I have Sub a Pa to be a term of T', is it possible to have a general proof that applies for both a, b? I'm confused here as from eqType.v it feels as though insub is the one to be used to project from a type into its subtype.

我不确定你的意思。 insub 不会 "project" 但会尝试嵌入 [这并不总是可能的]。在你的情况下，证明很简单，你不必把事情复杂化太多：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive T : Set := a | b | c.

Definition is_ab (x:T) : bool := match x with
 | a | b => true
 | c => false
 end.

Definition abT := { x : T | is_ab x }.

Lemma abT_is_ab (x : abT) : is_ab (val x).
Proof. exact: valP. Qed.

使用 ssreflect 进行子类型化

Subtyping using ssreflect

subtype

coq

ssreflect