Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] BigOp equality over differing indices

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] BigOp equality over differing indices


Chronological Thread 
  • From: Kiran Corbett Gopinathan <e0427802 AT u.nus.edu>
  • To: Laurent Thery <Laurent.Thery AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] BigOp equality over differing indices
  • Date: Thu, 28 Nov 2019 15:28:02 +0000
  • Accept-language: en-GB, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=u.nus.edu; dmarc=pass action=none header.from=u.nus.edu; dkim=pass header.d=u.nus.edu; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=hFIIpoXuSV6ACm/qR8bYBEfwHPpB56CwlDSNTOwrL0w=; b=d5X35PdRXqDIcxSja82NG77ORfabGEp8B+vkna+iIJv1dp4Mu/VYJ8zrz5S1d+UAB+Iu+Nw5PbG8xTcPDjHPhZK7+7m7YZlF/MHk0dtSe0ZxCExrObIExgqL7G0DpNSZUoZZ9MG5YIYnyjqfeZymToMnll/k69CuzwZZaL3m++NXk1bg2cYFPNF1FyXTgQUu+TCLyzZbNOTgrvVTXm4X6W3nSznGCjCcUkQPb/R3W3cCB0SwzIlNhwmTzD0lpWK6/x+0zkigM2VS1r/1VZteCjLM/IQkyTIzdR5llnKyA/8jnJGZQOhZvtVK94sMqJzpD2wJf+dNWsoXIUyxCzHZwg==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=ejFsHVmgCGqDwyCt4BFV6XPbepA/jjJgjwTLMAXuhgpfaA5UsX044zu7m1h/BloitWmZ/l2TKHBbMEg6SRgSmeqc0rz1O8rGN2keGGOZxHy25SAPJHwemsrJwycEZH8ACdg27EoTCOTQOYCg391UrMQI2cUwyvWiPR721u42eAAq+bK/lnNK1hDi0C+xSwKpCb6bx8l9iWOwhQZ+btVcWVTD6s96WmZMbnNGNLBeDls2GJxFWWJU8XnYtVZtquXbCIKVIiqABulHEfdxeAoDKmLkO/dgtjJr5cUTLS5QcZaodUg4fuVF1zQAINsGFI0bG/fQmiP7cSUTnR+ux35a/A==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e0427802 AT u.nus.edu; spf=Pass smtp.mailfrom=e0427802 AT u.nus.edu; spf=Pass smtp.helo=postmaster AT APC01-PU1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:6CpVihIskRpu9iMRgNmcpTZWNBhigK39O0sv0rFitYgXKv77rarrMEGX3/hxlliBBdydt6sfzbOI7Ou/ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngi6oATTu8UZg4ZuN7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6mb4YXD+QPI/tWr5XzqVUNoxuxBwisC//gxTJTnHD6wbE23v49HQ3awgAtGc8FvnTOrNXyMacfSeW7zKjSzTrZafNdxCnw6I/Sch86v/6MQa5wetfQx0koDwPFj1OQppb5PzOVzOsNtXWQ4u1+Wu6zhGMrtQN8rzuzyssykYTJm5gZylbZ9SVi2oo6O8C3SFNibNOiDZBetDmaOpN5T88+WW1kpTo2x78ctZKmciUG1o4ryhrCZ/CfboSF7BDuWPyMLTp2mn5pYqyziwus/US6y+DwTse030hJoyZZl9TBs2oC2hzd58WHT/Zw8Ees1i2S2A3W5OxIPFs7mbfeJpI8wLM/iJQevELeFSHsgkr2lrWZdkA89+io9evnZrLmq4eAOoFulAzyLrkiltWlD+s2LwQCRm+b9v+i27H5+k35XalKgeYxkqnEtpDVON4XprajAw9SzoYs9QqwDyun0NQfm3kLNlVFeA+bj4jtPFHOJ/P4Ae2jjFSrlTdn3/HGPrv/DZXRNnXOn6vtcaxg50JAygc/181T6pxKBr0bJP//R1f9tNnCAR84Nwy0zfznCNJ41o4GR22DHqCUPL3QvFKL+u4jPfKBZJIPtDb7Nvgl/OTigmEkll8AZaWpx4cYaGikHvR6JEWUeWbsgtcfHmcQvgszV+3riFyHUTFIfXa9Rbgw5jA9CIK8DIfMXJqhgLKb3C2jBJ1ZenhGCkyQEXfvb4iLR/AMaDuLLsB9ljwESKOuRpQ61RCusQ/606BoIvDV+i0er5Lj1cJ66/fdlREopnRICJG52nyXQmdo1l8ISiUnlPRbqFFnx1Gfl5R4juZJPd1V/fJAFAkgY9qUhed9EpX5Xh/LVtaPUlevBNu8S3llRdUohtQKfkxVGtO4jxmF0TD8UJEPkLneJ50u+6SU9H/rLcth1z7p07EgiVA6QsJJfTmr3vIlqFiLXabU1UOEjOCneblKj32Fz3uK0Wfb5BIQawV3S6iQGClHPhKH/+S83VvLSvqVMZpiNwJAzcCYLa4TM4/0y1NbX7HuNMmMOjvtyVf1Pg6Bw/a3VKSvY38UhXyPFQ4CjhtV8HqbZ1BnW3WR5lnGBTkrLmrBJkPh9e4i9yGSdmRslkSyUhQk0LC4vBkImfabVvUfmKoevzssoCl1G1D72M/KD92HpExqe6AOON4=
Hi Laurent,

Apologies, my example wasn't quite clear enough to exactly capture the difficulty in my situation.

One problem is that my summation doesn't split quite as nicely as the one in the example, and the corresponding elements on each summand may be interleaved, ruling out the possibility of simply splitting the summation. Additionally, the size of the mapping between summands (2 in the example) is actually given by an _expression_ on the index of the sum - i.e rather than 2 * f(even(i)), I have something like g(i) * f(even(i)).

Now, in my case, I can prove there exists a mapping between the summands of each summation - for each element in one sum, I can find g(i) distinct unique elements in the other sum, but I'm not sure how to manipulate the goal such that applying this mapping is possible.

Thanks,
-----
Kiran Gopinathan.
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Laurent Thery <Laurent.Thery AT inria.fr>
Sent: 28 November 2019 21:17
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] BigOp equality over differing indices
 
        - External Email -



Hi,

I am not sure this will help you in your general problem.
But in your particular example, you can split the sum to make
the reindexing possible.

Lemma example: forall f, \sum_(0 <= i < 4) (2 * f (even i)) = \sum_(0 <=
i < 8) (f (even i)).
Proof.
move=> f.
rewrite [RHS](big_cat_nat _ _  _ (_ : 0 <= 4)) //=.
 rewrite -[4]/(0 + 4) big_addn /= add0n.
rewrite  [X in _ = _ + X](eq_bigr (fun i => f (even i))) => [|i _]; last
first.
  by rewrite addnC /=;  case: i => [|i]; rewrite  ?negbK.
rewrite -big_split.
by apply: eq_bigr => i _ ; rewrite /= mul2n addnn.
Qed.

--
Laurent

Ps : this 8.10 code

Archive powered by MHonArc 2.6.18.

Top of Page