证明乘法是可交换的

所以这是我一直从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）。

来源

2016-01-13 Sibi

IMO这看起来不错 - 我只有一个快速浏览，但如果你从第一原则出发，这或多或少是你必须做的（看看[Whitehead和Russel]（https://en.wikipedia.org/wiki/Principia_Mathematica）必须做的事情，直到他们能证明1 + 1 = 2;）） - 说了这些（并仔细看了一下） - 也许你不需要'mult_comm_helper'，如果你在'm'上进行归纳（你的'*'是如何定义的？我还没有咖啡，所以它可能是废话） – Carsten

@Carsten提供了一个很好的观点 - 有几种稍微不同的方式来定义乘法，并且确切地说，简单的和难的似乎对您选择的非常敏感。当然，让一件事情变得容易的事情几乎肯定会让事情变得更加困难。 – dfeuer

@Carsten即使我在'm'上进行了归纳，我仍然需要'mult_comm_helper'（只是在这种情况下，重写方向会不同）。 '*'是根据加法定义的。 :) – Sibi

如果您想写这更简洁（且无需使用战术，解算器，等...），你可以依靠的事实，大部分的需要引理是在表达方面你的主要目标定理为。

例如：

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.

NB：懒惰标准库的方式来做到这将是ring战术：

Require Import Arith. 

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

来源

2016-01-13 09:00:15

好吧，这可能不是你想要的，但是因为你（最初）在Haskell中加了标签，而且我恰好在Haskell 今天上做了这个工作，请写一些代码！

{-# 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}

来源

2016-01-13 04:49:12 dfeuer

从中删除'E.'时效果很好。谢谢你。 +1。尽管我对Coq解决方案更感兴趣。 :) – Sibi

@Sibi，我想。我和Haskell玩过很多次，伊德里斯也很棒，Agda也很少。我从来没有碰过Coq，所以你可能不得不等待别人。无论你如何做，我认为这些东西都是一个噱头。尽管如此，构建整数并不那么痛苦。 – dfeuer

证明乘法是可交换的

回答

相关问题