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: Lily Chung <ikdc AT mit.edu>
To: coq-club AT inria.fr
Cc: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>, Fritjof Bornebusch <fritjof.bornebusch AT dfki.de>
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton
Date: Tue, 02 Oct 2018 10:01:53 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-8.mit.edu
Importance: Normal
Ironport-phdr: 9a23:kA3FrxJDsiW/50bL3dmcpTZWNBhigK39O0sv0rFitYgRKPzxwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJPUMhMVCJOAIOyYZUMAOQbPOlXoJXyqVQVoBu+HgahHv/jxiNUinL026AxzuQvERvB3AwlB98AtnXUrNH1NawPT+21zLTIzTPMb/hL3jr96YvIfQ09rvyXWLJwcNbRxVMxGAzYk1WdsIroNC6W2OQVq2WX8ultWfithmI9qgx8oSKjy8kuh4XRm44YyUrI+CtlzIovJdC1SFR3bcCqHZZTsSyRKpF4Tdk4Q25yvSY30r0GtoC/fCgN0Jko2hvfav2ef4iN+B3jVeKRISxmi315Yb6/nAq9/lKmyu36SMa0yk9GoylfntnJt3ANywbf5daaRftg5kuh2DCP2B7P6uxcPEw5lrDXJpw7zrMxlZcfq0rOEy3ulEXzlqCWd0Ek+uay6+TgZ7Xrvp6cN4xphQ7iKakun82/AfgiPgcQQmeb5Pyw1Kf/8k3hXLVKkvo2n7HFv5DdPMQXv7K2AwtI0ok48Bu/FDen0NEAnXYdNl5FeRSHj5LoO17UOvz4A+2/0ByQl2JgwOmDNbn8CL3MKGLCmfHvZ+VT8UlZnS4yycEXzJJJDL5JdPPwVkTZsd3ESBI1LlrnkK7cFNxh29ZGCiq0CaiDPfaX6AfQv7N9E6y3fIYQ/Q3FBb0g7v/qg2U+nA5PeKi1m5YbdSLhR6g0EwCieXPpx+w5PyISpANvHunrlBuPXSMBPy/vDZJ53SkyDcedNamGRo2ph+fYjiu+DNhTb2FCEV2HVGzjfoOCVu1JOGSXI9MnnzAZB+Cs

Probably you need to generalize over s in your inductive hypothesis.

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