如何证明如果平方相等，则操作数也相等？

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.

如何证明如果平方相等，则操作数也相等？

How to show that if squares are equal, then the operands are equal as well?

coq