The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Vincent,

I just tried  Require Import Psatz. for invert (A+A=B+B so A=B? Prove
it!), and lia works without any problem.

Cheers,
Mukesh

On Fri, Jun 28, 2019 at 7:31 PM Vincent 
<vincent.siles AT gmail.com>
 wrote:
>
> I'll definitely try lia ! I tried with the Require Import but got an error. 
> Maybe it was disable for this particular (very simple) exercise. Will try 
> again :)
>
> Le ven. 28 juin 2019 à 10:57, Théo Zimmermann 
> <theo.zimmi AT gmail.com>
>  a écrit :
>>
>> Hi Vincent,
>>
>> "omega" is available actually: you just need to import it "Require
>> Import Omega."
>> Most people nowadays use "lia" though since "omega" is about to be
>> deprecated in favor of "lia". (Using "lia" requires you to "Require
>> Import Lia.")
>>
>> Théo
>>
>> Le ven. 28 juin 2019 à 10:47, Vincent Siles
>> <vincent.siles AT ens-lyon.org>
>>  a écrit :
>> >
>> > I played a bit with it this morning, it's nice. I have the same remark 
>> > as Agnishom plus a minor one: could Omega be available ? That would be 
>> > helpful to discharge some annoying arithmetic proofs :D
>> >
>> > Le ven. 28 juin 2019 à 10:30, Agnishom Chattopadhyay 
>> > <agnishom AT cmi.ac.in>
>> >  a écrit :
>> >>
>> >> This is great. Somewhat similar to Proof Ground and Proving for Fun.
>> >>
>> >> It is actually quiet difficult to work with the web interface since it 
>> >> does not provide the interactive Coq environment. So maybe we can have 
>> >> a Coq IDE or links for downloading the ``Preloaded" files?
>> >>
>> >> --Agnishom
>> >>
>> >> On Fri, Jun 28, 2019 at 7:13 AM Donald Leung 
>> >> <i.donaldl AT me.com>
>> >>  wrote:
>> >>>
>> >>> I hereby write to you to invite you to sign up for an account on 
>> >>> Codewars: https://www.codewars.com
>> >>>
>> >>> Codewars is a training platform where programmers of all disciplines 
>> >>> train on code challenges called Kata in order to improve their 
>> >>> programming skills. The Coq proof assistant was recently added to 
>> >>> Codewars (approx. April 2019) and there are currently insufficient Coq 
>> >>> users to push newly authored Coq challenges out of the Beta (testing) 
>> >>> phase; therefore, it would be an honor to have a seasoned Coq user 
>> >>> like you on Codewars to test them out and contribute more interesting 
>> >>> Coq challenges to the community.
>> >>>
>> >>> Should you choose to create an account on Codewars, you are also 
>> >>> welcome to ask any questions about the Codewars platform in general or 
>> >>> simply chat with other Codewarriors via our Gitter channel: 
>> >>> https://gitter.im/Codewars/codewars.com
>> >>>
>> >>> Yours sincerely,
>> >>> Donald Sebastian Leung
>> >>> A Year 2 CSE undergraduate at The Hong Kong University of Science and 
>> >>> Technology