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

Last updated: Jul 15 2022 at 23:21 UTC