Stream: Coq users

Topic: Less than and conjunction in coq


view this post on Zulip Julin S (Sep 18 2021 at 16:56):

How can we say

((x > 3) and (y < 2))  ( - 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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