Faire Agda réduire une expression dans un type d'objectif

Question

En utilisant ℕ et _≟_ de the standard library, je

open import Data.Nat 
open import Relation.Binary.PropositionalEquality 
open import Relation.Nullary 

foo : ℕ -> ℕ -> ℕ 
foo x y with x ≟ y 
foo x .x | yes refl = x 
foo x y | no contra = y 

data Bar : ℕ -> Set where 
    bar : (x : ℕ) -> Bar (foo x x) 

Je veux mettre en œuvre

mkBar : (x : ℕ) -> Bar x 
mkBar x = bar x 

Agda se plaint,

Type mismatch: 
expected: x 
    actual: foo x x | x ≟ x 
when checking that the expression bar x 
has type Bar x 

Cette a du sens pour moi: Agda ne sait pas a priori que x ≟ x évalue toujours à yes refl, donc il ne va pas évaluer foo x x jusqu'à ce qu'il en sache un peu plus sur x.

J'ai donc essayé de réécrire le but de forcer x ≟ x à résoudre à yes refl,

eq-refl : forall x -> (x ≟ x) ≡ yes refl 
eq-refl x with x ≟ x 
eq-refl x | yes refl = refl 
eq-refl x | no contra = ⊥-elim (contra refl) 

mkBar : (x : ℕ) -> Bar x 
mkBar x rewrite eq-refl x = bar x 

mais en vain. Même message d'erreur J'ai aussi essayé de réécriture par foo x x ≡ x:

foo-eq : forall x -> foo x x ≡ x 
foo-eq x rewrite eq-refl x = refl 

mkBar : (x : ℕ) -> Bar x 
mkBar x rewrite foo-eq x = bar x 

This answer suggère modèle correspondant à x ≟ x sur le côté gauche de mkBar, mais il semble aussi avoir aucun effet:

mkBar : (x : ℕ) -> Bar x 
mkBar x with x ≟ x 
mkBar x | yes refl = bar x 
mkBar x | no contra = ⊥-elim (contra refl) 

je dois manquer une astuce ici. Comment puis-je me débarrasser du | dans le type de but et faire foo x x réduire à ? (Je préfère ne pas examiner x directement dans le LHS de mkBar.)

Answer 1

Vous étiez presque là: la chose importante à noter est que rewrite prend un x ≡ y et remplace x par y dans le but. foo-eq x a le type foo x x ≡ x mais il n'y a pas foo x x à remplacer dans le but!

Ce que vous devez faire est de récrire par sym (foo-eq x) comme ceci:

mkBar : (x : ℕ) → Bar x 
mkBar x rewrite sym (foo-eq x) = bar x 

Bar x devient alors Bar (foo x x) qui signifie que vous pouvez appliquer votre constructeur.