coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: noam neer <noamneer AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] proving a simple equality
Date: Sat, 19 Nov 2016 04:03:56 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=noamneer AT gmail.com; spf=Pass smtp.mailfrom=noamneer AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
Ironport-phdr: 9a23:BI6+VBTUnZu0Pdsnz/62CTIwsNpsv+yvbD5Q0YIujvd0So/mwa68YxeN2/xhgRfzUJnB7Loc0qyN4vumAD1LvcrJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBu7oR/MusQSjodvJak8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5Vr4/6p1QUqBu1GA+sC/3xxT9Sm3T72qs60+M7HgHD2gwvAcwBsG7PodX6MacdS+G1zK3SwTrfaPNW3C7w5Y7VeR4iufGBRbB9fMXLxUUyCQ/Ijk+cpI/7Mz+P1ukBr26W5Pd6W+21kW4osQRxryCvxsgyjonJgZoYylXe+iV4xIY5PNO5SEtnbdK9Hptdtz2WO5F5QsMlRGFotyI6xaMctZGneygKzYwrxx/Za/OZb4iF+hDuWemLLTtlmn5oeKizihWs/US6yuDwStG40FNQoSpEltnMuGoN1xvW6sWfTPt9+V2u2TOJ1w/N9O5EO1s5laXeK5E7w74wkoAfvljEHi/zgEn2lrOZdl04+ui07OTqeqnpppiFN4Ntlg7+NrkuldekDOQjMgkOWnCb9v6m2L3i+035WrRKgecsnqnXqpCJbfgc86W+Gkpe1pspwxe5FTavltoCzlcdK1cQfhWOisDvNlzUaKT+Cv66hVmhih9kwvnHOvvqBZCbfSuLq6voYbsosx0U8wE0190Kv58=

hi,

I'm relatively new to Coq, and I'm mainly interested in real (in)equalities.

I just tried to prove by myself the simple identity

(a+b)^2 = a^2+2ab+b^2

and succeeded with

Require Import Reals.

Open Scope R_scope.

Goal forall a b, (a+b)^2 = a^2 + 2*a*b + b^2.

intros.

field.

Qed.

but then I tried the same thing with the real power operator, i.e.

Goal forall a b, a>0 -> b>0 -> Rpower (a+b) 2 = (Rpower a 2) + 2*a*b + (Rpower b 2).

and I wasn't able to finish the proof.

what would be the easiest way to prove this?

thanx, Noam.

[Coq-Club] proving a simple equality, noam neer, 11/19/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/19/2016
  - Re: [Coq-Club] proving a simple equality, noam neer, 11/20/2016
    - Re: [Coq-Club] proving a simple equality, Gaetan Gilbert, 11/21/2016
    - Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/21/2016
      - Re: [Coq-Club] proving a simple equality, noam neer, 11/22/2016
        
        [Coq-Club] Re : Re: proving a simple equality, Laurent Thery, 11/22/2016
        
        Re: [Coq-Club] proving a simple equality, Guillaume Melquiond, 11/22/2016