Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Set the syntax to be Coq in the post

Browse Source
This commit is contained in:
Danila Fedorin 2019-08-13 21:32:05 -07:00
parent fce8e75dde
commit fe0437eabf
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
content/blog/coq_palindrome.md
View File

@ -14,7 +14,7 @@ Of course, my definition led to only having palindromes of even length. In order
* A list with a single value is a palindrome. * A list with a single value is a palindrome.
This translates readily into Coq: This translates readily into Coq:
``` ```Coq
Inductive palindrome { X : Type } : list X -> Prop := Inductive palindrome { X : Type } : list X -> Prop :=
| palindrome_nil : palindrome [] | palindrome_nil : palindrome []
| palindrome_x : forall (x : X), palindrome [x] | palindrome_x : forall (x : X), palindrome [x]
@ -24,7 +24,7 @@ Inductive palindrome { X : Type } : list X -> Prop :=
### The first direction ### The first direction
It’s nearly trivial to show that a palindrome is its own inverse: It’s nearly trivial to show that a palindrome is its own inverse:
``` ```Coq
Theorem pal_rev { X : Type } : forall (l : list X), palindrome l -> l = rev l. Theorem pal_rev { X : Type } : forall (l : list X), palindrome l -> l = rev l.
Proof. Proof.
intros l H. intros l H.
@ -49,7 +49,7 @@ Then, the proposition holds for all values of that type. This can be easily seen
As I was working with my definition of a palindrome, it dawned on me that generalizing a single variable in that definition would create another inductive definition of a list. If we change the inductive rule in the palindrome definition from saying “surrounding another palindrome with x on both sides” to “surrounding another list with some x on one side and some y on the other”, we can effectively construct any list. We can then state a different structural induction principle: As I was working with my definition of a palindrome, it dawned on me that generalizing a single variable in that definition would create another inductive definition of a list. If we change the inductive rule in the palindrome definition from saying “surrounding another palindrome with x on both sides” to “surrounding another list with some x on one side and some y on the other”, we can effectively construct any list. We can then state a different structural induction principle:
``` ```Coq
Theorem alt_induction { X : Type } : forall (P : list X -> Prop), Theorem alt_induction { X : Type } : forall (P : list X -> Prop),
P [] -> P [] ->
(forall (x : X), P [x]) -> (forall (x : X), P [x]) ->
@ -61,7 +61,7 @@ But how would we go about proving this? If we try to just use induction on `ln`,
#### Proving Equivalence #### Proving Equivalence
What’s missing is that there’s nothing as yet stating that appending values to the back and the front of another list is an equivalent way to appending a value only to the front of a list. We need to state this explicitly; but how? I decided that the easiest way would be by defining a new inductive property, `list_alt` which holds for all lists that can be constructed by adding things to the back and the front. Then, we can show that it holds for all lists, and, therefore, that any list can be constructed this way. I defined the property as such: What’s missing is that there’s nothing as yet stating that appending values to the back and the front of another list is an equivalent way to appending a value only to the front of a list. We need to state this explicitly; but how? I decided that the easiest way would be by defining a new inductive property, `list_alt` which holds for all lists that can be constructed by adding things to the back and the front. Then, we can show that it holds for all lists, and, therefore, that any list can be constructed this way. I defined the property as such:
``` ```Coq
Inductive list_alt { X : Type } : list X -> Prop := Inductive list_alt { X : Type } : list X -> Prop :=
| list_alt_base : list_alt [] | list_alt_base : list_alt []
| list_alt_x : forall (x : X), list_alt [x] | list_alt_x : forall (x : X), list_alt [x]
@ -70,7 +70,7 @@ Inductive list_alt { X : Type } : list X -> Prop :=
Then, to prove it true for all lists, I first showed what is effectively the inductive hypothesis of a proof by induction on the structure of a list: Then, to prove it true for all lists, I first showed what is effectively the inductive hypothesis of a proof by induction on the structure of a list:
``` ```Coq
Theorem list_alt_cons { X : Type } : forall (x : X) (l : list X), Theorem list_alt_cons { X : Type } : forall (x : X) (l : list X),
list_alt l -> list_alt (x::l). list_alt l -> list_alt (x::l).
Proof. Proof.
@ -91,7 +91,7 @@ Qed.
``` ```
Next, the actual proof of equivalence simply used the previous theorem: Next, the actual proof of equivalence simply used the previous theorem:
``` ```Coq
Theorem list_alt_correct { X : Type } : forall (l : list X), list_alt l. Theorem list_alt_correct { X : Type } : forall (l : list X), list_alt l.
Proof. Proof.
induction l. induction l.
@ -102,7 +102,7 @@ Qed.
Finally, we can prove our custom principle of induction (by induction (!) on the property list_alt, which we now know holds for all lists): Finally, we can prove our custom principle of induction (by induction (!) on the property list_alt, which we now know holds for all lists):
``` ```Coq
Theorem alt_induction { X : Type } : forall (P : list X -> Prop), Theorem alt_induction { X : Type } : forall (P : list X -> Prop),
P [] -> P [] ->
(forall (x : X), P [x]) -> (forall (x : X), P [x]) ->
@ -118,7 +118,7 @@ Proof.
Finally, the palindrome proof can simply use this principle. Coq turns out to have a mechanism to use a custom induction principle via `induction … using …`: Finally, the palindrome proof can simply use this principle. Coq turns out to have a mechanism to use a custom induction principle via `induction … using …`:
``` ```Coq
Theorem rev_pal' { X : Type } : forall (l : list X), l = rev l -> palindrome l. Theorem rev_pal' { X : Type } : forall (l : list X), l = rev l -> palindrome l.
Proof. Proof.
intros l H. induction l using alt_induction. intros l H. induction l using alt_induction.