<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 `x`es)


---

