Coq nie może znaleźć subterm podczas stosowania taktyki przepisywania

Question

Próbuję wykonać zmodyfikowany dowód compile_correct z first chapter certyfikowanego programowania z zależnymi typami. W mojej wersji staram się wykorzystać fakt, że progDenote jest fałdą, i użyć słabszej hipotezy indukcyjnej w dowodzie głównego lematu w priving compile_correct.

Kod, który jest identyczny z książki brzmi:

Require Import Bool Arith List. 
Set Implicit Arguments. 

Inductive binop : Set := Plus | Times. 

Inductive exp : Set := 
    | Const : nat -> exp 
    | Binop : binop -> exp -> exp -> exp. 

Definition binopDenote (b : binop) : nat -> nat -> nat := 
    match b with 
    | Plus => plus 
    | Times => mult 
    end. 

Fixpoint expDenote (e : exp) : nat := 
    match e with 
    | Const n => n 
    | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) 
    end. 

Inductive instr : Set := 
    | iConst : nat -> instr 
    | iBinop : binop -> instr. 

Definition prog := list instr. 
Definition stack := list nat. 

Definition instrDenote (i : instr) (s : stack) : option stack := 
    match i with 
    | iConst n => Some (n :: s) 
    | iBinop b => 
     match s with 
     | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') 
     | _ => None 
     end 
    end. 

Fixpoint compile (e : exp) : prog := 
    match e with 
    | Const n => iConst n :: nil 
    | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil 
    end. 

Potem zdefiniować własną wersję prog_denote który jest składany nad listą instrukcji w programie:

Definition bind {A B : Type} (a : option A) (f : A -> option B) : option B := 
    match a with 
    | Some x => f x 
    | None => None 
    end. 

Definition instrDenote' (s : option stack) (i : instr) : option stack := 
    bind s (instrDenote i). 

Definition progDenote (p : prog) (s : stack) : option stack := 
    fold_left instrDenote' p (Some s). 

I następnie spróbuj udowodnić słabszą wersję compile_correct z książki:

Lemma compile_correct' : forall e s, 
    progDenote (compile e) s = Some (expDenote e :: s). 
induction e. 
intro s. 
unfold compile. 
unfold expDenote. 
unfold progDenote at 1. 
simpl. 
reflexivity. 
intro s. 
unfold compile. 
fold compile. 
unfold expDenote. 
fold expDenote. 
unfold progDenote. 
rewrite fold_left_app. 
rewrite fold_left_app. 
unfold progDenote in IHe2. 
rewrite (IHe2 s). 
unfold progDenote in IHe1. 
rewrite (IHe1 (expDenote e2 :: s)). 

Mój dowód łamie w ostatniej kolejce, ze stanem dowód

1 subgoal 
b : binop 
e1 : exp 
e2 : exp 
IHe1 : forall s : stack, 
     fold_left instrDenote' (compile e1) (Some s) = 
     Some (expDenote e1 :: s) 
IHe2 : forall s : stack, 
     fold_left instrDenote' (compile e2) (Some s) = 
     Some (expDenote e2 :: s) 
s : stack 
______________________________________(1/1) 
fold_left instrDenote' (iBinop b :: nil) 
    (fold_left instrDenote' (compile e1) (Some (expDenote e2 :: s))) = 
Some (binopDenote b (expDenote e1) (expDenote e2) :: s) 

a błąd jest

Error: 
Found no subterm matching "fold_left instrDenote' (compile e1) 
          (Some (expDenote e2 :: s))" in the current goal. 

Na tym etapie dowodów, robie indukcję na e wyrażenie jest kompilowany, i zajmowanie się konstruktorem Binop z exp. Nie rozumiem, dlaczego pojawia się ten błąd, ponieważ po zastosowaniu IHe1 do expDenote e2 :: s nie ma żadnych powiązanych zmiennych. Wydaje się, że to zwykły problem z zastosowaniem reguł przepisywania nie działa. Sprawdziłem również, czy termin, który próbuję utworzyć, to:

fold_left instrDenote' (iBinop b :: nil) 
    (Some (expDenote e1 :: expDenote e2 :: s)) = 
Some (binopDenote b (expDenote e1) (expDenote e2) :: s) 

kontrola typu.

Co jeszcze może pójść nie tak z zasadą przepisywania, gdy podwyrażenie, na które się narzeka, jest wyraźnie widoczne w celu?

EDYCJA: Zgodnie z sugestią, zmieniłem ustawienia wyświetlania w coqide na odpowiednik Ustaw wszystkie drukowania. Ujawniło to problem polegający na tym, że definicja stack została rozłożona na list nat w jednym miejscu w celu, co uniemożliwiło rozpoznanie subterm. Celem wydrukowany z nowymi ustawieniami był

1 subgoal 
b : binop 
e1 : exp 
e2 : exp 
IHe1 : forall s : stack, 
     @eq (option stack) 
     (@fold_left (option stack) instr instrDenote' (compile e1) 
      (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e1) s)) 
IHe2 : forall s : stack, 
     @eq (option stack) 
     (@fold_left (option stack) instr instrDenote' (compile e2) 
      (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e2) s)) 
s : stack 
______________________________________(1/1) 
@eq (option stack) 
    (@fold_left (option stack) instr instrDenote' 
    (@cons instr (iBinop b) (@nil instr)) 
    (@fold_left (option stack) instr instrDenote' (compile e1) 
     (@Some (list nat) (@cons nat (expDenote e2) s)))) 
    (@Some (list nat) 
    (@cons nat (binopDenote b (expDenote e1) (expDenote e2)) s)) 

a błąd był

Error: 
Found no subterm matching "@fold_left (option stack) instr instrDenote' 
          (compile e1) 
          (@Some stack (@cons nat (expDenote e2) s))" in the current goal. 

Answer 1

Nawet z ustawieniami wyświetlania domyślnych subterm wydaje się pojawiać w cel, z Set Printing All włączona, to staje się jasne, że podokres nie pasuje do celu, ponieważ w bramce stack został rozłożony na list nat. Tak więc fold stack jest potrzebny, aby zmienić list nat z powrotem w stack w cel.

Wydaje się, że jako początkujący zostałem wyzwolony przez następujące składniki:

• unfold taktyka rozwija więcej definicji niż początkujący byłoby się spodziewać.

• Domyślne ustawienia wyświetlania (w CoqIDE w moim przypadku) mogą to ukryć, ponieważ składają niektóre terminy.

Dzięki Arthur Azevedo De Amorim za sugerowanie umożliwiając Set Printing All.