# Induction with (deprecated) even

## Background

I’m exploring different ways of proving the following otherwise tedious proposition:

``````Lemma tauto1 p: p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ p)))))))).
``````

Here are a few sample tactic-based proofs (each line is a separate proof).

``````  tauto.

repeat (split; easy || intros ->).
repeat (repeat split; assumption || (intros; assumption) || intros ->).
``````

But the point of the exercise for me was to explore proving `tauto1` by equivalence with the following:

``````Fixpoint B n p :=
match n with
| 0 => True
| 1 => p
| S n => p ↔ B n p
end.
``````

It should be clear that `tauto1 = B 10`. Further, though this takes a little thought, for any `p` and even `n`, `B n p` is a tautology. I’ve explored several different ways of stating this fact. Here are two using the standard library:

``````Lemma B2 n p: B (2 * n) p.
Proof.
induction n; [ easy | ].

simpl (2 * 1) in *.
destruct n; [ easy | ].

(* because for some reason rewrite in * isn't working *)
replace (2 * S n) with (2 * 1 + 2 * n)
in IHn |- *
by now rewrite <- (PeanoNat.Nat.mul_add_distr_l 2 1 n).
simpl (2 * 1) in *.

split;
[ split; intros _; assumption
| intros [_ ?]; auto ].
Qed.

Lemma B2_Even n p: PeanoNat.Nat.Even n → B n p.
Proof.
intros [k Hk]; subst.
apply B2.
Qed.
``````

This gives the following possible additional proves of `tauto1` after `change (B (2 * 5) p).`:

``````  apply B2_Even; now exists 5.
exact (B2 5 p).
``````

But `B2` is a tedious proof (though I have been perhaps more explicit than necessary on purpose). My preferred version of that proof would be induction on evidence for even-ness, so that I can simply jump by 2s in the naturals.

Here is one version, with proof that my `ev` is equivalent to `Even`:

``````Inductive ev: nat → Prop :=
| ev_0: ev 0
| ev_SS n: ev n → ev (S (S n)).

(* spec *)
Theorem ev_Even n: ev n ↔ PeanoNat.Nat.Even n.
Proof.
split; intros Hevn.
- induction Hevn; [ now exists 0 | ].
destruct IHHevn as [k Hevk]; subst.
exists (S k).
now replace (2 * S k) with (2 * 1 + 2 * k)
by now rewrite <- (PeanoNat.Nat.mul_add_distr_l 2 1 k).
- destruct Hevn as [k Hevk]; subst.
generalize dependent k.
induction k; [ exact ev_0 | ].
replace (2 * S k) with (2 * 1 + 2 * k)
by now rewrite <- (PeanoNat.Nat.mul_add_distr_l 2 1 k).
exact (ev_SS _ IHk).
Qed.

Lemma B2_ev n p: ev n → B n p.
Proof.
intros H; induction H; [ exact I | ].
simpl; split.
- now destruct n.
- destruct n; [ auto | intros ->; exact IHev ].
Qed.
``````

And the corresponding proof of `tauto1` is `apply B2_ev; repeat constructor.`.

## Question

The next natural step is to reformulate in terms of the deprecated `even` property in the standard library. Then `ev` would be unecessary.

The difficulty is that, when proving by induction on `even n` in

``````Lemma B2_even n p: even n → B n p.
``````

We have no effective induction hypothesis because of the mutually recursive but unrelated constructors. I’ve seen this before once, and my solution then was to build a stronger induction principle to use. With an induction principle in place, I can get

``````Proof.
intros Heven; induction Heven using even_ind_odd; [ exact I | ].
simpl; split.
- now destruct n.
- destruct n; [ auto | intros ->; exact IHHeven ].
Qed.
``````

readily, with ` apply B2_even; repeat constructor.` a proof of `tauto1` again.

The problem is creating the induction principle. After a messy failed attempt to use `fix` in the definition directly, I resorted to a tactic definition mimicing the structure I wanted. Intuitively it is correct, but alas…

``````Definition even_ind_odd (P: nat → Prop)
(P0: P 0)
(PSS: ∀ n, P n → P (S (S n)))
: ∀ n, even n → P n.
Proof.
refine (fix f n Evn := _).
remember n. (* to see why the complaint is bogus *)
destruct_with_eqn Evn; [ exact P0 | ].
destruct_with_eqn o.
apply PSS.
apply f.
exact e.
``````

Note: the proof is `Admitted` because the `fix` definition is “ill-formed”:

``````Recursive definition of f is ill-formed.
In environment
P : nat → Prop
P0 : P 0
PSS : ∀ n : nat, P n → P (S (S n))
f : ∀ n : nat, even n → P n
n : nat
Evn : even n
n0 : nat
o : odd n0
Heqn0 : S n0 = n
Evn0 : even (S n0)
Heqe : Evn0 = even_S n0 o
n1 : nat
e : even n1
Heqn1 : S (S n1) = n
Evn1 : even (S (S n1))
o0 : odd (S n1)
Heqo0 : o0 = odd_S n1 e
Heqe0 : Evn1 = even_S (S n1) (odd_S n1 e)
Recursive call to f has principal argument equal to
"n1" instead of a subterm of "n".
Recursive definition is:
"λ (n : nat) (Evn : even n),
let n0 := n in
let Heqn0 : n0 = n := eq_refl in
let e : even n0 := Evn in
let Heqe : Evn = e := eq_refl in
match
e as e0 in (even n1)
return (n1 = n → ∀ Evn0 : even n1, Evn0 = e0 → P n1)
with
| even_O => λ (_ : 0 = n) (Evn0 : even 0) (_ : Evn0 = even_O), P0
| even_S n1 o =>
λ (Heqn1 : S n1 = n) (Evn0 : even (S n1)) (Heqe0 : Evn0 = even_S n1 o),
let o0 : odd n1 := o in
let Heqo0 : o = o0 := eq_refl in
match
o0 as o1 in (odd n2)
return
(S n2 = n
→ ∀ (Evn1 : even (S n2)) (o2 : odd n2),
o2 = o1 → Evn1 = even_S n2 o1 → P (S n2))
with
| odd_S n2 e0 =>
λ (_ : S (S n2) = n) (Evn1 : even (S (S n2)))
(o1 : odd (S n2)) (_ : o1 = odd_S n2 e0)
(_ : Evn1 = even_S (S n2) (odd_S n2 e0)),
PSS n2 (f n2 e0)
end Heqn1 Evn0 o Heqo0 Heqe0
end Heqn0 Evn Heqe".
``````

(Without `remember n` it is less obvious that the complaint is wrong, but with the equation `Heqn1` it is clear `n1` is a subterm of `n`!)

2 questions, then:

1. Is this induction principle reasonable? It seems like it must be, since it effectively mimics that of `ev`.
2. If it is, how can I convince Coq to accept the definition? I would not have been able to come up with the term given in that message on my own, let alone one not showing the failure in the tactic version. I had something like
``````   fix f n Evn := match Evn with
| even_O => P0
| even_S n' (odd_S n'' Hevn'') => PSS _ (f n'' Hevn'')
end.
``````

that lead to a similar complaint. In the tactic version, `destruct_with_eqn` was necessary to maintain certain connections.

Imports:

``````Require Import Coq.Unicode.Utf8.
Require Setoid.
Require Arith.
Require Import Even.
``````

`refine (fix f n Evn := _).`

This starts a fixpoint recursing on `n` but you want to recurse on `Evn`. Do `refine (fix f n Evn {struct Evn} := _)` or more idiomatically `fix f 2; intros n Evn` (2 because you recurse on the 2nd argument in the goal).

simpler proof by tactics:

``````
Definition even_ind_odd (P: nat → Prop)
(P0: P 0)
(PSS: ∀ n, P n → P (S (S n)))
: ∀ n, even n → P n.
Proof.
fix f 2;intros n Evn.
destruct Evn as [|_ [n Evn]].
- exact P0.
- apply PSS;exact (f n Evn).
Defined.
``````

The term this produces can be used with less annotations:

``````  fix f n Evn :=
match Evn with
| even_O => P0
| even_S _ oddk =>
match oddk with
| odd_S _ Evm => PSS _ (f _ Evm)
end
end
``````

Beautiful, thanks. I could have sworn I tried a version of that last `fix` expression, but probably not having the nested match got me screwed up.

Indeed it seems coq isn’t capable of handling

``````fix f n Evn :=
match Evn with
| even_O => P0
| even_S _ (odd_S _ Evm) => PSS _ (f _ Evm)
end
``````