The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

Long story short: you have uncovered a problem of psatz - thanks for the bug 
report!
revert  H0 ; generalize (1/0) ; psatz R 1 does the trick

The problem is that you goal is not syntactically linear.
psatz tries to linearise goals by reconstructing rational constants.
My guess is that it fails because of the division by zero - I would need to 
investigate further...
Here, it should not produce a partial proof term but really fail— there is an 
unfortunate try in the tactic. 

Best,
—
Frédéric

> On 05 Apr 2016, at 06:00, Burak Ekici 
> <ekcburak AT hotmail.com>
>  wrote:
> 
> 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.
>