Comment fonctionne exactement la réécriture dans Idris?

Question

j'ai écrit la proposition suivante à Idris:

total 
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m) 
plusOneCommutes Z  k  = Refl 
plusOneCommutes (S k) j  = 
let inductiveHypothesis = plusOneCommutes k j in 
    rewrite inductiveHypothesis in Refl 

En utilisant l'inspiration à partir du code source Prelude.Nat, je comprends pourquoi il est logique d'utiliser l'appel récursif (dans le second cas) comme une hypothèse d'induction afin de prouver l'affaire. Cependant, en passant par les détails de la réécriture avec des trous, je ne sais pas vraiment ce qui se passe et pourquoi cela fonctionne.

Si je vous écris:

plusOneCommutes (S k) j  = ?hole 

Je reçois le texte suivant du compilateur:

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

qui ne semble pas vraiment droit. Selon la signature de plusOneCommutes ce trou devrait avoir le type (plus (S k) (S j)) = (plus (S (S k)) j).

Dans une étape ultérieure et l'introduction d'hypothèse de récurrence, si j'écrire:

plusOneCommutes (S k) j  = 
let inductiveHypothesis = plusOneCommutes k j in 
    ?hole 

puis type de hole devient:

- + HolyGrail.hole [P] 
    `--     k : Nat 
         j : Nat 
     inductiveHypothesis : k + S j = S k + j 
     ------------------------------------------------------------------------- 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

puis en utilisant la règle de réécriture donnée par inductiveHypothesis

- + HolyGrail.hole [P] 
    `--     k : Nat 
         j : Nat 
     inductiveHypothesis : k + S j = S k + j 
      _rewrite_rule : k + S j = S k + j 
     ------------------------------------------------------------------------- 
     HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j) 

qui conduit à S (plus (S k) j) = S (S (plus k j)) whi ch est le type attendu, et Idris peut compléter la preuve en remplaçant automatiquement ?hole par Refl. Ce qui m'intrigue alors est la différence inattendue de types entre ce que je déduis de la signature et ce que le compilateur déduit du trou. Si je présente volontairement une erreur:

Je reçois le message suivant:

- + Errors (1) 
    `-- HolyGrail.idr line 121 col 16: 
     When checking right hand side of plusOneCommutes with expected type 
       S k + S j = S (S k) + j 

     Type mismatch between 
       S (S (plus k j)) = S (S (plus k j)) (Type of Refl) 
     and 
       S (plus k (S j)) = S (S (plus k j)) (Expected type) 

     Specifically: 
       Type mismatch between 
         S (plus k j) 
       and 
         plus k (S j) 

La partie Type mismatch... est compatible avec les étapes ci-dessus, mais pas la partie When checking ... qui donne le type que je me attends.

Answer 1

Le suivant du compilateur fait réellement sens:

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

Dans le côté gauche de = dans le type que vous avez n + S m. Après le modèle correspondant sur n vous avez (S k) et devrait avoir S k + S j dans le type qui est plus (S k) (S j). Dans this question j'ai expliqué un point important: du fait comment la fonction plus est écrite et le fait que le compilateur peut effectuer la correspondance de modèle dans les types que vous voyez S (plus k (S j)) qui applique simplement plus à (S k) et (S j). Situation similaire avec S n + m.

Maintenant à rewrite. Dans Agda langage de programmation rewrite est juste la syntaxe de sucre pour la correspondance de modèle sur Refl.Et parfois, vous pouvez remplacer rewrite avec motif correspondant dans Idris mais pas dans ce cas.

Nous pouvons essayer de faire quelque chose de similaire. Considérons ensuite:

total 
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m) 
plusOneCommutes Z  k  = Refl 
plusOneCommutes (S k) j  = case plusOneCommutes k j of 
    prf => ?hole 

compilateur dit ensuite des choses très raisonnables:

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
       prf : k + S j = S k + j 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

prf est quelque chose qui prouve k + S j = S k + j ce qui est logique. Et après avoir utilisé rewrite:

plusOneCommutes (S k) j  = case plusOneCommutes k j of 
    prf => rewrite prf in ?hole 

Nous avons obtenu:

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
       prf : k + S j = S k + j 
     _rewrite_rule : k + S j = S k + j 
    ------------------------------------------------------------------------- 
     HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j) 

rewrite à Idris prend objet de type Refl, recherche côté gauche de = dans l'expression après in et le remplace par le côté droit de = de donné Refl. Donc, avant le rewrite, nous avions le type de résultat S (plus k (S j)) = S (S (plus k j)). Le type de votre inductiveHypothesis est k + S j = S k + j et nous avons obtenu k + S j juste dans le type que nous voulons. Vous pouvez voir cette partie comme replaced dans ce lambda. Après remplacement S k + j au lieu de k + S j vous avez obtenu S (plus (S k) j) = S (S (plus k j)) de la même manière que vous l'avez correctement noté. Mais rappelez-vous que Idris peut effectuer une correspondance de motif ce qu'il fait. Et S (plus (S k) j) devient naturellement S (S (plus k j)). QED.