<html><head><style>
body {
font-family: "Helvetica Neue", Helvetica, Arial, sans-serif;
padding:1em;
margin:auto;
background:#fefefe;
}
h1, h2, h3, h4, h5, h6 {
font-weight: bold;
}
h1 {
color: #000000;
font-size: 28pt;
}
h2 {
border-bottom: 1px solid #CCCCCC;
color: #000000;
font-size: 24px;
}
h3 {
font-size: 18px;
}
h4 {
font-size: 16px;
}
h5 {
font-size: 14px;
}
h6 {
color: #777777;
background-color: inherit;
font-size: 14px;
}
hr {
height: 0.2em;
border: 0;
color: #CCCCCC;
background-color: #CCCCCC;
display: inherit;
}
p, blockquote, ul, ol, dl, li, table, pre {
margin: 15px 0;
}
a, a:visited {
color: #4183C4;
background-color: inherit;
text-decoration: none;
}
#message {
border-radius: 6px;
border: 1px solid #ccc;
display:block;
width:100%;
height:60px;
margin:6px 0px;
}
button, #ws {
font-size: 12 pt;
padding: 4px 6px;
border-radius: 5px;
border: 1px solid #bbb;
background-color: #eee;
}
code, pre, #ws, #message {
font-family: Monaco;
font-size: 10pt;
border-radius: 3px;
background-color: #F8F8F8;
color: inherit;
}
code {
border: 1px solid #EAEAEA;
margin: 0 2px;
padding: 0 5px;
}
pre {
border: 1px solid #CCCCCC;
overflow: auto;
padding: 4px 8px;
}
pre > code {
border: 0;
margin: 0;
padding: 0;
}
#ws { background-color: #f8f8f8; }
.bloop_markdown table {
border-collapse: collapse;
font-family: Helvetica, arial, freesans, clean, sans-serif;
color: rgb(51, 51, 51);
font-size: 15px; line-height: 25px;
padding: 0; }
.bloop_markdown table tr {
border-top: 1px solid #cccccc;
background-color: white;
margin: 0;
padding: 0; }
.bloop_markdown table tr:nth-child(2n) {
background-color: #f8f8f8; }
.bloop_markdown table tr th {
font-weight: bold;
border: 1px solid #cccccc;
margin: 0;
padding: 6px 13px; }
.bloop_markdown table tr td {
border: 1px solid #cccccc;
margin: 0;
padding: 6px 13px; }
.bloop_markdown table tr th :first-child, table tr td :first-child {
margin-top: 0; }
.bloop_markdown table tr th :last-child, table tr td :last-child {
margin-bottom: 0; }
.bloop_markdown blockquote{
border-left: 4px solid #dddddd;
padding: 0 15px;
color: #777777; }
blockquote > :first-child {
margin-top: 0; }
blockquote > :last-child {
margin-bottom: 0; }
code, pre, #ws, #message {
word-break: normal;
word-wrap: normal;
}
hr {
display: inherit;
}
.bloop_markdown :first-child {
-webkit-margin-before: 0;
}
code, pre, #ws, #message {
font-family: Menlo, Consolas, Liberation Mono, Courier, monospace;
}
.send { color:#77bb77; }
.server { color:#7799bb; }
.error { color:#AA0000; }</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="bloop_markdown"><p>You probably want to use the “inspect” idiom.</p>
<p>See here:</p>
<p>https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/PropositionalEquality.agda</p>
<p>Under “inspect on steroids”</p>
<p></p></div><div class="bloop_original_html"><style>body{font-family:Helvetica,Arial;font-size:13px}</style><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div> <br> <div class="bloop_sign" id="bloop_sign_1418621402087010816"><span style="font-family:helvetica,arial;font-size:13px"></span>-- <br>Liam O'Connor<br><span>Sent with Airmail</span></div> <br><p style="color:#000;">On 15 December 2014 at 4:28:07 pm, Peter Selinger (<a href="mailto:selinger@mathstat.dal.ca">selinger@mathstat.dal.ca</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div></div><div>This is a newbie question. I am being driven mad by proofs about
<br>definitions that use the "with" notation. The situation is typically
<br>like this:
<br>
<br>lemma : A -> B
<br>lemma x with expr
<br>lemma x | y = ?
<br>
<br>Within the proof context '?', a variable y is available, of the same
<br>type as expr. However, often, to complete the proof, one has to use
<br>the fact that y == expr. This fact is obviously true, but typically
<br>does not follow from anything in the proof context.
<br>
<br>The "rewrite" notation does not help here, because its purpose is to
<br>use an equation, not to prove one.
<br>
<br>Here is a concrete example (full definitions and proofs appended
<br>below). I have defined an operation for computing the maximum of a
<br>list of natural numbers:
<br>
<br>maximum : (L : List Nat) -> Nat
<br>
<br>I have also proved a lemma showing that the maximum is indeed an upper
<br>bound for the list:
<br>
<br>lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L
<br>
<br>One can then easily prove a theorem stating that there are infinitely
<br>many natural numbers:
<br>
<br>theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)
<br>
<br>Since existential witnesses are not very convenient to use, I'd like
<br>to split this theorem into a first and second component: the first
<br>component is a function computing a natural number not in a given
<br>list, and the second component is the lemma saying that the number is
<br>indeed not in the list:
<br>
<br>-- Return a natural number not in L.
<br>newNat : (L : List Nat) -> Nat
<br>newNat L with theorem-infinite L
<br>newNat L | ([ n , p ]) = n
<br>
<br>-- The defining property of newNat.
<br>lemma-newNat : (L : List Nat) -> newNat L ∉ L
<br>lemma-newNat L with theorem-infinite L
<br>lemma-newNat L | ([ n , p ]) = ?
<br>
<br>However, I cannot complete the last proof. In principle, the question
<br>mark should just be "p". However, the prover (modulo beta reduction)
<br>serves
<br>
<br>Goal: newNat L ∉ L
<br>
<br>as the goal, and gives
<br>
<br>p : n ∉ L
<br>n : Nat
<br>L : List Nat
<br>
<br>as the hypotheses. Obviously, [ n , p ] was obtained by pattern
<br>matching theorem-infinite L, so we know that
<br>
<br>[ n , p ] == theorem-infinite L.
<br>
<br>>From this, we could immediately conclude that newNat L == n, which
<br>would immediately prove the goal. But I have not been able to find any
<br>combination of dot-patterns that the type checker would actually
<br>accept.
<br>
<br>Two questions:
<br>
<br>(1) what is the concrete solution to my problem?
<br>
<br> I realize that I can solve the problem by defining general first
<br> and second projections from the existential type:
<br>
<br> ∃fst : {A : Set} {B : A -> Set} -> ∃[ x ∈ A ] B x -> A
<br> ∃snd : {A : Set} {B : A -> Set} -> (p : ∃[ x ∈ A ] B x) -> B (∃fst p)
<br>
<br> and then I can just define newNat and lemma-newNat in terms of
<br> these. However, I am more concerned with what one can do when one
<br> is stuck in a proof context, rather than such an "external"
<br> solution to the problem.
<br>
<br>(2) why doesn't Agda do the obvious, namely, when matching a "with"
<br> expression "expr" against a pattern "p", just add the equation
<br> "expr == p" to the proof context? Is there an existing mechanism
<br> that can achieve this?
<br>
<br>Thanks, -- Peter
<br>
<br>Here's the full example. It requires no libraries.
<br>
<br>module InfNat where
<br>
<br>-- Falsity.
<br>data False : Set where
<br> -- no constructors.
<br>
<br>-- Negation.
<br>Not : Set -> Set
<br>Not A = A -> False
<br>
<br>-- Existential quantifier.
<br>data Exists (A : Set) (B : A -> Set) : Set where
<br> [_,_] : (a : A) -> B a -> Exists A B
<br>syntax Exists A (λ x -> B) = ∃[ x ∈ A ] B
<br>
<br>-- The natural numbers.
<br>data Nat : Set where
<br> zero : Nat
<br> succ : Nat -> Nat
<br>
<br>-- Order.
<br>data _<=_ : Nat -> Nat -> Set where
<br> z<=n : ∀ {n} → zero <= n
<br> s<=s : ∀ {m n} (m<=n : m <= n) → succ m <= succ n
<br>
<br>-- Order is reflexive.
<br>lemma-order-refl : ∀ {n} -> n <= n
<br>lemma-order-refl {zero} = z<=n
<br>lemma-order-refl {succ n} = s<=s lemma-order-refl
<br>
<br>-- Order is transitive.
<br>lemma-order-trans : ∀ {n m k} -> n <= m -> m <= k -> n <= k
<br>lemma-order-trans z<=n q = z<=n
<br>lemma-order-trans (s<=s p) (s<=s q) = s<=s (lemma-order-trans p q)
<br>
<br>-- Successor is not smaller.
<br>lemma-order-succ : ∀ {n} -> Not (succ n <= n)
<br>lemma-order-succ (s<=s h) = lemma-order-succ h
<br>
<br>-- The maximum of two numbers.
<br>max : Nat -> Nat -> Nat
<br>max zero m = m
<br>max n zero = n
<br>max (succ n) (succ m) = succ (max n m)
<br>
<br>-- Introduction rules for maximum.
<br>lemma-max-intro1 : ∀ n m -> n <= max n m
<br>lemma-max-intro1 zero m = z<=n
<br>lemma-max-intro1 (succ n) zero = lemma-order-refl
<br>lemma-max-intro1 (succ n) (succ m) = s<=s (lemma-max-intro1 n m)
<br>
<br>lemma-max-intro2 : ∀ n m -> m <= max n m
<br>lemma-max-intro2 zero m = lemma-order-refl
<br>lemma-max-intro2 (succ n) zero = z<=n
<br>lemma-max-intro2 (succ n) (succ m) = s<=s (lemma-max-intro2 n m)
<br>
<br>-- Lists.
<br>data List (A : Set) : Set where
<br> [] : List A
<br> _::_ : A -> List A -> List A
<br>
<br>-- Membership.
<br>data _∈_ {A : Set} (x : A) : (B : List A) -> Set where
<br> mem-head : {xs : List A} -> x ∈ (x :: xs)
<br> mem-tail : {xs : List A} {y : A} -> x ∈ xs -> x ∈ (y :: xs)
<br>
<br>-- Not member.
<br>_∉_ : {A : Set} -> (x : A) -> (B : List A) -> Set
<br>x ∉ B = Not (x ∈ B)
<br>
<br>-- Calculate the maximum of a list of numbers.
<br>maximum : (L : List Nat) -> Nat
<br>maximum [] = zero
<br>maximum (n :: L) = max n (maximum L)
<br>
<br>-- The maximum is an upper bound.
<br>lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L
<br>lemma-maximum (n :: L) .n mem-head = lemma-max-intro1 n (maximum L)
<br>lemma-maximum (n :: L) m (mem-tail p) = lemma-order-trans (lemma-maximum L m p) (lemma-max-intro2 n (maximum L))
<br>
<br>-- Theorem: there are infinitely many natural numbers.
<br>theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)
<br>theorem-infinite L = [ n , p ]
<br> where
<br> n = succ (maximum L)
<br> p : n ∉ L
<br> p h = let q = lemma-maximum L n h in lemma-order-succ q
<br>
<br>-- Return a natural number not in L.
<br>newNat : (L : List Nat) -> Nat
<br>newNat L with theorem-infinite L
<br>newNat L | ([ n , p ]) = n
<br>
<br>-- The defining property of newNat.
<br>lemma-newNat : (L : List Nat) -> newNat L ∉ L
<br>lemma-newNat L with theorem-infinite L
<br>lemma-newNat L | ([ n , p ]) = {!!}
<br>_______________________________________________
<br>Agda mailing list
<br>Agda@lists.chalmers.se
<br>https://lists.chalmers.se/mailman/listinfo/agda
<br></div></div></span></blockquote></div><div class="bloop_markdown"><p></p></div></body></html>