Nie można znaleźć instancji zmiennej

Question

Kontekst: Pracuję nad ćwiczeniami w 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. 

Przed ostatnim wierszu, mój subgoal to:

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

I chcę, aby przekształcić go w ten sposób:

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

Gdy próbuję przejść przez rewrite -> neg_move jednak, generuje ten błąd:

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

Jestem pewien, że to naprawdę proste, ale co robię źle? (Proszę, nie oddawaj niczego za rozwiązanie evenb_n__oddb_Sn, chyba że robię to całkowicie źle).

Answer 1

Jak wspomniał danportin, Coq informuje Cię, że nie wie, jak utworzyć instancję y. Rzeczywiście, gdy robisz rewrite -> neg_move, poprosisz go o zastąpienie niektórych negb x przez y. Co teraz powinno używać tutaj Coq y? Nie może tego rozgryźć.

Jedną z opcji jest do wystąpienia y wyraźnie na przepisanie:

rewrite -> neg_move with (y:=some_term)

ten wykona przepisanie i poprosi, aby udowodnić przesłanki, tu będzie dodać subgoal formularza x = negb some_term.

Inną opcją jest specjalizują neg_move na przepisanie:

rewrite -> (neg_move _ _ H)

Tutaj H musi być określenie typu some_x = negb some_y. Umieściłem dwa symbole wieloznaczne dla parametrów x iz neg_move, ponieważ Coq jest w stanie wywnioskować je odpowiednio z H jako some_x i some_y. Coq spróbuje przepisać wystąpienie negb some_x w twoim celu za pomocą some_y. Ale najpierw trzeba uzyskać ten H termin w swoich hipotez, które mogłyby być jakiś dodatkowy ciężar ...

(Zauważ, że pierwsza opcja dałem powinna być równoważna rewrite -> (neg_move _ some_term))

Inną opcją jest erewrite -> negb_move , która doda niepotrzebne zmienne, które będą wyglądały jak ?x i ?y, i spróbuje przepisać. Będziesz musiał udowodnić założenie, które będzie wyglądać jak (evenb (S (S n'))) = negb ?y, i mam nadzieję, że w procesie rozwiązywania tego subgoalu, Coq dowie się, co powinno być od ?y (istnieją jednak pewne ograniczenia i mogą pojawić się problemy Coq rozwiązuje ten cel, nie zastanawiając się, co musi być ?y).

---

Jednak dla danego problemu, to jest całkiem prosta:

========== 
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')) 

A to, co chciał (b Dalej, zrób kolejny symmetry., jeśli ci na tym zależy.