Stream: Coq users

Topic: Boolean inequality to prop


view this post on Zulip Julin Shaji (Dec 10 2023 at 08:13):

How can this be solved?

Require Import Arith ssreflect.

Goal forall a b: nat,
  (if a <=? b then false else true) = true -> a <= b.
Proof.

view this post on Zulip Julin Shaji (Dec 10 2023 at 08:13):

It is possible, right? Since we are going from decidable inequality to a Prop version.

view this post on Zulip Quentin VERMANDE (Dec 10 2023 at 08:51):

if x then false else true amounts to the boolean negation of x, so your statement looks wrong. Besides, unless you import libraries that contain something linking <=? and <=, you will probably use induction.

view this post on Zulip Paolo Giarrusso (Dec 10 2023 at 09:32):

Best use lemmas like Nat.leb_le or Nat.leb_spec; they should be imported by Require Arith


Last updated: Jun 13 2024 at 19:02 UTC