如何證明如果方塊相等，那麼操作數也是相等的？

Question

我完成這個引理的證明一個問題：

Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 

任何暗示將是非常有益的。

我開始喜歡證明了這一點：

Require Import Arith Omega Nat. 
Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 
Proof. 
intros. 
destruct (Nat.eq_dec m n). 
trivial. 
induction n. 
induction m. 
auto. 
simpl in H;congruence. 

Answer 1

一個提示：把你的假設兩側的平方根，那麼它馬上得出的結論。對於平方根函數，使用Arith模塊中的Nat.sqrt。

首先溶液：

Require Import Coq.Arith.Arith. 

Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 
Proof. 
    intros m n H. apply (f_equal Nat.sqrt) in H. 
    now repeat rewrite Nat.sqrt_square in H. 
Qed. 

第二溶液：

該引理還可以使用本nia戰術，爲整數非線性算術一個不完整的證明過程加以證明：

Require Import Psatz. 

Lemma l1 m n : m * m = n * n -> m = n. 
Proof. nia. Qed. 

解決方案三：

讓我們用一對夫婦倍的標準Nat.square_le_simpl_nonneg引理：

forall n m : nat, 0 <= m -> n * n <= m * m -> n <= m 

這裏，我們去：

Require Import Coq.Arith.Arith. 

Lemma l1 (m n : nat) : 
    m * m = n * n -> m = n. 
Proof with (auto with arith). 
    intros H. 
    pose proof (Nat.eq_le_incl _ _ H) as Hle. 
    pose proof (Nat.eq_le_incl _ _ (eq_sym H)) as Hge. 
    apply Nat.square_le_simpl_nonneg in Hle... 
    apply Nat.square_le_simpl_nonneg in Hge... 
Qed. 

方案四：

這裏是一個經典基於以下等式

m * m - n * n = (m + n) * (m - n) 

首先，我們需要一個輔助引理，證明上述等式（奇怪的是，它似乎是標準庫缺少這個引理）：

Require Import Coq.Arith.Arith. 

(* can be proved using `nia` tactic *) 
Lemma sqr_diff (m n : nat) : 
    m * m - n * n = (m + n) * (m - n). 
Proof with (auto with arith). 
    destruct (Nat.lt_trichotomy m n) as [H | [H | H]]. 
    - pose proof H as H'. (* copy hypothesis *) 
    apply Nat.square_lt_mono_nonneg in H... 
    repeat match goal with 
     h : _ < _ |- _ => apply Nat.lt_le_incl, Nat.sub_0_le in h 
    end. 
    rewrite H, H'... 
    - now rewrite H, !Nat.sub_diag. 
    - rewrite Nat.mul_add_distr_r, !Nat.mul_sub_distr_l. 
    rewrite Nat.add_sub_assoc... 
    replace (n * m) with (m * n) by apply Nat.mul_comm. 
    rewrite Nat.sub_add... 
Qed. 

現在我們可以證明主要引理：

Lemma l1 (m n : nat) : 
    m * m = n * n -> m = n. 
Proof. 
    intros H. 
    pose proof (Nat.eq_le_incl _ _ H) as Hle; 
    pose proof (Nat.eq_le_incl _ _ (eq_sym H)) as Hge; clear H. 
    rewrite <- Nat.sub_0_le in *. 
    rewrite sqr_diff in *. 
    destruct (mult_is_O _ _ Hle) as [H | H]. 
    now destruct (plus_is_O _ _ H); subst. 
    destruct (mult_is_O _ _ Hge) as [H' | H']. 
    now destruct (plus_is_O _ _ H'); subst. 
    rewrite Nat.sub_0_le in *. 
    apply Nat.le_antisymm; assumption. 
Qed.