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
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
change (B (2 * 5) p).:
apply B2_Even; now exists 5. exact (B2 5 p).
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
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
apply B2_ev; repeat constructor..
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.
apply B2_even; repeat constructor. a proof of
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".
remember n it is less obvious that the complaint is wrong, but with the equation
Heqn1 it is clear
n1 is a subterm of
2 questions, then:
- Is this induction principle reasonable? It seems like it must be, since it effectively mimics that of
- 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.
Require Import Coq.Unicode.Utf8. Require Setoid. Require Arith. Require Import Even.