choisir automatiquement une hypothèse de contexte local

J'ai un script preuve d'une section qui ressemble à ceci:choisir automatiquement une hypothèse de contexte local

- destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence. 
    - destruct (IHx1 _ _ H6). congruence. 
    - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence. 
    - destruct (IHx1 _ _ H6). congruence. 
    - destruct (IHx _ _ H2). congruence. 
    - destruct (IHx _ _ H5). congruence. 
    - destruct (IHx _ _ H2). congruence. 
    - destruct (IHx _ _ H8). congruence. 
    - destruct (IHx _ _ H8). congruence. 
    - destruct (IHx _ _ H8). congruence. 
    - destruct (IHx _ _ H8). congruence. 
    - destruct (IHx _ _ H7). congruence. 
    - destruct (IHx _ _ H4). congruence. 
    - destruct (IHx1 _ _ H8). congruence. 
    - destruct (IHx1 _ _ H5). subst. destruct (IHx2 _ _ H9).

Il semble que ce serait un candidat de choix pour l'utilisation ; pour résoudre proprement, malheureusement, les hypothèses sont partout. Comment puis-je réduire les différentes sous-preuves ensemble?

Source

2017-05-27 Carl Patenaude Poulin

Veuillez éviter de mettre des solutions complètes aux exercices en SF sur Internet! –

N'avez-vous pas vu la seule chose en rouge dans [l'introduction] (https://www.cis.upenn.edu/~bcpierce/sf/current/Preface.html#lab12)? –

Je suis désolé! Je vais éditer ma solution dès qu'elle aura une réponse. Je l'enlèverais maintenant mais je n'ai pas une autre bonne démonstration du problème que j'essaie de démontrer. –

Les cas où nous avons une seule hypothèse d'induction peut être résolu en utilisant la pièce suivante Ltac (voir le manuel, chapter 9):

match goal with 
    IH : forall st2 s2, ?c/?st \\ s2/st2 -> _, 
    H : ?c/?st \\ _/_ 
    |- _ => now destruct (IH _ _ H) 
end

Lorsque les variables préfixées avec des points d'interrogation, par exemple ?c, ?st, etc. sont des métavariables d'appariement de motifs, des virgules séparées d'hypothèses et le symbole de tourniquet (|-) sépare les hypothèses du but. Ici, nous recherchons une hypothèse de récurrence IH et une hypothèse compatible H afin que nous puissions appliquer IH à H. La partie ?c/?st garantit que IH et H sont compatibles.

Les sous-buts avec deux hypothèses d'induction peuvent être résolus de manière analogue:

match goal with 
    IH1 : forall st2 s2, ?c1/?st \\ s2/st2 -> _, 
    IH2 : forall st2 s2, ?c2/_ \\ s2/st2 -> _, 
    H1 : ?c1/?st \\ _/?st'', 
    H2 : ?c2/?st'' \\ _/st2 
    |- _ => now destruct (IH1 _ _ H1); subst; destruct (IH2 _ _ H2) 
end

Bien sûr, si vous voulez, vous pouvez lier des noms à ces tactiques personnalisés, utilisez tactique avec eux et ainsi de suite:

Ltac solve1 := 
    try match goal with 
     IH : forall st2 s2, ?c/?st || s2/st2 -> _, 
     H : ?c/?st || _/_ 
     |- _ => now destruct (IH _ _ H) 
     end.

Source

2017-05-29 07:40:20

choisir automatiquement une hypothèse de contexte local

Répondre

Questions connexes