coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof about applying a function on each element of a list using automaton

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: Lily Chung <ikdc AT mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton
Date: Tue, 2 Oct 2018 17:13:37 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT smtp.uni-bremen.de
Ironport-phdr: 9a23:rq3uiR+ze7LPpv9uRHKM819IXTAuvvDOBiVQ1KB41+IcTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhHohikZKjA382/XhcNsg61Goh2svAB/z5LObY2JKPZyYqHQcNUHTmRBRMZRUClBD5u8YYsVDuoBIeRYr47zp1ATsBa+AhOsBOXxxTBTm3/2xrE10+Q8GgzB0gwgBdMOsGjWrNXyOqcfSv21zK/JzTnadPxWwyny6I3WfRAnu/2DQKx/fNPXxEIyFA3Flk2dpZHrMj6azOgBrnSX4/R6We+vl2IrsRx9rzq3yssxhITEiZgZxk3Y+Sln2oo5O8C0RU1hbdK6DZdcqyeXPJZsTMw4WWFnoiM6x6UGuZGleCgKz4wqxwXaa/yba4iE+A/jVOCQITthn31lYqywhxOs/kim0OHzS9e73E5LripDjNbMqmgA2wHd58WIUPdx41ut1SiV2w3T9u1IO104mKjDJ54k2LEwl54TsUrZHi/xnUX7lKGWdl8l+ui06eTnZbvmq4SBN49yiwHyK78hmtahDuQ9LAcOWXKX9vmi27H75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXiP7nwSr7NM37M2OPgfrp2w0td1Ew+wc0JtLxODbRUDujyRk32upTyCQU/Pgap2O3nQIFzzIICW2WBKrKfMebYq1KN6+RpL+TaN9xdgyr0N/Vwv62mtnQ+g1JIJfD4j6tSU2ixG7FdG2vcZHPthtkbFmJT41gjSu2vgkePVDNVIXq/DftlumMLTbm+BIKGfbiDxaSb1X7mTIBQZyVMEF2JHHGue4jWA65ROhLXGddol3k/bZbkS4Il0kv25hT/16IhM+zVvycCuJfu0p556r+LmA==

On Tue, Oct 02, 2018 at 10:01:53AM -0400, Lily Chung wrote:
> <div dir='auto'>Probably you need to generalize over s in your inductive
> hypothesis.</div>

thank you, that does the trick.

regards,
--f.

Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Fritjof Bornebusch, 10/01/2018
- Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Jason -Zhong Sheng- Hu, 10/01/2018
  - Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Fritjof Bornebusch, 10/02/2018
    - Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Lily Chung, 10/02/2018
      - Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Fritjof Bornebusch, 10/02/2018