fold term in set tactic (#1194)

- tactic set x ≔ t: replace all subterms equal to t by x
- move eq_alpha from Eval to LibTerm

CHANGES.md

@@ -5,6 +5,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## Unreleased
 
+### Added
+
+- tactic set x ≔ t: replace all subterms equal to t by x
+
 ### Fixed
 
 - Notations on external symbols are now exported

src/core/eval.ml

@@ -113,27 +113,6 @@ end
 
 type config = Config.t
 
-(** [eq_alpha a b] tests the equality modulo alpha of [a] and [b]. *)
-let rec eq_alpha a b =
-  match unfold a, unfold b with
-  | Vari x, Vari y -> Bindlib.eq_vars x y
-  | Type, Type
-  | Kind, Kind -> true
-  | Symb s1, Symb s2 -> s1==s2
-  | Prod(a1,b1), Prod(a2,b2)
-  | Abst(a1,b1), Abst(a2,b2) ->
-      eq_alpha a1 a2 && let _,b1,b2 = Bindlib.unbind2 b1 b2 in eq_alpha b1 b2
-  | Appl(a1,b1), Appl(a2,b2) -> eq_alpha a1 a2 && eq_alpha b1 b2
-  | Meta(m1,a1), Meta(m2,a2) -> m1 == m2 && Array.for_all2 eq_alpha a1 a2
-  | LLet(a1,t1,u1), LLet(a2,t2,u2) ->
-      eq_alpha a1 a2 && eq_alpha t1 t2
-      && let _,u1,u2 = Bindlib.unbind2 u1 u2 in eq_alpha u1 u2
-  | Patt(Some i,_,ts), Patt(Some j,_,us) ->
-      i=j && Array.for_all2 eq_alpha ts us
-  | Patt(None,_,_), _ | _, Patt(None,_,_) -> assert false
-  | TEnv _, _| _, TEnv _ -> assert false
-  | _ -> false
-
 (** [eq_modulo whnf a b] tests the convertibility of [a] and [b] using
     [whnf]. *)
 let eq_modulo : (config -> term -> term) -> config -> term -> term -> bool =
@@ -143,7 +122,7 @@ let eq_modulo : (config -> term -> term) -> config -> term -> term -> bool =
     | [] -> ()
     | (a,b)::l ->
     if Logger.log_enabled () then log_conv "eq: %a ≡ %a" term a term b;
-    if eq_alpha a b then eq cfg l else
+    if LibTerm.eq_alpha a b then eq cfg l else
     let a = Config.unfold cfg a and b = Config.unfold cfg b in
     match a, b with
     | LLet(_,t,u), _ ->

src/core/libTerm.ml

@@ -170,3 +170,43 @@ let rec codom_binder : int -> term -> tbinder = fun n t ->
   | Prod(_,b) ->
       if n <= 0 then b else codom_binder (n-1) (Bindlib.subst b mk_Kind)
   | _ -> assert false
+
+(** [eq_alpha a b] tests the equality modulo alpha of [a] and [b]. *)
+let rec eq_alpha a b =
+  match unfold a, unfold b with
+  | Vari x, Vari y -> Bindlib.eq_vars x y
+  | Type, Type
+  | Kind, Kind -> true
+  | Symb s1, Symb s2 -> s1==s2
+  | Prod(a1,b1), Prod(a2,b2)
+  | Abst(a1,b1), Abst(a2,b2) ->
+      eq_alpha a1 a2 && let _,b1,b2 = Bindlib.unbind2 b1 b2 in eq_alpha b1 b2
+  | Appl(a1,b1), Appl(a2,b2) -> eq_alpha a1 a2 && eq_alpha b1 b2
+  | Meta(m1,a1), Meta(m2,a2) -> m1 == m2 && Array.for_all2 eq_alpha a1 a2
+  | LLet(a1,t1,u1), LLet(a2,t2,u2) ->
+      eq_alpha a1 a2 && eq_alpha t1 t2
+      && let _,u1,u2 = Bindlib.unbind2 u1 u2 in eq_alpha u1 u2
+  | Patt(Some i,_,ts), Patt(Some j,_,us) ->
+      i=j && Array.for_all2 eq_alpha ts us
+  | Patt(None,_,_), _ | _, Patt(None,_,_) -> assert false
+  | TEnv _, _| _, TEnv _ -> assert false
+  | _ -> false
+
+(** [fold id t a] returns term binder [b] with binder name [id] such that
+    [Bindlib.subst b t ≡ a]. *)
+let fold (x:tvar) (t:term): term -> term =
+  let rec aux u =
+    if eq_alpha t u then mk_Vari x
+    else
+      match unfold u with
+      | Appl(a,b) -> mk_Appl(aux a, aux b)
+      | Abst(a,b) ->
+          let x,b = Bindlib.unbind b in mk_Abst(aux a, bind x lift b)
+      | Prod(a,b) ->
+          let x,b = Bindlib.unbind b in mk_Prod(aux a, bind x lift b)
+      | LLet(a,d,b) ->
+          let x,b = Bindlib.unbind b in mk_LLet(aux a, aux d, bind x lift b)
+      | Meta(m,us) -> mk_Meta(m,Array.map aux us)
+      | _ -> u
+  in
+  aux

src/handle/tactic.ml

@@ -321,7 +321,7 @@ let rec handle :
         tac_refine pos ps gt gs p u
       end
   | P_tac_set(id,t) ->
-      (* From a goal [e ⊢ ?[e]:a], generate a new goal [e,id:b ⊢ ?1[e,x]:a],
+      (* From a goal [e ⊢ ?[e]:a], generate a new goal [e,x:b≔t ⊢ ?1[e,x]:a],
          where [b] is the type of [t], and refine [?[e]] with [?1[e,t]]. *)
       check id;
       let p = new_problem() in
@@ -334,14 +334,15 @@ let rec handle :
           let x = new_tvar id.elt in
           let bt = lift t in
           let e' = Env.add x (lift b) (Some bt) env in
-          let a = lift gt.goal_type in
-          let m = LibMeta.fresh p (Env.to_prod e' a) (List.length e') in
+          let n = List.length e' in
+          let v = LibTerm.fold x t gt.goal_type in
+          let m = LibMeta.fresh p (Env.to_prod e' (lift v)) n in
           let u = _Meta m (Array.append (Env.to_tbox env) [|bt|]) in
           (*tac_refine pos ps gt gs p (Bindlib.unbox u)*)
           LibMeta.set p gt.goal_meta
             (Bindlib.unbox (Bindlib.bind_mvar (Env.vars env) u));
           (*let g = Goal.of_meta m in*)
-          let g = Typ {goal_meta=m; goal_hyps=e'; goal_type=gt.goal_type} in
+          let g = Typ {goal_meta=m; goal_hyps=e'; goal_type=v} in
           {ps with proof_goals = g :: gs}
       end
   | P_tac_induction -> tac_induction pos ps gt gs