Подтипирование с помощью ssreflect

Я пытался научиться делать подтипы с помощью ssreflect, http://ssr.msr-inria.inria.fr/~jenkins/current/mathcomp.ssreflect.eqtype.html в качестве моей основной ссылки, но столкнулся с проблемами. То, что я пытаюсь сделать, это создать из типа T с тремя терминами подтип T' с двумя терминами a,b. (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.

subtype coq ssreflect
person Zhangsheng    schedule 21.08.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

(1) в чем разница между {x:T | P x} и подтип P?

subType P — это запись, содержащая все соответствующие доказательства для P для установления подтипа некоторых типов val : U -> T.

{x : T | P x} — это обычный сигма-тип, и если P — логический предикат, math-comp объявил канонический способ построения записи 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.
person ejgallego    schedule 21.08.2018
comment
Мое понимание insub относится к x : T, insub x : abT, поскольку это общая частичная проекция T в подтип S T, и аналогично для x : abT у нас будет val x : T. Можете ли вы также объяснить лемму abT_is_ab и как она используется? - person Zhangsheng; 24.08.2018
comment
Лемма abT_is_ab — это просто псевдоним для valP, то есть каждый элемент подтипа удовлетворяет предикату P. Доказательство тривиально и сводится к уничтожению записи, если бы у нас была лучшая поддержка примитивных проекций в math-comp valP, то оно было бы верным по определению. insub x просто проверяет, находится ли элемент x в подтипе. Это равносильно проверке результата P x. Обратите внимание, что insub x : option abT, поскольку ни один элемент x : T не соответствует предикату ab. - person ejgallego; 28.08.2018