Julien Puydt (May 25 2022 at 12:03): 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.
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 *)
@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?
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.
For the next release, no idea (hopefully before the end of the year), but that's a relatively minor point anyway.
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!
Notification Bot (May 25 2022 at 20:17):Julien Puydt has marked this topic as resolved.
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: Oct 13 2024 at 01:02 UTC