New tactic: "proc change"

This tactic allows to change an expression in a statement by some
other expression. When applied, the user has to prove that the two
expressions are equal (generalizing over all the program variables)

This tactic applies to any program logic.

The syntax is:

    proc change <side?> <codepos> : <form>

This tactic is in the TCB.

Test plan:

 - unit test (tests/prochange.ec)

Author: strub

src/ecHiTacticals.ml

@@ -227,6 +227,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
+    | Pprocchange (s, p, f)     -> EcPhlRewrite.process_change s p f
   in
 
   try  tx tc

src/ecParser.mly

@@ -3233,6 +3233,9 @@ phltactic:
 | LOSSLESS
     { Plossless }
 
+| PROC CHANGE side=side? pos=codepos COLON f=sform
+    { Pprocchange (side, pos, f) }
+
 bdhoare_split:
 | b1=sform b2=sform b3=sform?
     { BDH_split_bop (b1,b2,b3) }

src/ecParsetree.ml

@@ -749,6 +749,7 @@ type phltactic =
   | Prw_equiv      of rw_eqv_info
   | Psymmetry
   | Pbdhoare_split of bdh_split
+  | Pprocchange    of side option * codepos * pformula
 
     (* Eager *)
   | Peager_seq       of (eager_info * codepos1 pair * pformula)

src/phl/ecPhlRewrite.ml

@@ -0,0 +1,43 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcAst
+open EcCoreGoal
+open EcModules
+open EcFol
+
+(* -------------------------------------------------------------------- *)
+let process_change
+    (side : side option)
+    (pos  : codepos)
+    (form : pformula)
+    (tc   : tcenv1)
+=
+  let concl = FApi.tc1_goal tc in
+
+  let change i =
+    let (e, mk) =
+      match i.i_node with
+      | Sasgn (lv, e) -> (e, (fun e -> i_asgn (lv, e)))
+      | Srnd  (lv, e) -> (e, (fun e -> i_rnd  (lv, e)))
+      | _             -> assert false in
+
+    let m, e' = EcProofTyping.tc1_process_Xhl_form ?side tc e.e_ty form in
+    let mid = EcMemory.memory m in
+    let e' = expr_of_form mid e' in
+
+    let f  = form_of_expr mid e in
+    let f' = form_of_expr mid e' in
+
+    ([f_forall_mems [m] (f_eq f f')], [mk e'])
+  in
+
+  let kinds = [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] in
+
+  if not (EcLowPhlGoal.is_program_logic concl kinds) then
+    assert false;
+
+  let s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let goals, s = EcMatching.Zipper.map pos change s in
+  let concl = EcLowPhlGoal.hl_set_stmt side concl s in
+
+  FApi.xmutate1 tc `ProcChange (goals @ [concl])

src/phl/ecPhlRewrite.mli

@@ -0,0 +1,6 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcCoreGoal.FApi
+
+(* -------------------------------------------------------------------- *)
+val process_change : side option -> codepos -> pformula -> backward

tests/procchange.ec

@@ -0,0 +1,14 @@
+require import AllCore.
+
+module M = {
+  proc f(x : int) = {
+    x <- x + 0;
+  }
+}.
+
+lemma L : equiv[M.f ~ M.f : true ==> true].
+proof.
+proc.
+proc change {1} 1 : x.
+- smt().
+abort.