Short question is: how to prove (or how to postulate in a "better" way) theorem even_sum_right_0 (or even_sum_commute or both of them) from the code below
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS (even_sum e e2)
end.
Theorem add_comm_right_0 : forall n, n = n + 0.
induction n; crush.
Defined.
Theorem add_comm : forall (n m : nat), n + m = m + n.
induction n; intros.
apply add_comm_right_0.
crush.
Defined.
Theorem even_sum_commut' : forall n1 n2, even (n1 + n2) -> even (n2 + n1).
intros.
rewrite add_comm.
apply H.
Defined.
Theorem odd_sum_commut' : forall n1 n2, odd (n1 + n2) -> odd (n2 + n1).
intros. rewrite add_comm. assumption.
Defined.
Scheme even_mut := Induction for even Sort Prop
with odd_mut := Induction for odd Sort Prop.
Theorem even_sum_right_0 : forall n1 (e1 : even n1),
e1 = even_sum_commut' n1 0 (even_sum e1 EZ).
Proof.
apply (even_mut (fun n en => en = even_sum_commut' n 0 (even_sum en EZ))
(fun n on => on = odd_sum_commut' n 0 (odd_sum on EZ))).
- simpl. reflexivity.
- intros. simpl.
Admitted.
Theorem even_sum_commut : forall n1 n2 (e1 : even n1) (e2 : even n2),
even_sum e1 e2 = even_sum_commut' _ _ (even_sum e2 e1).
Proof.
Admitted.
As I see, even_sum e1 e2 and even_sum e2 e1 is the same term (by definition of even_sum). So, it looks to me like theorem should be provable. But I'm not sure (types are different and it looks to me like this is part of the problem).
The long story is below.
I'm reading Adam Chlipala's cpdt (great thanks to the author!). And also I'm trying to solve exercises he provides. The first 4 exercises were a pleasure for me to solve them (because it is rather quick thing). But I faced an exercise which can became a bit more interesting if one modifies it.
Chapter 0.1 From InductiveTypes, exercise 5.
- Define mutually inductive types of even and odd natural numbers, such that any natural number is isomorphic to a value of one of the two types. (This problem does not ask you to prove that correspondence, though some interpretations of the task may be interesting exercises.) Write a function that computes the sum of two even numbers, such that the function type guarantees that the output is even as well. Prove that this function is commutative.
This task can be easily solved using next definition:
Inductive nat_even : Type :=
| EZ' : nat_even
| EN' : nat_odd -> nat_even
with nat_odd : Type :=
| ON' : nat_even -> nat_odd.
But I would like to try a bit another definition given above (inspired by one which is given in the book).
A small explanation. Please, pay your attention: this is not a textbook exercise, this is a (my own) modification which makes task a bit not trivial to solve (at least for me). Original task from the book is rather straighforward (well, you need to think about it a bit, but still). So, there is no any possible "breaks of code of honor" here...
Any ideas are welcome, I'm intersted to know about "how to do it in a better way" or just "how to do it in another way". I mean "how to formulate and prove theorem for different types and is this possible".
It may be somebody could give me a link to textbook/paper to read. This would be great too.
The best way to solve this kind of issue is by forgetting the type dependency. In this case, the proofs of even n and odd n are completely characterized by n, as the following lemmas show.
From Coq Require Import ssreflect ssrfun.
Require Import Coq.Arith.Arith.
Set Implicit Arguments.
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_or_odd (n : nat) : even n + odd n :=
match n with
| 0 => inl EZ
| S m => match even_or_odd m with
| inl p => inr (OS p)
| inr p => inl (ES p)
end
end.
Fixpoint nat_of_evenK n (p : even n) : even_or_odd n = inl p :=
match p with
| EZ => erefl
| @ES m p => congr1 (fun r : even m + odd m =>
match r with
| inl q => inr (OS q)
| inr q => inl (ES q)
end)
(nat_of_oddK p)
end
with nat_of_oddK n (p : odd n) : even_or_odd n = inr p :=
match p with
| @OS m p => congr1 (fun r : even m + odd m =>
match r with
| inl q => inr (OS q)
| inr q => inl (ES q)
end)
(nat_of_evenK p)
end.
Lemma even_irrel n (p q : even n) : p = q.
Proof.
suff [//] : inl p = inl q :> even n + odd n.
by rewrite -2!nat_of_evenK.
Qed.
Lemma odd_irrel n (p q : odd n) : p = q.
Proof.
suff [//] : inr p = inr q :> even n + odd n.
by rewrite -2!nat_of_oddK.
Qed.
In particular,
Definition even_comm_cast n m : even (n + m) -> even (m + n) :=
let: erefl := Nat.add_comm n m in id.
Lemma even_addC n m (p : even (n + m)) (q : even (m + n)) :
p = even_comm_cast m n q.
Proof.
rewrite /even_comm_cast.
case: (n + m) / Nat.add_comm p => //= p; exact: even_irrel.
Qed.