Beweisen, dass Multiplikation ist kommutativ

Also dies ist eine der Übung, die ich gearbeitet habe von Software Foundations, in dem ich beweisen muss, dass die Multiplikation ist kommutativ. Und das ist meine Lösung:Beweisen, dass Multiplikation ist kommutativ

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.

Jetzt ist meiner Meinung nach dieser Beweis recht sperrig. Gibt es eine prägnantere Möglichkeit, dies zu tun, ohne eine Bibliothek zu benutzen? (Beachten Sie, dass Sie zur Verwendung der Case-Taktik einen vordefinierten Code benötigen. Ein eigenständiger Arbeitscode ist in der folgenden Liste enthalten: https://gist.github.com/psibi/1c80d61ca574ae62c23e).

Quelle

2016-01-13 Sibi

IMO das sieht gut aus - ich hatte nur einen kurzen Blick aber Wenn Sie von den ersten Prinzipien ausgehen, ist dies mehr oder weniger das, was Sie tun müssten (schauen Sie, was [Whitehead und Russel] (https://en.wikipedia.org/wiki/Principia_Mathematica) tun mussten, bis sie dies nachweisen konnten 1 + 1 = 2;)) - nachdem du das gesagt hast (und genauer hinsehen) - brauchst du vielleicht nicht 'mult_comm_helper' wenn du zu deiner Induktion auf' m' stehst (wie ist dein '*' definiert?) - aber Ich hatte noch keinen Kaffee, also ist es wahrscheinlich Schwachsinn) – Carsten

@Carsten macht einen guten Punkt - es gibt mehrere leicht unterschiedliche Möglichkeiten, die Multiplikation zu definieren, und genau das, was leicht ist und was schwer ist, scheint ziemlich empfindlich zu sein, für das Sie sich entscheiden. Natürlich macht das, was eines leicht macht, fast sicher ein anderes schwer. – dfeuer

@Carsten Selbst wenn ich Induktion auf 'm' hätte, würde ich immer noch' mult_comm_helper' brauchen (nur die Rewrite-Richtung würde in diesem Fall anders sein). Das '*' ist in Addition definiert. :) – Sibi

Wenn Sie möchten, dass diese prägnanter schreiben (und ohne den Einsatz von Taktiken, Löser, etc ...), können Sie sich darauf verlassen, dass die meisten Ihrer benötigten Lemmata ausdrückbar sind in Bezug auf die Ihre wichtigsten Zielsätze.

Zum Beispiel:

n * 0 = 0 folgt aus mult_comm.
n + 0 = n folgt aus plus_comm.
S (n + m) = n + S m folgt aus plus_comm (durch zwei überschreiben und Reduktion).

mit solchen Dingen zu berücksichtigen, ist mult_comm relativ bequem beweisbar mit nur plus_assoc und plus_comm als Lemmata:

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: der faule Standardbibliothek Weg, dies zu tun, wäre die ring Taktik:

Require Import Arith. 

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

Quelle

2016-01-13 09:00:15

Nun, das ist wahrscheinlich nicht das, was Sie wollten, aber seit Sie (ursprünglich) getaggt in Haskell, und ich gerade passiert, um herauszufinden, wie man dies in Haskell heute, haben Sie etwas Code!

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

Einige zusätzliche free stuff!

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}

Quelle

2016-01-13 04:49:12 dfeuer

Funktioniert gut, wenn "E." davon entfernt wird. Danke dafür. +1. Obwohl ich mehr an einer Coq-Lösung interessiert bin. :) – Sibi

@Sibi, dachte ich. Ich habe viel mit Haskell gespielt und Idris ein gutes Stück und Agda eine sehr kleine Summe. Ich habe Coq noch nie berührt, also musst du wahrscheinlich auf jemand anderen warten. Ich denke, einige dieser Sachen sind ein Trick, egal wie du es machst. Es ist nicht annähernd so schmerzhaft wie die ganzen Zahlen zu konstruieren. – dfeuer

Beweisen, dass Multiplikation ist kommutativ

Antwort

Verwandte Themen