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?
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.