Induction over a type containing pairs
This Coq-club thread discusses how to do induction over types such as
Inductive foo : nat * nat -> Prop :=
| foo1 : forall i j k, i = j + k -> foo (i, j)
| foo2 : forall i j k, foo (i, j + k) -> foo (i, j).
Naively applying induction will forget the structure of foo's argument.
Doing induction on a term that does not contain only variables (there is a pair and a sum in (n, m+p)
). The first way to go is to reshape your hypothesis on which you do induction so it contains only variables. Example:
Require Import Omega.
Inductive foo : nat * nat -> Prop :=
| foo1 : forall i j k, i = j + k -> foo (i, j)
| foo2 : forall i j k, foo (i, j + k) -> foo (i, j).
Lemma bar : forall n m p, foo (n, m + p) -> m <= n.
intros n m p H.
assert (Haux: forall u, foo u -> forall p, u = (n, m + p) -> m <= n).
intros u Hu; elim Hu; intros i j k.
intros Eq1 p1 Eq2; injection Eq2; intros; omega.
intros _ Hrec p1 Eq2; apply Hrec with (p1 + k).
apply f_equal2 with (f := @pair nat nat); injection Eq2; intros; omega.
apply Haux with (1 := H) (p := p); trivial.
Qed.
The second way to go is to reshape your conclusion so it explicitly exhibits the dependancy with the term that is not a variable in your case (n, m + p)
. Example:
Lemma bar1 : forall n m p, foo (n, m + p) -> m <= n.
intros n m p H.
replace m with ((m + p) - p); try omega.
change ((fun x => (snd x - p <= fst x)) (n, m + p)).
elim H; simpl; intros; omega.
Qed.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.