Questions tagged [pattern-matching]
The pattern-matching tag has no usage guidance.
12
questions
1
vote
1
answer
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
1
answer
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 ...
2
votes
1
answer
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
2
votes
1
answer
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, ...
- 470
4
votes
2
answers
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
0
votes
0
answers
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
3
votes
1
answer
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
5
votes
1
answer
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
1
answer
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 ...
- 1,502
3
votes
3
answers
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
...
4
votes
1
answer
2k
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 257
4
votes
1
answer
81
views
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 ...
- 6,346