Last active
January 3, 2024 09:30
-
-
Save ice1000/2b0ce5b989530b5c1dd43018498e456c to your computer and use it in GitHub Desktop.
A proof that inductive-inductive even is equivalent to directly defined even
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive nat: Type := | |
| S (n: nat) | |
| O. | |
Inductive even: nat -> Prop := | |
| Base: even O | |
| Ind: forall n, even n -> even (S (S n)). | |
Inductive ev: nat -> Prop := | |
| ev_Base: ev O | |
| ev_Ind: forall n, odd n -> ev (S n) | |
with odd: nat -> Prop := | |
| odd_Ind: forall n, ev n -> odd (S n). | |
(* The hard part *) | |
(* It can only be done in this way, mutual Lemma won't work because | |
* Coq don't know how the decreasing argument works. | |
* The fact that we first intro & induction on n then apply the constructor | |
* is very important, we can't apply the constructor first or it will fall | |
* into the same problem. | |
*) | |
Lemma ev_even: forall n, | |
( | |
((ev n) -> even n) * | |
((odd n) -> even (S n)) | |
). | |
intros n. | |
induction n as [ n f |]. | |
constructor. | |
intro h. inversion h. apply f. assumption. | |
intro h. constructor. inversion h. apply f. assumption. | |
repeat constructor. | |
intro h. | |
inversion h. | |
Qed. | |
Theorem ev_even_eq: forall n, ev n <-> even n. | |
Proof. | |
intros. constructor. | |
apply ev_even. | |
intros h. induction h. constructor. repeat constructor. assumption. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment