Ssreflect Users Discussion List

[Georges Gonthier <>]

  Basically, Yves's final "suspicion" is correct:
 STRUCTURE types like eqType, finType, finGroupType, etc. are NOT sorts, 
i.e., types of Types; a quick glance at their definition will show that they 
are types of RECORDS, one of whose components is a Type. The fact that the 
projection on that component is often declared as a coercion allows some 
abuse of notation that is both harmless and convenient for ABSTRACT 
structures, e.g., declared as section variables as in
  Variable T : finType.
but this ambiguity should not be extended to INSTANCES of structures for 
specific types, or, as both Yves and Assia experienced, chaos ensues.
  Specifically (and I wrote explicitly about this last fall), one should 
NEVER use a structure definition to declare a type at the vernacular (Module
or Section) level, as Yves was trying to do with
  Definition evolution := seq_finType [:: -1; 0; 1].
The reason is that this does not define evolution as a Type that has nice 
properties; it defines a record whose FinType.sort projection has nice 
properties. The problem is that this is a concrete definition, and that Coq
can at any time (and will!) iota-convert (evolution : Type) into the actual 
Type component of evolution, namely {x : Z | x \in [:: -1; 0; 1]}, which 
doesn't have all these nice properties, and has no connection with the 
evolution definition.
  The thing to do, instead, is to define evolution as the Type above, and 
then use the predefined canonical structures to give it lots of interesting 
properties; ssreflect defines a set of [someType of ...] forms that makes 
this fairly painless.
  It would be even better to follow Assia's suggestion and define evolution 
as a NEW Inductive type altogether, because of Coq has a tendancy to 
"overreduce" during type inference, which means that it can unfold past the 
definition of evolution, for example when it's looking for a coercion class.
The downside in this particular case is that fintype.v is missing some 
infrastructure for putting a finType structure on the new type -- basically 
I'd need to generalize seq_finType to work with any subType structure rather 
than only the one defined for Coq's sig ... type.
  Note that because Coq can use any defined constant as a coercion class, it 
is POSSIBLE to coerce from or to the "class" of all projections of a 
structure, e.g., EqType.sort can be used as a coercion class. However, this 
should NEVER be done, and Assia's "first mystery" shows why.
  In an odd dual to the "overreduction" problem, if Coq identifies 
EqType.sort as a coercion class, then it will never attempt to reduce a type 
of the form EqType.sort ... to find a coercion. This is what happens in 
Assia's script: in n == p, the expected type for p is EqType.sort nat_eqType
so Coq looks for coercions from the class of p -- ordinal here -- to 
EqType.sort if EqType.sort is a coercion class, and doesn't find any.
  Normally this is not the case, so instead Coq reduces the expected type of 
p to its head normal form to get the class -- nat -- for which it does find 
the coercion nat_of_ord.
  Therefore, one should never declare coercions to structure projections, 
unless it's part of the general architecture (for predType and groupType, in 
the current library). This is tricky, because the coercion class is itself a 
coercion, and therefore usually invisible! Fortunately, one is usually 
prevented from declaring coercions FROM a projection to a specific type by 
the so-called uniform inheritance rule -- this is why Yves' declaration got 
rejected. Unfortunately, there is little protection against declaring 
coercions TO a projection, and this is what happened to Assia : because her 
definition of Z_of_evo didn't have a type constraint, Coq extracted the 
target class directly from the inferred return type, EqType.sort Z_eqType.
  As for the second mystery, the answer is a bit trivial: vrefl uses prenex 
implicits, and the file did not include the Import Prenex Implicits directive 
that is required to make prenex implicits work across files. That 
technicality should go away with Coq 8.2 which (finally, after more than 5 
years of lobbying) support these directly.
  I'm inclding a few more comments in a revised version of Assia's script 
below.

  Cheers,

Georges

