cómo nombrar la suposición al recordar una expresión?

Question

La documentación de Coq contiene la advertencia general no para confiar en el mecanismo de nomenclatura incorporado, pero seleccione los nombres propios, para que los cambios en el mecanismo de nomenclatura no invaliden las pruebas pasadas.

Al considerar expresiones del formulario remember Expr as v, establecemos la variable v en la expresión Expr. Pero el nombre de la suposición está seleccionada de forma automática, y es algo así como Heqv, por lo que tenemos:

Heqv: v = Expr

¿Cómo puedo seleccionar mi propio nombre en lugar de Heqv? Siempre puedo cambiarle el nombre a lo que quiera usando el comando rename, pero eso no mantiene mis pruebas independientes de los futuros cambios hipotéticos en el mecanismo de nomenclatura incorporado en Coq.

Answer 1

Si puede deshacerse de la igualdad por separado, intente set (name := val). Use unfold en lugar de rewrite para recuperar el valor en su lugar.

Si necesita la igualdad para más que el rewrite <-, no conozco una táctica integrada que lo haga. Sin embargo, puedes hacerlo manualmente o crear una táctica/notación. Solo lancé esto juntos. (Nota: No soy un experto, esto podría hacerse más fácilmente.)

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) := 
    let v  := fresh in 
    let HHelp := fresh in 
    set (v := expr); 
    (assert (HHelp : sigT (fun x => x = v)) by (apply (existT _ v); reflexivity)); 
    inversion HHelp as [vname eqname]; 
    unfold v in *; clear v HHelp; 
    rewrite <- eqname in *. 

uso como remember_as_eq (2+2) four Heqfour para obtener el mismo resultado que con remember (2+2) as four.

---

Nota: Actualizada para manejar más casos, la versión anterior falló en algunas combinaciones de valor y tipo de objetivo. Deje un comentario si encuentra otro caso que funcione con rewrite pero no este.