Coq không thể tìm thấy subterm khi sử dụng chiến thuật viết lại

Question

Tôi đang cố gắng để làm một bằng chứng sửa đổi của compile_correct từ first chapter của lập trình được chứng nhận với các loại phụ thuộc. Trong phiên bản của tôi, tôi cố gắng sử dụng thực tế rằng progDenote là một lần, và sử dụng một giả thuyết quy nạp yếu hơn trong bằng chứng về bổ đề chính trong tư nhân compile_correct.

Mã đó là giống hệt với cuốn sách là:

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. 

Sau đó, tôi xác định phiên bản riêng của tôi về prog_denote mà là một lần trong danh sách các hướng dẫn trong một chương trình:

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

tôi sau đó cố gắng chứng minh phiên bản yếu hơn của compile_correct từ sách:

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

bằng chứng của tôi phá vỡ ở dòng cuối cùng, với tình trạng chứng

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) 

Và lỗi là

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

Ở giai đoạn này trong chứng minh, tôi đang làm cảm ứng trên e, khái niệm được biên soạn, và xử lý công cụ xây dựng Binop của exp. Tôi không hiểu tại sao tôi gặp lỗi này, bởi vì khi tôi áp dụng IHe1 đến expDenote e2 :: s, không có biến nào bị ràng buộc. Điều này có vẻ là vấn đề thường gặp khi áp dụng quy tắc viết lại không hoạt động. Tôi cũng đã kiểm tra cụm từ mà tôi đang cố gắng tạo:

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

kiểm tra loại.

Điều gì khác có thể xảy ra với quy tắc viết lại, khi biểu đạt phụ mà nó phàn nàn rõ ràng là có trong mục tiêu?

CHỈNH SỬA: Như đã đề xuất, tôi đã thay đổi cài đặt hiển thị ở dạng coqide thành tương đương với Đặt tất cả in. Điều này cho thấy vấn đề là định nghĩa của stack đã được mở ra thành list nat tại một nơi trong mục tiêu, điều này đã ngăn không cho nhận được subterm. Mục đích in với các thiết lập mới là

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

Và lỗi là

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

Mặc dù với các thiết lập hiển thị mặc định, các subterm dường như xuất hiện trong mục tiêu, với Set Printing All được kích hoạt, nó trở nên rõ ràng rằng các subterm không phù hợp với mục tiêu bởi vì trong mục tiêu, stack đã được mở ra để list nat. Vì vậy, fold stack là cần thiết để biến list nat trở lại thành stack trong mục tiêu.

Nó có vẻ như là một người mới bắt đầu tôi đã vấp lên bởi sự kết hợp các nội dung sau:

• Các unfold chiến thuật mở ra nhiều định nghĩa hơn là một người mới bắt đầu mong đợi.

• Cài đặt hiển thị mặc định (trong CoqIDE trong trường hợp của tôi) có thể ẩn điều này vì chúng gấp một số cụm từ.

Cảm ơn Arthur Azevedo De Amorim đã đề xuất kích hoạt Set Printing All.