Stream: math-comp users

Topic: Awful proof on rationals


view this post on Zulip Julien Puydt (May 25 2022 at 12:03):

I did manage to get through to my goal, but the proof is... awful, so I'm looking for help to improve it:

From mathcomp Require Import all_ssreflect all_algebra ssrnum.
From mathcomp.algebra_tactics Require Import ring.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope rat_scope.

Section Trivial.

Variable a: rat.

Lemma noname: ((a == -1%Q) || (a == 1/2%:Q)) && (lt_rat 0 a) -> (a == 1/2%:Q).
Proof.
have aminus: a == -1%Q -> ~(numq a > 0)%R.
  move/eqP=> H.
  rewrite H.
  by [].
move=> /andP [/orP H0 H1].
rewrite gt_rat0 in H1.
have H2:= (contraPnot _ _ aminus H1).
move: H0.
elim.
  move=> H3.
  by have _ := (H2 H3).
by [].
Qed.

End Trivial.

view this post on Zulip Pierre Roux (May 25 2022 at 12:15):

I didn't look at the proof but regarding the statement, I'd rather write something like (not tested):

Local Open Scope ring_scope.
(* no need to open rat_scope, and don't use `Open Scope` without `Local` if you don't have a very good reason to do so *)

Lemma noname : (a == -1) || (a == 1 / 2%:R) -> 0 < a -> a == 1 / 2%:R.

Note that this should be solved by lra which should be available for MC in algebra-tactics in the near future.
Also 1 / 2%:R could be written 1 / 2 or 0.5 in future MC (opening rat_scope after ring_scope for the last one).

For the proof, maybe something like (untested):

move=> -[] /eqP -> //.
(* proof that -1 < 0 is false, rewriting it to 0 < 1 then using ltr01 *)

view this post on Zulip Julien Puydt (May 25 2022 at 13:01):

@Pierre Roux We,, it does look a bit better with your formulation ; for the proof, the line you propose doesn't do anything. When will the next MC with better numbers get out?

view this post on Zulip Pierre Roux (May 25 2022 at 13:13):

Right, I forgot /orP, this seems to work:

From mathcomp Require Import all_ssreflect ssralg ssrnum rat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.

Import Order.Theory GRing.Theory Num.Theory.

Section Trivial.

Variable a: rat.

Lemma noname: (a == -1) || (a == 1 / 2%:R) -> 0 < a -> a == 1 / 2%:R.
Proof. by move=> /orP[] /eqP->. Qed.

view this post on Zulip Pierre Roux (May 25 2022 at 13:14):

For the next release, no idea (hopefully before the end of the year), but that's a relatively minor point anyway.


Last updated: Feb 08 2023 at 04:04 UTC