Ssreflect Users Discussion List

[<>]

> or using the flexible "view" application for the reverse view move/(_ t1 t2
...), 
> so you could write move/(_ h) above. 

This, i.e, move/(_ h), is exactly what I envisaged. 

Let me motivate the extension by explaining my situation.

I have a lot of axioms like the following: 

Axiom load_value: 
forall p e l ofs, entail p (lvalue e l ofs) ->
forall q n, entail p (con q (mapsto l ofs n)) ->
forall n2, cast n = n2 ->
entail p (expr e n2).

My script tries to instantiate the axiom by proving the assumptions one by one
and by accumulating the proved facts in the context. 

Then I have the following facts in the context, 
so I want to generalize the load_value axiom using them. 

hyp_l: entail p (lvalue e l ofs) ->
hyp_m: entail p (con q (mapsto l ofs n)) ->
hyp_c: cast n = n2 ->

My script was

generalize (load_value p e l ofs hyp_l q n hyp_m n2 hyp_c)

This is awful. I have been suffering from many bugs 
due to typos, misplaced arguments, etc. 
This kind of bugs are painful to debug. 

Now I can do: 

let h := fresh "h" in
move/load_value: hyp_l;
move => h; move/h: hyp_m => {h};
move => h; move/h: hyp_c => {h}

This will decrease the potential bugs.
Besides, I thought it would be more elegant 
if I need not generate the fresh name.

A sequence of wildcards can be dazzling; so I prefer the above script. 

> (e.g., porting to Coq v8.2 is more important).

Yes. I am waiting to use a latest feature of Coq, which became available in 
the svn version last May, and ssr at the same time. 
The feature enables me to call an external decision procedure from Coq 
script; 
I am experimenting both by having
two branches of the development compiled with different versions of Coq. 
This is painful. 

Kind regards,
Keiko