Ssreflect Users Discussion List

[Yves Bertot <>]

I wanted to create a finite subtype of Z.  Here is my example.

Require Import ssreflect ssrbool eqtype ssrnat seq fintype finfun.
Require Import ZArith.

Open Scope Z_scope.

Section Zeqtype.

Definition eqz (x y:Z) : bool :=
 let (b, _) := Z_eq_bool x y in b.

Lemma eqzP : reflect_eq eqz.
Proof.
move => n m; apply: (iffP idP); rewrite /eqz.
case (Z_eq_bool n m) => x; by case x.
case (Z_eq_bool n m) => x; case x => //.
Qed.

Canonical Structure Z_eqMixin := EqMixin eqzP.
Canonical Structure Z_eqType := EqClass Z_eqMixin.

End Zeqtype.

Section evolution.

Definition evolution := seq_finType [:: -1; 0; 1].

Definition Z_of_evolution (x:evolution) : Z.
move => x; case x => y _; exact y.
Defined.

(* mark here, for later reference *)
End evolution.

Section network.

Variable t : finType.

Variable n : nat.

Hypothesis npos : (0 < n)%nat.

Definition state := finfun t I_(n).

Definition licit (p:I_(n)) : pred evolution :=
 fun x => if 0%nat == p then negb(-1 == x)
          else if n == p then negb( 1 == x)
          else true.

The definition of licit is not accepted, because x has type evolution,
while the expected type is Z.  A coercion is missing.  I wanted to add
this coercion at the place marked by (* mark here, ... *), but the following
command is rejected:

Coercion Z_of_evolution : evolution >-> Z.

By comparison, the following Coq command is accepted.

Require Import ZArith.           

Definition s := {x:Z | x^2 <= 1}.
Open Scope Z_scope.

Definition s := {x:Z | x^2 <= 1}.
Definition Z_of_s (x:s) : Z. 
intros x; case x; intros v _; exact v.
Defined.
Coercion Z_of_s : s >-> Z.

My guess is that finType is not considered as a sort, and thus its elements
are not accepted as coercion classes.  Is there a way around this 
limitation?

Yves