coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions
Date: Wed, 8 Jul 2020 18:56:42 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:uGLgUx1/A37gHSy8smDT+DRfVm0co7zxezQtwd8ZseIfLPad9pjvdHbS+e9qxAeQG9mCtbQd26GM4+igATVGvc/c9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMt8Qam5ZuJ6U+xhfXoXZDZuBayX91KV6JkBvw+8e98IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QDtgGxCRW2Ce711jNEmn370Ksn2OohCwHG2wkgEsoSvXTbqtX1NbwSUeCyzKnN0D7OcfNW1i3h6IjUdRAhueuDUq9wccvR00YuFx7Og1KKpozqOTOV1/8Ns2ic7+plTu+gl2snqwBrrje12sggkIjJhoQMx13C6C52z5o7K8eiR05nfd6rDoFQtyeCOodqTc0vXmFltSImxrAYpJO2eDYHxpQ6yhPBZPKKfIaG7g/+WOqMPzp2imxodbC9ihi88EWtyvPwW8mp3VtKoCdIlMTHuH4K1xzW8MeHS/1981+g2TaJzQDT6/tLLVo6larBLZMq370+loILvEjeAyP7mF/6gLGZe0gn4OSk9fnrbq/7qpKfK4N4kh/yPrgql8ClAuk1MhICU3Wa9Om9zrHv4E70TKhMg/YriKfWqoraKt4epqOhAw9azIIj6xGnAjejytsYnH0HIEhZdxKCjojlIUvBL+ziAfe+hVSgiDZrx/bYMb39GpjBM2XPnbf7cbpj5ENRyxA/wc5C655OF70MI+7/Vlf0tNPCDx85NwK0w/zgCNV4zo4RQ22PAqmYMKPJsV+I4ecvLvKQa48QuTbxMeIq6OL0gX84n18RZbOp0ocPaHCkAvRmJF2UbmbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTAVeVVHzsao+sWvEWaSvULNUyvCYDUO2IRIkgzhGpsUfRy7N7Mu3M8yEYpJvynIx86OvSjhE18BR/CsXb2mrLTmcizTBAfCM/wK0q+R818VyEy6Ut26UFR+wW3OtAV0IBDbCZz+F+DImsCAfIf9PPQ1OnBNytRzA3HIpon40+Jn1lEtDntSjtmjKwCuZMxbeOBdo9+eTd2Sqpfpcv+zP9zKAkymIebI5KPGyiiLR48lGKVYXMkgOQnOCrc/ZF0Q==

Thanks for pointing out this feature of => i. I will look into the documentation and try to understand how it works.

On Wed, Jul 8, 2020 at 6:49 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi,

I am not sure I follow everything but it seems that in your particular
example you could use Nat.min_0_r.

More generally if you look at the documentation of under you can
handle binders :

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html

For example, interactively this gives:

From mathcomp Require Import ssreflect.
Require Import List PeanoNat.

Goal forall l, (map (fun i => i + 1) l) = l.
Proof.
move=> l.
under map_ext => i.
replace (i + 1) with (1 + i); last first.
by rewrite Nat.add_comm.
over.

Hope this helps

--
Laurent

[Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Agnishom Chattopadhyay, 07/08/2020
- Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Laurent Thery, 07/08/2020
  - Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Erik Martin-Dorel, 07/08/2020
    - Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Agnishom Chattopadhyay, 07/08/2020
      - Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Laurent Thery, 07/08/2020
        
        Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Agnishom Chattopadhyay, 07/09/2020
        
        Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Laurent Thery, 07/09/2020
        
        Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Agnishom Chattopadhyay, 07/09/2020
        Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Kyle Stemen, 07/09/2020
        
        Re: [Coq-Club] Rewriting inside map expressions to manipulate finite/indexed sum expessions, Kyle Stemen, 07/09/2020