lib: add named_eta and no_name_eta methods

These allow selective eta-contraction in the goal based on the bound
variable's name. The `no_name_eta` method speficially targets
abstractions where the variable has no name, which can come up in
complicated unification scenarios.

These nameless abstractions can cause symbolic execution lemmas to no
longer pick up on the name of the bound variable in do-notation,
requiring multiple rename_tac invocations.

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

lib/NICTATools.thy

@@ -21,6 +21,7 @@ imports
   ShowTypes
   Locale_Abbrev
   Value_Type
+  Named_Eta
 begin
 
 section "Detect unused meta-forall"

lib/Named_Eta.thy

@@ -0,0 +1,86 @@
+(*
+ * Copyright 2022, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Manipulation of eta-contractable terms taking into account their bound name. *)
+
+theory Named_Eta
+imports Main
+begin
+
+(* Eta-contraction applied only to lambda terms where the abstracted variable has a specific name.
+   Primary use-case is getting rid of such terms where the name is an empty string. Such situations
+   may arise during unification, especially involving schematics that depend on constants.
+
+   Ordinarily this would not be an issue, but it inhibits preservation of bound names during further
+   unification, which is especially relevant during symbolic execution.
+
+   For example, when we have some kind of \<open>P (do my_name <- f; g my_name)\<close> and apply a rule that
+   includes \<open>\<And>rv. P (g rv) \<Longrightarrow> P (g >>= (\<lambda>rv. g rv))\<close>, we want to get \<open>P (g my_name)\<close> and *not*
+   \<open>P (g rv)\<close>!
+
+   This ability of unification to preserve names will not work if the goal internally looks like:
+   \<open>P (\<lambda>a. (do my_name <- (\<lambda>a. f a); (\<lambda>a. (g my_name) a) a)\<close> (where "a" is the output for "")
+   because to unify with these extra bound variables, you'd first need to eta-contract, which will
+   take out the my_name binding as well. *)
+
+ML \<open>
+structure Named_Eta = struct
+
+(* copied from Pure/envir.ML *)
+fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
+  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
+  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
+  | decr _ _ = raise Same.SAME
+and decrh lev t = (decr lev t handle Same.SAME => t);
+
+(* copied from Pure/envir.ML and modified to only target a specific bound variable name (i.e. "") *)
+fun named_eta name (Abs (a, T, body)) =
+    if a = name then
+      (case named_eta name body of
+          body' as (f $ Bound 0) =>
+            if Term.is_dependent f then Abs (a, T, body')
+            else decrh 0 f
+       | body' => Abs (a, T, body')) handle Same.SAME =>
+          (case body of
+            f $ Bound 0 =>
+              if Term.is_dependent f then raise Same.SAME
+              else decrh 0 f
+          | _ => raise Same.SAME)
+     else Abs (a, T, named_eta name body)
+  | named_eta name (t $ u) =
+      (named_eta name t $ Same.commit (named_eta name) u handle Same.SAME => t $ named_eta name u)
+  | named_eta _ _ = raise Same.SAME;
+
+fun named_eta_contract name t = Same.commit (named_eta name) t
+
+(* To make a conversion out of this partial eta contraction function, we observe that a
+   partially eta-contracted term is eta-equivalent with the original term. This means: if
+   we fully eta contract the partially contracted term and fully eta contract the original
+   term, we must get the same normal form. That in turn means we have "partial == norm" and
+   "full == norm", so with transitivity and symmetry, we get "full == partial", which is
+   the theorem we want out of a conversion. *)
+fun named_eta_conv name ctxt ct =
+  let val eta_full_eq = Thm.eta_conversion ct
+      val eta_partial_ct = Thm.cterm_of ctxt (named_eta_contract name (Thm.term_of ct))
+      val eta_partial_eq = Thm.eta_conversion eta_partial_ct
+  in
+    Thm.transitive eta_full_eq (Thm.symmetric eta_partial_eq)
+  end
+
+end;
+
+(* Apply as a tactic *)
+fun named_eta_tac name ctxt = CONVERSION (Named_Eta.named_eta_conv name ctxt) 1
+val no_name_eta_tac = named_eta_tac ""
+\<close>
+
+method_setup no_name_eta = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (no_name_eta_tac ctxt))\<close>
+  "Perform eta-contraction only on bound variables that do not have a name."
+
+method_setup named_eta = \<open>Scan.lift Parse.name >> (fn v => fn ctxt => SIMPLE_METHOD (named_eta_tac v ctxt))\<close>
+  "Perform eta-contraction only on bound variables with a specific name."
+
+end

lib/ROOT

@@ -83,6 +83,7 @@ session Lib (lib) = Word_Lib +
     GenericTag
     ML_Goal_Test
     Value_Type
+    Named_Eta
 
     (* should really be a separate session, but too entangled atm: *)
     NonDetMonadLemmaBucket
@@ -161,6 +162,7 @@ session LibTest (lib) in test = Refine +
     Qualify_Test
     Locale_Abbrev_Test
     Value_Type_Test
+    Named_Eta_Test
   (* use virtual memory function as an example, only makes sense on ARM: *)
   theories [condition = "L4V_ARCH_IS_ARM"]
     Corres_Test

lib/test/Named_Eta_Test.thy

@@ -0,0 +1,60 @@
+(*
+ * Copyright 2022, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+theory Named_Eta_Test
+imports Lib.Named_Eta
+begin
+
+experiment
+begin
+
+declare [[eta_contract=false]] (* for display only, it does not affect terms *)
+
+(* tactical invocation example *)
+schematic_goal
+  "\<And>y. ?Q y False \<Longrightarrow> ?P y (\<lambda>x. f x)"
+  apply (tactic \<open>named_eta_tac "x" @{context}\<close>)
+  apply assumption
+  done
+
+(* method invocation example *)
+schematic_goal
+  "\<And>y. ?Q y False \<Longrightarrow> ?P y (\<lambda>x. f x)"
+  apply (named_eta x)
+  apply assumption
+  done
+
+lemma
+  "P x (\<lambda>z. g (\<lambda>x. f x) z)"
+  "\<And>P z. Q z \<Longrightarrow> P (\<lambda>x. f x)"
+  apply -
+  (* only affects one subgoal *)
+  prefer 2
+  apply (named_eta x)
+  prefer 2
+  (* only contract "z" *)
+  apply (named_eta z)
+  (* now only contract "x" *)
+  apply (named_eta x)
+  oops
+
+lemma (* nested lambdas *)
+  "\<lbrakk> X; P (\<lambda>x. (f (\<lambda>x. g y x))) \<rbrakk> \<Longrightarrow> P (\<lambda>x. (f (\<lambda>x. g y x)))"
+  apply (named_eta x)
+  apply assumption
+  done
+
+ML \<open>
+  (* nameless abstractions: *)
+  val t = Abs ("", @{typ bool}, @{term "f (\<lambda>x. g x) :: bool \<Rightarrow> bool"} $ Bound 0)
+  val ct = Thm.cterm_of @{context} t
+  (* contracts only the nameless "a" lambda: *)
+  val thm = Named_Eta.named_eta_conv "" @{context} ct
+\<close>
+
+end
+
+end