Stream: math-comp users

Topic: n.+1 vs (n + 1)


view this post on Zulip Julin Shaji (Feb 21 2024 at 18:12):

I was trying to prove this goal:

From mathcomp Require Import all_ssreflect.
Require Import Arith.

Goal forall n m:nat,
  n.+1 < m.+1 -> n < m.
Proof.
  move => n m H.
  Check (ltn_add2r 1) n m.

(ltn_add2r 1) n m would give (n + 1 < m + 1) = (n < m) but I couldn't figure how to use it.

I guess it's because mathcomp uses addn and coq stdlib uses Nat.add?

How can we get around this?

I tried unfolding with rewrite /addn, but that changed nothing.

view this post on Zulip Julin Shaji (Feb 21 2024 at 18:17):


Oh, I just needed ltP:

Goal forall n m:nat,
  n.+1 < m.+1 -> n < m.
Proof.
  move => n m /ltP //=.
Qed.

view this post on Zulip Julin Shaji (Feb 21 2024 at 18:23):


But how could this be solved though?

Goal forall (n m: nat),
  (forall a b:nat, a < b) -> n.+1 < m.+1.
Proof.
  move => n m IH.
(*
1 subgoal

n, m : nat
IH : forall a b : nat, a < b

========================= (1 / 1)

n.+1 < m.+1
*)

view this post on Zulip Julin Shaji (Feb 21 2024 at 18:24):

I guess this is a way:

Goal forall (n m: nat),
  (forall a b:nat, a < b) -> n.+1 < m.+1.
Proof.
  move => n m H.
  have HH := H n m.
  move: HH.
  by move /ltP.
Qed.

view this post on Zulip Cyril Cohen (Feb 22 2024 at 08:04):

From mathcomp Require Import all_ssreflect.

Goal forall n m : nat, n.+1 < m.+1 -> n < m.
Proof. by []. Qed.

The reason is .+1 is a notation for constructor S and the definition of < (or in fact <=) reduces partially.

view this post on Zulip Cyril Cohen (Feb 22 2024 at 08:07):

From mathcomp Require Import all_ssreflect.

Goal forall (n m : nat), (forall a b : nat, a < b) -> n.+1 < m.+1.
Proof. by move=> n m ->. Qed.

because the conclusion of the third hypothesis is in fact (?a < ?b) = true and the left hand side matches the goal.

view this post on Zulip Ana de Almeida Borges (Feb 22 2024 at 14:19):

Julin Shaji said:

I was trying to prove this goal:

From mathcomp Require Import all_ssreflect.
Require Import Arith.

Goal forall n m:nat,
  n.+1 < m.+1 -> n < m.
Proof.
  move => n m H.
  Check (ltn_add2r 1) n m.

(ltn_add2r 1) n m would give (n + 1 < m + 1) = (n < m) but I couldn't figure how to use it.

I guess it's because mathcomp uses addn and coq stdlib uses Nat.add?

How can we get around this?

I tried unfolding with rewrite /addn, but that changed nothing.

Do you mean to be mixing mathcomp nat and stdlib nat? Typically once one has the former there is no need to import Arith.

view this post on Zulip Julin Shaji (Feb 22 2024 at 16:59):

I had a few lemmas which were made without mathcomp. I wanted to use them in a proof where mathcomp is also imported.


Last updated: Jul 15 2024 at 21:02 UTC