The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

I think that you want a notation instead of a definition.

 Require Import ZArith.
 Open Scope Z_scope.

 Definition Plus x y := x + y.

 Notation "x 'PLUS' y " := (x + y) (at level 50).

 Lemma PLUS_comm : forall x y, x PLUS y =  y PLUS x.
   intros;ring.
 Qed.

 Lemma Plus_comm : forall x y, Plus x y = Plus y x.
 (*intros;ring.
    Error: Tactic failure not a valid ring equation *)
  intros;unfold Plus;ring.
 Qed.

Best.

Sean Wilson wrote:
> Hi,
>
> I'm writing some automated tactics and want to check if there is a reduction 
> tactic that can simplify the current goal in a certain way. It's sometimes 
> useful to use definitions as shorthands for common expressions e.g.
>
> Definition permutation x y := forall n, count n x = count n y.
>
> In my domain, it is normally required that all 'simple' definitions like this 
> (i.e. non-recursive functions) be unfolded first for my automation to work. 
> As a simple example of what I need, given this definition:
>
> Definition f x y := plus x y.
>
> The following is true:
>
> Goal forall x y, f x y = f y x.
>
> My proof automation can prove this goal but only if "f" is unfolded first. 
> I've tried various combinations to have this done automatically (i.e. I don't 
> want to have to tell it what to unfold explicitly) but I cannot find a 
> suitable reduction tactic. The closest I've found is compute which gives 
> this:
>
> forall x y : nat,
> (fix plus (n m : nat) : nat := match n with
>                                | 0 => m
>                                | S p => S (p + m)
>                                end) x y =
> (fix plus (n m : nat) : nat := match n with
>                                | 0 => m
>                                | S p => S (p + m)
>                                end) y x
>
> I can then "fold plus" to get the simplification I want:
>
> forall x y : nat, x + y = y + x
>
> However, I'd like a tactic that does this automatically. Is there a tactic 
> that can do unfolding like this without me having explicitly name 
> definitions? Perhaps there is a way to automatically fold up goals 
> containing "fix plus" like terms? Even a function only available in OCaml 
> would be suitable.
>
> Thanks,
>
> Sean
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>