coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic
Date: Tue, 16 Jan 2018 14:28:15 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f52.google.com
Ironport-phdr: 9a23:GusMQhCGWdMfIiZ4oZ/BUyQJP3N1i/DPJgcQr6AfoPdwSPv8oMbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2ybIUBEvQPMvpDoonhu1cDtweyCRWwCO7tzDJDm3/43bc90+QkCQzIxg0gEMwUsHTOstr+KbkfUeeozKnS0TXDbu1Z2Srg44XPahAhoO+DXahqccXP00UgCwTFjkiKqYz5PjOayPkNvnOU7+plT+2vimonpxttrTiow8chk4/EjZ8WxFDc7Sh13po5KNmiREN4YdOoCoVcuzyZOodsQs4uXWdlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF4hf5W+aQJTd0nXVleLOjixqr/0ityvPwWtO70FZNqSpFnd3MuW4X2xPP7ciHT+Nx/kan2TmRywDe8v9ILVwwmKbBKJMswqQ8moQOvUnABCP7mFv6gLeTdko+++io7+rnYq/hpp+ZL4J0kgD+Pbo0msylH+s0KBQBX2+G+eSmyL3j/FP2QKhRg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4Md/DahJC/buUAelv9vBSxQ9LgacwuD9Cdw72JlICkyVBarMCKLfq0WFrskoPvOQZYII8GLlKvU//fOohngkg0MccLSB0p4eaXT+FfNjdRbKKUHwi8sMRD9Z9jE1S/bn3RjbCWYKNiSCGpkk7zR+M7qISILKR4SjmruEhX7pEZhfZ2QAAVeJQy6xK9e0HswUYSfXGfdP1yQeXOH4GYAk3BCq8gT9zug/d7eGymgjrZvmkeNNyajTmBU1r2EmCs2c1ySKTjkxkD5SATAx2697rAp2zVLRiaU=

Please give self contained code, otherwise it is difficult to answer
your question.

2018-01-16 8:35 GMT+01:00 Guillaume Melquiond
<guillaume.melquiond AT inria.fr>:
>
> That is because you are generalizing too much information. Instead, try
>
> generalize (eq_refl (S steps)).
> generalize (S steps) at -2.
> intro n.

Or equivalently:

remember (S steps) as n.

Best
Pierre

[Coq-Club] [HELP] Recovering information after the `generalize` tactic, Ramkumar Ramachandra, 01/16/2018
- Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Guillaume Melquiond, 01/16/2018
  - Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Pierre Courtieu, 01/16/2018
    - Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Ramkumar Ramachandra, 01/17/2018
      - Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Pierre Courtieu, 01/17/2018
        
        Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Ramkumar Ramachandra, 01/18/2018
        
        Re: [Coq-Club] [HELP] Recovering information after the `generalize` tactic, Pierre Courtieu, 01/18/2018