How to guarantee constrained values on a type in Coq?

Question

If I have something like:

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

How could I add hard guarantees about values in this type, like:

hotfix v > 0 && hotfix v < 8

And no one could create a Version with wrong values.

Answer 1

You just have to add a field for the proof. To tidy it up, you could wrap hotfix in its own type:

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