The Coq mailing list

[Burak Ekici <ekcburak AT hotmail.com>]

Hi all,

I've been trying to prove Coq reals as an algebraic field instance.

Please find my code here:
https://github.com/ekiciburak/algebraic-groups-fields/blob/master/algebraic_groups_fields.v

Considering the last instance (at line 128):

"Program Instance field_reals: `(@field R (Req_setoid) _ rmult _ rid2 _ rinv2 
group_reals)."

I was not able to prove the below obligation (at line 132):

"Obligation 4 of field_reals:
forall a : R, a == rid -> rmult (rinv2 a) a == rid2 -> False."

This basically looks like

1 subgoals
H0 : 1 / 0 * 0 = 1
______________________________________(1/1)
False

after unfolds. When to say "revert H0; psatz R 1.", Coq does not
complain, but it is not happy either; I'm getting something like

1 subgoals
______________________________________(1/1)
let __wit := nil in
let __varmap := VarMap.Empty R in
let __ff :=
  Tauto.I
    (Tauto.A
       {|
       Flhs := EnvRing.PEc
                 (RMicromega.CMult
                    (RMicromega.CMult RMicromega.C1
                       (RMicromega.CInv RMicromega.C0)) RMicromega.C0);
       Fop := OpEq;
       Frhs := EnvRing.PEc RMicromega.C1 |})
    (Tauto.FF (Formula RMicromega.Rcst)) in
1 / 0 * 0 = 1 -> False.

I guess, this is because there is no witness for "psatz R 1" but I don't
know how to provide one.

I'd be more than appreciated if you could point me a way to get around
it. The problem might be a consequence of the way that I've
implemented things?

Many thanks in advance!

Best,
Burak.