Ssreflect Users Discussion List

[Georges Gonthier <>]

  I'm aware of the issue, but I'm not sure there's a good solution.
 I sort of like the idea that you have to specify either the function of the 
argument an application, if only by giving it a meaningful name:
  you write either
   move/(_ _ h) => {h} ...
or
   move=> add_f; move/add_f: h => {add_f} ...
I've been contemplating some minor improvements to the scheme, like
automatically clearing view assumptions (so the => {add_f} above would not be 
needed), although this would break backward compatibility, or using the 
flexible "view" application for the reverse view move/(_ t1 t2 ...), so you 
could write move/(_ h) above. They're not really high on my to-do list (e.g., 
porting to Coq v8.2 is more important).

Georges

-----Original Message-----
From:  []
Sent: 01 July 2008 13:31
To: 
Subject: wildcards insertion in the Specialising assumptions mechanism

Hello.

I am wondering if there is a way to let ssr insert wildcards
and instantiate the possible quantified variables, without explicitly giving
wildcards,
unlike the "Specialising assumptions" mechanism (Section 7.6).
It seems the behavior I am asking for is similar to, or almost opposite to,
the "Interpreting assumptions" mechanism (7.6).

Concretely I have been considering if I can improve the second line in the 
Goal
below.

Require Import ssreflect.

Variable a : nat.
Variable f: nat -> nat.
Variable p: nat -> Prop.

Goal (p a) -> (forall a, p a -> p (f a)) -> True.
move => h. (* Suppose h was introduced in the context long before *)
move => h1; move: h; move/h1; clear h1.

In particular, it would be nicer if I can avoid introducing the fresh name h1.
(But in some cases I prefer to introduce fresh names
rather than to manually insert wildcards.
I.e, I am aware that "move/(_ _ h)" does the same job. *)

With best regards,
Keiko