brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2025-10-09 14:31:13 +00:00
Code Issues Projects Releases Packages Activity

Added medium post metadata

Browse source
This commit is contained in:
Brandon Rozek 2023-02-01 19:36:22 -05:00
parent 8a93e4fb70
commit 6ad0dc95ac
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
3 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

12
content/blog/induction-lean3.md
View file

@ -1,10 +1,12 @@
---
title: "Induction in Lean 3: Three Techniques"
date: 2023-01-30T21:07:43-05:00
draft: false
tags: ["Formal Methods"]
date: 2023-01-30 21:07:43-05:00
draft: false
math: true
medium_enabled: true
medium_post_id: 5b4a36988c6d
tags:
- Formal Methods
title: 'Induction in Lean 3: Three Techniques'
---
When proving properties of an inductive data type, chances are that we need to perform the induction tactic on the data structure. There are multiple ways to approach this though and each comes with its own pros and cons.
@ -116,4 +118,4 @@ Personally, this one is the easiest for me to follow. The main issue that I have
## Conclusion
Each approach comes with its tradeoffs. The `rec_on` approach looks clean for single induction proofs. Meanwhile, the pattern matching approach works great with multiple induction. The easiest approach to determining the appropriate subgoals is to use the `induction` tactic. In fact, it sometimes is more efficient to write the entire proof via tactics first and then work towards making it more readable with additional subproofs and rewriting.
Each approach comes with its tradeoffs. The `rec_on` approach looks clean for single induction proofs. Meanwhile, the pattern matching approach works great with multiple induction. The easiest approach to determining the appropriate subgoals is to use the `induction` tactic. In fact, it sometimes is more efficient to write the entire proof via tactics first and then work towards making it more readable with additional subproofs and rewriting.