The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 1 Nov 2013 02:38:10 +0200,
Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>
 a écrit :

> https://github.com/zaarcis/linear_algebra_in_Coq
> 
> (Matrix multiplication is incomplete yet. I have no idea right now,
> how to finish it, but trying now.)
> 
> Any criticism/suggestions how I could make it better (but with sigma
> types)? Advanced tactics are in my close future plans too, of course.
> 
> Thanks in advance.

For now, I just looked your field.v and have the following remarks:

Mathemetical nomenclature:
* "fld_trans" should probably renamed as "fld_distributivity".

Coq programmer point of view:
* You may find the "Class" keyword of interest later. I do not develop
  it, as this topic could be considered an advanced one, and you may
  not be at ease yet. Just keep this in memory for later.
* If you do not have some axiom of choice, I recommend to define an
  opposite and an inverse function, rather than asserting existence of
  an inverse element and existence of an opposite element.
  fld_opp: fld_T -> fld_T;
  fld_opp_spe: forall (a: fld_T), fld_plus a (fld_opp a) = fld_zero;
  replacing your fld_opp_ex.
  For inverse, it is harder, as you have many ways to deal with the zero
  problem. Here is one of the solutions:
  fld_inv: fld_T -> fld_T;
  fld_inv_spe: forall (a: fld_T), a <> fld_zero -> fld_mult a (fld_inv
  a) = fld_one;
  (that is, we allow "fld_inv fld_zero" to exist, but we do not specify
  anything on it. Having a "fld_inv : ∀ x, x≠fld_zero → fld_T" would
  also be usable, but often not very convenient as you need to give non
  zero proofs everywhere, and will probably need to prove
  "∀ x H K, fld_inv x H = fld_inv x K" which would be provable, I
  think, using "fld_inv_spe" [note that without it, it would not be
  provable]).