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
128
129
130
131
132
133
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Explaining how to use the inspect idiom and elaborating on the way
-- it is implemented in the standard library.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module README.Inspect where
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product.Base using (_×_; _,_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Binary.PropositionalEquality using (inspect; [_])
------------------------------------------------------------------------
-- Using inspect
-- We start with the definition of a (silly) predicate: `Plus m n p` states
-- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it
-- distinguishes two cases: whether `p` is 0 or not.
Plus-eq : (m n p : ℕ) → Set
Plus-eq m n zero = m ≡ 0 × n ≡ 0
Plus-eq m n p@(suc _) = m + n ≡ p
-- A sensible lemma to prove of this predicate is that whenever `p` is literally
-- `m + n` then `Plus m n p` holds. That is to say `∀ m n → Plus m n (m + n)`.
-- To be able to prove `Plus-eq m n (m + n)`, we need `m + n` to have either
-- the shape `zero` or `suc _` so that `Plus-eq` may reduce.
-- We could follow the way `_+_` computes by mimicking the same splitting
-- strategy, thus forcing `m + n` to reduce:
plus-eq-+ : ∀ m n → Plus-eq m n (m + n)
plus-eq-+ zero zero = refl , refl
plus-eq-+ zero (suc n) = refl
plus-eq-+ (suc m) n = refl
-- Or we could attempt to compute `m + n` first and check whether the result
-- is `zero` or `suc p`. By using `with m + n` and naming the result `p`,
-- the goal will become `Plus-eq m n p`. We can further refine this definition
-- by distinguishing two cases like so:
-- plus-eq-with : ∀ m n → Plus-eq m n (m + n)
-- plus-eq-with m n with m + n
-- ... | zero = {!!}
-- ... | suc p = {!!}
-- The problem however is that we have abolutely lost the connection between the
-- computation `m + n` and its result `p`. Which makes the two goals unprovable:
-- 1. `m ≡ 0 × n ≡ 0`, with no assumption whatsoever
-- 2. `m + n ≡ suc p`, with no assumption either
-- By using the `with` construct, we have generated an auxiliary function that
-- looks like this:
-- `plus-eq-with-aux : ∀ m n p → Plus-eq m n p`
-- when we would have wanted a more precise type of the form:
-- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`.
-- This is where we can use `inspect`. By using `with f x | inspect f x`,
-- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`.
-- Splitting on the result of `m + n`, we get two cases:
-- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero`
-- 2. `m + n ≡ suc p` under the assumption that `m + n ≡ suc p`
-- The first one can be discharged using lemmas from Data.Nat.Properties and
-- the second one is trivial.
plus-eq-with : ∀ m n → Plus-eq m n (m + n)
plus-eq-with m n with m + n | inspect (m +_) n
... | zero | [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
... | suc p | [ m+n≡1+p ] = m+n≡1+p
------------------------------------------------------------------------
-- Understanding the implementation of inspect
-- So why is it that we have to go through the record type `Reveal_·_is_`
-- and the ̀inspect` function? The fact is: we don't have to if we write
-- our own auxiliary lemma:
plus-eq-aux : ∀ m n → Plus-eq m n (m + n)
plus-eq-aux m n = aux m n (m + n) refl where
aux : ∀ m n p → m + n ≡ p → Plus-eq m n p
aux m n zero m+n≡0 = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
aux m n (suc p) m+n≡1+p = m+n≡1+p
-- The problem is that when we write ̀with f x | pr`, `with` decides to call `y`
-- the result `f x` and to replace *all* of the occurences of `f x` in the type
-- of `pr` with `y`. That is to say that if we were to write:
-- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n)
-- plus-eq-naïve m n with m + n | refl {x = m + n}
-- ... | p | eq = {!!}
-- then `with` would abstract `m + n` as `p` on *both* sides of the equality
-- proven by `refl` thus giving us the following goal with an extra, useless,
-- assumption:
-- 1. `Plus-eq m n p` under the assumption that `p ≡ p`
-- So how does `inspect` work? The standard library uses a more general version
-- of the following type and function:
record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where
constructor [_]
field eq : f x ≡ y
my-inspect : ∀ f n → MyReveal f · n is (f n)
my-inspect f n = [ refl ]
-- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we
-- write `with f n | inspect f n`, the only `f n` that can be abstracted in the
-- type of `inspect f n` is the third argument to `Reveal_·_is_`.
-- That is to say that the auxiliary definition generated looks like this:
plus-eq-reveal : ∀ m n → Plus-eq m n (m + n)
plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where
aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p
aux m n zero [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p
-- At the cost of having to unwrap the constructor `[_]` around the equality
-- we care about, we can keep relying on `with` and avoid having to roll out
-- handwritten auxiliary definitions.
|
