coq - How can I prove the injectivity of plus? - Stack Overflow

admin管理员组

文章数量:1333428

Here's what I'm trying to prove: Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

I've tried Coq's built-in tactices, but they don't work. Is there an easy way to prove this? Here's what I've done:

Theorem plus_injective : forall n m, n + n = m + m -> n = m.
Proof. intros n m H.
       induction n.
       - simpl in H. induction m.
         + reflexivity.
         + rewrite H. discriminate.
       - simpl in H. induction m.
         + simpl in H. rewrite <- H. discriminate.
         + rewrite <- H in IHn. rewrite IHn in IHm.
            
Qed.

and its got stuck with one subgoal

Here's what I'm trying to prove: Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

I've tried Coq's built-in tactices, but they don't work. Is there an easy way to prove this? Here's what I've done:

Theorem plus_injective : forall n m, n + n = m + m -> n = m.
Proof. intros n m H.
       induction n.
       - simpl in H. induction m.
         + reflexivity.
         + rewrite H. discriminate.
       - simpl in H. induction m.
         + simpl in H. rewrite <- H. discriminate.
         + rewrite <- H in IHn. rewrite IHn in IHm.
            
Qed.

and its got stuck with one subgoal

• coq
• coq-tactic

Share Improve this question Follow edited Nov 21, 2024 at 6:34 DarkBee 15.6k88 gold badges7272 silver badges117117 bronze badges asked Nov 21, 2024 at 6:33 wulalalawulalala 1111 silver badge11 bronze badge 2

• 1 2n = 2m -> n = m is not the injectivity of plus but that of twice ! – Dominique Larchey-Wendling Commented Nov 21, 2024 at 22:47
• 1 You need to show (S n) + (S n) = S (S (n+n)) to proceed by induction as you want. In turn, this means you need n+S m = S (n+m) which is part of the StdLib used to show that + is eg commutative. – Dominique Larchey-Wendling Commented Nov 21, 2024 at 22:50

Add a comment  | 

2 Answers 2

Sorted by: Reset to default 3

You can not use your induction hypothesis because H simplifies to n + n = m + m while IHn expects n + n = S m + S m. In other words, the argument m you want to feed the induction hypothesis changed, which is a symptom that you need to generalize over m (with revert m) before doing induction n (actually you can just not introduce m and H before doing induction n). Besides, you can also destruct m instead of doing an induction on it, the induction hypothesis IHm is useless.

How would you prove it on paper? I'd say probably not by induction. Maybe you already have the inverse of +n?

Note that there is also the lia tactic for solving linear integer arithmetic problems. You just need to import it with the following command.

From Coq Require Import Lia.

本文标签： coqHow can I prove the injectivity of plusStack Overflow