Stream: New Members & Projects

Topic: Eisbach match method for schematic variables in proof goals

Matt (Nov 12 2024 at 15:20):

I've been working on a project with large, repetitive proofs that benefit from Eisbach automation. However, I ran into the same problem as @Hanno Becker where the match method included with Eisbach seems to replace schematic variables/terms in the proof goal with skolem variables/terms.

This behaviour can be replicated in the following example, where the first rule exI tactic produces the schematic variable ?x, then the subgoal tactic (?) replaces it with the skolem variable x which can not be instantiated within the subgoal (...).

lemma "∃x. P x"
  apply (rule exI)
  subgoal
    ...

For my use case, it would be impractical to instantiate the schematic variables/terms when they are introduced. Instead, the repeated application of introduction rules usually resolves them.

Thus, I developed a new match method which preserves schematic variables in proof goals.
This is achieved by adding a flag fix_schematics and guards to the focus_concl method in match_method.ML:

fun focus_concl fix_schematics ctxt i bindings goal =
  let
    val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
      Subgoal.focus_params ctxt i bindings goal;

    val ((_, inst), ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';

    val schematic_terms =
      Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];

    val instantiate_goal = (if fix_schematics then Thm.instantiate (TVars.empty, Vars.make schematic_terms) else I)
    val instantiate_concl = (if fix_schematics then Thm.instantiate_cterm (TVars.empty, Vars.make schematic_terms) else I)
    val instantiate_schematics = (if fix_schematics then fold Vars.add schematic_terms else I)

    val goal'' = instantiate_goal goal';
    val concl' = instantiate_concl concl;
    val (schematic_types, schematic_terms') = schematics;
    val schematics' = (schematic_types, instantiate_schematics schematic_terms');
  in
    ({context = ctxt'', concl = concl', params = params, prems = prems,
      schematics = schematics', asms = asms} : Subgoal.focus, goal'')
  end;

I wanted to share these changes, though I am unsure if an AFP entry, or a change to the Eisbach library is the best approach. Could someone advise?

Fabian Huch (Nov 13 2024 at 09:00):

This sounds like something to add to Eisbach, in which case you want to contact the local expert so they can have a look at the proposed changes.
I don't know who the current expert is for Eisbach, perhaps @Fabian Immler or @Maximilian Schäffeler ?

Maximilian Schäffeler (Nov 14 2024 at 18:29):

Unfortunately, not at all. I put together a single Eisbach method 6 years ago but don’t remember much.

Last updated: Dec 21 2024 at 16:20 UTC