I'm learning to use the LEAN theorem prover and I got stuck in a proof of a simple fact in first-order logic: $$ p(x) \rightarrow \forall x p(x) $$ My code is the following:

variables (A : Type) (p q : A → Prop)

example (x : A) : p x → (∀ x, p x) :=

assume H : p x,

take x : A,

show p x, from H

but it keeps saying that H has type p x_1, instead of what I expected, which is type p x.

  • $\begingroup$ This question is off-topic here. Please check tour and help center. $\endgroup$ – Kaveh Aug 24 '15 at 0:11

Your example is not true, that's why you cannot prove it. If we assume your example is true (which we do using the sorry tactic), then we can prove false. The proof goes as follows. We first pick x to be 0 and p to be the property that a number n is equal to 0. So p x is p 0 is 0 == 0 which is obviously true. Your example now provides us with the proof that p holds for all numbers. We pick 1, which is a contradiction because 0 <> 1.

variables (A : Type) (p : A → Prop)

lemma lma (x : A) : p x → (∀ x', p x') :=
  assume H : p x,
  take x' : A,

lemma inconsistent : false :=
  assert h : 0 == 0 → (∀ x, x == 0), from (lma num (λ n, n==0) 0),
  assert e : 1 == 0, begin
    refine (h _ 1), 
  show false, by cases e

The formula that you posted is also false in first order logic, even ∀ x, p x → (∀ x, p x) is not a true statement. Note that your example is different from the true statement (∀ x, p x) → (∀ x, p x).

The error message that you see stems from the fact that you are trying to use the hypothesis p x where the hypothesis p x' is expected (you are confusing the xes)


Not the answer you're looking for? Browse other questions tagged or ask your own question.