Coq non è in grado di trovare sottotermine quando si utilizza la tattica di riscrittura

Question

Sto provando a eseguire una prova modificata di compile_correct da first chapter di Programmazione certificata con tipi dipendenti. Nella mia versione, cerco di far uso del fatto che progDenote è una piega e di utilizzare un'ipotesi induttiva più debole nella dimostrazione del lemma principale in priving compile_correct.

Il codice che è identico con il libro è:

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. 

Poi ho definire la mia versione di prog_denote che è una piega sopra l'elenco delle istruzioni in un programma:

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 quindi prova a provare una versione più debole di compile_correct dal libro:

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)). 

La mia prova si rompe l'ultima riga, con lo Stato prova

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) 

E l'errore è

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

In questa fase la prova, sto facendo induzione sulla e, l'espressione in fase di compilazione, e si occupa del costruttore Binop di exp. Non capisco perché sto ricevendo questo errore, perché una volta che ho applicato IHe1 a expDenote e2 :: s non ci sono variabili vincolate. Questo sembra essere il solito problema con l'applicazione delle regole di riscrittura non funziona. Ho anche verificato che il termine che sto cercando di creare:

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

controlli di tipo.

Cos'altro può andare storto con una regola di riscrittura, quando la sottoespressione di cui si lamenta è chiaramente lì nell'obiettivo?

MODIFICA: come suggerito, ho modificato le impostazioni del display in coqide all'equivalente di Set Printing All. Ciò ha rivelato che il problema era che la definizione di stack era stata aperta a list nat in un punto dell'obiettivo, che impediva il riconoscimento del sottotema. L'obiettivo stampato con le nuove impostazioni è stato

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

E l'errore è stato

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

Anche se con le impostazioni di visualizzazione di default, il sottotermine sembra apparire in meta, con Set Printing All abilitato, diventa chiaro che il sottotema non corrisponde all'obiettivo perché nell'obiettivo, stack è stato aperto a list nat. Quindi è necessario fold stack per trasformare list nat in stack nell'obiettivo.

Sembra come un principiante ero inciampato dalla combinazione dei seguenti elementi:

• Il unfold tattica si svolge altre definizioni di un principiante si aspetta.

• Le impostazioni di visualizzazione predefinite (in CoqIDE nel mio caso) possono nasconderle perché vengono piegati alcuni termini.

Grazie a Arthur Azevedo De Amorim per aver suggerito di abilitare Set Printing All.