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
.Coq nie może znaleźć subterm podczas stosowania taktyki przepisywania
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.
Czy możesz dodać to, co zostanie wydrukowane, jeśli włączysz opcję "Set Printing All"? (Po prostu dodaj tę linię przed dowodem). –
Zrobione, dziękuję za sugestię. Teraz widzę, że wyrażenia są różne, ponieważ 'stack' pojawia się jako' list nat' w celu. Nie wiem wystarczająco dużo o Coq, aby zrozumieć, dlaczego definicja "stosu" została rozszerzona w ten cel (i dlaczego jest nadal wyświetlany jako "stos" z domyślnymi ustawieniami drukowania). –
Teraz, gdy widzę, co się stało, 'fold stack' rozwiązuje problem. Z tego, co przeczytałem, taktyka 'unfold' nie jest dla początkującego zupełnie oczywista, jeśli chodzi o to, jak głęboko rozwija ona ekspresję, więc w połączeniu z domyślnymi ustawieniami wyświetlania wydaje się być przyczyną problemu. –