Как сделать тип с конечным множеством, используя MSets с «обычным» равенством? - PullRequest
Новая
       6

Как сделать тип с конечным множеством, используя MSets с «обычным» равенством?

0 голосов
/ 26 февраля 2020

Извините, что задаю простой вопрос, но я искал ответ в течение нескольких часов, и я не нашел достаточно простого для меня объяснения (я не очень понимаю систему модулей Coq)

У меня есть следующие типы 

Def var := nat.

Inductive type : Type :=
| Unit
| Arrow (a : type) (b : type)
| Ref (a : type)
.

Inductive Judgement : Type :=
| judge (v : var) (t : type)
.

Я хотел бы иметь возможность создавать (конечные) наборы Judgements. Из исследования, которое я провел, похоже, MSets - это то, что я хочу. В частности, я (думаю, что я) заинтересован в «слабых» наборах, так как я бы хотел избежать использования упорядоченности var/nat. Однако я не могу понять, как на самом деле создать тип, соответствующий набору суждений.

Самый близкий пример, который мне удалось найти, это this, но я хотел бы иметь возможность создавать наборы неупорядоченных элементов

1 Ответ

0 голосов
/ 26 февраля 2020

Разве вы не можете обойти это, используя список суждений, а не MSet суждений?

Использование MSets включает в себя определение упорядоченного типа, который может быть довольно незначительным.

См. Пример nats в стандартных библиотеках Nat_as_OT 

Module Nat_as_OT <: UsualOrderedType.

  Definition t := nat.

  Definition eq := @eq nat.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt := lt.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := eq_nat_dec.

End Nat_as_OT.
...