invalid pattern, constructor marked with '[match pattern]'

Stream: new members

[Vivek Rajesh Joshi]

I want to define an inductive type that describes the elementary row operations on a matrix. Could anyone explain why this error is popping up, and how to rectify it?

inductive elemOp : Type where
| scalarMul : Rat → Fin m → elemOp
| rowSwap : Fin m → Fin m → elemOp
| rowMulAdd : Rat → Fin m → Fin m → elemOp
deriving Repr

def elemOpOnMatrix (A : Matrix (Fin m) (Fin n) Rat) (E : elemOp (m:=m)) : Matrix (Fin m) (Fin n) Rat :=
match E with
| scalarMul c i => A.updateRow i (c · (A i))
--invalid pattern, constructor or constant marked with '[match pattern]' expected

[Kevin Buzzard]

I suspect that scalarMul is not matching with the constructor, whose name is elemOp.scalarMul. This might be one problem.

[Kevin Buzzard]

You can probably use .scalarMul, or namespace elemOp, or def elemOp.OnMatrix; these would all fix this problem.

[Vivek Rajesh Joshi]

Thanks!

[Victor Maia]

is this the right place to ask quick questions? I'm wondering why this doesn't check:

-- create an IsEven(n) inductive type for Nat
inductive IsEven : Nat → Prop where
  | ez : IsEven zero
  | es : ∀ n, IsEven n → IsEven (Nat.succ (Nat.succ n))

-- create a foo function that only receives even nats
def foo (n : Nat) (h : IsEven n) : Nat :=
  match n with
  | zero          => n
  | succ (succ p) => _

errors with invalid pattern, constructor or constant marked with '[match_pattern]' expected. why?

[Notification Bot]

A message was moved here from #general > v4.9.0-rc1 discussion by Mario Carneiro.

[Mario Carneiro]

@Victor Maia (moved the message here, that discussion is for reporting recent regressions)

[Mario Carneiro]

You are missing open Nat most likely, otherwise zero => will be interpreted as declaring a new variable and succ (succ p) is invalid syntax. The most recent version (or possibly the next version, since I think it isn't live yet) will have additional help to identify this mistake and suggest to use Nat.zero or .zero instead of zero

[Victor Maia]

that "discussion"? I thought that was just the general channel? sorry zulip is confusing lol

[Victor Maia]

okay so you mean I need the Nat., right? something like this works then:

-- create a foo function that only receives even nats
def foo (n : Nat) (h : IsEven n) : Nat :=
  match n with
  | Nat.zero              => n
  | Nat.succ Nat.zero     => _
  | Nat.succ (Nat.succ p) => n

but how do I mark this case as unreachable?

[Victor Maia]

can I disable the positivity checker so I can have proper HOAS?

[Kyle Miller]

def foo (n : Nat) (h : IsEven n) : Nat :=
  match n, h with
  | Nat.zero, _              => n
  | Nat.succ (Nat.succ p), _ => n

[Victor Maia]

nice, ty

[Victor Maia]

so just to be sure, no way to disable the positivity checker right?

[Kyle Miller]

If you want to prove anything about the function, no. (I assume you mean "termination checker" here, right? I know of positivity as a concept for inductive types, and maybe some systems use that also for checking structural recursion?)

[Victor Maia]

@Kyle Miller I just want to be able to write a HOAS type (like, lam : (Term -> Term) -> Term), which doesn't pass the positivity checker (which is likely part of the termination checker indeed). from your message, I assume I can actually disable it somehow? in agda for example, we can disable the termination checker. of course, that means our proofs may have inconsistencies, but it basically tells the type checker that you'll take care of this, so it only has to do the type checking, not the termination checking. and you can still write proofs the same

[Kyle Miller]

Ok, so you do mean positivity checker for the inductive types — I was confused because the context of your question was this foo function (and I was wondering how foo had anything to do with HOAS). The termination checker is completely different.

[Henrik Böving]

No you can't disable the positivity checker, Lean will not allow you to make it an inconsistent system apart from explicitly introducing axioms. You can instead use a PHOAS type to do the things you might do with HOAS: https://lean-lang.org/lean4/doc/examples/phoas.lean.html

[Victor Maia]

ah, that's unfortunate. phoas compiles to a considerably slower representation, which is very relevant if you want to build a fast interpreter. it is also considerably harder to prove things about and reason about, which is why I asked. hoas by itself is perfectly terminating. sad that we can't do it in lean, but fair enough

[Kyle Miller]

How does Agda do termination checking? Is it a decision procedure, or is it more like Lean, where the output of termination checking is the definition compiled as a recursor expression?

[Victor Maia]

idk but you can disable it and essentially say "for my project let me take care of termination, just check the types" (which IMO is the right take, specially because any termination checker will necessarily blacklist perfectly good programs)

[Kyle Miller]

Do these definitions still reduce? Lean relies on the fact the definitions are "compiled" to be recursor terms for reduction to succeed. If you skip this with the partial keyword, then the definitions become opaque.

[Victor Maia]

yes they reduce! it just disables the termination checker, that changes nothing on how the evaluator works. this is not related to axioms

[Victor Maia]

ah you can still have total coverage AND unrestricted recursion / negative types

[Kyle Miller]

In Lean there's also a difference between the kernel typechecker and the VM evaluator. You can evaluate things in the latter sense even if they can't be reduced in the DTT sense or have theorems proved about them.

[Victor Maia]

that is quite cool, but I'd still like to be able to prove things about a HOAS-based interpreter (I mean, otherwise I'd be using Haskell probably!) - but that is fair, I'll take that as an annoying limitation and move on

[Kyle Miller]

By the way, here's what factorial looks like after "termination checking":

def fact (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | k+1 => n * fact k

set_option pp.match false
#print fact
/-
def fact : Nat → Nat :=
fun n => Nat.brecOn n fun n f => fact.match_1 (fun n => Nat.below n → Nat) n (fun a x => 1) (fun k x => n * x.fst.fst) f
-/
#print fact.match_1
/-
def fact.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (n : Nat) → (Unit → motive 0) → ((k : Nat) → motive k.succ) → motive n :=
fun motive n h_1 h_2 => Nat.casesOn n (h_1 ()) fun n => h_2 n
-/

(I'm putting "termination checking" in quotes because it's not just a check.)

[Kyle Miller]

It also generates a couple lemmas so you never have to deal with these internal details.

#print fact.eq_1
/-
theorem fact.eq_1 : fact 0 = 1 :=
Eq.refl (fact 0)
-/
#print fact.eq_2
/-
theorem fact.eq_2 : ∀ (k : Nat), fact k.succ = k.succ * fact k :=
fun k => Eq.refl (fact k.succ)
-/

[Kyle Miller]

Just sharing this to give you a better idea of the limitations and what you might be able to expect or not expect from Lean

[Victor Maia]

thanks for sharing. interesting

[Mario Carneiro]

Henrik Böving said:

No you can't disable the positivity checker, Lean will not allow you to make it an inconsistent system apart from explicitly introducing axioms. You can instead use a PHOAS type to do the things you might do with HOAS: https://lean-lang.org/lean4/doc/examples/phoas.lean.html

Actually that's not true, with unsafe inductive lean will let you violate positivity