changing goal to exists

Stream: new members

[Arthur Paulino]

Suppose I have this:

example {n : ℕ} : n = n :=
begin
-- n : ℕ
-- ⊢ n = n
  sorry,
end

Is it possible (and does it make sense) to legally change the goal to state to

⊢ ∃ n : ℕ, n = n

(clearing out n from the context)

[Eric Wieser]

I don't think this question is well posed, any true goal can legally be changed to any other true goal

[Kevin Buzzard]

Right -- the issue is that you can solve the true goal with any number, not just n. If you were to ask instead whether you could reduce ⊢ P n to ⊢ ∃ a : ℕ, P a then the answer is no, because P might be false for n but true for 37. Of course the logic is fine the other way around; you can reduce ⊢ ∃ a : ℕ, P a to ⊢ P n, but in general it's not an iff. In your case it is an iff because both predicates are true.

[Arthur Paulino]

I see, thanks!

[Kyle Miller]

Another answer to this is that the correct quantifier would be for-all rather than there-exists. The tactic to do this transformation is tactic#revert.

example {n : ℕ} : n = n :=
begin
  revert n,
  -- ⊢ ∀ {n : ℕ}, n = n
  sorry,
end