[Agda] Reasoning with Pattern Match with Default Cases

[Dan Licata]

Yes, it does, at least in my experience.  E.g. when I've done Okasaki red-black trees (extrinsically), it all goes nicely, except there's a 140-line proof characterizing the view, because the function does some pretty deep pattern matching before the catch-all case (here's the original version of the code, without the view):

 balance : Tree → Color → (Key × Value) → Tree → Tree
    balance (Node (Node a Red x b) Red y c) Black z d =
            Node (Node a Black x b) Red y (Node c Black z d)
    balance (Node a Red x (Node b Red y c)) Black z d =
            Node (Node a Black x b) Red y (Node c Black z d)
    balance a Black x (Node (Node b Red y c) Red z d) =
            Node (Node a Black x b) Red y (Node c Black z d)
    balance a Black x (Node b Red y (Node c Red z d)) =
            Node (Node a Black x b) Red y (Node c Black z d)
    balance l c kv r = Node l c kv r

On the other hand, the view lemma can be reused for all of the later proofs, so at least the view puts the annoying part in one place.  Anyway, this is basically to +1 the request for better handling of catch-all cases, but given the compilation to case trees, I'm not sure what could be done.  

-Dan

On Nov 12, 2015, at 10:23 AM, Peter Selinger <selinger at mathstat.dal.ca> wrote:

> Doesn't that just push the same problem into proving properties of the
> function boolView? Suppose he had defined
> 
> f : Ty → Nat
> f τ  with boolView τ
> f .bool | bool   0
> f τ     | other  1
> 
> and he wanted to prove
> 
> lemma : (τ : Ty) -> f τ ≡ 1 -> not (τ ≡ bool)
> 
> You still need to prove something like
> (other : BoolView τ) -> not (τ ≡ bool),
> which gives the same problem as in the original post, for the function
> boolView, right?
> 
> -- Peter
> 
> Ulf Norell wrote:
>> 
>> data Ty : Set where
>>  int bool : Ty
>>  _=>_ : Ty → Ty → Ty
>> 
>> data BoolView : Ty → Set where
>>  bool : BoolView bool
>>  other : ∀ {τ} → BoolView τ
>> 
>> boolView : ∀ τ → BoolView τ
>> boolView bool  bool
>> boolView τ  other
>> 
>> f : Ty → Nat
>> f τ  with boolView τ
>> f .bool | bool   0
>> f τ     | other  0
>> 
>> lemma : (τ : Ty) -> f τ ≡ 0
>> lemma τ  with boolView τ
>> lemma .bool | bool   refl
>> lemma τ     | other  refl
>> 
>> / Ulf
>> 
>> On Thu, Nov 12, 2015 at 3:05 PM, Marco Vassena <vassena at chalmers.se> wrote:
>> 
>>> Suppose I have defined a function by pattern match.
>>> In the function I am interested in one specific case, therefore I
>>> explicitly
>>> match that one, while all the others are implicitly covered:
>>> 
>>> f : Ty -> ℕ
>>> f Bool  0
>>> f τ  0
>>> 
>>> Now I want to prove something about this function, however the
>>> proof cannot be as concise as the definition of f:
>>> 
>>> lemma : (τ : Ty) -> f τ ≡ 0
>>> lemma Bool  refl
>>> lemma τ  {! refl !}  -- f τ ! zero
>>> 
>>> I have to explicitly go through all the other cases, otherwise f τ won't
>>> reduce:
>>> 
>>> lemma : (τ : Ty) -> f τ ≡ 0
>>> lemma Bool  refl
>>> lemma Int  refl
>>> lemma (τ => τ₁)  refl
>>> ...
>>> 
>>> As you can imagine this can be very repetitive and annoying if the proofs
>>> are more involved
>>> and there are many values that fall in the "default" case.
>>> 
>>> Do you know if it is possible to abstract over this pattern when reasoning
>>> about
>>> functions defined by pattern matching with a default case?
>>> 
>>> All the best,
>>> Marco
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>> 
>>> 
>> 
>> --001a113edf486e1d5c0524594fb4
>> Content-Type: text/html; charset=UTF-8
>> Content-Transfer-Encoding: quoted-printable
>> 
>> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"><div dir="ltr">The best you can do, in my experience, is not use default cases in functions you want to prove lots of properties about. That doesn't mean you should spell out all the cases, though. Instead you can define a view for the particular set of patterns you are interested in. In your case<div><br></div><div><div>data Ty : Set where</div><div>&nbsp; int bool : Ty</div><div>&nbsp; _=&gt;_ : Ty → Ty → Ty</div><div><br></div><div>data BoolView : Ty → Set where</div><div>&nbsp; bool : BoolView bool</div><div>&nbsp; other : ∀ {τ} → BoolView τ</div><div><br></div><div>boolView : ∀ τ → BoolView τ</div><div>boolView bool  bool</div><div>boolView τ  other</div><div><br></div><div>f : Ty → Nat</div><div>f τ &nbsp;with boolView τ</div><div>f .bool | bool &nbsp; 0</div><div>f τ &nbsp; &nbsp; | other  0</div><div><br></div><div>lemma : (τ : Ty) -&gt; f τ ≡ 0</div><div>lemma τ &nbs
> p;with boolView τ</div><div>lemma .bool | bool &nbsp; refl</div><div>lemma τ &nbsp; &nbsp; | other  refl</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 12, 2015 at 3:05 PM, Marco Vassena <span dir="ltr">&lt;<a href="mailto:vassena at chalmers.se" target="_blank">vassena at chalmers.se</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Suppose I have defined a function by pattern match.<br>
>> In the function I am interested in one specific case, therefore I explicitly<br>
>> match that one, while all the others are implicitly covered:<br>
>> <br>
>> f : Ty -&gt; ℕ<br>
>> f Bool  0<br>
>> f τ  0<br>
>> <br>
>> Now I want to prove something about this function, however the<br>
>> proof cannot be as concise as the definition of f:<br>
>> <br>
>> lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
>> lemma Bool  refl<br>
>> lemma τ  {! refl !}&nbsp; -- f τ ! zero<br>
>> <br>
>> I have to explicitly go through all the other cases, otherwise f τ won't reduce:<br>
>> <br>
>> lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
>> lemma Bool  refl<br>
>> lemma Int  refl<br>
>> lemma (τ =&gt; τ₁)  refl<br>
>> ...<br>
>> <br>
>> As you can imagine this can be very repetitive and annoying if the proofs are more involved<br>
>> and there are many values that fall in the &quot;default&quot; case.<br>
>> <br>
>> Do you know if it is possible to abstract over this pattern when reasoning about<br>
>> functions defined by pattern matching with a default case?<br>
>> <br>
>> All the best,<br>
>> Marco<br>_______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda at lists.chalmers.se">Agda at lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> <br></blockquote></div><br></div>
>> 
>> --001a113edf486e1d5c0524594fb4--
>> 
>> --==============
>> Content-Transfer-Encoding: 7bit
>> Content-Disposition: inline
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> --==============
>> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda