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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the reflective ring solver may be used.
------------------------------------------------------------------------
module README.Tactic.RingSolver where
-- You can ignore this bit! We're just overloading the literals Agda uses for
-- numbers. This bit isn't necessary if you're just using Nats, or if you
-- construct your type directly. We only really do it here so that we can use
-- different numeric types in the same file.
open import Agda.Builtin.FromNat
open import Data.Nat using (ℕ)
open import Data.Integer using (ℤ)
import Data.Nat.Literals as ℕ
import Data.Integer.Literals as ℤ
instance
numberNat : Number ℕ
numberNat = ℕ.number
instance
numberInt : Number ℤ
numberInt = ℤ.number
------------------------------------------------------------------------------
-- Imports!
open import Data.List.Base as List using (List; _∷_; [])
open import Relation.Binary.PropositionalEquality
using (subst; cong; _≡_; module ≡-Reasoning)
open import Data.Bool as Bool using (Bool; true; false; if_then_else_)
open import Data.Unit using (⊤; tt)
open import Tactic.RingSolver.Core.AlmostCommutativeRing
using (AlmostCommutativeRing)
------------------------------------------------------------------------
-- Integer examples
------------------------------------------------------------------------
module IntegerExamples where
open import Data.Integer hiding (_^_)
open import Data.Integer.Tactic.RingSolver
open AlmostCommutativeRing ring using (_^_)
-- Everything is automatic: you just ask Agda to solve it and it does!
-- Addition
lemma₁ : ∀ x y → x + y + 3 ≡ 2 + y + x + 1
lemma₁ = solve-∀
-- Multiplication
lemma₂ : ∀ x → x * 2 + 1 ≡ x + 1 + x
lemma₂ = solve-∀
-- Negation
lemma₃ : ∀ x y → (- x) + (- y) ≡ - (x + y)
lemma₃ = solve-∀
-- Subtraction
lemma₄ : ∀ x y → (x - y) * 2 - 2 ≡ (- 2) * y - 1 + 2 * x - 1
lemma₄ = solve-∀
-- Exponentiation by constant literals
lemma₅ : ∀ x y → (x + y) ^ 2 ≡ x ^ 2 + 2 * x * y + y ^ 2
lemma₅ = solve-∀
-- It can be interleaved with manual proofs as well.
lemma₆ : ∀ x y z → y ≡ z → x + y * 1 + 3 ≡ 2 + z + x + 1
lemma₆ x y z y≡z = begin
x + y * 1 + 3 ≡⟨ solve (x ∷ y ∷ []) ⟩
2 + y + x + 1 ≡⟨ cong (λ v → 2 + v + x + 1) y≡z ⟩
2 + z + x + 1 ∎
where open ≡-Reasoning
------------------------------------------------------------------------
-- Natural examples
------------------------------------------------------------------------
module NaturalExamples where
open import Data.Nat
open import Data.Nat.Tactic.RingSolver
-- The solver is flexible enough to work with ℕ (even though it asks
-- for rings!)
lemma₁ : ∀ x y → x + y * 1 + 3 ≡ 2 + 1 + y + x
lemma₁ = solve-∀
------------------------------------------------------------------------
-- Checking invariants
------------------------------------------------------------------------
-- The solver makes it easy to prove invariants, without having to
-- rewrite proof code every time something changes in the data
-- structure.
module _ {a} {A : Set a} (_≤_ : A → A → Bool) where
open import Data.Nat hiding (_≤_)
open import Data.Nat.Tactic.RingSolver
-- A Skew Heap, indexed by its size.
data Tree : ℕ → Set a where
leaf : Tree 0
node : ∀ {n m} → A → Tree n → Tree m → Tree (1 + n + m)
-- A substitution operator, to clean things up.
infixr 1 _⇒_
_⇒_ : ∀ {n} → Tree n → ∀ {m} → n ≡ m → Tree m
x ⇒ n≡m = subst Tree n≡m x
open ≡-Reasoning
_∪_ : ∀ {n m} → Tree n → Tree m → Tree (n + m)
leaf ∪ ys = ys
node {a} {b} x xl xr ∪ leaf =
node x xl xr ⇒ solve (a ∷ b ∷ [])
node {a} {b} x xl xr ∪ node {c} {d} y yl yr =
if x ≤ y
then node x (node y yl yr ∪ xr) xl ⇒ begin
1 + (1 + c + d + b) + a ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
1 + a + b + (1 + c + d) ∎
else node y (node x xl xr ∪ yr) yl ⇒ begin
1 + (1 + a + b + d) + c ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
1 + a + b + (1 + c + d) ∎
|
