## Stream: Coq users

### Topic: Less than and conjunction in coq

#### Julin S (Sep 18 2021 at 16:56):

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?

#### Karl Palmskog (Sep 18 2021 at 16:57):

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

#### Karl Palmskog (Sep 18 2021 at 17:01):

but most people would instead write `x > 3 -> y < 2 -> x*x - 2*y > 5` in Coq, since that's easier to use.

#### Julin S (Sep 18 2021 at 17:35):

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?

#### Karl Palmskog (Sep 18 2021 at 17:42):

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.

#### Julin S (Sep 18 2021 at 18:20):

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

What module should we import to get the `impossible` tactic?

#### Karl Palmskog (Sep 18 2021 at 18:22):

you can do `inversion H` for example, no imports needed

Last updated: Feb 01 2023 at 13:03 UTC