我试图证明以下来自软件基础>归纳法
的定理我正在使用 Coq 8.19.2
我的解决方案的开头如下：
Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
(* c *)
Proof.
(* FILL IN HERE *)
induction p as [|p' IHp'].
rewrite mult_0_r.
rewrite mult_0_r.
rewrite mult_0_r.
reflexivity.
Admitted.
我陷入了这个子目标
(n + m) * S p' = n * S p' + m * S p'(n + m) * S p'(n + m) * p + (n + m)' and as我想尽可能坚持手册，避免使用之前未介绍过的命令，例如，
auto到目前为止我已经证明了以下内容：
Theorem plus_O_n : forall n : nat, 0 + n = n.
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Theorem andb_commutative : forall b c, andb b c = andb c b.
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
Theorem eqb_refle : forall n : nat, (eqb n n) = true.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Theorem plus_id_exercise : forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Theorem mult_n_0_m_0 : forall p q : nat,
(p * 0) + (q * 0) = 0.
Theorem mult_n_1 : forall p : nat,
p * 1 = p.
Theorem plus_1_neq_0_firsttry : forall n : nat,
(n + 1) =? 0 = false.
Theorem plus_1_neq_0 : forall n : nat,
(n + 1) =? 0 = false.
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Theorem andb3_exchange :
forall b c d, andb (andb b c) d = andb (andb b d) c.
Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Theorem plus_1_neq_0' : forall n : nat,
(n + 1) =? 0 = false.
Theorem andb_commutative'' :
forall b c, andb b c = andb c b.
Theorem zero_nbeq_plus_1 : forall n : nat,
0 =? (n + 1) = false.
Theorem letter_comparison_Eq :
forall l, letter_comparison l l = Eq.
Theorem lower_letter_lowers: forall (l : letter),
letter_comparison (lower_letter l) l = Lt.
Theorem lower_letter_F_is_F:
lower_letter F = F.
Theorem add_0_r_firsttry : forall n:nat,
n + 0 = n.
Theorem add_0_r : forall n:nat,
n + 0 = n.
Theorem mul_0_r : forall n:nat,
n * 0 = 0.
Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Theorem add_comm : forall n m : nat,
n + m = m + n.
Theorem add_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Theorem add_assoc2 : forall n m p : nat,
n + (m + p) = n + m + p.
Theorem even_S : forall n : nat,
even (S n) = negb (even n).
Theorem mult_0_plus' : forall n m : nat,
(n + 0 + 0) * m = n * m.
Theorem plus_rearrange_firsttry : forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Theorem plus_rearrange : forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Theorem add_shuffle3 : forall n m p : nat,
n + (m + p) = m + (n + p).
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Theorem mul_comm : forall m n : nat,
m * n = n * m.
Theorem plus_leb_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Theorem leb_refl : forall n:nat,
(n <=? n) = true.
Theorem zero_neqb_S : forall n:nat,
0 =? (S n) = false.
Theorem andb_false_r : forall b : bool,
andb b false = false.
Theorem S_neqb_0 : forall n:nat,
(S n) =? 0 = false.
Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.
Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
Theorem negation_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = negb x) ->
forall (b : bool), f (f b) = b.
Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) ->
b = c.
Theorem all3_spec : forall b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
我会回顾这些并思考如何重写它或者改变我的归纳假设，尽管我相信在这种情况下是正确的。
如果打印 mult 的定义，您会发现它是由
npnNat.mul =
fix mul (n m : nat) {struct n} : nat :=
match n with
| 0 => 0
| S p => m + mul p m
end : nat -> nat -> nat Arguments Nat.mul (n m)%nat_scope