fix(library/hop_match): in locally bound variable management

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/hop_match.cpp

@@ -40,11 +40,10 @@ class hop_match_fn {
 
     void assign(expr const & p, expr const & t, unsigned ctx_size) {
         lean_assert(is_free_var(p, ctx_size));
-        lean_assert(!has_locally_bound_var(t, ctx_size));
         lean_assert(!get_subst(p, ctx_size));
         unsigned vidx = var_idx(p) - ctx_size;
         unsigned sz = m_subst.size();
-        m_subst[sz - vidx - 1] = lower_free_vars(t, ctx_size, ctx_size);
+        m_subst[sz - vidx - 1] = t;
     }
 
     bool args_are_distinct_locally_bound_vars(expr const & p, unsigned ctx_size, buffer<expr> & vars) {
@@ -142,7 +141,7 @@ class hop_match_fn {
             } else if (has_locally_bound_var(t, ctx_size)) {
                 return false;
             } else {
-                assign(p, t, ctx_size);
+                assign(p, lower_free_vars(t, ctx_size, ctx_size), ctx_size);
                 return true;
             }
         } else if (is_app(p) && is_free_var(arg(p, 0), ctx_size)) {

src/library/hop_match.h

@@ -9,6 +9,22 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
+/**
+   \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.
+   The substitution is stored in \c subst.
+
+   \c subst is an assignment for the free variables occurring in \c p.
+
+   The free variables occurring in \c t are treated as constants.
+
+   We say non-free variables occurring in \c p and \c t are "locally bound".
+
+   \c p is a higher-order pattern when in all applications in \c p
+      1- A free variable is to the function OR
+      2- A free variable is the function, but all other arguments are distinct locally bound variables.
+
+   \pre \c subst must be big enough to store all free variables occurring in subst
+*/
 bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst);
 void open_hop_match(lua_State * L);
 }

src/library/kernel_bindings.cpp

@@ -603,6 +603,14 @@ static int expr_hash(lua_State * L) {
     return 1;
 }
 
+static int expr_head_beta_reduce(lua_State * L) {
+    return push_expr(L, head_beta_reduce(to_expr(L, 1)));
+}
+
+static int expr_beta_reduce(lua_State * L) {
+    return push_expr(L, beta_reduce(to_expr(L, 1)));
+}
+
 static const struct luaL_Reg expr_m[] = {
     {"__gc",             expr_gc}, // never throws
     {"__tostring",       safe_function<expr_tostring>},
@@ -632,6 +640,8 @@ static const struct luaL_Reg expr_m[] = {
     {"lift_free_vars",   safe_function<expr_lift_free_vars>},
     {"lower_free_vars",  safe_function<expr_lower_free_vars>},
     {"instantiate",      safe_function<expr_instantiate>},
+    {"beta_reduce",      safe_function<expr_beta_reduce>},
+    {"head_beta_reduce", safe_function<expr_head_beta_reduce>},
     {"abstract",         safe_function<expr_abstract>},
     {"occurs",           safe_function<expr_occurs>},
     {"has_metavar",      safe_function<expr_has_metavar>},

tests/lua/hop2.lua

@@ -0,0 +1,72 @@
+import("util.lua")
+
+function pibody(e)
+   while (e:is_pi()) do
+      local _, _, r = e:fields()
+      e = r
+   end
+   return e
+end
+
+function funbody(e)
+   while (e:is_lambda()) do
+      local _, _, r = e:fields()
+      e = r
+   end
+   return e
+end
+
+function hoptst(rule, target, expected)
+   if expected == nil then
+      expected = true
+   end
+   local th  = parse_lean(rule)
+   local p   = pibody(th):arg(2)
+   local t   = funbody(parse_lean(target))
+   local r   = hop_match(p, t)
+   if (r and not expected) or (not r and expected) then
+      error("test failed: " .. tostring(rule) .. " === " .. tostring(target))
+   end
+   if r then
+      local s = p:instantiate(r):beta_reduce()
+      print "Solution:"
+      for i = 1, #r do
+         print("#" .. tostring(i) .. " <--- " .. tostring(r[i]))
+      end
+      print ""
+      if s ~= t then
+         print("Mismatch")
+         print(s)
+         print(t)
+      end
+      assert(s == t)
+   end
+end
+
+parse_lean_cmds([[
+  variable f : Nat -> Nat -> Nat
+  variable g : Nat -> Nat
+  variable p : Nat -> Bool
+]])
+
+hoptst([[forall (A : TypeU) (P Q : A -> Bool), (forall x : A, P x /\ Q x) = ((forall x : A, P x) /\ (forall x : A, Q x))]],
+       [[forall x : Nat, p (f x 0) /\ f (f x x) 1 >= 0]])
+
+hoptst([[forall (F G : Nat -> Nat), (forall x y : Nat, F x = x /\ G y = y) = (F = G)]],
+       [[(forall x y : Nat, f x (g x) = x /\ g (g (g y)) = y)]])
+
+hoptst([[forall (F G : Nat -> Nat), (forall x y : Nat, F x = x /\ G y = y) = (F = G)]],
+       [[fun (a b c : Nat), (forall x y : Nat, f x (f (g b) c) = x /\ (f (g (g (f y c))) a) = y)]])
+
+hoptst([[forall (a b c : Bool), ((a /\ b) /\ c) = (a /\ (b /\ c))]],
+       [[fun (p1 p2 p3 p4 p5 : Bool), (((p1 ∧ p2) ∧ p3) ∧ (p4 ∧ p2))]])
+
+hoptst([[forall (F G : Nat -> Bool), (forall x : Nat, F x = (F x ∧ G x)) = (F = G)]],
+       [[forall x : Nat, p (f x x) = (p (f x x) ∧ p (f x 0))]])
+
+hoptst([[forall (F G : Nat -> Bool), (forall x : Nat, F x = (F x ∧ G x)) = (F = G)]],
+       [[forall x : Nat, p (f x x) = (p (f (g x) x) ∧ p (f x 0))]], false)
+
+hoptst([[forall (F G : Nat -> Nat), (forall x y : Nat, F x = x /\ G y = y) = (F = G)]],
+       [[fun (a b c : Nat), (forall x y : Nat, f x (f (g y) c) = x /\ (f (g (g (f y c))) a) = y)]], false)
+