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

<pre><code>variables (A : Type) (p : A → Prop)

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

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), 
    reflexivity
  end,
  show false, by cases e
</code></pre>

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

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

CC BY-SA 3.0
2015-08-23T17:02:47.097Z
2015-08-23T17:18:05.023Z
2015-08-23T17:18:05.023Z
Konstantin Weitz
<p>I'm learning to use the <a href="https://leanprover.github.io/" rel="nofollow noreferrer">LEAN theorem prover</a> and I got stuck in a proof of a simple fact in first-order logic:
<span class="math-container">$$ p(x) \rightarrow \forall x p(x) $$</span>
My code is the following:</p>
<blockquote>
<p>variables (A : Type) (p q : A → Prop)</p>
<p>example (x : A) : p x → (∀ x, p x) :=</p>
<p>assume H : p x,</p>
<p>take x : A,</p>
<p>show p x, from H</p>
</blockquote>
<p>but it keeps saying that H has type p x_1, instead of what I expected, which is type p x.</p>

CC BY-SA 3.0
2015-08-24T00:11:23.060Z
This question is off-topic here. Please check [tour] and [help/on-topic].
Kaveh
<lo.logic><type-theory><coq>
What's wrong with this LEAN proof?
StudentType
# What's wrong with this LEAN proof?

(Asked by: username_0 on 2015-08-23)

I'm learning to use the [LEAN theorem prover](https://leanprover.github.io/) 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.

**Tags:** lo.logic, type-theory, coq

> **Comments:**
> **username_1**: This question is off-topic here. Please check [tour] and [help/on-topic].  

---

## 1 answers

### Answer by username_2 on 2015-08-23. Score: 6 | Accepted answer

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,
  sorry

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), 
    reflexivity
  end,
  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)


---

