Доказване, че умножението е комутативно

Така че това е едно от упражненията, които работя от Софтуерни основи, в който трябва да докажа, че умножението е комутативно. И това е моето решение:

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).


coq
person Sibi    schedule 13.01.2016    source източник
comment
@Carsten прави добра гледна точка — има няколко малко по-различни начина за дефиниране на умножението и точно кое е лесно и кое е трудно изглежда доста чувствително към това, което избирате. Разбира се, това, което прави едно нещо лесно, почти сигурно ще направи друго трудно.   -  person dfeuer    schedule 13.01.2016
comment
@Carsten Дори и да направих индукция на m, пак ще имам нужда от mult_comm_helper (Само посоката на пренаписване ще бъде различна в доказателството в този случай). * се определя от гледна точка на добавяне. :)   -  person Sibi    schedule 13.01.2016
comment
@Sibi - както казах, вероятно не е вярно (току-що си спомних нещо подобно, където изборът имаше голямо значение) - че * се дефинира по отношение на добавянето е очевидно - въпросът е дали го дефинирате с n * S m = ... или S n * m = ... - но няма значение вероятно няма да ви помогне изобщо - да се надяваме, че някой, който също е правил упражненията, в крайна сметка ще дойде и ще ни просветли (може би ще погледна тази вечер)   -  person Random Dev    schedule 13.01.2016
comment
Вашето решение е същото като в Стандартна библиотека на Agda.   -  person user3237465    schedule 13.01.2016
comment
@user3237465 Виждам само комутативно свойство на добавяне, доказано там. Доказано ли е за умножение там?   -  person Sibi    schedule 13.01.2016
comment
@Sibi Тук е.   -  person András Kovács    schedule 13.01.2016

Отговори (3)


arrow_upward
14
arrow_downward

Ако искате да напишете това по-сбито (и без използването на тактики, решаващи средства и т.н...), можете да разчитате на факта, че повечето от необходимите ви леми са изразими по отношение на вашите основни теореми за целта.

Например:

  • 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.
person András Kovács    schedule 13.01.2016

arrow_upward
9
arrow_downward

Е, това вероятно не е това, което искахте, но тъй като вие (първоначално) отбелязахте в 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}
person dfeuer    schedule 13.01.2016
comment
Работи добре при премахване на E. от това. Благодаря за това. +1. Въпреки че повече се интересувам от решение на Coq. :) - person Sibi; 13.01.2016
comment
@Сиби, разбрах. Играл съм с Haskell много, с Idris прилична част и Agda много малко. Дори не съм пипал Coq, така че вероятно ще трябва да изчакате някой друг. Мисля, че някои от тези неща са лозунг, без значение как го правите. Въпреки това не е толкова болезнено, колкото конструирането на цели числа. - person dfeuer; 13.01.2016

arrow_upward
1
arrow_downward

Можете също да го решите така:

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
person Matthieu Jacquot    schedule 20.06.2020