naming_convention.org

Naming convention for validsdp

Naming convention

Type classes for arithmetic operations (associated with a notation)

• (Class name, constructor name) := (foo, foo_op)
• Example:

Class add B := add_op : B -> B -> B.
Local Notation "+%C" := add_op.
Local Notation "x + y" := (add_op x y) : computable_scope.

• PR: maybe we could just make Float_infnan_spec (or even Float_round_up_infnan_spec) a record typeclass with all operations, we only need floats anyway ?
• EMD: I don’t think so: the use of operational typeclasses (roughly, one typeclass for each operation) is important in CoqEAL’s approach to facilitate the specification and refinement of these operations.

Type classes associated with no notation

• (Class name, constructor name) := (foo_class, foo)
• Example:

Class row_class I B := row : forall (m n : nat), I m -> B m n -> B 1 n.

Type classes for specifications

• (Class name, constructor name) := (foo_spec, foo_prop)
• Example:

Class I0_spec
  (ord : nat -> Type) (n : nat)
  `{!I0_class ord n, !nat_of_class ord n}
  := I0_prop : nat_of I0 = 0%N.
Arguments I0_spec _ _ {_ _}.

• PR: shouldn’t we put the spec in a common record with the specified function ? (we don’t plan to use the function without its spec)
• EMD: the quick answer is no, because of my remark above on operational typeclasses; however it is true that this formalization style (with I0_spec, etc.) is not the only possible one: indeed we could preferably state a similar result for proof-oriented instances only (here, I0_ssr), prove a refinement result (param_I0) and derive if need be the result on computation-oriented instances by refinement, without declaring *_spec typeclasses everywhere… we’ll discuss this on next meeting if you want.

Type-class instances and related definitions

• for proof-oriented instances : suffix ssr
• for computation-oriented instances :
  • (prefix cpt, eff, raw ?)
  • suffix seqmx := list-based matrices
  • suffix instN := natural numbers
  • suffix instFI := float_infnan_spec.FI (_ : Float_infnan_spec)
  • suffix instFI_b64 := float_infnan_spec.FI binary64_infnan
  • suffix instFI_flx53 := float_infnan_spec.FI coqinterval_infnan
  • suffix instF_flx53 := Interval_specific_ops.s_float _ _, without the proof invariant FI_prop : mantissa_bounded FI_val
• all “canonical” instances should be declared as global instances

Lemma names

• param_(Def) or (Pred)_(Def) for “parametricity lemmas”, e.g.: Rseqmx_rowseqmx
• refines_(Goal) for necessary/sufficient cond. of refinement pred., e.g.: refines_nth, refines_seqmxP
• (…)