[Agda] Reasoning with Pattern Match with Default Cases

[Peter Selinger]

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  f τ     | other 
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 > boolView τ > 
> f : Ty → Nat
> f τ  with boolView τ
> f .bool | bool  > f τ     | other > 
> lemma : (τ : Ty) -> f τ ≡ 0
> lemma τ  with boolView τ
> lemma .bool | bool  > lemma τ     | other > 
> / 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 > > f τ > >
> > 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 > > lemma τ > >
> > I have to explicitly go through all the other cases, otherwise f τ won't
> > reduce:
> >
> > lemma : (τ : Ty) -> f τ ≡ 0
> > lemma Bool > > lemma Int > > lemma (τ => τ₁) > > ...
> >
> > 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  p;with boolView τ</div><div>lemma .bool | bool &nbsp;> 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 > f τ > <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 > lemma τ > <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 > lemma Int > lemma (τ =&gt; τ₁) > ...<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--
> 
> --======= 03912850391895811=Content-Type: text/plain; charset="us-ascii"
> Content-Transfer-Encoding: 7bit
> Content-Disposition: inline
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
> --======= 03912850391895811=--
>