coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Strange behaviour of induction with eqn: option

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: Rui Baptista <rpgcbaptista AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Strange behaviour of induction with eqn: option
Date: Thu, 24 Oct 2013 12:07:37 +0000
Accept-language: de-DE, en-US

Dear Rui,

but doesn’t this always lead to the situation that in the induction step cases, the pre-condition added to the induction hypothesis contradicts the case hypothesis (as below n=p contradicts n=S p)?

Best regards,

Michael

[Coq-Club] Strange behaviour of induction with eqn: option, michael.soegtrop, 10/24/2013
- Re: [Coq-Club] Strange behaviour of induction with eqn: option, Rui Baptista, 10/24/2013
  - RE: [Coq-Club] Strange behaviour of induction with eqn: option, Soegtrop, Michael, 10/24/2013
    - Re: [Coq-Club] Strange behaviour of induction with eqn: option, Cedric Auger, 10/24/2013
      - Re: [Coq-Club] Strange behaviour of induction with eqn: option, Rui Baptista, 10/25/2013
        
        RE: [Coq-Club] Strange behaviour of induction with eqn: option, Soegtrop, Michael, 10/28/2013
- RE: [Coq-Club] Strange behaviour of induction with eqn: option, Georges Gonthier, 10/24/2013