Jak dopasować wyrażenie "dopasuj"?

Question

Próbuję napisać regułę dla hipotez, skomponowany z pomocą match budowy:

Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat. 
intros. 

x : nat 
H : match x with 
    | 0%nat => 10%nat 
    | 1%nat => 5%nat 
    | S (S _) => 10%nat 
    end = 5%nat 
============================ 
x = 1%nat 

Jak mogę dopasować takie hipotezy? Poniższy prosty sposób do przodu kończy się niepowodzeniem:

match goal with 
    |[H:match ?e with | ?a => ?x | ?b => ?y | ?c => ?z end = ?b] => idtac 
end. 

> Syntax error: 'end' expected after [branches] (in [match_constr]). 

Answer 1

Wzór dopasowywania na match stwierdzeń jest nieco dziwne.

Pierwszą rzeczą, którą powinieneś wiedzieć, jest to, że wewnątrz Coqa nie ma czegoś takiego jak match dla wielu zmiennych lub z głębokim dopasowaniem: wszystko jest tłumaczone na podstawie prostszych instrukcji match. Zatem termin napisałeś jest cukier faktycznie składnia następującym cyklu:

match x with 
| 0 => 10 
| S x' => 
    match x' with 
    | 0 => 5 
    | S x'' => 10 
    end 
end 

co jest, co jest Coq sugerując kiedy drukuje swój stan próbny. Problem polega na tym, że ten cukier składniowy nie działa na wzorcach Ltac: dlatego, pisząc wzór Ltac wymieniający match, zawsze powinieneś próbować dopasować go tak, jakby był jednopoziomowym match.

Drugim problemem jest to, że nie można wiązać wzór część match: coś jak

match goal with 
| H : match ?x => _ | ?y => _ end = 5 |- _ => (* ... *) 
end 

naprawdę nie ma sensu w Ltac.

Masz dwie możliwości rozwiązania problemu, a następnie:

1. Zapisz match można oczekiwać z dokładną listą konstruktorów typu ze strony wzór, na przykład

   match goal with 
   | H : match x with 0 => _ | S _ => _ end = 5 |- _ => (* ... *) 
   end 
   

2. pomocą specjalnej składni match (* ... *) with _ => _ end, który pasuje dowolnymatch cokolwiek:

   match goal with 
   | H : match x with _ => _ end = 5 |- _ => (* ... *) 
   end 
   

Często, jak w twoim przypadku, jeden nadal chce rozważyć wszystkie gałęzie match , w tym głębokie. Ten idiom często jest przydatny w tym przypadku:

repeat match goal with 
| H : match ?x with _ => _ end = _ |- _ => 
    destruct x; try solve [inversion H] 
end.