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.

view this post on Zulip Julien Puydt (May 25 2022 at 20:17):

Eh, it turns out the result I needed was a bit stronger than the simple case I asked about ; I was still able to adapt it, so here is what I turned up with:

Let only_positive_root: forall a: RR, (a == -1) || (a == 1 / 2%:R) -> (0 < a) -> a == 1 / 2%:R.
Proof.
move=> a /orP[] /eqP -> //. (* this one line works for a: rat *)
by rewrite Num.Theory.ltr0N1.
Qed.

where Definition RR := { realclosure rat }., coming from MC-real-closed.

@Pierre Roux Thanks!

view this post on Zulip Notification Bot (May 25 2022 at 20:17):

Julien Puydt has marked this topic as resolved.

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

Indeed, if a is not of a "concrete" type like rat, 0 < -1 cannot be simplified to false. Note that we often Import Num.Theory to avoid typing it again and again.


Last updated: Jul 25 2024 at 16:02 UTC