Fix list rendering in some posts.
This commit is contained in:
@@ -7,10 +7,12 @@ Going through the Software Foundations textbook, I found an exercise which I rea
|
||||
|
||||
### The inductive definition
|
||||
I wasn’t sure at first why the problem said that the inductive definition should have three constructors. I came up with two ways to construct a palindrome:
|
||||
|
||||
* An empty list is a palindrome.
|
||||
* Adding the same value to the back and the front of another palindrome makes a longer palindrome.
|
||||
|
||||
Of course, my definition led to only having palindromes of even length. In order to allow for palindromes of odd length, one more rule is needed (another base case):
|
||||
|
||||
* A list with a single value is a palindrome.
|
||||
|
||||
This translates readily into Coq:
|
||||
@@ -42,6 +44,7 @@ The proof in the other direction took me a significant amount of time. It was cl
|
||||
|
||||
#### A different kind of induction
|
||||
Coq’s basic induction wouldn’t do. But structural induction doesn’t limit us to a particular definition of a list; it just states that if:
|
||||
|
||||
* We can prove that a proposition holds for the primitive values of a type
|
||||
* We can prove that if the proposition holds for the building blocks of a value of the type then the proposition holds for the value built of those blocks
|
||||
|
||||
|
||||
Reference in New Issue
Block a user