Vfrdtyky

I've been learning about Coq's tactics and familiarizing myself with the system by reproving basic facts about natural numbers.

I've been trying to avoid using the theorems that are already proven in the library, and reproving things like the associativity of multiplication, etc.

However, I've been stymied in a couple of cases, where I have a property for n m:nat that I want to prove, but when I try to do induction on both n and m, the structure of the inductive hypothesises is useless for trying to prove the property.

I proved n = m -> o * n = o * m very easily:

Theorem times_alg_left : forall n m o:nat, n = m -> o * n = o * m.

intros n m o H.

rewrite H; reflexivity.

Defined.

But trying to prove S o * n = S o * m -> n = m completely flumoxed me. I decided, after considerable struggles, to try to prove 2 * n = 2 * m -> n = m, but that was no easier.

I end up with situations like this:

Theorem m2_eq : forall n m:nat, 2 * n = 2 * m -> n = m.

intros n m H.

induction n.

destruct m.

reflexivity.

discriminate.

induction m.

discriminate.



1 subgoal

n, m : nat

H : 2 * S n = 2 * S m

IHn : 2 * n = 2 * S m -> n = S m

IHm : 2 * S n = 2 * m -> (2 * n = 2 * m -> n = m) -> S n = m

______________________________________(1/1)

S n = S m

I've got 2 * S n = 2 * S m, but my inductive premises are talking about 2 * n = 2 * S m and 2 * S n = 2 * m.

I can't make anything happen from this situation.

Similarly, I started trying to proof things about Nat.sub and less than or equal to get around this limitation, but I ran into the same situation.

Theorem sub0_imp_le : forall n m:nat, n - m = 0 -> n <= m.

intros n m H.

induction n; induction m.

apply le_n.

apply le_0.

rewrite sub0 in H.

discriminate.



1 subgoal

n, m : nat

H : S n - S m = 0

IHn : n - S m = 0 -> n <= S m

IHm : S n - m = 0 -> (n - m = 0 -> n <= m) -> S n <= m

______________________________________(1/1)

S n <= S m

But I'm in the same pickle where my inductive premises are worthless.

How do I structure my tactics to solve these type of theorems, with 2 nat variables, and some kind of equality or subtraction situation going on?

You need to do induct on one number while generalizing the other, using the generalize dependent tactic, for instance. This is explained in detail in the Software Foundations book.

Using the Software Foundations book Arthur mentioned, I found the exmaple in question. I need to not introduce m before doing induction on n. I needed to do induction on n first instead, then introduce m.

https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html#lab143

Theorem times_alg_rem_left : forall n o m:nat, (S o) * n = (S o) * m -> n = m.

intros n o.

induction n.

simpl.

intros m eq.

destruct m.

reflexivity.

rewrite (timesz o) in eq.

simpl in eq.

discriminate.

intros m eq.

destruct m.

rewrite (timesz (S o)) in eq.

inversion eq.

apply f_equal.

apply IHn.

rewrite (times_nSm (S o) n) in eq.

rewrite (times_nSm (S o) m) in eq.

apply plus_alg_rem_right in eq.

assumption.

Defined.