Dans Idris, utiliser réécrire sous un lambda

Question

Selon https://homes.cs.washington.edu/~jrw12/InductionExercises.html Je suis tring pour prouver sum et sum_cont sont équivalents. Je reçois à:

sum : List Nat -> Nat 
sum [] = 0 
sum (x :: xs) = x + sum xs 

sum_cont' : {a : Type} -> List Nat -> (Nat -> a) -> a 
sum_cont' [] k = k 0 
sum_cont' (x :: xs) k = sum_cont' xs (\ans => k (x + ans)) 

sum_cont : List Nat -> Nat 
sum_cont l = sum_cont' l (\x => x) 

sum_cont_correct' : (xs : List Nat) -> (x : Nat) -> sum_cont' xs (\ans => plus x ans) = plus x (sum xs) 
sum_cont_correct' [] acc = Refl 
sum_cont_correct' (x :: xs) acc = 
    rewrite plusAssociative acc x (sum xs) in 
    ?todo 

Lorsque le trou todo est de type:

sum_cont' xs (\ans => plus acc (plus x ans)) = plus (plus acc x) (sum xs) 

Je voudrais appliquer la réécriture plusAssociative acc x ans, mais ans n'est pas portée au sommet. Comment puis-je appliquer la réécriture sous le lambda, à une variable que je ne peux pas lier? La question How do I prove a "seemingly obvious" fact when relevant types are abstracted by a lambda in Idris? semble répondre à certains points similaires, mais suggère finalement d'utiliser cong, ce qui est inapproprié ici car je ne peux pas rendre les pièces extérieures similaires qu'après avoir appliqué la réécriture interne.

Answer 1

Vous ne pouvez pas réécrire sous lambdas sauf si vous êtes prêt à assumer l'axiome d'extensionalité fonctionnelle. À mon avis, la réponse que vous avez liée explique très bien. Par ailleurs, un système connexe - Coq possède des fonctionnalités (à savoir la tactique setoid_rewrite) qui facilitent la réécriture sous les classeurs (j'ai essayé de l'expliquer en this answer). Mais je ne suis pas au courant de son analogue dans Idris. Cependant, vous pouvez faire la preuve sans l'axiome ou d'autres machines comme les setoïdes comme suit.

Prouvons un lemme plus général d'abord:

sum_cont_correct' : (k : Nat -> ty) -> (xs : List Nat) -> sum_cont' xs k = k (sum xs) 
sum_cont_correct' k [] = Refl 
sum_cont_correct' k (x :: xs) = sum_cont_correct' (k . (x+)) xs 

maintenant la preuve du lemme sum_cont_correct est juste un one-liner:

sum_cont_correct : (xs : List Nat) -> sum_cont xs = sum xs 
sum_cont_correct = sum_cont_correct' id