coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] BigOp equality over differing indices
Date: Thu, 28 Nov 2019 14:17:50 +0100
Autocrypt: addr=thery AT sophia.inria.fr; prefer-encrypt=mutual; keydata= mQENBE3a3V8BCADTeORKU7I7UmBBcs4VhSCq1IgKD8vdmdrGAlF3IJSFng7Fk8+MgS2gWYcS Ukf5t+rjNM3Z6brfYXc1naZlf2JPGHvAGiz8+TkXL+/ZA6+gAoIKy/iKyD+hCD8m92WH3rPH vCX6EJ44FEI7gUJ37GlTjvuP0I55vaFcwEg8nDgkALaCJvrSHtePuPKR1Q+9q2dgR7fTObal HYGMAsgT6k6n2ofe4Q6VFRLJhruU02qAfV5zgIoa3xgrTwSr4RRDILHttAw7EN6aLG6JycJ7 sPsPsiQzrd/tFsNbiHYeojJCkU2pDSQ3pBtXAJL/z2pMWTeTXvA60l9w0sDO7M3mkC3vABEB AAG0J0xhdXJlbnQgVGjDqXJ5IDxMYXVyZW50LlRoZXJ5QGlucmlhLmZyPokBOAQTAQIAIgUC TdrdXwIbAwYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQHHaWvRTi0tpIgggAnSUYcU2N uchXkGGwmPuLmvSUMiLkyFPs9GF2YF1ONOuJtpnQMcpsseCkcmIjESz0h5OpknpyraUXvbh0 ZdFqaLC2E+GyV8/YQi71wSsTPgWP450u0XUt0ysjwkKW6aIxIhSzrtgNp4E6w5KzXVJxA/yM V5RNFHg/5uifgfv4b7xaGHV8L93NbSvedk1O7yje5Hqgfab0t6J5Kf0M3sG+pB3gEkDVK9B7 +0fhe7/5u1Nj5HoLWid8UNZfFzJzb18Xe2ckzNye0KdDtQFac8qGUzhLbEYt3ScYjRYTq9/d V4Cin39j7Oo64Nk71iiLBISyuk0Q9D+Jq7nwwcQr/R8s1rkBDQRN2t1fAQgA7H6aX6BfdO/X Vlf4EGEoyFQ5u/JDe+giIHWSS34YWDWVUYyp320CrAYAkh9lQ1Nvh1tsmgiUh5xnY7wY0tOi wJSm94XlYAmHrddmWVNXRn09GvZJhfI2LdVBg3oxPfc8+bV+Hz83z/5BMPLOogxB22QMPJ6e iD2EsUMPNsuCVQ8WNo6ZmueuuYe7vEUXLYdRXNumJJgekEuG/q1BD4xgfzWpWfUODm6WygWZ oov50DomcDcAHW03bgnHlqnYu20Qg00GqgR3FKlORTvnOxD5TMCXe+eLUxkQfvnjbIPhtrnJ hgJMKVkRBEoaQ/XA4FdvxloInYPbqxNZ72yd09BbewARAQABiQEfBBgBAgAJBQJN2t1fAhsM AAoJEBx2lr0U4tLaWNQH/2/fIaF9ngbKPBJbDxYa7glJuCfamJgy3R8mJ//VYsS4RbdroSX3 29EgWlTx2reu1b4C5n5k7l4KpLgsRIc3bLUasGv15nf8BqmKIMulidzsxJv86S2imY/0870Q NOiO9SElHE7/2q4J1m2ew77SegiqGVWHl6Zs+4ROfOILTy24o26BQMAZhPX7jEs04Atv6yjw OUIPbzFO+XRuKqkBwHn9S8+GQelT0Gh84Dc5D2jIF0+kWY7uHqe2O+2LPfgO2CYhqmVfr/Ym mZv2xUyhJ7gui2hYaggncQ96cM2KhnKlgMw8nStY0GTqVXLEjPYblz8mqtF8aBPRSk/DjjrF QeI=

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

[Coq-Club] BigOp equality over differing indices, Kiran Corbett Gopinathan, 11/28/2019
- Re: [Coq-Club] BigOp equality over differing indices, Laurent Thery, 11/28/2019
  - Re: [Coq-Club] BigOp equality over differing indices, Kiran Corbett Gopinathan, 11/28/2019
    - Re: [Coq-Club] BigOp equality over differing indices, Laurent Thery, 11/28/2019
    - Re: [Coq-Club] BigOp equality over differing indices, Emilio Jesús Gallego Arias, 11/28/2019