Stream: Coq users

Topic: ssreflect: `a <? b = true` to `a < b`


view this post on Zulip Julin Shaji (Feb 21 2024 at 06:44):

Is it possible to go from a term of type (a <? b) = trueto a term of type a < b using views in ssreflect?
(I was trying to get familiar with views)

view this post on Zulip Julin Shaji (Feb 21 2024 at 06:45):

Goal forall a b: nat,
  (a <? b) = true -> a < b.
Proof.
  move => a b.

view this post on Zulip djao (Feb 21 2024 at 07:24):

I'm not sure what you mean by "using views" but here is how I would do it.

From Coq Require Import PeanoNat ssrbool ssrfun ssreflect.
Goal forall a b: nat, (a <? b) = true -> a < b.
Proof.
  move => a b /Nat.leb_le //.
Qed.

view this post on Zulip Pierre Roux (Feb 21 2024 at 07:25):

Vews are mostly using reflect so you just need a reflection lemma between a <? b and a < b

view this post on Zulip Julin Shaji (Feb 21 2024 at 07:38):

Is such a reflection lemma already there?

Search (reflect (_ <? _) _). didn't give anything. Is that the right way to look for predefined lemmas?

view this post on Zulip djao (Feb 21 2024 at 07:41):

Maybe Nat.ltb_spec0 : forall x y : nat, reflect (x < y) (x <? y)

From Coq Require Import PeanoNat ssrbool ssrfun ssreflect.
Goal forall a b: nat, (a <? b) = true -> a < b.
Proof.
  move => a b /Nat.ltb_spec0 //.
Qed.

view this post on Zulip Pierre Roux (Feb 21 2024 at 07:52):

Exactly, and the proper search command is probably something like Search reflect Nat.ltb ltn or something like that.

view this post on Zulip Julin Shaji (Feb 21 2024 at 07:57):

djao said:

Maybe Nat.ltb_spec0 : forall x y : nat, reflect (x < y) (x <? y)

From Coq Require Import PeanoNat ssrbool ssrfun ssreflect.
Goal forall a b: nat, (a <? b) = true -> a < b.
Proof.
  move => a b /Nat.ltb_spec0 //.
Qed.

I had imported mathcomp as well. Like:

From mathcomp Require Import all_ssreflect.
Require Import Arith.

And this proof doesn't finish. It ends with:

a, b : nat

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

(a < b)%coq_nat -> a < b

There are two interpretations of the _ < _ notation in my scope:

Locate "_ < _".
(*
Notation "m < n" := (lt m n) : coq_nat_scope
Notation "m < n" := (leq (S m) n) : nat_scope (default interpretation)
Notation "x < y" := (Order.lt x y) : order_scope
*)

I guess that's the problem?

Any idea how to fix this?

view this post on Zulip djao (Feb 21 2024 at 07:59):

That's just mathcomp having its own less than operator, separate from the built-in Coq operator.

From Coq Require Import PeanoNat.
From mathcomp Require Import all_ssreflect.
Goal forall a b: nat, (a <? b) = true -> a < b.
Proof.
  move => a b /Nat.ltb_spec0 /ltP //.
Qed.

view this post on Zulip djao (Feb 21 2024 at 08:01):

Maybe there is a better way to figure it out, but what I did was just run Search leq. and then Ctrl+F the search output for coq_nat

view this post on Zulip Julin Shaji (Feb 21 2024 at 08:09):

Thanks! That was it.

view this post on Zulip Julin Shaji (Feb 21 2024 at 08:10):

Doing Search reflect Nat.ltb ltn brought up those reflection lemmas.
I'm not sure why they didn't come up when I just did Search (reflect (_ <? _) _). .

view this post on Zulip djao (Feb 21 2024 at 08:20):

I guess you needed Search (reflect _ (_ <? _)).

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

Ah.. right... :sweat_smile:

view this post on Zulip Julin Shaji (Feb 21 2024 at 10:07):

A related doubt.

I have an assumption like

H1: a <? b
-----------
?Goal

for some goal.

I need to convert this to

H1: a <? b
H2: a < b
-----------
?Goal

I guess I can use Nat.ltb_spec0 and ltP for this.

But how do we go about using them?

I had been trying this (used False as goal for example's sake):

From mathcomp Require Import all_ssreflect.
Require Import Arith.

Goal forall a b: nat,
  a <? b -> False.
Proof.
  move => a b H1.
  move: H1 /Nat.ltb_spec0.
(*
dependents switch `/' in move tactic
*)

The last line showed an error message included as comment above.

How can I use the two lemmas right?

view this post on Zulip Julin Shaji (Feb 21 2024 at 10:09):

This made it work though:

Goal forall a b: nat,
  a <? b -> False.
Proof.
  move => a b /Nat.ltb_spec0 /ltP.
(*
1 subgoal

a, b : nat

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

a < b -> False
*)

view this post on Zulip Julin Shaji (Feb 21 2024 at 10:09):

I think I'm missing some of the basic ideas in using views..

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

Can't we apply a view on a term once it has been introduced before or something?

view this post on Zulip Julin Shaji (Feb 21 2024 at 10:11):

I guess views are applied using only move and not rewrite?

view this post on Zulip Pierre Roux (Feb 21 2024 at 12:27):

To create H2, you probably want something like (untested) have /Nat.ltb_spec0 H2 := H1. or have H2 := Nat.ltb_spec0 H1.

view this post on Zulip djao (Feb 21 2024 at 13:41):

I would do it this way.

From mathcomp Require Import all_ssreflect.
Require Import Arith.
Goal forall a b: nat, a <? b -> False.
Proof.
  move=> a b /[dup] H1 /Nat.ltb_spec0 /ltP H2.

view this post on Zulip djao (Feb 21 2024 at 13:43):

If you want to do it your way, you would have needed move: H1 => /Nat.ltb_spec0.

view this post on Zulip Pierre Roux (Feb 21 2024 at 14:06):

Then the "idiomatic" solution would probably be have /Nat.ltb_spec0/ltP H2 := H1.


Last updated: Jun 13 2024 at 19:02 UTC