Does Idris support unfolding function definitions?

Question

With dependent types, it's possible to define an inductive type for sorted lists, e.g.:

data IsSorted : {a: Type} -> (ltRel: (a -> a -> Type)) -> List a -> Type where
  IsSortedZero : IsSorted {a=a} ltRel Nil
  IsSortedOne : (x: a) -> IsSorted ltRel [x]
  IsSortedMany : (x: a) -> (y: a) -> .IsSorted rel (y::ys) -> .(rel x y) -> IsSorted rel (x::y::ys)

This can then be used to reason about sorted lists.

In Coq, one could also write a function Fixpoint is_sorted: {A: Type} (l: List A) : bool, and then make use of a type like is_sorted someList = true to prove things, by unfolding the definition of is_sorted. Is this latter approach possible in Idris, or does it only support the former approach?

Furthermore, for my own understanding: is the latter case an example of "proof by reflection", and is there any situation in which the latter approach would be preferable to the former?

Philip Dorrell Philip Dorrell · Accepted Answer · 2017-07-08T02:16:25

I think the following partially does what you want (I will add the caveat that I have no experience of using Coq):

infixl 4 &

(&) : Bool -> Bool -> Bool
(&) True True = True
(&) _ _ = False

elim_and : x & y = True -> (x = True, y = True)
elim_and {x = False} {y = False} x_and_y_is_true = (x_and_y_is_true, x_and_y_is_true)
elim_and {x = False} {y = True} x_and_y_is_true = (x_and_y_is_true, Refl)
elim_and {x = True} {y = False} x_and_y_is_true = (Refl, x_and_y_is_true)
elim_and {x = True} {y = True} x_and_y_is_true = (Refl, Refl)

is_sorted : {a: Type} -> (ltRel: a -> a -> Bool) -> List a -> Bool
is_sorted ltRel [] = True
is_sorted ltRel (x :: []) = True
is_sorted ltRel (x :: y :: xs) = (ltRel x y) & (is_sorted ltRel (y :: xs))

is_sorted_true_elim : {x : a} -> is_sorted ltRel (x :: y :: xs) = True -> (ltRel x y = True, 
                                                                           is_sorted ltRel (y :: xs) = True)
is_sorted_true_elim {x} {y} {xs} {ltRel} is_sorted_x_y_xs = elim_and is_sorted_x_y_xs

The important detail is that if your function definition is a simple set of equations, then the unification will somewhat magically substitute one side of the equation for the other when required. (I used a less efficient non-shortcircuited version of the logical "and" operator, because the standard "&&" or "if/then/else" operators introduce complications of laziness.)

Ideally there should be some straightforward way to unfold definitions that include 'with'-based pattern matching, but I don't know how to make that work, eg:

is_sorted : {a: Type} -> (ltRel: a -> a -> Bool) -> List a -> Bool
is_sorted ltRel [] = True
is_sorted ltRel (x :: []) = True
is_sorted ltRel (x :: y :: xs) with (ltRel x y)
  | True = is_sorted ltRel (y :: xs)
  | False = False

is_sorted_true_elim : {x : a} -> is_sorted ltRel (x :: y :: xs) = True -> (ltRel x y = True, 
                                                                           is_sorted ltRel (y :: xs) = True)
is_sorted_true_elim {x} {y} {xs} {ltRel} is_sorted_x_y_xs with (ltRel x y) proof x_lt_y_value
  | True = ?hole
  | False = ?hole2

Does Idris support unfolding function definitions?

1 Answers