Как гарантировать ограниченные значения для типа в Coq?

Question

Если у меня есть что-то вроде:

Record Version :=
  mkVersion { major:nat; minor:nat; branch:nat; hotfix:nat }.

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

hotfix v > 0 && hotfix v < 8

И никто не мог создать Версию с неправильными значениями.

Answer 1

Вам просто нужно добавить поле для доказательства.Чтобы привести в порядок, вы можете обернуть hotfix в его собственный тип:

Record hotfix_t := Hotfix { 
  hf_val : nat; 
  hf_pf : hf_val > 0 /\ hf_val < 8
}.
Record Version := mkVersion {
  major : nat;
  minor : nat;
  branch : nat;
  hotfix : hotfix_t
}.