89 lines
1.7 KiB
Coq
89 lines
1.7 KiB
Coq
(*
|
|
ring tactic needs ArithRing. Arith exports ArithRing as well.
|
|
|
|
https://coq.inria.fr/refman/addendum/ring.html#coq:tacn.ring_simplify
|
|
*)
|
|
Require Import Arith.
|
|
|
|
Fixpoint sumn1 (n:nat) : nat :=
|
|
match n with
|
|
| O => 0
|
|
| S n' => n + (sumn1 n')
|
|
end.
|
|
|
|
Theorem th_sumn1: forall n:nat,
|
|
2 * (sumn1 n) = n * (n+1).
|
|
Proof.
|
|
induction n.
|
|
- reflexivity.
|
|
- unfold sumn1.
|
|
fold sumn1.
|
|
Search (_ * (_+_)).
|
|
rewrite PeanoNat.Nat.mul_add_distr_l.
|
|
rewrite IHn.
|
|
SearchRewrite (_ * S _).
|
|
rewrite <- mult_n_Sm.
|
|
rewrite PeanoNat.Nat.mul_add_distr_l.
|
|
rewrite PeanoNat.Nat.mul_add_distr_l.
|
|
Search (_ * 1).
|
|
rewrite PeanoNat.Nat.mul_1_r.
|
|
rewrite PeanoNat.Nat.mul_1_r.
|
|
SearchRewrite (S _ * _).
|
|
rewrite PeanoNat.Nat.mul_succ_l.
|
|
rewrite PeanoNat.Nat.mul_succ_l.
|
|
rewrite PeanoNat.Nat.mul_succ_l.
|
|
simpl.
|
|
SearchRewrite (_ * S _).
|
|
rewrite <- mult_n_Sm.
|
|
Require Import Arith.
|
|
ring.
|
|
Qed.
|
|
|
|
|
|
(***************************************************)
|
|
|
|
Fixpoint sumn2 (n:nat) : nat :=
|
|
match n with
|
|
| O => 0
|
|
| S n' => n*n + (sumn2 n')
|
|
end.
|
|
|
|
Theorem th_sumn2: forall n:nat,
|
|
6 * sumn2 n = n*(n+1)*(2*n+1).
|
|
Proof.
|
|
intros n.
|
|
induction n.
|
|
- reflexivity.
|
|
- unfold sumn2.
|
|
fold sumn2.
|
|
Search (_ * (_+_)).
|
|
rewrite PeanoNat.Nat.mul_add_distr_l.
|
|
rewrite IHn.
|
|
ring.
|
|
Show Proof.
|
|
Qed.
|
|
|
|
|
|
(***************************************************)
|
|
|
|
|
|
Fixpoint sumn3 (n:nat) : nat :=
|
|
match n with
|
|
| O => 0
|
|
| S n' => n*n*n + (sumn3 n')
|
|
end.
|
|
|
|
Theorem th_sumn3: forall n:nat,
|
|
4 * sumn3 n = (n*(n+1)) * (n*(n+1)).
|
|
Proof.
|
|
intros n.
|
|
induction n.
|
|
- reflexivity.
|
|
- unfold sumn3.
|
|
fold sumn3.
|
|
SearchRewrite (_ * (_+_)).
|
|
rewrite Nat.mul_add_distr_l.
|
|
rewrite IHn.
|
|
ring.
|
|
Qed.
|