I want to define a small record in Coq which also includes certain conditions. In addition I want a definition to create a record in an easy way. Here is my approach:
Require Import Arith.
(* Define the qn record with conditions for q and n *)
Record qn := {
q : nat;
q_ge_2 : leb 2 q = true; (* Ensuring q is greater or equal than 2 *)
n : nat;
n_ge_1 : leb 1 n = true (* Ensuring n is greater or equal than 1 *)
}.
(* A support function to create instances of qn more conveniently *)
Definition make_qn (q n: nat) (Hq : leb 2 q = true) (Hn : leb 1 n = true) : qn :=
{| q := q; q_ge_2 := Hq; n := n; n_ge_1 := Hn |}.
(* Examples of qn *)
Example qn_example1 : qn := make_qn 2 1 (eq_refl true) (eq_refl true).
Example qn_example2 : qn := make_qn 3 5 (eq_refl true) (eq_refl true).
Example qn_example3 : qn := make_qn 4 2 (eq_refl true) (eq_refl true).
I tried already some different approaches - also to define the qn record, e.g. using Prop instead of bool.
Is there a way to simplify the make_qn definition to directly include the proofs? E.g. to use it like
Example qn_simple1 : qn := make_qn 2 1
Consider this definition of qn (where I have renamed few things for convenience):
(* Define [qn] with conditions for [q] and [n]. *)
Record qn := mkQn
{
qn_q : nat ;
qn_n : nat ;
qn_q_ge_2 : qn_q >= 2 ;
qn_n_ge_1 : qn_n >= 1 ;
}.
With the premise that all functions in Coq must be total, we can in fact prove that there is no "short-cutting qn constructor" as per your question, i.e. that there is no (total) function that, given arbitrary q and n, returns a qn such that its qn_q = q and qn_n = n:
(* The type of "short-cutting [qn] constructors". *)
Definition MkQnSc := forall q n : nat,
{ i : qn | i.(qn_q) = q /\ i.(qn_n) = n }.
(* [MkQnSc] is empty! *)
Lemma no_MkQnSc : MkQnSc -> False.
Proof.
unfold MkQnSc.
intros F.
destruct (F 0 0) as [[q n Hq Hn] [Eq _]].
simpl in Eq.
rewrite Eq in Hq.
inversion Hq.
Qed.
Incidentally, a possible approach to a "short-cutting qn constructor" (as per your question) is by having option qn as the return type, though of course that just moves the goalpost, as then the need becomes that of pattern-matching on the returned option / proving we got a Some vs None.
That said, a way to mitigate the inconvenience of having to supply proof terms every time in the constructor (also mentioned by @Villetaneuse in a comment to his answer) is the use of notations with tactics, which can indeed be used to construct terms, though cannot be used in pattern matching (I am not aware of other significant differences, at least not in this case):
From Coq Require Import Lia.
Notation mkQnSc q n :=
(mkQn q n ltac:(lia) ltac:(lia))
(only parsing).
Example ex_qn_2_1 : qn := mkQnSc 2 1. (* OK *)
Fail Example ex_qn_0_0 := mkQnSc 0 0.
(* OK: Cannot find witness *)
Fail Example ex_qn q n := mkQnSc q n.
(* OK: Cannot find witness *)
Fail Definition is_qn_2_1 (i : qn) : Prop :=
match i with
| mkQnSc 2 1 => True
| _ => False
end. (* ERROR: Quotations not supported in patterns *)
Definition is_qn_2_1 (i : qn) : Prop :=
match i with
| mkQn 2 1 _ _ => True
| _ => False
end. (* OK *)