Coq, yeniden yazma taktiğini kullanırken alt grubu bulamıyor

Question

first chapter'dan Bağımlı Türlerle Sertifikalı Programlamanın değiştirilmiş bir sürümünü compile_correct yapmaya çalışıyorum. Benim versiyonumda, progDenote'un bir katlama olduğu gerçeğini kullanmaya çalışıyorum ve compile_correct'u imzalamada ana lizamanın kanıtında daha zayıf bir indüktif hipotez kullanın.

kitap ile aynıdır kod şudur:

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:

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. 

Sonra bir programda yönergeleri listesinin üzerinde yönlüdür prog_denote benim kendi versiyonunu tanımlar daha sonra

'ün daha zayıf bir sürümünü ispatlamaya çalışın.Ben e üzerinde indüksiyon yapıyorum, My geçirmez geçirmez duruma

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) 

ile son satırında kırar Ve hata

kanıtı bu aşamada

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

olduğunu ifade Derlenmekte, ve exp'un Binop yapıcısı ile ilgilenir. Neden bu hatayı alıyorum anlamıyorum, çünkü bir kez IHe1expDenote e2 :: s başvurduğumda, hiçbir bağımlı değişken yoktur. Bu, yeniden yazma kurallarının uygulanmasında olağan bir sorun gibi görünüyor. Ayrıca, oluşturmaya çalıştığım terimi şu şekilde kontrol ettim:

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

tip çekler.

Tekrar yazdığı bir alt yazı, hedefte açıkça belirtildiği zaman, yeniden yazma kuralında ters gidebilir başka neler olabilir?

DÜZENLEME: Önerilen şekilde, ekran ayarlarını, Tümünü Ayarla Yazdır öğesinin eşdeğeri olarak değiştirdim. Bu, stack tanımının hedefte tek bir yerde list nat açılmasının ortaya çıkması sorununu ortaya çıkarmış ve bu da alt testin tanınmasını engellemiştir. yeni ayarlarla baskılı gol

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

oldu Ve hata Set Printing All etkinken, o ortaya çıkıyor,

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

Hatta varsayılan görüntü ayarları ile birlikte, subterm golü görünmesini görünüyor oldu alt hedef, hedefle eşleşmiyor çünkü hedefte stack, list nat'a açıldı. Bu nedenle, list nat'u stack hedefe geri döndürmek için gereklidir.

Bir acemi olarak aşağıdaki kombinasyonu ile takıldı gibi görünüyor:

• unfold taktik bir acemi beklenebilir daha tanımlara gözler önüne serilir.

• Varsayılan ekran ayarları (benim durumumdaki CoqIDE içinde), bazı terimleri katladıkları için bunu gizleyebilir.

Set Printing All'u etkinleştirmeyi öneren Arthur Azevedo De Amorim'e teşekkürler.