Is it possible to go from a term of type `(a <? b) = true`

to a term of type `a < b`

using views in ssreflect?

(I was trying to get familiar with views)

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

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.
```

Vews are mostly using `reflect`

so you just need a reflection lemma between `a <? b`

and `a < b`

Is such a reflection lemma already there?

`Search (reflect (_ <? _) _).`

didn't give anything. Is that the right way to look for predefined lemmas?

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.
```

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

or something like that.

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?

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.
```

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`

Thanks! That was it.

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 (_ <? _) _). `

.

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

Ah.. right... :sweat_smile:

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?

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
*)
```

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

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

I guess views are applied using only `move`

and not `rewrite`

?

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

or `have H2 := Nat.ltb_spec0 H1.`

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.
```

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

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

Last updated: Jun 13 2024 at 19:02 UTC