Stream: Coq users

Topic: Simple proof


view this post on Zulip Julin S (Apr 24 2021 at 09:04):

I was trying to prove

Suppose x>3and y<2. Then x²−2y>5.

But couldn't figure how to get with it.

Can you give me some pointers on how to proceed?

I did

Theorem simple : forall x y : nat, x > 3 /\ y < 2 -> x*x - 2*y > 5.
Proof.
  intros x y H.
  destruct H as [H1 H2].
Qed.

view this post on Zulip Kenji Maillard (Apr 24 2021 at 09:23):

As a first preliminary step to any formalization, how would you prove it on paper ? What's the main ideas and proof steps that make this statement hold ?

view this post on Zulip Théo Winterhalter (Apr 24 2021 at 09:31):

Also—while in this case it seems fine—be wary of subtraction on natural numbers. Since they are natural numbers, they cannot go below zero so 2 - 3 is in fact 0.

view this post on Zulip Lessness (Apr 24 2021 at 11:44):

For 'unimportant' proof steps you can use lia tactic (after Require Import Lia.).
The hardest step in this proof is to prove that x*x > 9 or even x*x >= 16 (using assert and induction on H1: x > 3). After that you can use lia to finish proof.

[Edit] I'm dumb. One can prove the statement using lia already in the beginning.

view this post on Zulip Laurent Théry (Apr 24 2021 at 13:09):

If you want a proof without automation here it is

Require Import Arith.

Theorem simple :  forall x y : nat, 3 < x /\ y < 2 -> 5 < x*x - 2*y.
Proof.
  intros x y [Hx Hy].
  Search concl : (_ < _ - _).
  apply Nat.lt_add_lt_sub_l.
  Search concl : (_ < _ * _).
  Search nat "trans".
  apply Nat.le_lt_trans with (m := 3 * 3).
  Search concl : (_ + _ <= _).
  change (3 * 3) with (2 * 2 + 5).
  apply plus_le_compat_r.
  Search concl : (_ <= _ * _).
  apply Nat.mul_le_mono_l.
  Search concl : (_ <= _) (_ < _).
  apply Nat.lt_le_incl.
  trivial.
  Search concl : (_ < _ * _).
  apply -> Nat.square_lt_mono.
  trivial.
Qed.

Last updated: Jan 29 2023 at 01:02 UTC