# Questions tagged [pattern-matching]

The tag has no usage guidance.

12 questions
Filter by
Sorted by
Tagged with
1 vote
25 views

### Passing functions to casesOn which do not depend on a pattern match

In Chapter 8 of Theorem Proving with Lean4, there's the following example of a tail function for dependent lists: ...
• 113
1 vote
71 views

### Lean Proving a Prop that has a match

I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem ...
64 views

### 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 (...
• 2,320
154 views

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

def IsEven: Nat → Prop | Nat.zero => True | Nat.succ pred => ¬IsEven pred inductive Example: Nat → Prop | IsExample: IsEven n → Example (n + 10) Here, ...
217 views

### 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 ...
• 3,240
77 views

### 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 ...
• 121
278 views

### 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 ...
• 2,320
253 views

### 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 ...
• 243
1 vote
150 views

### 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 ...
440 views

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