Coq：卡住使用子类型

Question

我有以下定义：（将正整数定义为 nat 的子类型）

Definition Z_pos_filter (p: nat) : bool :=
  if (beq_nat p 0) then false else true.
Definition Z_pos: Set := {n : nat | is_true (Z_pos_filter n) }.

Definition Z_pos__N (p: Z_pos): nat := proj1_sig p.

Definition Z_pos_mult (p q: Z_pos): Z_pos.
destruct (Z_pos_filter (Z_pos__N p * Z_pos__N q)) eqn:prf.
- exact ((exist _ (Z_pos__N p * Z_pos__N q) prf)).
- assert (forall n: nat, S n <> 0) by (intros; omega).
  assert (forall a b: nat, a <> 0 /\ b <> 0 -> a * b <> 0).
  { intros. destruct a, b. omega. omega. omega. simpl. apply H. }
  assert (forall r: Z_pos, Z_pos__N r <> 0) by apply Z_pos_nonzero_N.
  assert (Z_pos__N p * Z_pos__N q <> 0) by (apply H0; split; apply H1).
  unfold Z_pos_filter in prf.
  rewrite <- beq_nat_false_iff in H2.
  rewrite H2 in prf. inversion prf.
Defined.

但我坚持证明Z_pos_mult 与自然数乘法兼容：

Lemma compat: forall p q: Z_pos, Z_pos__N (Z_pos_mult p q) = Z_pos__N p * Z_pos__N q.

我该如何解决这个问题？

Answer 1

您对 Z_pos_mult 的定义太复杂了。它依赖于依赖模式匹配 从一开始。我建议仅将这种依赖模式匹配用于证明，而不是用于定义。

这是另一种定义。并不是说它在做任何证明之前就修复了返回的值。

Definition Z_pos_mult (p q : Z_pos) : Z_pos.
exists (Z_pos__N p * Z_pos__N q).
destruct p as [p ph]; destruct q as [q qh].
unfold Z_pos_filter in ph, qh |- *; simpl.
destruct (p =? 0) eqn: ph'; try discriminate.
destruct (q =? 0) eqn: qh'; try discriminate.
rewrite beq_nat_false_iff in ph'.
rewrite beq_nat_false_iff in qh'.
destruct (p * q =? 0) eqn:pqh'; auto.
rewrite beq_nat_true_iff in pqh'.
destruct p; destruct q; try solve[discriminate | case ph'; auto | case qh'; auto].
Defined.

有了这个定义，你要求的证明就很容易写了。

Lemma compat: forall p q: Z_pos, Z_pos__N (Z_pos_mult p q) = Z_pos__N p * Z_pos__N q.
Proof.
intros [p ph] [q qh]; unfold Z_pos_mult; simpl; auto.
Qed.

原则上，你的代码的证明也是可能的，但这是非常困难的。

Answer 2

恕我直言，以原始形式回答这个问题是在倡导一种有问题的风格。我认为这些数字的乘法应该只是基类型的乘法；并且证明应该只遵循投影的注入性，就像在 mathcomp 中所做的那样。

一般来说，如果非完全不透明的证明出现在你的约简之后，你会遇到很多问题。

Answer 3

这就是我在 vanilla Coq 中的做法。我假设我们仍然可以调整定义。

From Coq Require Import Arith.
Local Coercion is_true : bool >-> Sortclass.

Definition Z_pos: Set := {n : nat | 0 <? n }.

Definition Z_pos__N (p: Z_pos): nat := proj1_sig p.

Definition Z_pos_mult : Z_pos -> Z_pos -> Z_pos.
  intros [x xpos%Nat.ltb_lt] [y ypos%Nat.ltb_lt].
  refine (exist  _ (x * y) _).
  now apply Nat.ltb_lt, Nat.mul_pos_pos.
Defined.

Lemma compat: forall p q: Z_pos, Z_pos__N (Z_pos_mult p q) = Z_pos__N p * Z_pos__N q.
Proof. now intros [x xpos] [y ypos]. Qed.

让我补充一点，在 SSReflect/Mathcomp 中处理这种事情要愉快得多。