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.