Stream: Coq users

Topic: nested let destructs


view this post on Zulip Vincent Siles (Nov 13 2020 at 07:50):

Hi ! I have a function that returns a (nat * (A * B)) and atm I have to use let (n, foo) := ... in let (a, b) := foo in ... to get everything out. I kind of remember there was a way to write a more nested pattern, like let (n, (a, b)) := ... directly but can't find it again. Is is possible ? Am I mistaken ?

view this post on Zulip Théo Winterhalter (Nov 13 2020 at 07:53):

Hi, you just add ' in front of the pattern.

view this post on Zulip Théo Winterhalter (Nov 13 2020 at 07:53):

let '(a, (b,c)) := foo in ...

view this post on Zulip Vincent Siles (Nov 13 2020 at 08:01):

' , lovely thank you. I remembered something around : but not '. Is it in the doc ? I really tried to look it up but with no luck

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:04):

Yes, it's documented here: https://coq.github.io/doc/v8.12/refman/language/extensions/match.html#second-destructuring-let-syntax

view this post on Zulip Karl Palmskog (Nov 13 2020 at 08:18):

are you using ssreflect? In this case let: will be the go-to choice: https://coq.github.io/doc/v8.12/refman/proof-engine/ssreflect-proof-language.html#pattern-assignment

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:36):

@Karl Palmskog: Do you have any concrete reason to recommend let: over let '? We were precisely discussing with @Enrico Tassi about getting rid (at least) of the implementation of let: and plug it to mean let ' or even about deprecating the syntax (this last part was less clear given the probably large number of use cases in existing code).

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:38):

BTW, note that the ' irrefutable pattern syntax can also be used directly in the binder syntax, e.g., when defining a function (https://coq.github.io/doc/v8.12/refman/language/core/assumptions.html#binders).

view this post on Zulip Vincent Siles (Nov 13 2020 at 08:39):

Karl Palmskog said:

are you using ssreflect? In this case let: will be the go-to choice: https://coq.github.io/doc/v8.12/refman/proof-engine/ssreflect-proof-language.html#pattern-assignment

So this is where my memory comes from :) I used to when I was in Chalmers, but I kind of forgot my way through ssr libs, so I'm using plain Coq atm

view this post on Zulip Karl Palmskog (Nov 13 2020 at 08:55):

@Théo Zimmermann basically, if you are committing to using ssreflect, you use all its operators/idioms. If not, then not. There is indeed tons of code using let:, so getting rid of it would be a big endeavour

view this post on Zulip Karl Palmskog (Nov 13 2020 at 08:57):

I don't really care how it's implemented under the hood as long as semantics and syntax is preserved

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:58):

Our point (and this was the plan since the SSR integration in Coq 8.7) is to make SSR a proof language and only that. So all of its extensions to the vernacular / to Gallina must be eventually merged into Coq. Syntax-wise, the merging might indeed require to keep the existing syntax ad vitam eternam if the compatibility impact of deprecating one of them would be too important.

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 09:00):

As another example, as you know, we are going to eventually remove the Search command that was provided by SSR but only once all SSR users are satisfied with the alternative we provide, and of course, it is easier to do with respect to compatibility since Search calls are rarely kept in finished proof scripts.


Last updated: Jan 31 2023 at 13:02 UTC