105 lines
2.2 KiB
Coq
105 lines
2.2 KiB
Coq
Require Import Arith.
|
|
|
|
(* Theorem about addition (Plus) *)
|
|
Theorem OddOddEvenP: forall n m:nat,
|
|
Nat.Odd n -> Nat.Odd m -> Nat.Even (n+m).
|
|
Proof.
|
|
intros n m Hp Hq.
|
|
destruct Hp as [p Hp].
|
|
destruct Hq as [q Hq].
|
|
unfold Nat.Even.
|
|
exists (p+q+1).
|
|
rewrite Nat.mul_add_distr_l.
|
|
rewrite Nat.mul_add_distr_l.
|
|
rewrite Nat.mul_1_r.
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
ring.
|
|
Qed.
|
|
|
|
Theorem OddEvenOddP: forall n m:nat,
|
|
Nat.Odd n -> Nat.Even m -> Nat.Odd (n+m).
|
|
Proof.
|
|
intros n m [p Hp] [q Hq].
|
|
unfold Nat.Odd.
|
|
exists (p+q).
|
|
rewrite Nat.mul_add_distr_l.
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
ring.
|
|
Qed.
|
|
|
|
Theorem EvenEvenEvenP: forall n m:nat,
|
|
Nat.Even n -> Nat.Even m -> Nat.Even (n+m).
|
|
Proof.
|
|
intros n m [p Hp] [q Hq].
|
|
unfold Nat.Even.
|
|
exists (p+q).
|
|
rewrite Nat.mul_add_distr_l.
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
ring.
|
|
Qed.
|
|
|
|
|
|
(* Theorem about subtraction (Minus) *)
|
|
Theorem OddOddEvenM: forall n m:nat,
|
|
Nat.Odd n -> Nat.Odd m -> Nat.Even (n-m).
|
|
Proof.
|
|
intros n m [p Hp] [q Hq].
|
|
unfold Nat.Even.
|
|
exists (p-q).
|
|
rewrite Nat.mul_sub_distr_l.
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
(* doing [lia] here would solve this goal *)
|
|
simpl.
|
|
rewrite Nat.add_0_r.
|
|
rewrite Nat.add_0_r.
|
|
rewrite (Nat.add_comm (q+q) 1).
|
|
replace (p + p + 1) with (1 + p + p) by ring.
|
|
Print Nat.sub.
|
|
simpl.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem EvenEvenEvenM: forall n m:nat,
|
|
Nat.Even n -> Nat.Even m -> Nat.Even (n-m).
|
|
Proof.
|
|
intros n m [p Hp] [q Hq].
|
|
unfold Nat.Even.
|
|
exists (p-q).
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
rewrite Nat.mul_sub_distr_l.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Require Import Lia.
|
|
(* 1-2 is 0 but is even. So m<=n constraint has to be there *)
|
|
Theorem OddEvenOddM: forall n m:nat,
|
|
Nat.Odd n -> Nat.Even m -> m<=n -> Nat.Odd (n-m).
|
|
Proof.
|
|
intros n m [p Hp] [q Hq] H.
|
|
unfold Nat.Odd.
|
|
exists (p-q).
|
|
rewrite Hp.
|
|
rewrite Hq.
|
|
rewrite Nat.mul_sub_distr_l.
|
|
replace (2*p+1) with (1+2*p) by ring.
|
|
rewrite (Nat.add_comm (2*p-2*q) 1).
|
|
SearchRewrite (_ + (_ - _)).
|
|
rewrite Nat.add_sub_assoc.
|
|
- reflexivity.
|
|
- lia.
|
|
|
|
Restart.
|
|
(* Another way *)
|
|
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/lia.20shows.20error.2E *)
|
|
(* Thanks to Pierre Castéran *)
|
|
intros n m [p Hp] [q Hq] H.
|
|
subst.
|
|
exists (p-q).
|
|
lia.
|
|
Qed.
|