Est-ce que Idris prend en charge les définitions de fonctions dépliantes?

Question

Avec des types dépendants, il est possible de définir un type inductif pour les listes triées, .: par exemple

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) 

Cela peut ensuite être utilisé pour raisonner sur les listes triées.

En Coq, on pourrait aussi écrire une fonction Fixpoint is_sorted: {A: Type} (l: List A) : bool, puis utiliser un type comme is_sorted someList = true pour prouver des choses, par unfold la définition de ing is_sorted. Cette dernière approche est-elle possible dans Idris, ou soutient-elle seulement la première approche? En outre, pour ma propre compréhension: ce dernier cas est-il un exemple de «preuve par réflexion», et y a-t-il une situation dans laquelle cette dernière approche serait préférable à la première?

Answer 1

Je pense que ce qui suit ne partiellement ce que vous voulez (je vais ajouter la mise en garde que je n'ai aucune expérience de l'utilisation 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 

Le détail important est que si votre définition de la fonction est un simple ensemble de les équations, alors l'unification va magiquement substituer un côté de l'équation pour l'autre si nécessaire. (J'ai utilisé un moins efficace non-circuitée version du « et » logique opérateur, parce que la norme « & & » ou « if/then/else » Les opérateurs introduisent des complications de la paresse.)

Idéalement, il devrait y avoir un simple façon de déployer les définitions qui incluent « pattern matching basé with', mais je ne sais pas comment faire ce travail, par exemple:

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