The Coq mailing list

[Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>]

On Sat, Feb 15, 2014 at 11:29:23PM +0200, Ömer Sinan A?acan wrote:
> 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)

For constructors yes, because constructors are injective. I don't know of any 
clever tactic for this, but if you prove injectivity as a lemma, then you can 
just "apply" the lemma.

    Lemma S_injective : forall n m, S n = S m -> n = m.
    Proof.
      intros n m H; injection H; auto.
    Qed.

    Hypothesis tl : list bool.
    Hypothesis n : nat.
    Goal length tl = n - 1.
      apply S_injective.
      (* goal is now
         S (length tl) = S (n - 1)  *)

Vilhelm Sjöberg