No se puede encontrar una instancia para la variable

Question

Contexto: Estoy trabajando en ejercicios en Software Foundations.

Theorem neg_move : forall x y : bool, 
    x = negb y -> negb x = y. 
Proof. Admitted. 

Theorem evenb_n__oddb_Sn : forall n : nat, 
    evenb n = negb (evenb (S n)). 
Proof. 
    intros n. induction n as [| n']. 
    Case "n = 0". 
    simpl. reflexivity. 
    Case "n = S n'". 
    rewrite -> neg_move. 

Antes de la última línea, mi subobjetivo es la siguiente:

evenb (S n') = negb (evenb (S (S n'))) 

y quiero transformarlo en esto:

negb (evenb (S n')) = evenb (S (S n')) 

Cuando intento para pasar por rewrite -> neg_move, sin embargo, produce este error:

Error: Unable to find an instance for the variable y.

Estoy seguro de que esto es realmente simple, pero ¿qué estoy haciendo mal? (Por favor, no des nada por resolver evenb_n__oddb_Sn, a menos que lo esté haciendo completamente mal).

Answer 1

Como se mencionó anteriormente, Coq te está diciendo que no sabe cómo crear instancias y. De hecho, cuando lo haces rewrite -> neg_move, le pides que reemplace algunos negb x por un y. Ahora, ¿qué y se supone que Coq debe usar aquí? No puede resolverlo.

Una opción es crear una instancia de y explícitamente en la reescritura:

rewrite -> neg_move with (y:=some_term)

Esto realizará la reescritura y pedirle que compruebe las premisas, aquí se añadirá un sub-objetivo de la forma x = negb some_term.

Otra opción es especializarse neg_move sobre la reescritura:

rewrite -> (neg_move _ _ H)

Aquí H debe haber un término de tipo some_x = negb some_y. Puse dos comodines para los parámetros x y y de neg_move ya que Coq puede inferirlos de H como some_x y some_y respectivamente. Coq intentará reescribir una ocurrencia de negb some_x en su objetivo con some_y. Pero primero tiene que conseguir este término H en sus hipótesis, lo que podría haber alguna carga adicional ...

(Tenga en cuenta que la primera opción que te di debe ser equivalente a rewrite -> (neg_move _ some_term))

Otra opción es erewrite -> negb_move , que agregará variables desinstaladas que se verán como ?x y ?y, e intentará hacer la reescritura. A continuación, tendrá que probar la premisa, que se verá como (evenb (S (S n'))) = negb ?y, y con suerte en el proceso de resolver este subobjetivo, Coq descubrirá qué debería haber sido ?y desde el principio (aunque existen algunas restricciones, y pueden surgir algunos problemas). Coq resuelve el objetivo sin averiguar qué debe ser ?y).

---

Sin embargo, para su problema particular, es muy fácil:

========== 
evenb (S n') = negb (evenb (S (S n'))) 

symmetry.

========== 
negb (evenb (S (S n'))) = evenb (S n') 

apply neg_move.

========== 
evenb (S (S n')) = negb (evenb (S n')) 

Y eso es lo que quería (b ackwards, haz otro symmetry. si te importa).