coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The tactic induction fails :-(

From: David Leduc <david.leduc6 AT googlemail.com>
To: Tom Prince <tom.prince AT ualberta.net>
Cc: Coq-Club <coq-club AT inria.fr>, Kenneth Roe <kendroe AT hotmail.com>, Adam Chlipala <adamc AT csail.mit.edu>
Subject: Re: [Coq-Club] The tactic induction fails :-(
Date: Mon, 7 Nov 2011 13:05:02 +0000

> eq is leibniz equality, which is, essentially syntactic equality.

In the context where x and y are of type nat, I allows me to prove
that x+y = y+x. This does not sound like syntactic equality to me.

[Coq-Club] The tactic induction fails :-(, David Leduc
- Re: [Coq-Club] The tactic induction fails :-(, Adam Chlipala
  - RE: [Coq-Club] The tactic induction fails :-(, Kenneth Roe
    - Re: [Coq-Club] The tactic induction fails :-(, Hugo Herbelin
      - Re: [Coq-Club] The tactic induction fails :-(, David Leduc
        
        Re: [Coq-Club] The tactic induction fails :-(, Tom Prince
        
        Re: [Coq-Club] The tactic induction fails :-(, David Leduc
        
        Re: [Coq-Club] The tactic induction fails :-(, Thorsten Altenkirch
- Message not available
  - Re: [Coq-Club] The tactic induction fails :-(, Bruno Barras