How can we say
((x > 3) and (y < 2)) → (x² - 2y > 5)
→ 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
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
you can do
inversion H for example, no imports needed
Last updated: Feb 01 2023 at 13:03 UTC