Stream: Beginner Questions

Topic: Why is this goal provable by assumption?

o7 (Dec 18 2024 at 17:16):

I have the following subgoal

goal (1 subgoal):
 1. ⋀x y. P x (?y6 x y) ⟹ P (?x8 x y) y

Apparently this can be proven by assumption. Why is this? The left side of the implication doesn't look anything like right right hand side.

This goal comes from the following lemma with proof

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
  apply (rule impI)
  apply (erule exE, rule allI)
apply (erule allE)
  apply (rule exI)
  apply assumption
  done

Mathias Fleury (Dec 18 2024 at 17:58):

?y6 x y are variable that you can pick

Mathias Fleury (Dec 18 2024 at 17:58):

they are left-overs from the unification algorithm

Jan van Brügge (Dec 18 2024 at 18:01):

So you can pick ?y6 := y and ?x8 := x and the assumption and goal become the same

Mathias Fleury (Dec 18 2024 at 18:07):

If you want to play with such goals, you can use schematic_goal:

schematic_goal ‹P 0 ⟹ P ?a ∧ Q ?a›
  apply (rule conjI)
   apply assumption
(*
goal instantiation:
    ?a ↝ 0
*)
  sorry

Last updated: Dec 21 2024 at 16:20 UTC