Ssreflect Users Discussion List

[Frederic Chyzak <>]

Le jeudi 24 avril 2014 à 10:22 +0000, Georges Gonthier a écrit :
>    We ought to fix this, but meanwhile there is a simple workaround: unfold 
> with occurrences does no let-expansion, so
>    rewrite {+}/f in  v
> should work for you (if you want to expand a single occurrence rewrite 
> {1}/f in v will work as well). You don't need to emulate manually the 'in' 
> tactical.

Thank you for the explanation, which made me re-open the manual to get
the meaning of {+<num>*}.

Now, reading on page 15 (Occurrence selection), I'm tempted to say there
is a bug: if “a list {+<num>*} [is the list] of occurrences affected by
the tactic”, I would expect {+} to mean that the list of occurrences
affected by the tactic is the empty list.  Therefore, “rewrite {+}/f”
should not rewrite anything.  The current behaviour also makes
occurrence selection not monotonous the way I would expect: compare
“rewrite {+ 1 2 3}/f”, “rewrite {+ 1 2}/f”, “rewrite {+ 1}/f”, and
“rewrite {+}/f” in the execution below.

By the same token, I would have expected “rewrite {-}/f” to have been
the trick in my situation: no occurrence is not to be affected; in other
words, all occurrences are affected.

Can you/one justify the present behaviour?

In any case, a sentence should be added into the documentation for the
exceptional/conventional cases of {+} and {-} with empty lists.

Frédéric





[chyzak@slowfox ~]$ rlwrap coqtop
Welcome to Coq 8.4pl3 (January 2014)

Coq < Require Import ssreflect.

Small Scale Reflection version 1.5 loaded.
Copyright 2005-2012 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.

[Loading ML file ssreflect.cmxs ... done]

Coq < Definition f (n : nat) : nat := n + n.
f is defined

Coq < Lemma foo (a b c : nat) : f a + f b + f c = 0.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0

foo < rewrite {+1 2 3}/f.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   a + a + (b + b) + (c + c) = 0

foo < Undo.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0

foo < rewrite {+1 3}/f.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   a + a + f b + (c + c) = 0

foo < Undo.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0

foo < rewrite {+3}/f.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + (c + c) = 0

foo < Undo.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0

foo < rewrite {+}/f.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   a + a + (b + b) + (c + c) = 0

foo < Undo.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0

foo < rewrite {-}/f.
1 subgoal
  
  a : nat
  b : nat
  c : nat
  ============================
   f a + f b + f c = 0