Извлечь / использовать подтверждение членства из набора ssreflect - PullRequest
Новая
       31

Извлечь / использовать подтверждение членства из набора ssreflect

0 голосов
/ 18 февраля 2019

РЕДАКТИРОВАТЬ: я сделал пример более минимальным, введя структуру, которая увеличивает элемент путем переноса доказательства принадлежности указанного элемента к набору: 

Structure elem_and_in_proof {T : finType} (s : {set T}) := {el :> T ; Helin : el \in s}.

Canonical eip_subType {T : finType} (s : {set T}) := Eval hnf in [subType for (@el T s)].
Canonical eip_eqType {T : finType} (s : {set T}) := Eval hnf in EqType _ [eqMixin of (elem_and_in_proof s) by <:].
Canonical eip_choiceType {T : finType} (s : {set T}) := Eval hnf in ChoiceType _ [choiceMixin of (elem_and_in_proof s) by <:].
Canonical eip_countType {T : finType} (s : {set T}) := Eval hnf in CountType _ [countMixin of (elem_and_in_proof s) by <:].
Canonical eip_subCountType {T : finType} (s : {set T}) := Eval hnf in [subCountType of (elem_and_in_proof s)].
Canonical eip_finType {T : finType} (s : {set T}) := Eval hnf in FinType _ [finMixin of (elem_and_in_proof s) by <:].

Однако мне нужно применитьэто преобразование в любой заданный набор, и я не могу сделать это либо: 

Lemma equip_set_with_Helin {ft : finType} (s : {set ft}) : {set (elem_and_in_proof s)}.
Proof.
Admitted.

Так как equip_set_with_Helin позволяет мне написать функцию uniq_cons, любая помощь по этому или исходному вопросу будет принята с благодарностью.Спасибо!

У меня есть тип dbranch, состоящий из последовательности по конечному типу ft и доказательства uniq этой последовательности.Я хочу иметь возможность, учитывая элемент t типа ft и finset над dbranch, возвращать один и тот же набор, где все dbranches были «скомпонованы» с t.

Мне нужно было написать функцию consдля ветвей, принимающих в качестве аргумента гипотезу о том, что данный элемент уже не является частью ветви.Я не знал, как написать ее как обычную функцию, поэтому я подошел к ней в качестве доказательства.

Затем я написал uniq_cons, который пытается поднять dcons до набора dbranches.Однако применение его аргумента H требует доказательства b \ in t (это заполнитель в моем коде).

From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
From mathcomp
Require Import tuple finfun bigop finset.

Variable ft : finType.

Structure dbranch := {branch :> seq ft ; buniq : uniq branch}.

Canonical dbranch_subType := Eval hnf in [subType for branch].
Canonical dbranch_eqType := Eval hnf in EqType _ [eqMixin of dbranch by <:].
Canonical dbranch_choiceType := Eval hnf in ChoiceType _ [choiceMixin of dbranch by <:].
Canonical dbranch_countType := Eval hnf in CountType _ [countMixin of dbranch by <:].
Canonical dbranch_subCountType := Eval hnf in [subCountType of dbranch].
Lemma dbranchFin : Finite.mixin_of [eqType of dbranch].
Admitted. 
Canonical dbranch_finType := Eval hnf in FinType _ dbranchFin.

Definition dcons (t : ft) (b : dbranch) (H : t \notin (branch b)) : dbranch.
Proof.
exists (t :: b) ; apply/andP ; split.
  - apply H.
  - apply (buniq b).
Qed.  

Definition uniq_cons (al : ft) (t : {set dbranch}) (H : forall b, (b \in t -> al \notin (branch b))) := 
  [set (dcons al b (H b _)) | b in t].

Тот факт, что b находится в t, должен быть очевиден, как это непосредственно указывается во всеобъемлющей записи.Тем не менее, я не смог найти в finset.va способ «извлечь» или использовать эту информацию, и Coq не может сделать это самостоятельно.Заранее благодарю за помощь.

1 Ответ

0 голосов
/ 19 февраля 2019

Чтобы ответить на ваш исправленный вопрос, вы можете сделать что-то вроде этого: 

From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finset.

Definition equip (T : finType) (A : {set T}) : {set {x : T | x \in A}} :=
  [set x in pmap insub (enum A)].

Последовательность enum A перечисляет все элементы набора A.Функция insub : T -> option sT приводит элемент x : T к подтипу sT : subType P, равному T, при условии, что предикат P имеет значение x.Учитывая, что все элементы enum A находятся в A по определению, эта функция просто ведет себя как Some.Наконец, pmap отображает частичную функцию над последовательностью, отбрасывая все результаты None.

...