Stream: Coq users

Topic: Matching on Prop


view this post on Zulip Christopher Lam (Feb 08 2024 at 20:48):

Hello! I'm trying to match on in Coq and I'm running into what feels like weird behavior.
image.png

The attached image computes to true, and the kernel won't let me add another case in the match statement because it calls it redundant. Why does matching on one constant match the case of a different, disjoint constant?

view this post on Zulip Gaëtan Gilbert (Feb 08 2024 at 20:49):

True isn't a constructor so it's a binding variable
so what you wrote is the same as match False with x => true end

view this post on Zulip Gaëtan Gilbert (Feb 08 2024 at 20:50):

(constants and inductive types cannot be used in match patterns, they are built only from constructors and variables)

view this post on Zulip Enrico Tassi (Feb 08 2024 at 20:51):

Coq < Check (match True with False => false end).
false
     : bool

looks like the patter matching compiler is doing nuts

view this post on Zulip Christopher Lam (Feb 08 2024 at 20:55):

Okay, thank you! Is there a constructor for True in Prop?

view this post on Zulip Gaëtan Gilbert (Feb 08 2024 at 20:57):

True is declared as Inductive True : Prop := I.

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 08:13):

Enrico Tassi said:

Coq < Check (match True with False => false end).
false
     : bool

looks like the patter matching compiler is doing nuts

Looks like a bug to me :-). Is it already known?

view this post on Zulip Théo Winterhalter (Feb 09 2024 at 08:15):

Why would it be a bug?

view this post on Zulip Théo Winterhalter (Feb 09 2024 at 08:16):

As Gaëtan explained, this is the expected behaviour.

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 08:16):

Yes, it is known, but it is not necessarily a bug. It is a consequence of the algorithm for compiling things like match x, y, z with. You do not want spurious matches on z in branches where only x and y matter. But as a consequence, the single variable case looks strange.

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 08:16):

pattern matching on a value that is not in an inductive type?

view this post on Zulip Théo Winterhalter (Feb 09 2024 at 08:17):

Well it's not elaborated to a case internally.
match t with x => f end is one way to write the substitution f[x := t].

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 08:23):

Gaëtan didn't explain that match True with had a meaning. He explained why | True => xxx was not interpreted as Christopher thought.
I didn't know this. It looks weird :-)

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 08:26):

By the way, the fact that match t with x => f end is the substitution f[x := t] is a bug in my opinion, because it has some very adverse consequences on computation and extraction. It would be much better if it was compiled to let x := t in f.

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 08:31):

The well-known example is

Definition foo f x := match x, f x with O, O => O | _, y => y + y end.

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 08:33):

So if I understand well, pattern matching is first compiled and then the matched terms are checked to be of some inductive types. So the ones that disappears aren't.

view this post on Zulip Pierre-Marie Pédrot (Feb 09 2024 at 08:34):

The problem boils down to the fact that constructors and definitions share the same syntactic class in Coq. In OCaml they do not.

view this post on Zulip Pierre-Marie Pédrot (Feb 09 2024 at 08:35):

When the case elaborator sees a pattern matching with a single ident as lhs, it has to check whether this is a constructor or not. If it is, this is a normal pattern-matching, otherwise this is just a variable.

view this post on Zulip Pierre-Marie Pédrot (Feb 09 2024 at 08:35):

I thought we had a warning when this name happens to clash with a definition imported as a single ident, but it seems it's not the case?

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 08:40):

If I remember correctly, we have a warning only when using an identifier where _ would suffice. But here, _ does not suffice since the variable is used.

view this post on Zulip Pierre-Marie Pédrot (Feb 09 2024 at 08:42):

IMO we should really have a warning in case of potential name clash, this is definitely confusing even for knowledgeable users.

view this post on Zulip Théo Winterhalter (Feb 09 2024 at 08:43):

Or if you made a typo and suddenly you have a catch all instead of a concrete case (and then you forget others when you extend the definition).

view this post on Zulip Enrico Tassi (Feb 09 2024 at 08:56):

In this case, the problem is that the match "optimization" algorithm does not check anything at all.
First of all, if the match it is completely useless then why did the user write it? It should be signalled.

The problem is that, internally, this "optimization" is the base case of some recursion the match "optimizer" does, so if you remove it you break the algorithm (if you leave the match there, so that the type checker can do its job). At least, this is my recalling of an attempt by @Maxime Dénès

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 09:04):

Something is checked: the term between match and with is type checked, but it must just have a type. Check (match (forall x,x=0) with True => False end). is ok but match (forall x,true=0) with True => False end isn't.

view this post on Zulip Janno (Feb 09 2024 at 09:10):

I vaguely remember the ability to match on anything being a load-bearing feature for notations with tactic in terms. I think the idiom is Notation "..." := (match <big term using various parts bound in the notation> with | x => ltac:(<use x in some way>) end). This is probably documented in some issue somewhere.

view this post on Zulip Enrico Tassi (Feb 09 2024 at 12:08):

Pierre Courtieu said:

Something is checked: the term between match and with is type checked, but it must just have a type. Check (match (forall x,x=0) with True => False end). is ok but match (forall x,true=0) with True => False end isn't.

Then it is not as bad as I thought... it should not be too hard to check it is inductive then.

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 13:13):

Enrico Tassi said:

Then it is not as bad as I thought... it should not be too hard to check it is inductive then.

I am already starting getting used to it :-).
In some curious sense it makes the "match" being a particular case of "let" (well, let + zeta as pointed out by @Guillaume Melquiond ) instead of the opposite.

view this post on Zulip Pierre Courtieu (Feb 09 2024 at 13:14):

and let is ok with a non-inductive (until you use constructors in the pattern).


Last updated: Jun 13 2024 at 21:01 UTC