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.


closed as off-topic by Kaveh, Emil Jeřábek supports Monica, R B, Andrej Bauer, jbapple Aug 26 '15 at 21:32

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Kaveh, Emil Jeřábek supports Monica, R B, Andrej Bauer, jbapple
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\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.