Require Import ZArith.
(* Coq libraries are not very nice as they Export other libraries,  *)
(* so you should Import libraries like ZArith before you Import the *)
(* ssreflect ones, otherwise they will reimpose the Coq notations   *)
(* for arithmetic, and you'll lose part of the ssreflect library.   *)
(*   Also it's better to split your Import line so that the core    *)
(* ssreflect libraries don't appear on the last line, otherwise you *)
(* will be bombarded with a screenful of spurrious warnings about   *)
(* redefined notation, etc.                                         *)
Require Import ssreflect ssrbool eqtype ssrnat seq.
Require Import fintype finfun.

Import Prenex Implicits.
(* Don't forget this! Also, you probably want to                    *
Set Implicit Arguments
Unset Strict Implicits.
 * if you're defining lemmas and constants that use structures.     *)

(* You shouldn't Open Scope at toplevel in a file, otherwise the    *)
(* Scope will be forced on all the files that Import this file.     *)
Module Import Zscope. Open Scope Z_scope. End Zscope.

Section Zeqtype.

(* eqType gives a more usable name to "proj1_sig" *)
Definition eqz x y := sval (Z_eq_bool x y).

(* Ssreflect makes it unnecessary to introduce assumptions with    *)
(* dummy names, only to destruct them immediately after. Removing  *)
(* all this sillyness REALLY shortens proof scripts.               *)
Lemma eqzP : reflect_eq eqz.
Proof. by rewrite /eqz => n m; case: Z_eq_bool; case; constructor. Qed.

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

End Zeqtype.

Section evolution.

(* This defines a REAL type. The predArgType constraint isn't all *)
(* that essential; it's just there to let Coq coerce evolution    *)
(* into its total predicate, so we'll later be able to write      *)
(*   Lemma card_evolution : #|evolution| = 3.                     *)
Definition evolution : predArgType := {x : Z | x \in [:: -1; 0; 1]}.

(* This works because val has prenex implicits, and because       *)
(* there's a canonical subType structure for all sigs whose       *)
(* predicate is in bool. We could also have written sval directly *)
(* since it is the value of @val _ _ (sig_subType _ _), and it    *)
(* also has prenex implicits.                                     *)
Coercion z_of_evo := val : evolution -> Z.

(* It's always nicer to use Eval hnf in combinations with the     *)
(*  [.. of ..] forms, because this computates the Structure once  *)
(* and for all -- otherwise Coq will redo the computation every   *)
(* single time the Structure is used!                             *)
Canonical Structure evolution_subType := Eval hnf in
  [subType for z_of_evo].
Canonical Structure evolution_eqType := Eval hnf in
  [subEqType for z_of_evo].
Canonical Structure evolution_finType := Eval hnf in
  [finType of evolution for seq_finType _].
Canonical Structure evolution_subFinType := Eval hnf in
  [subFinType of evolution].
(* Since we're instanciating both the finType and subType         *)
(* structures, we should also instanciate their least upper bound *)
(* in the class lattice.                                          *)

End evolution.

(* This is Assia's version, which I've outcommented since it      *
 * doesn't do what Yves wanted in the first place -- define a     *
 * a finite subtype of Z. I don't recommend using predArgType     *
 * here either -- it's just not worth the hassle.                 *
Section evolution.

Inductive evolution : Type := Evolution (x : Z) of x \in [:: -1; 0; 1].

Coercion z_of_evo x := let: Evolution y _ := x in y.

Canonical Structure evolution_subType :=
  SubType z_of_evo evolution_rect vrefl.
Canonical Structure evolution_eqType := Eval hnf in
  [subEqType for z_of_evo].

End evolution.
*)

Section network.

Variable t : finType.

(* The scope delimiter for nat is %N in ssreflect! *)
Variable n : nat.
Hypothesis npos : (0 < n)%N.
(* You might consider packaging the n > 0 constraint by declaring *
Variable n : pos_nat.
 * instead; n will coerce to a nat, and there's a nice set of     *
 * declared canonical instances for the pos_nat.                  *)

Definition state := {ffun t -> I_(n)}.
(* You should always use the {ffun ...} notation, even though Coq *)
(* will accept finfun t I_(n) here with t an abstract finType.    *)
(* This is because when you USE your library at a specific type,  *)
(* you'd rather see that type, rather that the obscure denotation *)
(* of its finType structure, in the types of proof variables. You *)
(* should also consider defining a {state ...} notation, using    *)
(* the same techniques as {ffun ...}, {set ...}, {perm ...}, etc. *)

(* This now works! *)
Definition licit (p : I_(n)) : pred evolution :=
  fun x => if 0%N == p then -1 != x
           else if n == p then 1 != x
           else true.

End network.