Stream: Beginner Questions

Topic: Non-constructor pattern


view this post on Zulip Gergely Buday (Jan 27 2021 at 10:27):

In order to simplify multiplicative expressions I wrote

fun times :: "aexp ⇒ aexp ⇒ aexp" where
  "times (N i) (N j) = N(i*j)"
| "times (N 0) a = (N 0)"
| "times (N 1) a = a"
| "times (N i) a = Times (N i) a"
| "times a (N 0) = (N 0)"
| "times a (N 1) = a"
| "times a (N i) = Times (N i) a"
| "times a1 a2   = Times a1 a2"

for that I got

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀a. times (N 0) a = N 0

According to

https://stackoverflow.com/questions/38975187/error-non-constructor-pattern-not-allowed-in-sequential-mode-isabelle

this need not be a concern as 0 is a constant. Is N being int => aexp instead of nat => aexp the problem?

Once I did this exercise and I vaguely remember that it is by no accident that this works only:

fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i⇩1) (N i⇩2) = N(i⇩1+i⇩2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"

with an if. From my ML intuition that might not be carried to HOL, constructor + constant is a neat idea in a pattern. Why is it not here?

The full file is Ex_3_4.thy

view this post on Zulip Mathias Fleury (Jan 27 2021 at 11:02):

Pattern matching on ints does not work, because they are not defined with constructors.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:05):

Even pattern matching on nats is, well, you can do it, but it can cause some pain. If it's just 0 that you're matching on, that's fine, but if you're matching on e.g. 3 you have to write ‘f (Suc (Suc (Suc 0))) = …’ and you get equations for 0, Suc 0, Suc (Suc 0), and Suc (Suc (Suc (Suc n))), which is a bit excessive.

The problem is that the function package only allows to match on constructor patterns and not on things like equality. It could, in principle, but it is not implemented (and would probably be quite a bit of work to implement now).

view this post on Zulip Gergely Buday (Jan 27 2021 at 11:06):

It also implies that I cannot do a case analysis on the value? Basically, case analysis and pattern matching is the same thing, right?

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:06):

You can define functions with more complex matching (even conditional matching like in Haskell), but then you have to prove exhaustiveness and non-overlapping of patterns yourself. See the Function package documentation for more information on that.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:06):

Also you lose executability.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:07):

(Although it can be restored by giving a code equation.)

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:07):

Gergely Buday said:

It also implies that I cannot do a case analysis on the value? Basically, case analysis and pattern matching is the same thing, right?

Not sure what you mean by that.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:07):

Do you mean the case combinator? If yes, I think that also only works on constructor patterns.

view this post on Zulip Gergely Buday (Jan 27 2021 at 11:08):

@Manuel Eberl yes, pattern matching as above, case analysis with the case keyword

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:08):

I actually don't know how case works exactly, it's a bit of black magic because you can write nested pattern matches with case and they somehow get transformed magically into calls to specific case combinators like case_nat, case_option etc.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:08):

Probably checking phase or something like that.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:09):

(And similar caveats apply for case; if your case expressions become too elaborate you can get an exponential blow up in the term size. I vaguely recall some other system having smarter case expressions; Isabelle's are rather simplistic.)

view this post on Zulip Mathias Fleury (Jan 27 2021 at 11:10):

Manuel Eberl said:

The problem is that the function package only allows to match on constructor patterns and not on things like equality. It could, in principle, but it is not implemented (and would probably be quite a bit of work to implement now).

Not sure. The problem is that the function package does disambiguation on the patterns. If you add equality, I am so not sure that it is still possible.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:10):

Yeah but you would have to write the disambiguator and extend the exhaustiveness/non-overlappingness prover to handle that.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:11):

I mean, I'm sure it is feasible, but I don't think it's trivial.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:11):

Feel free to do it if you feel like it. :grinning:

view this post on Zulip Mathias Fleury (Jan 27 2021 at 11:13):

My intuition says that it is not possible in general, but I might be wrong :surprise:

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:14):

Ah, you meant ‘I am not sure’? Because you wrote ‘I am so sure’.

view this post on Zulip Mathias Fleury (Jan 27 2021 at 11:15):

Sorry, typo…

view this post on Zulip Gergely Buday (Jan 27 2021 at 11:16):

The simplifier handled well the if-then-else constructs. Probably they are less readable for humans but the simplifier is another beast.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:17):

True, equality will probably cause some problems. To imitate what e.g. SML/Haskell do, you would have to add a precondition ≠ foo to every equation after an equation of the form f foo = … except when the function package can statically prove that the thing is ≠ foo.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:17):

And proving exhaustiveness is probably impossible in general unless you have a ‘catch-all’ equation somewhere.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:18):

Probably wouldn't be terribly usable all in all…

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:18):

Gergely Buday said:

The simplifier handled well the if-then-else constructs. Probably they are less readable for humans but the simplifier is another beast.

Yes, if-then-else works well. The conditional matching I mentioned is basically a similar way to get the same thing.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:18):

You can still derive versions without the if as derived simp rules.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:19):

For instance, if you have f x = (if x = 1 then foo else bar x), you can prove e.g. f 1 = foo and x ≠ 1 ⟹ f x = bar x. That can sometimes come in useful.

view this post on Zulip Manuel Eberl (Jan 27 2021 at 11:20):

(In particular, you can then declare these as simprules and delete the original simp rule. I for one don't like it when ifs crop up somewhere without me explicitly telling them to.


Last updated: Sep 25 2022 at 23:25 UTC