-
Notifications
You must be signed in to change notification settings - Fork 0
/
A3_arith.v
101 lines (79 loc) · 3.2 KB
/
A3_arith.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
(*
A3. Arithmetic Properties
=========================
*)
From graph_pebbling Require Import A1_misc A2_lift.
Infix ".≤" := (liftR le) (at level 60).
Infix ".+" := (lift2 Nat.add) (at level 50).
Infix ".-" := (lift2 Nat.sub) (at level 50).
Infix ".*" := (lift2 Nat.mul) (at level 50).
Notation "(+)" := Nat.add (only parsing).
Notation "(-)" := Nat.sub (only parsing).
Notation "(.+)" := (lift2 Nat.add) (only parsing).
Notation "(.-)" := (lift2 Nat.sub) (only parsing).
Notation "(.*)" := (lift2 Nat.mul) (only parsing).
Notation min := Nat.min.
Notation max := Nat.max.
Notation lift_min := (lift2 min).
Notation lift_max := (lift2 max).
Notation gcd := Nat.gcd.
Notation "m ∣ n" := ((m | n)) (at level 50).
Ltac inst_lift_le x :=
repeat match goal with
| H : _ .≤ _ |- _ => inst H x; clear H
end.
Ltac ext_lia :=
let x := fresh "x" in
extensionality x;
inst_lift_le x; cbn; lia.
(* Nat.sub with the subtrahend first. *)
Definition subtract (n k : nat) := k - n.
Global Arguments subtract _ _ /.
Global Arguments min _ _ : simpl nomatch.
Section Properties.
Ltac see H := repeat intro; cbn; apply H.
Global Instance : IdemP (=) Nat.max := Nat.max_id.
Global Instance : IdemP (=) Nat.min := Nat.min_id.
Global Instance : LeftId (=) 0 Nat.max := Nat.max_0_l.
Global Instance : RightId (=) 0 Nat.max := Nat.max_0_r.
Global Instance : LeftId (=) 0 Nat.add := Nat.add_0_l.
Global Instance : RightId (=) 0 Nat.add := Nat.add_0_r.
Global Instance : LeftId (=) 1 Nat.mul := Nat.mul_1_l.
Global Instance : RightId (=) 1 Nat.mul := Nat.mul_1_r.
Global Instance : LeftAbsorb (=) 0 Nat.min := Nat.min_0_l.
Global Instance : RightAbsorb (=) 0 Nat.min := Nat.min_0_r.
Global Instance : LeftAbsorb (=) 0 Nat.mul := Nat.mul_0_l.
Global Instance : RightAbsorb (=) 0 Nat.mul := Nat.mul_0_r.
Global Instance : Assoc (=) Nat.min := Nat.min_assoc.
Global Instance : Assoc (=) Nat.max := Nat.max_assoc.
Global Instance : Assoc (=) Nat.add := Nat.add_assoc.
Global Instance : Assoc (=) Nat.mul := Nat.mul_assoc.
Global Instance : Comm (=) Nat.min := Nat.min_comm.
Global Instance : Comm (=) Nat.max := Nat.max_comm.
Global Instance : Comm (=) Nat.add := Nat.add_comm.
Global Instance : Comm (=) Nat.mul := Nat.mul_comm.
Global Instance : LeftDistr (=) Nat.mul Nat.add := Nat.mul_add_distr_l.
Global Instance : RightDistr (=) Nat.mul Nat.add := Nat.mul_add_distr_r.
Global Instance : LeftDistr (=) Nat.mul Nat.sub. see Nat.mul_sub_distr_l. Qed.
Global Instance : RightDistr (=) Nat.mul Nat.sub. see Nat.mul_sub_distr_r. Qed.
Global Instance : LeftDistr (=) Nat.mul subtract. see Nat.mul_sub_distr_l. Qed.
Global Instance : RightDistr (=) Nat.mul subtract. see Nat.mul_sub_distr_r. Qed.
Global Instance left_dominant_le n :
LeftDominant (le n) (+).
Proof. clia. Qed.
Global Instance left_comm_S_add :
CondLeftComm (=) (λ _, True) S (+).
Proof. clia. Qed.
Global Instance left_comm_add_add n :
CondLeftComm (=) (λ _, True) ((+) n) (+).
Proof. clia. Qed.
Global Instance left_comm_subtract_add n :
CondLeftComm (=) (le n) (subtract n) (+).
Proof. clia. Qed.
End Properties.
Lemma alter_add `{EqDecision A} (f : A -> nat) n a :
alter ((+) n) a f = f .+ <[a:=n]> (const 0).
Proof.
extensionality b; dec (b = a);
simpl_alter; cbn; simpl_insert; clia.
Qed.