From 9659382bcb25d84d31fcb186db398f292dcffbdd Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Thu, 31 Jul 2025 17:23:17 -0500 Subject: [PATCH 1/3] Add var type consistency check to e(tac) This patch adds a small but useful check to `e(tac)`: detecting seemingly identical variables that in fact have different types. ``` # g `f (x:num) = f 1`;; Warning: inventing type variables Warning: Free variables in goal: f, x val it : goalstack = 1 subgoal (1 total) `(f:num->?142774) x = (f:num->?142774) 1` # e (SUBGOAL_THEN `x = true` ASSUME_TAC);; Exception: Failure "var x appearing with different types: bool vs. num". ``` --- tactics.ml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/tactics.ml b/tactics.ml index 3f3e8639..07613467 100644 --- a/tactics.ml +++ b/tactics.ml @@ -922,7 +922,26 @@ let flush_goalstack() = let l = !current_goalstack in current_goalstack := [hd l];; -let e tac = refine(by(VALID tac));; +(* CHECK_VARTYPES_TAC detects whether there is are variables having the same *) +(* name but different types. *) + +let CHECK_VARTYPES_TAC: tactic = + fun (asl,w) -> + let fvars_concl = freesl (w::(map (concl o snd) asl)) in + let fvars_dest = map dest_var fvars_concl in + let fvars_sorted = sort (fun (n1,_) (n2,_) -> n1 < n2) fvars_dest in + let rec checkfn l = + match l with + | [] -> () + | h::[] -> () + | (v1,ty1)::(v2,ty2)::t -> + if v1 = v2 && ty1 <> ty2 + then failwith ("var " ^ v1 ^ " appearing with different types: " ^ + (string_of_type ty1) ^ " vs. " ^ (string_of_type ty2)) + else checkfn ((v2,ty2)::t) + in checkfn fvars_sorted; ALL_TAC (asl,w);; + +let e tac = refine(by(VALID tac THEN CHECK_VARTYPES_TAC));; let r n = refine(rotate n);; From 60dfeb2362fbb12c1a03da1c22769b6cd19bedaf Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Fri, 1 Aug 2025 09:44:08 -0500 Subject: [PATCH 2/3] Add CHECK_VARTYPES_TAC.hlp and e.hlp, fix typo in help for EQT_INTRO (#135) --- Help/CHECK_VARTYPES_TAC.hlp | 22 ++++++++++++++++++++++ Help/EQT_INTRO.hlp | 2 +- Help/e.hlp | 5 +++-- tactics.ml | 2 +- 4 files changed, 27 insertions(+), 4 deletions(-) create mode 100644 Help/CHECK_VARTYPES_TAC.hlp diff --git a/Help/CHECK_VARTYPES_TAC.hlp b/Help/CHECK_VARTYPES_TAC.hlp new file mode 100644 index 00000000..555781a4 --- /dev/null +++ b/Help/CHECK_VARTYPES_TAC.hlp @@ -0,0 +1,22 @@ +\DOC CHECK_VARTYPES_TAC + +\TYPE {CHECK_VARTYPES_TAC : tactic} + +\SYNOPSIS +Checks whether there are free variables in the goal with the same name +but different types. + +\DESCRIBE +Given any goal {A ?- p}, the tactic {CHECK_VARTYPES_TAC} checks whether +there are any free variables in the conclusion and assumptions that have the +same name but different types. + +{e tac} runs {CHECK_VARTYPES_TAC} after {tac} by default and detects such cases. + +\FAILURE +Fails if such variables exist. + +\SEEALSO +e + +\ENDDOC diff --git a/Help/EQT_INTRO.hlp b/Help/EQT_INTRO.hlp index 9e7a594c..78349878 100644 --- a/Help/EQT_INTRO.hlp +++ b/Help/EQT_INTRO.hlp @@ -11,7 +11,7 @@ rule, truth. \DESCRIBE { A |- tm - --------------- EQF_INTRO + --------------- EQT_INTRO A |- tm <=> T } diff --git a/Help/e.hlp b/Help/e.hlp index 7974e316..0b23f0a3 100644 --- a/Help/e.hlp +++ b/Help/e.hlp @@ -23,7 +23,8 @@ For a description of the subgoal package, see {set_goal}. the tactic diverges for the goal. It will fail if there are no unproven goals. This could be because no goal has been set using {set_goal} or because the last goal set has been completely proved. It will also fail in cases when the tactic -is invalid. +is invalid. It will also fail if any of the resulting subgoals include free +variables with the same name but different types ({CHECK_VARTYPES_TAC}). \EXAMPLE { @@ -52,6 +53,6 @@ is invalid. Doing a step in an interactive goal-directed proof. \SEEALSO -b, er, g, p, r, set_goal, top_goal, top_thm. +b, er, g, p, r, set_goal, top_goal, top_thm, CHECK_VARTYPES_TAC. \ENDDOC diff --git a/tactics.ml b/tactics.ml index 07613467..790ad217 100644 --- a/tactics.ml +++ b/tactics.ml @@ -922,7 +922,7 @@ let flush_goalstack() = let l = !current_goalstack in current_goalstack := [hd l];; -(* CHECK_VARTYPES_TAC detects whether there is are variables having the same *) +(* CHECK_VARTYPES_TAC detects whether there are variables having the same *) (* name but different types. *) let CHECK_VARTYPES_TAC: tactic = From a14f13a1a9676b9ee7401700e89f17d973b0e06a Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Sat, 15 Nov 2025 23:24:04 +0000 Subject: [PATCH 3/3] Add unit test --- unit_tests.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/unit_tests.ml b/unit_tests.ml index 1ea9a18a..0e5e2f58 100644 --- a/unit_tests.ml +++ b/unit_tests.ml @@ -168,6 +168,17 @@ e(CONJ_TAC);; top_thm();; +(* ------------------------------------------------------------------------- *) +(* Test that e() finds same variable names with different types() *) +(* ------------------------------------------------------------------------- *) + +g `(f:num->A) (x:num) = f 1`;; +try + e (SUBGOAL_THEN `x = true` ASSUME_TAC); + assert false; +with Failure _ -> () | Assert_failure _ as e -> raise e;; + + (* ------------------------------------------------------------------------- *) (* Test functions in lib. *) (* ------------------------------------------------------------------------- *)