Tipos que contienen cláusulas de/rewrite en agda, o, ¿cómo usar rewrite en lugar de subst?

Question

En primer lugar algunas importaciones aburrido:

import Relation.Binary.PropositionalEquality as PE 
import Relation.Binary.HeterogeneousEquality as HE 
import Algebra 
import Data.Nat 
import Data.Nat.Properties 
open PE 
open HE using (_≅_) 
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid) 
open CommutativeMonoid +-commutativeMonoid using() renaming (comm to +-comm) 

Supongamos ahora que tengo un tipo indexado por, por ejemplo, los productos naturales.

postulate Foo : ℕ -> Set 

Y que yo quiero probar algunas igualdades sobre las funciones que operan en este tipo Foo. Debido a que agda no es muy inteligente, estas serán igualdades heterogéneas. Un ejemplo sencillo sería

foo : (m n : ℕ) -> Foo (m + n) -> Foo (n + m) 
foo m n x rewrite +-comm n m = x 

bar : (m n : ℕ) (x : Foo (m + n)) -> foo m n x ≅ x 
bar m n x = {! ?0 !} 

El objetivo en el bar es

Goal: (foo m n x | n + m | .Data.Nat.Properties.+-comm n m) ≅ x 
———————————————————————————————————————————————————————————— 
x : Foo (m + n) 
n : ℕ 
m : ℕ 

¿Qué es esto | s haciendo en el objetivo? ¿Y cómo empiezo a construir un término de este tipo?

En este caso, puedo solucionar el problema manualmente haciendo la sustitución con subst, pero eso se pone realmente feo y tedioso para ecuaciones y tipos más grandes.

foo' : (m n : ℕ) -> Foo (m + n) -> Foo (n + m) 
foo' m n x = PE.subst Foo (+-comm m n) x 

bar' : (m n : ℕ) (x : Foo (m + n)) -> foo' m n x ≅ x 
bar' m n x = HE.≡-subst-removable Foo (+-comm m n) x 

Answer 1

Esos tubos indican que la reducción se suspendió en espera del resultado de las expresiones en cuestión, y que por lo general se reduce al hecho de que había un bloque with cuyo resultado lo que necesita saber para proceder. Esto se debe a que el constructo rewrite se expande a with de la expresión en cuestión junto con cualquier valor auxiliar que pueda ser necesario para que funcione, seguido de una coincidencia en refl.

En este caso, sólo significa que es necesario introducir el +-comm n m en un partido with bloque y el patrón en refl (y es probable que necesite para llevar a n + m alcance demasiado, ya que sugiere, por lo que la igualdad tiene algo para hablar). El modelo de evaluación de Agda es bastante sencillo, y si el patrón coincide en algo (excepto en las coincidencias de patrones falsos en los registros), no se reducirá hasta que coincida con el patrón en esa misma cosa. Incluso podría salirse con la suya escribiendo la misma expresión en su prueba, ya que solo hace lo que le describí.

Más precisamente, si se define:

f : ... 
f with a | b | c 
... | someDataConstructor | boundButNonConstructorVariable | someRecordConstructor = ... 

y luego se refieren a f como una expresión, obtendrá los tubos que observó para la expresión a única, ya que coincide con el someDataConstructor, por lo que en el mismo al menos para obtener f para reducir, tendrá que introducir a y luego coincidir en someDataConstructor desde él. Por otro lado, b y c, aunque se introdujeron en el mismo bloque, no se detiene la evaluación, porque b no coincide con el patrón, y 's someRecordConstructor se conoce estáticamente como el único constructor posible porque es un registro escribe con eta