## 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 | ].
rewrite (PeanoNat.Nat.mul_add_distr_l _ 1 n).
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.
Admitted.
```

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:

- Is this induction principle reasonable? It seems like it must be, since it effectively mimics that of
`ev`

. - 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.
```