The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2016-08-05 11:18 GMT+02:00 Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>:

Hi all!

1/ I don't remember the Internet tool to chat with Coq users, to ask
   simple questions. I used it once a long time ago, but I did not
   notice what I used, and I cannot find it again through google.

​IRC (Internet Relay Chat)?​

 

2/ The immediate question that I have now is how to prove that the
   hypothesis (1 / 3)%R = 1%R is contradictory? I tried discriminate,
   discrR and other field_simplify. But I cannot manage to finish it
   in a simple way. A research on google gave me nothing interesting
   but perhaps I did not put the good terms.

​Deciding equality on R is highly non trivial in general.​

But it should be easy to prove that

(1/3)%R = 1%R => (1/3)%R * 3%R = 1%R * 3%R => 1%R = 3%R.

From here, I am pretty sure that you have a lemma or an hypothesis telling that injection from Z to R is … injective. So that you should end with a last "=> 1%Z = 3%Z". At this point the proof of False is easy with discriminate or other tools.

 

Thanks.

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/