Stream: math-comp users

Topic: Converting `\in`-`pred` to function application


view this post on Zulip Julin Shaji (Mar 15 2024 at 16:11):

Is it possible to convert a term like l \in [pred l0 | size l0 == 2]
to (fun l0 => size l0 == 2) l?

I was looking for a way to do a rewriting to replace the size l0
part in the \in version.

From mathcomp Require Import all_ssreflect.

Definition l: seq nat := [:: 0; 1].

Check l \in [pred l0 | size l0 == 2].
Check (fun l0 => size l0 == 2) l.

view this post on Zulip Julin Shaji (Mar 15 2024 at 16:19):

And how can we search for definitions involving [pred .. ]?

To find definition name, Locate "[pred _]". gave nothing.

view this post on Zulip Pierre Roux (Mar 15 2024 at 16:40):

Then try something less specific like Locate "pred".

view this post on Zulip Pierre Roux (Mar 15 2024 at 16:43):

Note that your two terms are convertible

Goal l \in [pred l0 | size l0 == 2] = (fun l0 => size l0 == 2) l.
Proof.
(* rewrite inE. *)  (* gives (size l == 2) == (size l == 2) *)
reflexivity.
Qed.

view this post on Zulip Julin Shaji (Mar 15 2024 at 16:46):

Yeah, I was trying to figure out a way to convert from one form to the other. Couldn't find a way to rewrite size l0 when l0 is not even an assumption.

view this post on Zulip Julin Shaji (Mar 15 2024 at 16:46):

I mean, without having to prove a separate lemma.

view this post on Zulip Pierre Roux (Mar 15 2024 at 16:48):

Maybe there is some extensionality lemma that can be used with the under tactic, like eq_bigr for bigops.

view this post on Zulip Julin Shaji (Mar 15 2024 at 17:13):

I'm not (yet) familiar with under.

But for now, I think I can work with this (though I'm not sure if I'm treading in the right track):

Goal forall (A: Type) (l:seq A) (bexp: bool),
  l \in [pred l0 | bexp] = (fun l0 => bexp) l.
Proof. by []. Qed.

view this post on Zulip Julin Shaji (Mar 15 2024 at 17:17):

Or not.. I can't get it to work. I guess I better dig through under.


Last updated: Jul 25 2024 at 16:02 UTC