0

我一直在尝试学习如何使用 ssreflect 进行子类型化，http ://ssr.msr-inria.inria.fr/~jenkins/current/mathcomp.ssreflect.eqtype.html作为我的主要参考，但一直遇到问题. 我想要做的是从T具有三个术语的类型，创建一个T'具有两个术语的子类型a,b。{x:T | P x}(1)和有什么区别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.
4

1 回答 1

2

(1) {x:T | 有什么区别？P x} 和子类型 P?

subType P是包含所有相关证明的记录，用于P建立某些类型的子类型val : U -> T。

{x : T | P x}是一个常规的 sigma 类型，并且 if是一个布尔谓词 math-comp 已经声明了一种为该类型P构建记录的规范方法。subType P

(2) 从我下面的代码中，我有 Sub a Pa 是 T' 的一个术语，是否有可能有一个适用于 a、b 的一般证明？我在这里感到困惑，因为从 eqType.v 感觉好像 insub 是用来从一个类型投影到它的子类型的那个。

我不确定你的意思。insub不“投射”但尝试嵌入[这并不总是可能的]。在您的情况下，证明很简单，您不必使事情变得如此复杂：

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.
于 2018-08-21T18:49:30.610 回答