With-clause doesn't take advantage of ruled out patterns to normalise

[edwinb]

Issue by ohad
Saturday Oct 26, 2019 at 21:04 GMT
Originally opened as edwinb/Idris2-boot#140

---

I'm not sure this is really a language problem, maybe a feature request?
Potentially related to #139.
Also, the example below is not realistic (because of the go_figure hole), it's just there to illustrate the problem in a short example.

Steps to Reproduce

Foo.idr

foo : Nat -> Bool
foo n = case compare n Z of
          LT => False
          _  => True
          
foo_true : (n : Nat) -> foo n = True
foo_true  n with (compare n Z)
 foo_true n | LT = ?go_figure  -- That's fine
 foo_true n | _  = ?hole       -- That's not

Expected Behavior

$ idris2 Foo.idr
Foo> :t hole
   n : Nat
-------------------------------------
hole : True = True

Observed Behavior

   n : Nat
-------------------------------------
hole : (case _ of { LT => False ; _ => True }) = True

We can, of course, prove the foo_true lemma (modulo go_figure) by exhausting all the other cases:

foo_true' : (n : Nat) -> foo n = True
foo_true'  n with (compare n Z)
 foo_true' n | LT = ?go_figure' -- That's fine
 foo_true' n | GT = Refl         
 foo_true' n | EQ = Refl

But it would be nicer to follow the same pattern that execution takes.

[edwinb]

Comment by edwinb
Saturday Dec 07, 2019 at 15:11 GMT

---

This'd be nice, but would require the normaliser to keep track of a lot of information. I think this is a feature request that's very unlikely to get done, unfortunately. I've added a label, just in case anyone is enthusiastic enough to do it, but my feeling is that it'd be very complicated to achieve.

(My feeling on this sort of thing is often wrong though, so who knows...)

[gallais]

For the record, the typical solution here is to define a view
that has one case for each match of interest & a catchall
constructor for the rest.

Instead of:

foo : s -> ...
foo x = case x of 
  C => ...
  _ => ...

write:

data View s = C | Default

view : (x : s) -> View x
view x = case x of
  C => C
  _ => Default

foo : s -> ...
foo x with (view x)
  foo x | C = ...
  foo x | Default = ...

and you can then prove foo's properties by using the same with (view x).