证明乘法是可交换的

Question

所以这是我从 Software Foundations 开始做的练习之一，我必须在其中证明乘法是可交换的。这是我的解决方案：

Theorem brack_help : forall n m p: nat,
  n + (m + p) = n + m + p.
Proof.
  intros n m p.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma plus_help: forall n m: nat,
  S (n + m) = n + S m.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    reflexivity.
Qed.

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n.
  induction n as [|n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    rewrite <- plus_n_O.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    rewrite -> plus_help.
    reflexivity.
Qed.

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.  
  intros n m p.
  rewrite -> brack_help.
  assert (H: n + m = m + n).
    Case "Proof of assertion".
    rewrite -> plus_comm.
    reflexivity.
  rewrite -> H.
  rewrite <- brack_help.
  reflexivity.
Qed.

Lemma mult_help : forall m n : nat,
  m + (m * n) = m * (S n).
Proof.
  intros m n.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite <- IHm'.
    rewrite -> plus_swap.
    reflexivity.
Qed.    

Lemma mult_identity : forall m : nat,
 m * 1 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Lemma plus_0_r : forall m : nat,
 m + 0 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Theorem mult_comm_helper : forall m n : nat,
  m * S n = m + m * n.
Proof.
  intros m n.
  simpl.
  induction n as [| n'].
  Case "n = 0".
    assert (H: m * 0 = 0).
    rewrite -> mult_0_r.
    reflexivity.
    rewrite -> H.
    rewrite -> mult_identity.
    assert (H2: m + 0 = m).
    rewrite -> plus_0_r.
    reflexivity.
    rewrite -> H2.
    reflexivity.
  Case "n = S n'".
    rewrite -> IHn'.
    assert (H3: m + m * n' = m * S n').
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H3.
    assert (H4: m + m * S n' = m * S (S n')).
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H4.
    reflexivity.
Qed.

Theorem mult_comm : forall m n : nat,
 m * n = n * m.
Proof.
  intros m n.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    rewrite -> mult_0_r.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite <- IHn'.
    rewrite -> mult_comm_helper.
    reflexivity.
Qed.

现在在我看来，这个证明相当庞大。有没有不使用任何库的更简洁的方法？（请注意，要使用 Case 策略，您需要一些预定义代码。自包含的工作代码在以下要点中：https://gist.github.com/psibi/1c80d61ca574ae62c23e）。

Answer 1

好吧，这可能不是您想要的，但是由于您（最初）在 Haskell 中进行了标记，而我恰好在 Haskell [=16= 中弄清楚了如何执行此操作]今天，有一些代码！

{-# LANGUAGE TypeFamilies, GADTs, TypeOperators,
             ScopedTypeVariables, UndecidableInstances,
             PolyKinds, DataKinds #-}

import Data.Type.Equality
import Data.Proxy

data Nat = Z | S Nat
data SNat :: Nat -> * where
  Zy :: SNat 'Z
  Sy :: SNat n -> SNat ('S n)

infixl 6 :+
type family (:+) (m :: Nat) (n :: Nat) :: Nat where
  'Z :+ n = n
  'S m :+ n = 'S (m :+ n)

infixl 7 :*
type family (:*) (m :: Nat) (n :: Nat) :: Nat where
  'Z :* n = 'Z
  ('S m) :* n = n :+ (m :* n)

add :: SNat m -> SNat n -> SNat (m :+ n)
add Zy n = n
add (Sy m) n = Sy (add m n)

mul :: SNat m -> SNat n -> SNat (m :* n)
mul Zy _n = Zy
mul (Sy m) n = add n (mul m n)

addP :: proxy1 m -> proxy2 n -> Proxy (m :+ n)
addP _ _ = Proxy

mulP :: proxy1 m -> proxy2 n -> Proxy (m :* n)
mulP _ _ = Proxy

addAssoc :: SNat m -> proxy1 n -> proxy2 o ->
            m :+ (n :+ o) :~: (m :+ n) :+ o
addAssoc Zy _ _ = Refl
addAssoc (Sy m) n o = case addAssoc m n o of Refl -> Refl

zeroAddRightUnit :: SNat m -> m :+ 'Z :~: m
zeroAddRightUnit Zy = Refl
zeroAddRightUnit (Sy n) =
  case zeroAddRightUnit n of Refl -> Refl

plusSuccRightSucc :: SNat m -> proxy n ->
                     'S (m :+ n) :~: (m :+ 'S n)
plusSuccRightSucc Zy _ = Refl
plusSuccRightSucc (Sy m) n =
  case plusSuccRightSucc m n of Refl -> Refl

addComm :: SNat m -> SNat n ->
           m :+ n :~: n :+ m
addComm Zy n = sym $ zeroAddRightUnit n
addComm (Sy m) n =
  case addComm m n of
    Refl -> plusSuccRightSucc n m

mulComm :: SNat m -> SNat n ->
           m :* n :~: n :* m
mulComm Zy Zy = Refl
mulComm (Sy pm) Zy =
  case mulComm pm Zy of Refl -> Refl
mulComm Zy (Sy pn) = 
  case mulComm Zy pn of Refl -> Refl
mulComm (Sy m) (Sy n) =
  case mulComm m (Sy n) of {Refl ->
  case mulComm n (Sy m) of {Refl ->
  case addAssoc n m (mulP n m) of {Refl ->
  case addAssoc m n (mulP m n) of {Refl ->
  case addComm m n of {Refl ->
  case mulComm m n of Refl -> Refl}}}}}

一些额外的免费内容！

distrR :: forall m n o proxy . SNat m -> proxy n -> SNat o ->
          (m :+ n) :* o :~: m :* o :+ n :* o
distrR Zy _ _ = Refl
distrR (Sy pm) n o =
  case distrR pm n o of {Refl ->
  case addAssoc o (mulP pm o) (mulP n o) of
    Refl -> Refl}

distrL :: SNat m -> SNat n -> SNat o ->
          m :* (n :+ o) :~: m :* n :+ m :* o
distrL m n o =
  case mulComm m (add n o) of {Refl ->
  case distrR n o m of {Refl ->
  case mulComm n m of {Refl ->
  case mulComm o m of Refl -> Refl}}}

mulAssoc :: SNat m -> SNat n -> SNat o ->
            m :* (n :* o) :~: (m :* n) :* o
mulAssoc Zy _ _ = Refl
mulAssoc (Sy pm) n o = case mulAssoc pm n o of {Refl ->
                       case distrR n (mulP pm n) o of Refl -> Refl}

Answer 2

如果你想写得更简洁（并且不使用策略、求解器等...），你可以依赖这样一个事实，即你需要的大部分引理都可以用你的主要内容来表达目标定理。

例如：

n * 0 = 0 来自 mult_comm。
n + 0 = n 遵循 plus_comm.
S (n + m) = n + S m 来自 plus_comm（通过两次重写和缩减）。

考虑到这些因素，mult_comm 仅用 plus_assoc 和 plus_comm 作为引理就可以相对轻松地证明：

Theorem plus_assoc : forall a b c, a + (b + c) = a + b + c.
Proof.
  intros.
  induction a.
    (* Case Z *)   reflexivity.
    (* Case S a *) simpl. rewrite IHa. reflexivity.
Qed.

Theorem plus_comm : forall a b, a + b = b + a.
Proof.
  induction a.
    (* Case Z *)
      induction b.
        (* Case Z *)   reflexivity.
        (* Case S b *) simpl. rewrite <- IHb. reflexivity.
    (* Case a = S a *)
      induction b.
        (* Case Z  *)
          simpl. rewrite (IHa 0). reflexivity.
        (* Case S b *)
          simpl. rewrite <- IHb.
          simpl. rewrite (IHa (S b)).
          simpl. rewrite (IHa b).
          reflexivity.
Qed.

Theorem mul_comm : forall a b, a * b = b * a.
Proof.
  induction a.
  (* Case Z *)
    induction b.
      (* Case Z *)   reflexivity.
      (* Case S b *) simpl. rewrite <- IHb. reflexivity.
  (* Case S a *)
    induction b.
      (* Case Z *)
        simpl. rewrite (IHa 0). reflexivity.
      (* Case S b *)
        simpl. rewrite <- IHb.
        rewrite (IHa (S b)).
        simpl. rewrite (IHa b).
        rewrite (plus_assoc b a (b * a)).
        rewrite (plus_assoc a b (b * a)).
        rewrite (plus_comm a b).
        reflexivity.
Qed.

注意：懒惰的标准库方法是 ring 策略：

Require Import Arith.

Theorem plus_comm2 : forall a b, a * b = b * a.
Proof. intros. ring. Qed.

Answer 3

你也可以这样解决:

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros.
  induction m.
  - rewrite <- mult_n_O. reflexivity.
  - rewrite <- mult_n_Sm.
    rewrite <- plus_1_l.
    simpl.
    rewrite <- IHm.
    rewrite -> plus_comm.
    reflexivity.
Qed.

诀窍是将 S m * n 重写为 (1 + m) * n（使用 plus_1_l）

然后将简化为 n + m * n

供参考：

mult_n_O : forall n : nat, 0 = n * 0
mult_n_Sm : forall n m : nat, n * m + n = n * S m
plus_1_l : forall n : nat, 1 + n = S n
plus_comm : forall n m : nat, n + m = m + n

Answer 4

这是我针对此问题提出的解决方案，使用 assert 创建辅助定理，我相信这就是本书在该特定部分讨论的主题。

Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros m n.
  induction m as [| m' IHm'].
  - rewrite mul_0_r.
    reflexivity.
  - simpl.
    rewrite -> IHm'.
    assert (H: forall a b : nat, a * (1 + b) = a + a * b).
    {
      intros a b.
      induction a as [| a' IHa'].
      - reflexivity.
      - rewrite <- mult_n_Sm.
        rewrite -> add_comm.
        reflexivity.
    }
    rewrite -> H.
    reflexivity.
Qed.

证明乘法是可交换的

Proving that Multiplication is commutative

coq