Skip to content

drule.ml: fail term_match early when a substitution would let a bound variable escape #191

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
aqjune-aws wants to merge 2 commits into
base: master
Choose a base branch
from
Open

drule.ml: fail term_match early when a substitution would let a bound variable escape #191

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
10d32dd
drule.ml: fail matching early when a substitution would let a bound v…
aqjune-aws Jun 13, 2026
5a58814
Merge branch 'master' into term_pmatch-earlyfail
aqjune-aws Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions Help/term_match.hlp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,12 @@ This function can occasionally `succeed' yet produce a match that does not in
fact work. In typical uses, this will be implicitly checked by a subsequent
inference process. However, to get a self-contained matching effect, the user
should check that the instantiation returned does achieve a match, e.g. by
applying {instantiate}.
applying {instantiate}. The variant {term_match_checked}, which is the one used
by {PART_MATCH}, rules out one common family of such spurious matches, those
assigning to a pattern variable a subterm in which a variable bound on the
other side occurs free, at the cost of a little more work per match.

\SEEALSO
instantiate, INSTANTIATE, PART_MATCH.
instantiate, INSTANTIATE, PART_MATCH, term_match_checked.

\ENDDOC
56 changes: 56 additions & 0 deletions Help/term_match_checked.hlp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
\DOC term_match_checked

\TYPE {term_match_checked : term list -> term -> term -> instantiation}

\SYNOPSIS
Match one term against another, failing early on out-of-scope assignments.

\DESCRIBE
The call {term_match_checked lcs t t'} behaves like {term_match lcs t t'},
attempting to find an instantiation for the free variables of {t}, not
permitting assignment of `local constant' variables in the list {lcs}, so that
{t} becomes alpha-equivalent to {t'}. It differs in that it fails at once if
matching would assign to a free variable of {t} a subterm of {t'} in which some
variable bound in {t'} over that subterm occurs free. Such an assignment can
never yield a term alpha-equivalent to {t'}, since instantiation renames the
pattern's own binder instead of capturing the variable; {term_match} accepts it
anyway and leaves the mismatch to be detected downstream. This is the matcher
used by {PART_MATCH} and {GEN_PART_MATCH}, where detecting the mismatch during
matching is much cheaper than instantiating the theorem and finding it
afterwards.

\FAILURE
Fails if the terms cannot be matched, and in particular on the out-of-scope
matches described above, where {term_match} succeeds.

\EXAMPLE
Matching the pattern of {EXISTS_SIMP} against an existential whose body does
use the bound variable cannot work, but only the checked matcher says so:
{
# term_match [] `?x:A. t` `?y:num. y = 1`;;
val it : instantiation = ([], [(`y = 1`, `t`)], [(`:num`, `:A`)])

# term_match_checked [] `?x:A. t` `?y:num. y = 1`;;
Exception: Failure "term_pmatch: bound variable would escape".
}
\noindent while genuine matches, including higher order ones, are unaffected:
{
# term_match_checked [] `?x:A. t` `?y:num. 1 = 1`;;
val it : instantiation = ([], [(`1 = 1`, `t`)], [(`:num`, `:A`)])

# term_match_checked [] `~(?x:A. P x)` `~(?n. 5 < n /\ n < 6)`;;
val it : instantiation =
([(1, `P`)], [(`\n. 5 < n /\ n < 6`, `P`)], [(`:num`, `:A`)])
}

\COMMENTS
The check covers the first order case only; the higher order paths of the
matcher can still return an instantiation in which a bound variable of {t'}
escapes. So, just as with {term_match}, a user wanting a self-contained
matching effect should check that the instantiation returned does achieve a
match, e.g. by applying {instantiate}.

\SEEALSO
instantiate, INSTANTIATE, PART_MATCH, term_match.

\ENDDOC
47 changes: 47 additions & 0 deletions UnitTests/basic_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -224,6 +224,53 @@ let test_fn = function

set_jrh_lexer;;

(* ------------------------------------------------------------------------- *)
(* term_match (permissive) vs term_match_checked. *)
(* *)
(* Matching `?x. t` against `?y. P y` would bind t := `P y`, letting the *)
(* target's bound variable y escape into a free position. term_match still *)
(* accepts this, as its documentation says it may; term_match_checked *)
(* rejects it at once, before any costly INSTANTIATE. *)
(* ------------------------------------------------------------------------- *)

(* Permissive matcher: succeeds, as it always has. *)
let _ =
let pat = `(?x:A. t):bool` in
let tm = `?y:num. (P:num->bool) y` in
let _ = term_match [] pat tm in ();;

(* Checked matcher: rejects the escaping substitution. *)
let _ =
let pat = `(?x:A. t):bool` in
let tm = `?y:num. (P:num->bool) y` in
try
let _ = term_match_checked [] pat tm in
failwith "term_match_checked should have rejected escaping bound variable"
with Failure msg
when msg <> "term_match_checked should have rejected escaping bound variable" -> ();;

(* Both matchers must agree on a non-escaping (first-order) match. *)
let _ =
let pat = `(f:num->num->num) (a:num) (b:num)` in
let tm = `(f:num->num->num) 3 5` in
let _,m1,_ = term_match [] pat tm in
let _,m2,_ = term_match_checked [] pat tm in
assert (m1 = m2);;

(* PART_MATCH / REWR_CONV route through term_match_checked, so the same *)
(* shape must still fail early (the performance win is preserved). *)
let _ =
try
let _ = REWR_CONV EXISTS_SIMP `?y:num. (P:num->bool) y` in
failwith "REWR_CONV EXISTS_SIMP should reject `?y. P y`"
with Failure msg when msg <> "REWR_CONV EXISTS_SIMP should reject `?y. P y`" -> ();;

(* Sanity: when the body genuinely doesn't mention the bound var, the same *)
(* rewrite must still succeed. *)
let _ =
let th = REWR_CONV EXISTS_SIMP `?y:num. T` in
assert (concl th = `(?y:num. T) <=> T`);;

(* ------------------------------------------------------------------------- *)
(* Test check_axioms. *)
(* ------------------------------------------------------------------------- *)
Expand Down
226 changes: 120 additions & 106 deletions drule.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,9 +160,16 @@ let (INSTANTIATE_ALL : instantiation->thm->thm) =
(* but there's usually an implicit check outside that the match worked *)
(* anyway. A test could be put in (see if any "env" variables are left in *)
(* the term after abstracting out the pattern instances) but it'd be slower. *)
(* *)
(* The "term_match_checked" variant does perform that test for the first *)
(* order case, i.e. whenever a pattern variable would be assigned a subterm *)
(* with a free occurrence of a variable bound on the target side, so that *)
(* such matches fail at once rather than being rejected downstream. The *)
(* higher order paths below are unchanged, so it is still only a partial *)
(* check and the implicit check outside remains the real guarantee. *)
(* ------------------------------------------------------------------------- *)

let (term_match:term list -> term -> term -> instantiation) =
let term_match,term_match_checked =
let safe_inserta ((y,x) as n) l =
try let z = rev_assoc x l in
if aconv y z then l else failwith "safe_inserta"
Expand All @@ -177,109 +184,116 @@ let (term_match:term list -> term -> term -> instantiation) =
let name = fst(dest_var(genvar aty)) in
fun ty -> mk_var(name,ty) in

let rec term_pmatch lconsts env vtm ctm ((insts,homs) as sofar) =
match (vtm,ctm) with
Var(_,_),_ ->
(try let ctm' = rev_assoc vtm env in
if compare ctm' ctm = 0 then sofar
else failwith "term_pmatch"
with Failure "find" ->
if mem vtm lconsts then
if compare ctm vtm = 0 then sofar
else failwith "term_pmatch: can't instantiate local constant"
else safe_inserta (ctm,vtm) insts,homs)
| Const(vname,vty),Const(cname,cty) ->
if compare vname cname = 0 then
if compare vty cty = 0 then sofar
else safe_insert (mk_dummy cty,mk_dummy vty) insts,homs
else failwith "term_pmatch"
| Abs(vv,vbod),Abs(cv,cbod) ->
let sofar' = safe_insert
(mk_dummy(snd(dest_var cv)),mk_dummy(snd(dest_var vv))) insts,homs in
term_pmatch lconsts ((cv,vv)::env) vbod cbod sofar'
| _ ->
let vhop = repeat rator vtm in
if is_var vhop && not (mem vhop lconsts) &&
not (can (rev_assoc vhop) env) then
let vty = type_of vtm and cty = type_of ctm in
let insts' =
if compare vty cty = 0 then insts
else safe_insert (mk_dummy cty,mk_dummy vty) insts in
(insts',(env,ctm,vtm)::homs)
else
let lv,rv = dest_comb vtm
and lc,rc = dest_comb ctm in
let sofar' = term_pmatch lconsts env lv lc sofar in
term_pmatch lconsts env rv rc sofar' in

let get_type_insts insts =
itlist (fun (t,x) -> type_match (snd(dest_var x)) (type_of t)) insts in

let separate_insts insts =
let realinsts,patterns = partition (is_var o snd) insts in
let betacounts =
if patterns = [] then [] else
itlist
(fun (_,p) sof ->
let hop,args = strip_comb p in
try safe_insert (length args,hop) sof with Failure _ ->
(warn true "Inconsistent patterning in higher order match"; sof))
patterns [] in
let tyins = get_type_insts realinsts [] in
betacounts,
mapfilter (fun (t,x) ->
let x' = let xn,xty = dest_var x in
mk_var(xn,type_subst tyins xty) in
if compare t x' = 0 then fail() else (t,x')) realinsts,
tyins in

let rec term_homatch lconsts tyins (insts,homs) =
if homs = [] then insts else
let (env,ctm,vtm) = hd homs in
if is_var vtm then
if compare ctm vtm = 0
then term_homatch lconsts tyins (insts,tl homs) else
let newtyins = safe_insert (type_of ctm,snd(dest_var vtm)) tyins
and newinsts = (ctm,vtm)::insts in
term_homatch lconsts newtyins (newinsts,tl homs) else
let vhop,vargs = strip_comb vtm in
let afvs = freesl vargs in
let inst_fn = inst tyins in
try let tmins = map
(fun a -> (try rev_assoc a env with Failure _ -> try
rev_assoc a insts with Failure _ ->
if mem a lconsts then a else fail()),
inst_fn a) afvs in
let pats0 = map inst_fn vargs in
let pats = map (vsubst tmins) pats0 in
let vhop' = inst_fn vhop in
let ni =
let chop,cargs = strip_comb ctm in
if compare cargs pats = 0 then
if compare chop vhop = 0
then insts else safe_inserta (chop,vhop) insts else
let ginsts = map
(fun p -> (if is_var p then p else genvar(type_of p)),p) pats in
let ctm' = subst ginsts ctm
and gvs = map fst ginsts in
let abstm = list_mk_abs(gvs,ctm') in
let vinsts = safe_inserta (abstm,vhop) insts in
let icpair = ctm',list_mk_comb(vhop',gvs) in
icpair::vinsts in
term_homatch lconsts tyins (ni,tl homs)
with Failure _ ->
let lc,rc = dest_comb ctm
and lv,rv = dest_comb vtm in
let pinsts_homs' =
term_pmatch lconsts env rv rc (insts,(env,lc,lv)::(tl homs)) in
let tyins' = get_type_insts (fst pinsts_homs') [] in
term_homatch lconsts tyins' pinsts_homs' in

fun lconsts vtm ctm ->
let pinsts_homs = term_pmatch lconsts [] vtm ctm ([],[]) in
let tyins = get_type_insts (fst pinsts_homs) [] in
let insts = term_homatch lconsts tyins pinsts_homs in
separate_insts insts;;
let gen_term_match check_escape =
let rec term_pmatch lconsts env vtm ctm ((insts,homs) as sofar) =
match (vtm,ctm) with
Var(_,_),_ ->
(try let ctm' = rev_assoc vtm env in
if compare ctm' ctm = 0 then sofar
else failwith "term_pmatch"
with Failure "find" ->
if mem vtm lconsts then
if compare ctm vtm = 0 then sofar
else failwith "term_pmatch: can't instantiate local constant"
else if check_escape &&
exists (fun (cv,_) -> vfree_in cv ctm) env then
failwith "term_pmatch: bound variable would escape"
else safe_inserta (ctm,vtm) insts,homs)
| Const(vname,vty),Const(cname,cty) ->
if compare vname cname = 0 then
if compare vty cty = 0 then sofar
else safe_insert (mk_dummy cty,mk_dummy vty) insts,homs
else failwith "term_pmatch"
| Abs(vv,vbod),Abs(cv,cbod) ->
let sofar' = safe_insert
(mk_dummy(snd(dest_var cv)),mk_dummy(snd(dest_var vv))) insts,homs in
term_pmatch lconsts ((cv,vv)::env) vbod cbod sofar'
| _ ->
let vhop = repeat rator vtm in
if is_var vhop && not (mem vhop lconsts) &&
not (can (rev_assoc vhop) env) then
let vty = type_of vtm and cty = type_of ctm in
let insts' =
if compare vty cty = 0 then insts
else safe_insert (mk_dummy cty,mk_dummy vty) insts in
(insts',(env,ctm,vtm)::homs)
else
let lv,rv = dest_comb vtm
and lc,rc = dest_comb ctm in
let sofar' = term_pmatch lconsts env lv lc sofar in
term_pmatch lconsts env rv rc sofar' in

let get_type_insts insts =
itlist (fun (t,x) -> type_match (snd(dest_var x)) (type_of t)) insts in

let separate_insts insts =
let realinsts,patterns = partition (is_var o snd) insts in
let betacounts =
if patterns = [] then [] else
itlist
(fun (_,p) sof ->
let hop,args = strip_comb p in
try safe_insert (length args,hop) sof with Failure _ ->
(warn true "Inconsistent patterning in higher order match"; sof))
patterns [] in
let tyins = get_type_insts realinsts [] in
betacounts,
mapfilter (fun (t,x) ->
let x' = let xn,xty = dest_var x in
mk_var(xn,type_subst tyins xty) in
if compare t x' = 0 then fail() else (t,x')) realinsts,
tyins in

let rec term_homatch lconsts tyins (insts,homs) =
if homs = [] then insts else
let (env,ctm,vtm) = hd homs in
if is_var vtm then
if compare ctm vtm = 0
then term_homatch lconsts tyins (insts,tl homs) else
let newtyins = safe_insert (type_of ctm,snd(dest_var vtm)) tyins
and newinsts = (ctm,vtm)::insts in
term_homatch lconsts newtyins (newinsts,tl homs) else
let vhop,vargs = strip_comb vtm in
let afvs = freesl vargs in
let inst_fn = inst tyins in
try let tmins = map
(fun a -> (try rev_assoc a env with Failure _ -> try
rev_assoc a insts with Failure _ ->
if mem a lconsts then a else fail()),
inst_fn a) afvs in
let pats0 = map inst_fn vargs in
let pats = map (vsubst tmins) pats0 in
let vhop' = inst_fn vhop in
let ni =
let chop,cargs = strip_comb ctm in
if compare cargs pats = 0 then
if compare chop vhop = 0
then insts else safe_inserta (chop,vhop) insts else
let ginsts = map
(fun p -> (if is_var p then p else genvar(type_of p)),p) pats in
let ctm' = subst ginsts ctm
and gvs = map fst ginsts in
let abstm = list_mk_abs(gvs,ctm') in
let vinsts = safe_inserta (abstm,vhop) insts in
let icpair = ctm',list_mk_comb(vhop',gvs) in
icpair::vinsts in
term_homatch lconsts tyins (ni,tl homs)
with Failure _ ->
let lc,rc = dest_comb ctm
and lv,rv = dest_comb vtm in
let pinsts_homs' =
term_pmatch lconsts env rv rc (insts,(env,lc,lv)::(tl homs)) in
let tyins' = get_type_insts (fst pinsts_homs') [] in
term_homatch lconsts tyins' pinsts_homs' in

fun lconsts vtm ctm ->
let pinsts_homs = term_pmatch lconsts [] vtm ctm ([],[]) in
let tyins = get_type_insts (fst pinsts_homs) [] in
let insts = term_homatch lconsts tyins pinsts_homs in
separate_insts insts in

(gen_term_match false:term list -> term -> term -> instantiation),
(gen_term_match true:term list -> term -> term -> instantiation);;

(* ------------------------------------------------------------------------- *)
(* First order unification of terms of the same type. *)
Expand Down Expand Up @@ -459,7 +473,7 @@ let PART_MATCH,GEN_PART_MATCH =
let bvms = match_bvs tm pbod [] in
let abod = deep_alpha bvms bod in
let ath = EQ_MP (ALPHA bod abod) sth in
let insts = term_match lconsts (partfn abod) tm in
let insts = term_match_checked lconsts (partfn abod) tm in
let fth = INSTANTIATE insts ath in
if hyp fth <> hyp ath then failwith "PART_MATCH: instantiated hyps" else
let tm' = partfn (concl fth) in
Expand All @@ -476,7 +490,7 @@ let PART_MATCH,GEN_PART_MATCH =
let bvms = match_bvs tm pbod [] in
let abod = deep_alpha bvms bod in
let ath = EQ_MP (ALPHA bod abod) sth in
let insts = term_match lconsts (partfn abod) tm in
let insts = term_match_checked lconsts (partfn abod) tm in
let eth = INSTANTIATE insts (GENL fvs ath) in
let fth = itlist (fun v th -> snd(SPEC_VAR th)) fvs eth in
if hyp fth <> hyp ath then failwith "PART_MATCH: instantiated hyps" else
Expand Down