Início / coding / Perguntas / 77738685
Accepted
Andreas Florath
Asked: 2023-12-31 17:07:56 +0800 CST

Construção eficiente de registros em Coq: a inclusão direta de provas é possível?

  • 772

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
coq

2 respostas

  1. Best Answer

    Considere esta definição de qn(onde renomeei algumas coisas por conveniência):

    (* 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 ;
}.

    Com a premissa de que todas as funções em Coq devem ser totais, podemos de fato provar que não existe um "construtor de atalho qn" conforme sua pergunta, ou seja, que não existe uma função (total) que, dada uma and arbitrária , retorne tal que é = e = :qnqnqn_qqqn_nn

    (* 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.

    Aliás, uma abordagem possível para um "construtor de atalho qn" (conforme sua pergunta) é ter option qncomo tipo de retorno, embora, é claro, isso apenas mova a trave, pois então a necessidade passa a ser a de correspondência de padrões no retornado option/ provando que temos um Somevs.None

    Dito isto, uma forma de mitigar a inconveniência de ter que fornecer termos de prova todas as vezes no construtor (também mencionado por @Villetaneuse em um comentário à sua resposta) é o uso de notações com táticas , que podem de fato ser usadas para construir termos, embora não possa ser usado na correspondência de padrões (não tenho conhecimento de outras diferenças significativas, pelo menos não neste caso):

    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 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 *)
    • 1

  2. Aqui está minha tentativa de simplificar seu código.

    1. Eu uso Propem vez de boolporque liagosto Propmais, mas booltambém poderia ser mantido com outras ferramentas para provar as desigualdades (ou mesmo cálculos simples).
    2. Em vez de definir make_qnfora do registro, dou um nome ao construtor do registro.
    3. Eu uso ltac:(tactic)para construir termos de prova nos exemplos.

    Provavelmente não é perfeito (por exemplo, a igualdade para este registro precisa usar alguma forma de irrelevância de prova).

    Não creio que exista uma solução mágica para construir elementos sem fornecer termos de prova.

    Require Import Arith.

(* Define the qn record with conditions for q and n *)
(* I have changed bool with Prop. *)
Record qn := MakeQn {
    q : nat;
    q_ge_2 : q >= 2; (* Ensuring q is greater or equal than 2 *)
    n : nat;
    n_ge_1 : n >= 1  (* Ensuring n is greater or equal than 1 *)
  }.

Require Import Lia.
(* Examples of qn *)
Example qn_example1 : qn := MakeQn 2 ltac:(lia) 1 ltac:(lia).
Example qn_example2 : qn := MakeQn 3 ltac:(lia) 5 ltac:(lia).
Example qn_example3 : qn := MakeQn 4 ltac:(lia) 2 ltac:(lia).
    • 0

relate perguntas