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: Oct 13 2024 at 01:02 UTC