How can we say

```
((x > 3) and (y < 2)) → (x² - 2y > 5)
```

in coq?

where `→`

is implies.

This is what I tried:

```
Theorem basic : forall (x y : nat), ((x > 3) andb (y < 2)) -> (x*x - 2*y) > 5.
(*
Illegal application (Non-functional construction):
The expression "x > 3" of type "Prop"
cannot be applied to the term
"andb" : "bool -> bool -> bool"
*)
```

How can this be corrected?

`andb`

is boolean conjunction ("symbolic"). You need the "semantic" conjunction for `Prop`

, `and`

(infix notation `/\`

). They are different in Coq (but not in some other similar systems)

but most people would instead write `x > 3 -> y < 2 -> x*x - 2*y > 5`

in Coq, since that's easier to use.

I tried using the `x > 3 -> y < 2 -> x*x - 2*y > 5`

way and did

```
Lemma plus_n_0 : forall (n : nat), n + 0 = n.
Proof.
intros.
induction n.
- reflexivity.
- simpl.
rewrite IHn.
reflexivity.
Qed.
Theorem one : forall (x y : nat), (x > 3) -> (y < 2) -> (x*x - 2*y) > 5.
Proof.
intros.
simpl.
rewrite plus_n_0.
induction x.
- simpl.
```

but got into a strange context.

After the last `simpl`

, the goal becomes `0 > 5`

:

```
y : nat
H : 0 > 3
H0 : y < 2
========================= (1 / 1)
0 > 5
```

What did I do wrong here?

you need to use the "impossible" `H: 0 > 3`

hypothesis to discharge the first goal. But there's not really any point in doing this proof other than for understanding Coq itself, the tactic `lia`

solves the top goal from scratch.

Yeah, I'm just trying to understand coq. :)

What module should we import to get the `impossible`

tactic?

you can do `inversion H`

for example, no imports needed

Last updated: Jun 25 2024 at 19:01 UTC