Stream: Coq users

Topic: Matching on Prop

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?

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

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)

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

Christopher Lam (Feb 08 2024 at 20:55):

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

Gaëtan Gilbert (Feb 08 2024 at 20:57):

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

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?

Théo Winterhalter (Feb 09 2024 at 08:15):

Why would it be a bug?

Théo Winterhalter (Feb 09 2024 at 08:16):

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

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.

Pierre Courtieu (Feb 09 2024 at 08:16):

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

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

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 :-)

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.

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.

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.

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.

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.

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?

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.

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.

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

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

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.

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.

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.

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.

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: Oct 13 2024 at 01:02 UTC