Stream: Beginner Questions

Topic: ✔ Instanciation of schematic variables in ML

Jan van Brügge (Aug 18 2021 at 10:13):

I am trying to solve a rather simple proof goal with a ML tactic. My goal has the form:

⋀x f1 f2 g1 g2. (⋀z1. z1 ∈ set1_sum2 x ⟹ f1 z1 = g1 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 x ⟹ f2 z2 = g2 z2) ⟹ map_sum2 f1 f2 x = map_sum2 g1 g2 x

and I have a theorem of the form

(⋀z1. z1 ∈ set1_sum2 ?x ⟹ ?f1.0 z1 = ?g1.0 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 ?x ⟹ ?f2.0 z2 = ?g2.0 z2) ⟹ map_sum2 ?f1.0 ?f2.0 ?x = map_sum2 ?g1.0 ?g2.0 ?x

So I need to instanciate the schematic variables of the theorem with the forall bound variables of the goal. I can get the bound variables with Subgoal.SUBPROOF, but I have no idea what the ML equivalent of the lowercase of is

Dmitriy Traytel (Aug 18 2021 at 10:50):

In this case, just resolving (resolve_tac) with the theorem should instantiate the schematic variables correctly.

Dmitriy Traytel (Aug 18 2021 at 10:53):

After the resolution step, Goal.assume_rule_tac (which is different from assume_tac in that it follows ==> recursively) should be able to solve the remaining subgoals.

Dmitriy Traytel (Aug 18 2021 at 10:57):

To answer you actual question: infer_instantiate is an equivalent of where and infer_instantiate' of of.

Jan van Brügge (Aug 18 2021 at 11:02):

Indeed, this works:

apply (tactic ‹resolve_tac @{context} [BNF_Def.map_cong0_of_bnf a] 1
      THEN REPEAT (Goal.assume_rule_tac @{context} 1)›)

Notification Bot (Aug 18 2021 at 11:02):

Jan van Brügge has marked this topic as resolved.

Last updated: Apr 19 2024 at 04:17 UTC