Skip to main content

Questions tagged [pattern-matching]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
tinlyx's user avatar
  • 2,034
2 votes
1 answer

How to recover implicit arguments of inductive types in a match expression?

def IsEven: Nat → Prop | => True | Nat.succ pred => ¬IsEven pred inductive Example: Nat → Prop | IsExample: IsEven n → Example (n + 10) Here, ...
Jozef Mikušinec's user avatar
4 votes
2 answers

Binding variables to terms involving later variables

Consider the following pseudocode in a hypothetical proof assistant: def f (n : ℕ) : P n := match n with | zero -> ?0 | suc k -> ?1 end ...
Mike Shulman's user avatar
  • 3,060
0 votes
0 answers

How to get term describing case of pattern match in Coq

In Coq, While trying to write a definition of a function with well-founded recursion, I found myself wanting/having to reference that a term I was trying to match ...
C.E.Sally's user avatar
  • 121
3 votes
1 answer

What is a pattern in dependent pattern matching?

I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
tinlyx's user avatar
  • 2,034
6 votes
1 answer

Why can addition be used in pattern matching Nats but not multiplication

Here's a simple dummy function in Lean 4: def foo : Nat → Nat | (m*2) => m | (m+2) => m | (m+1) => m | (0) => 0 Lean has no trouble ...
Nate Glenn's user avatar
1 vote
1 answer

How to deduce this equality based on the fact that these two terms must be the same?

Brief (but possibly inaccurate) Summary: I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get ...
Agnishom Chattopadhyay's user avatar
3 votes
3 answers

Pattern matching from `Prop` to `Type` in Lean

I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately. I wanted to write a function like ...
Celso Bonutti's user avatar
4 votes
1 answer

Doing case-by-case proofs about match statements in Lean4

In Lean4, I am stuck in a proof with a goal like this: ...
Jeremy Salwen's user avatar
4 votes
1 answer

Is it a good idea to modify the context during type checking of patterns?

So I'm working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have ...
ice1000's user avatar
  • 6,186