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: Dec 07 2023 at 20:16 UTC