Subtyping using ssreflect

Question

I have been trying to learn how to do subtyping using ssreflect, http://ssr.msr-inria.inria.fr/~jenkins/current/mathcomp.ssreflect.eqtype.html as my main reference, but have been running into problems. What I'm trying to do is from a type T with three terms, create a subtype T' with two terms a,b. (1) what is the difference between {x:T | P x} and 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.

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 is a record containing all the relevant proofs for P to establish a subType of some types val : U -> T.

{x : T | P x} is a regular sigma type, and if P is a boolean predicate math-comp has declared a canonical way of building the subType P record for that type.

(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.

I am unsure about what you mean. insub does not "project" but tries to embed [which is not always possible]. In your case, the proof is easy enough, and you don't have to complicate things so much:

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.