Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hello,
 If this is what you want to do, then you probably should follow Benjamin's 
advices and use Ltac's facilities. Right now ssreflect has a form of 
declarative dataflow: at any point in a proof, you can find the tactic that 
created or last modified any given assumption by looking up the beginning of 
the script. I believe this is important for proof robustness.
  An "in *" tactical would break this property, and this is the main reason 
it was left out of the ssr language mainly for that reason (another one being 
that it's ill-defined: what "in *" means depends on the tactic it applies 
to). I've found that as long as one doesn't relinquish control
of the generation of assumptions, it's never difficult to specify exactly 
what gets affected by a tactic, and that doing so really helps ot document 
what's going on in the proof.
   Clearly, you have a more exploratory view of the proof process, and you're 
happy with working with meta-proofs that run through a set of
heuristics and call on you to fill in te missing pieces later. Ltac was 
designed precisely with this approach to proofs in mind, so it should suit 
you well.

Regards,
  Georges



-----Original Message-----
From:  []
Sent: 20 June 2008 12:16
To: 
Subject: Re: abbreviation by the set tactic for the entire context

Dear Assia,

thank you for the reply.

I want to use this facility for painlessly debugging my tactics
by compacting the context; I am afraid I can not exploit your suggestion.

More details:
I am developing a tactic library which performs, in brief,
symbolic evaluation for a language with the axiomatic semantics.
The tactics work by pattern matching to decide what to evaluate,
assuming all abbreviations are unfolded.

The problem is that the tactics may fail, because there are bugs in the 
tactics
or there is not sufficient information in the context for
symbolic evaluation to succeed. In either case, the tactics leave
traces of what they have successfully evaluated, as facts in the context.
Let me note that since traces are produced by the tactics, abbreviations are
unfolded and there is no way to fold them beforehand.
The traces blow up the context and I usually get dazzled.

This is where I want to benefit from the facility I asked;
debugging is a substantial part of the development.

Best regards,
Keiko