所以这是我一直在做的练习之一 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 )。
最佳答案
如果你想写得更简洁(并且不使用策略、求解器等),你可以依赖这样一个事实,即你需要的大多数引理都可以用你的主引理表达
目标定理。
例如:
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.
关于coq - 证明乘法是可交换的,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34758527/