Ssreflect Users Discussion List

[Frederic Chyzak <>]

Hi,

I'm having troubles with “rewrite /f in v” below: it says something
about discharged assumptions.  Is this expected?  If so, where in the
manual should I read to understand?  (I could not spot any warning
against this use in section 6.5.)

In the end, I could find the workaround “move: @v; rewrite {1}/f => v”.

(Just to describe my use case: I want to introduce a term “f x y z” and
let it grow by expanding /f, etc, then name and reuse a subterm of the
expansion, this without retyping the subterm by hand.  For this I feel
safer to work in a temporary variable in the context, rather than on the
goal itself.)

Frédéric



$ 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 < Require Import Reals.
[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file r_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file ring_plugin.cmxs ... done]
[Loading ML file field_plugin.cmxs ... done]
[Loading ML file fourier_plugin.cmxs ... done]

Coq < Definition f (x y z : R) : R := (x + y + z)%R.
f is defined

Coq < Lemma foo (x y z : R) : False.
1 subgoal
  
  x : R
  y : R
  z : R
  ============================
   False

foo < set v := f x y z.
1 subgoal
  
  x : R
  y : R
  z : R
  v := f x y z : R
  ============================
   False

foo < rewrite /f in v.
Toplevel input, characters 0-15:
> rewrite /f in v.
> ^^^^^^^^^^^^^^^
Error: tampering with discharged assumptions of "in" tactical

foo < have h : x = y by admit.
1 subgoal
  
  x : R
  y : R
  z : R
  v := f x y z : R
  h : x = y
  ============================
   False

foo < rewrite h in v.
1 subgoal
  
  x : R
  y : R
  z : R
  h : x = y
  v := f y y z : R
  ============================
   False