coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?

From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
To: coq club <coq-club AT inria.fr>
Subject: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?
Date: Sat, 15 Feb 2014 23:29:23 +0200

Hi all,

Let's say I have `length tl = n - 1` as goal and `H: n <> 0`. Can I
apply same constructor/function to both sides of the equation in goal?
Like applying S and having:

> S (length tl) = S (n - 1)

Is this possible? If not, why?

Thanks!

---
Ömer Sinan Ağacan
http://osa1.net

[Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Ömer Sinan Ağacan, 02/15/2014
- Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, AUGER Cédric, 02/15/2014
  - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Ömer Sinan Ağacan, 02/16/2014
    - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, AUGER Cédric, 02/16/2014
- Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Vilhelm SjÃ¶berg, 02/15/2014
  - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Abhishek Anand, 02/16/2014
    - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Robbert Krebbers, 02/16/2014
  - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Ömer Sinan Ağacan, 02/16/2014
- Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Mitchell Wand, 02/16/2014
  - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Ömer Sinan Ağacan, 02/16/2014
    - Re: [Coq-Club] Applying a constructor/function to both sides of an equation -- is this possible?, Jason Gross, 02/16/2014