Coq: Stuck using the subtype

Question

I have following definitions: (definition of positive integers as a subtype of 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.

But I stuck on showing that the Z_pos_mult is compatible with the multiplication b/w natural numbers:

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

How can I solve this?

Answer 1

Here is how I would do it in vanilla Coq. I'm assuming we can still tweak the definitions.

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.

Let me add that dealing with this kind of thing is much more pleasant in SSReflect/Mathcomp.

Answer 2

Your definition of Z_pos_mult is too complicated. It relies on dependent pattern matching right from the start. I advise to use this kind of dependent pattern matching only for proofs, not for definitions.

Here is an alternative definition. Not that it fixes the returned value before doing any proof.

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.

With this definition, the proof you request is easy to write.

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.

In principle, the proof for your code is also possible, but this is exceedingly difficult.

Answer 3

IMHO answering this question in the original form is advocating a questionable style. I think that multiplication for such numbers should be just the multiplication of the base type; and the proof should just follow from injectivity of the projection, as is done in mathcomp.

In general, you are going to have quite a lot of problems if non-fully opaque proofs appear in your terms after reduction.