Julin Shaji (Feb 21 2024 at 06:44): 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)
Julin Shaji (Feb 21 2024 at 06:45):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
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?
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.
Exactly, and the proper search command is probably something like Search reflect Nat.ltb ltn or something like that.
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?
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.
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
Julin Shaji (Feb 21 2024 at 08:09):Thanks! That was it.
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 (_ <? _) _). .
djao (Feb 21 2024 at 08:20):I guess you needed Search (reflect _ (_ <? _)).
Julin Shaji (Feb 21 2024 at 09:12):Ah.. right... :sweat_smile:
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?
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
*)
I think I'm missing some of the basic ideas in using views..
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?
Julin Shaji (Feb 21 2024 at 10:11):I guess views are applied using only move and not rewrite?
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.
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.
If you want to do it your way, you would have needed move: H1 => /Nat.ltb_spec0.
Pierre Roux (Feb 21 2024 at 14:06):Then the "idiomatic" solution would probably be have /Nat.ltb_spec0/ltP H2 := H1.
Last updated: Oct 13 2024 at 01:02 UTC