Quero definir um pequeno registro no Coq que também inclua certas condições. Além disso quero uma definição para criar um registro de maneira fácil. Aqui está minha abordagem:
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).
Já tentei algumas abordagens diferentes - também para definir o registro qn, por exemplo, usando Prop em vez de bool.
Existe uma maneira de simplificar a make_qndefinição para incluir diretamente as provas? Por exemplo, para usá-lo como
Example qn_simple1 : qn := make_qn 2 1