A walkthrough of an example from Chapter 2 of Certified Programming with Dependent Types by A. Chlipala where terms in one language (source language) are converted to terms in another language (target language) while preserving their meaning. Both languages are untyped.
Source and target language are defined within coq, along with a function to translate source language terms to corresponding terms in the target language. Finally, it is proven that the translation is correct.
Thanks a bunch to the people on coq zulip who helped me understand this. Mistakes are my own (and as usual, corrections much appreciated!).
(This blog post is quite verbose as output from coq is also included in generous measure.)
First, let's define a source language.
Let's say that it has the following requirements:
Plus and Mult.
Let's define the allowed binary operations (these will be used for the target language as well).
Inductive binop : Set := Plus | Mult.
ie, the allowed operations are addition (Plus) and
multiplication (Mult). Remember that these are names that
we gave and as of now they don't have any meaning. But we'll give them
meaning (with a binopDenote function).
(Only addition and multiplication operations are included in the source language to keep things simpler.
Subtraction of nat could lead to situations like
Compute Nat.sub 2 3. (* not a negative number *)
(*
= 0
: nat
*)
and division could result in stuff like
Compute Nat.div 3 2. (* not 1.5 *)
(*
= 1
: nat
*)
Compute Nat.div 3 0. (* not divide by zero error *)
(*
= 0
: nat
*)
because after all, nat represents natural numbers. )
Check Plus.
(*
Plus
: binop
*)
Now let's define the type of expressions, which consists of constants and binary operations.
Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.
Expressions need either be nat constants
(Const) or a binary operation taking two expressions to
return an expression.
Compute Const 3.
(*
= Const 3
: exp
*)
Compute Binop Plus (Const 3) (Const 4).
(*
= Binop Plus (Const 3) (Const 4)
: exp
*)
Okay, time to give meaning (semantics) to what we have defined so far
(we use denotational semantics). First, let's do it for
binop via a binopDenote function.
Definition binopDenote (op : binop) : nat -> nat -> nat :=
match op with
| Plus => plus (* Same as Nat.add *)
| Mult => mult (* Same as Nat.mul *)
end.
We map what we defined for the source language (our object language here) to corresponding values in Coq (our meta language).
(* Just an example. This is not the way this is meant to be used *)
Compute (binopDenote Plus) 3 4.
(*
= 7
: nat
*)
We can't use Const values yet as we haven't given
meaning to exp values at this point. Let's fix that a
expDenote function.
Fixpoint expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e1 e2 => (binopDenote op) (expDenote e1) (expDenote e2)
end.
Since nat is only type of constants in the source
language, the normalized value of any exp would be a
nat.
Now we can do
(* 3 + 4 *)
Compute expDenote (Binop Plus (Const 3) (Const 4)).
(*
= 7
: nat
*)
(* 3 + (4 * 2) +1 *)
Definition foo :=
(Binop Plus
(Binop Plus
(Const 3)
(Binop Mult
(Const 4)
(Const 2)))
(Const 1)).
Compute expDenote foo.
(*
= 12
: nat
*)
Source language has been defined. Let's define the target language next.
Let's say that our target language has the following properties:
nat values). Consists of a list of
instructions stored in a stack.Plus and Mult
Target language consists of instructions stored in the stack. The type of instructions may be defined as
Inductive instr : Set :=
| iConst : nat -> instr
| iBinop : binop -> instr.
iBinop doesn't take operands as parameters as the
operands will be obtained from the stack during evaluation.
Compute iConst 4.
(*
= iConst 4
: instr
*)
Compute iBinop Plus.
(*
= iBinop Plus
: instr
*)
Type of stack, which is just a list of nat values here,
may be defined as
Definition stack : Set := list nat.
where the head of the list is the top of the stack.
A small check to see if it's okay:
Check [3; 2]%list : stack.
(*
[3; 2] : stack
: stack
*)
Now let's give meaning to instr with a
instrDenote function.
Definition instrDenote (i : instr) (s : stack) : option stack :=
match i with
| iConst n => Some (n :: s)
| iBinop b =>
match s with
| (s2 :: s1 :: ss) =>
let nval := ((binopDenote b) s1 s2) in
Some (nval :: ss)
| _ => None (* Stack prematurely empty! *)
end
end.
If i is a binary operation (iBinop), it is
executed using operands obtained by popping two values from the stack
the result of which is pushed back into it. But if i is
constant (iConst), instrDenote merely pushes
the constant value into the stack.
Return type is option stack because sometimes problems
like stack underflow can happen and it may not be possible to evaluate
the instruction in which case None is returned.
We re-use the binop and binopDenote that we
had defined earlier as it's the same for both source and target
languages.
Right, let's give instrDenote a whirl.
Compute instrDenote (iConst 4) []%list.
(*
= Some [4]
: option stack
*)
Compute instrDenote (iBinop Plus) [3; 4]%list.
(*
= Some [7]
: option stack
*)
Compute instrDenote (iBinop Plus) [3]%list.
(*
= None
: option stack
*)
It seems to be working okay.
We could use a function to give meaning to a list of instructions all
at once. As a step towards that, let's define a type, program, which
represents a list of instr (after all, a program
is a list of instructions).
Definition prog : Set := list instr.
Small check:
Check [iConst 3; iBinop Plus; iBinop Mult]%list : prog.
(*
*[iConst 3; iBinop Plus; iBinop Mult] : prog
: prog
)
Now we give meaning to a prog:
Fixpoint progDenote (p : prog) (s : stack) : option stack :=
match p with
| (px::pxs) =>
match (instrDenote px s) with
| Some s' => progDenote pxs s'
| None => None
end
| _ => Some s
end.
In addition to a prog value, progDenote
takes a stack containing the values that the program might
need.
Giving progDenote a whirl,
Compute progDenote [iConst 3; iBinop Plus; iBinop Mult]%list [4; 5]%list.
(*
= Some [35]
: option stack
*)
Yep, looks alright.
We can now make a function to translate (or compile) source language terms to equivalent terms in the target language.
Fixpoint compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e1 e2 => (compile e2) ++ (compile e1) ++ [iBinop op]%list
end.
An example use:
Definition foo :=
(Binop Plus
(Binop Plus
(Const 3)
(Binop Mult
(Const 4)
(Const 2)))
(Const 1)).
Compute compile foo.
(*
= [iConst 3; iConst 4; iConst 2; iBinop Mult;
iBinop Plus; iConst 1; iBinop Plus]
: list instr
*)
So, to put all the definitions that we made so far together,
(** * Source language **)
Inductive binop : Set := Plus | Mult.
Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.
Definition binopDenote (op : binop) : nat -> nat -> nat :=
match op with
| Plus => plus (* Same as Nat.add *)
| Mult => mult (* Same as Nat.mul *)
end.
Fixpoint expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e1 e2 => (binopDenote op) (expDenote e1) (expDenote e2)
end.
(** * Target language **)
Inductive instr : Set :=
| iConst : nat -> instr
| iBinop : binop -> instr.
Definition stack : Set := list nat.
Definition instrDenote (i : instr) (s : stack) : option stack :=
match i with
| iConst n => Some (n :: s)
| iBinop b =>
match s with
| (s2 :: s1 :: ss) =>
let nval := ((binopDenote b) s1 s2) in
Some (nval :: ss)
| _ => None (* Stack prematurely empty! *)
end
end.
Definition prog : Set := list instr.
Fixpoint progDenote (p : prog) (s : stack) : option stack :=
match p with
| (px::pxs) =>
match (instrDenote px s) with
| Some s' => progDenote pxs s'
| None => None
end
| _ => Some s
end.
(** * Translation *)
Fixpoint compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e1 e2 => (compile e1) ++ (compile e2) ++ [iBinop op]%list
end.
Okay, we now have a way to translate source language terms to target language terms. Let's try proving that this translation is correct.
For this, it is sufficient to prove that
∀ (e : exp) (p : prog) (s : stack),
progDenote ((compile e) ++ p) s = progDenote p ((expDenote e)::s)
ie, the meaning of a program (ie, list instr) obtained
by compile-ing an exp, to which another
program p has been appended, when used with a stack
s is same as the meaning of p when having the
same s with the meaning of the same exp pushed
at the top of it.
Let's try proving that in Coq.
Theorem compile_correct : forall (e : exp) (p : prog) (s : stack),
progDenote ((compile e) ++ p) s = progDenote p ((expDenote e)::s).
Proof.
(* Goal:
1 subgoal
========================= (1 / 1)
forall (e : exp) (p : prog) (s : stack),
progDenote (compile e ++ p) s = progDenote p (expDenote e :: s)
*)
Doing induction on e.
induction e.
(*
2 subgoals
n : nat
========================= (1 / 2)
forall (p : prog) (s : stack),
progDenote (compile (Const n) ++ p) s =
progDenote p (expDenote (Const n) :: s)
========================= (2 / 2)
forall (p : prog) (s : stack),
progDenote (compile (Binop b e1 e2) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
*)
Now we got two (sub-)goals.
See how e : exp went away from the
forall.
An exp can be one of two things: Const or
Binop. Hence performing induction on e : exp
leads to two sub-goals, with each sub-goal having a possible
exp value.
When e : exp is replaced with a Const n,So,
progDenote (compile e ++ p) s = progDenote p (expDenote e :: s)
changes as follows:
| Old term | New e (e ↦) | New term |
|---------------------------------+---------------+-----------------------------------------------|
| progDenote (compile e ++ p) s = | | progDenote (compile (Const n) ++ p) s = |
| progDenote p (expDenote e :: s) | Const n | progDenote p (expDenote (Const n) :: s) |
|---------------------------------+---------------+-----------------------------------------------|
| progDenote (compile e ++ p) s = | | progDenote (compile (Binop b e1 e2) ++ p) s = |
| progDenote p (expDenote e :: s) | Binop b e1 e2 | progDenote p (expDenote (Binop b e1 e2) :: s) |
The goal is:
1 subgoal
(1 unfocused at this level)
n : nat
========================= (1 / 1)
forall (p : prog) (s : stack),
progDenote (compile (Const n) ++ p) s =
progDenote p (expDenote (Const n) :: s)
First, let's make the variables in the forall quantifier
free with intros.
- intros.
(*
1 subgoal
(1 unfocused at this level)
n : nat
p : prog
s : stack
========================= (1 / 1)
progDenote (compile (Const n) ++ p) s =
progDenote p (expDenote (Const n) :: s)
*)
The unfold tactic can replace 'an identifier with its
definition'. fold is for the other way around.
Replacing the occurrences of compile with its
definitions so that 'coq can see them' with unfold,
unfold compile.
(*
1 subgoal
(1 unfocused at this level)
n : nat
p : prog
s : stack
========================= (1 / 1)
progDenote ([iConst n] ++ p) s = progDenote p (expDenote (Const n) :: s)
*)
The progDenote (compile (Const n) ++ p) s changed to
progDenote ([iConst n] ++ p) s like
progDenote (compile (Const n) ++ p) s
↓
progDenote (
(fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e1 e2 => (compile e1) ++ (compile e2) ++ [iBinop op]%list
end)
(Const n) ++ p) s.
↓
progDenote ([iConst n]%list ++ p) s.
Let's see what simpl can make out of this:
simpl.
(*
1 subgoal
(1 unfocused at this level)
n : nat
p : prog
s : stack
========================= (1 / 1)
progDenote p (n :: s) = progDenote p (n :: s)
*)
simpl was able to make the following changes to the
goal:
| Old | New |
|-----------------------------------------+-----------------------|
| progDenote ([iConst n] ++ p) s | progDenote p (n :: s) |
| progDenote p (expDenote (Const n) :: s) | progDenote p (n :: s) |
The second change is straightforward as
expDenote (Const n) evaluates to to n.
The change to progDenote ([iConst n] ++ p) s is not that
straightforward. It looks something like a 'partial' evaluation of
progDenote. ⁵
That's because simpl
is not so simple as it sounds. It's sort of a special tactic. As the docs
suggest, it is a 'clever' tactic meant to give the most readable
result. (for example, a goal with a bunch of unfolded fixpoint
functions isn't so readable but their folded version is.)
simpl 'reduces a term to something still readable
instead of fully normalizing it'. ⁷
(That probably means complicated heuristics to determine what is
'readable' and what is not.)
Since by this point, both LHS and RHS of the goal are same, we can finish off this sub-goal with
reflexivity.
On to the second sub-goal!
The goal is:
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
========================= (1 / 1)
forall (p : prog) (s : stack),
progDenote (compile (Binop b e1 e2) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
Let's introduce the variables like in the other sub-goal,
- intros.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote (compile (Binop b e1 e2) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
*)
Replacing compile with its definitions using
unfold,
unfold compile.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote
(((fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]
| Binop op e0 e3 => compile e0 ++ compile e3 ++ [iBinop op]
end) e1 ++
(fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]
| Binop op e0 e3 => compile e0 ++ compile e3 ++ [iBinop op]
end) e2 ++ [iBinop b]) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
*)
e0 and e3 are names chosen by coq (since
e1 and e2 are names that are already
used).
progDenote (compile (Binop b e1 e2) ++ p) s changed
as
progDenote (compile (Binop b e1 e2) ++ p) s
↓
progDenote (
(fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e0 e3 => (compile e0) ++ (compile e3) ++ [iBinop op]%list
end)
(Binop b e1 e2) ++ p) s
↓
progDenote (
(compile e1) ++
(compile e2) ++
[iBinop b]%list ++
p) s
↓
progDenote (
(fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e0 e3 => (compile e0) ++ (compile e3) ++ [iBinop op]%list
end) e1 ++
(fix compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e0 e3 => (compile e0) ++ (compile e3) ++ [iBinop op]%list
end) e2 ++
[iBinop b]%list ++
p) s
Now, we fold compile back up.
It might seem pointless at first to do a fold right
after a unfold on the same function and one may feel
tempted to compare it with something like -2 + 2 of basic
arithmetic, something that changes nothing, but it isn't so.
Because here, unfold revealed what compile
is made up of, allowing coq to see deep into the definition of
compile itself.
If we do fold on compile now, coq will
readily change the goal to
progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
So,
fold compile.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (expDenote (Binop b e1 e2) :: s)
*)
The definitions of compile merely got replaced by the
name compile.
Unfolding expDenote next,
unfold expDenote.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s =
progDenote p
(binopDenote b
((fix expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3)
end) e1)
((fix expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3)
end) e2) :: s)
*)
The change in goal happened like
progDenote p (expDenote (Binop b e1 e2) :: s)
↓
progDenote p (
(fix expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3)
end)
(Binop b e1 e2) :: s)
↓
progDenote p (
(binopDenote b
(expDenote e1)
(expDenote e2)
) :: s)
↓
progDenote p (
(binopDenote b
((fix expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3)
end) e1)
((fix expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3)
end) e2)
) :: s)
Now folding expDenote back up,
fold expDenote.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
Now we need the help of a proof that attests to the associativity
property of list concatenation. Coq has a lemma for that built-in,
app_assoc_reverse, which is defined as:
app_assoc_reverse
: forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
Using app_assoc_reverse for a left-to-right rewrite,
rewrite app_assoc_reverse.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p) s =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
The goal changed from
progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s
| | | | |
+--------+ +----------------------+ +
l m n
to
progDenote (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p) s
| | | | |
+--------+ +----------------------+ +
l m n
Coming back to the proof, it's time for a few more rewrites…
rewrite IHe1.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote ((compile e2 ++ [iBinop b]) ++ p) (expDenote e1 :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
rewrite app_assoc_reverse.
(*
progDenote (compile e2 ++ [iBinop b] ++ p) (expDenote e1 :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
rewrite IHe2.
(*
progDenote ([iBinop b] ++ p) (expDenote e2 :: expDenote e1 :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
Unfolding only the first progDenote (the one in the LHS
of goal), evaluating and folding it back up (not really necessary, just
so that it will look nice. In fact, the proof can finish at this point
with a reflexivity) and finally finishing off the goal,
unfold progDenote at 1.
(*
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
(fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack :=
match p0 with
| [] => Some s0
| px :: pxs =>
match instrDenote px s0 with
| Some s' => progDenote pxs s'
| None => None
end
end) ([iBinop b] ++ p) (expDenote e2 :: expDenote e1 :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
simpl. (* the 'not-so-simple' simpl :) *)
(*
(fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack :=
match p0 with
| [] => Some s0
| px :: pxs =>
match instrDenote px s0 with
| Some s' => progDenote pxs s'
| None => None
end
end) p (binopDenote b (expDenote e1) (expDenote e2) :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
fold progDenote.
(*
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
*)
reflexivity.
(*
0 subgoals
All goals completed.
*)
And we're done! We've proven that the translation is indeed correct.
fold
tactic documentationunfold
tactic documentationAn overview of the proof steps along with the changing goals.
Second column has the goal after applying the tactic in the first column of the corresponding row.
| Step | Goal |
|----------------------------+--------------------------------------------------------------------------|
| | 1 subgoal |
| | |
| | |
| | ========================= (1 / 1) |
| | |
| | forall (e : exp) (p : prog) (s : stack), |
| | progDenote (compile e ++ p) s = progDenote p (expDenote e :: s) |
|----------------------------+--------------------------------------------------------------------------|
| induction e. | |
| (* | 2 subgoals |
| Induction on e. | |
| Generates 2 sub-goals. | n : nat |
| *) | |
| | ========================= (1 / 2) |
| | |
| | forall (p : prog) (s : stack), |
| | progDenote (compile (Const n) ++ p) s = |
| | progDenote p (expDenote (Const n) :: s) |
| | |
| | ========================= (2 / 2) |
| | |
| | forall (p : prog) (s : stack), |
| | progDenote (compile (Binop b e1 e2) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
| | |
| | |
|----------------------------+--------------------------------------------------------------------------|
| (* | 1 subgoal |
| Focusing on 1st sub-goal | (1 unfocused at this level) |
| *) | |
| | n : nat |
| | |
| | ========================= (1 / 1) |
| | |
| | forall (p : prog) (s : stack), |
| | progDenote (compile (Const n) ++ p) s = |
| | progDenote p (expDenote (Const n) :: s) |
| | |
|----------------------------+--------------------------------------------------------------------------|
| intros. | 1 subgoal |
| (* | (1 unfocused at this level) |
| Free variables | |
| *) | n : nat |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote (compile (Const n) ++ p) s = |
| | progDenote p (expDenote (Const n) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| unfold compile. | 1 subgoal |
| | (1 unfocused at this level) |
| | |
| | n : nat |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ([iConst n] ++ p) s = progDenote p (expDenote (Const n) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| simpl. | 1 subgoal |
| | (1 unfocused at this level) |
| | |
| | n : nat |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote p (n :: s) = progDenote p (n :: s) |
|----------------------------+--------------------------------------------------------------------------|
| reflexivity. | 0 subgoals |
| (* | (1 unfocused at this level) |
| 1 of 2 sub-goals complete | |
| *) | Next goal (use bullet '-'): |
| | |
| | forall (p : prog) (s : stack), |
| | progDenote (compile (Binop b e1 e2) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| (* | 1 subgoal |
| Focusing on 2nd sub-goal | |
| *) | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | |
| | ========================= (1 / 1) |
| | |
| | forall (p : prog) (s : stack), |
| | progDenote (compile (Binop b e1 e2) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| intros. | 1 subgoal |
| (* | |
| Free variables | b : binop |
| *) | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote (compile (Binop b e1 e2) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| unfold compile. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote |
| | (((fix compile (e : exp) : list instr := |
| | match e with |
| | │ Const n => [iConst n] |
| | │ Binop op e0 e3 => compile e0 ++ compile e3 ++ [iBinop op] |
| | end) e1 ++ |
| | (fix compile (e : exp) : list instr := |
| | match e with |
| | │ Const n => [iConst n] |
| | │ Binop op e0 e3 => compile e0 ++ compile e3 ++ [iBinop op] |
| | end) e2 ++ [iBinop b]) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| fold compile. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s = |
| | progDenote p (expDenote (Binop b e1 e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| unfold expDenote. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s = |
| | progDenote p |
| | (binopDenote b |
| | ((fix expDenote (e : exp) : nat := |
| | match e with |
| | │ Const n => n |
| | │ Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3) |
| | end) e1) |
| | ((fix expDenote (e : exp) : nat := |
| | match e with |
| | │ Const n => n |
| | │ Binop op e0 e3 => binopDenote op (expDenote e0) (expDenote e3) |
| | end) e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| fold expDenote. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ((compile e1 ++ compile e2 ++ [iBinop b]) ++ p) s = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| rewrite app_assoc_reverse. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote (compile e1 ++ (compile e2 ++ [iBinop b]) ++ p) s = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| rewrite IHe1. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ((compile e2 ++ [iBinop b]) ++ p) (expDenote e1 :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| rewrite app_assoc_reverse. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote (compile e2 ++ [iBinop b] ++ p) (expDenote e1 :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| rewrite IHe2. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote ([iBinop b] ++ p) (expDenote e2 :: expDenote e1 :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| unfold progDenote at 1. | 1 subgoal |
| (* | |
| Unfold only the first | b : binop |
| occurrence of progDenote | e1, e2 : exp |
| *) | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | (fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack := |
| | match p0 with |
| | │ [] => Some s0 |
| | │ px :: pxs => |
| | match instrDenote px s0 with |
| | │ Some s' => progDenote pxs s' |
| | │ None => None |
| | end |
| | end) ([iBinop b] ++ p) (expDenote e2 :: expDenote e1 :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| simpl. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | (fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack := |
| | match p0 with |
| | │ [] => Some s0 |
| | │ px :: pxs => |
| | match instrDenote px s0 with |
| | │ Some s' => progDenote pxs s' |
| | │ None => None |
| | end |
| | end) p (binopDenote b (expDenote e1) (expDenote e2) :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| fold progDenote. | 1 subgoal |
| | |
| | b : binop |
| | e1, e2 : exp |
| | IHe1 : forall (p : prog) (s : stack), |
| | progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) |
| | IHe2 : forall (p : prog) (s : stack), |
| | progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) |
| | p : prog |
| | s : stack |
| | |
| | ========================= (1 / 1) |
| | |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) = |
| | progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
|----------------------------+--------------------------------------------------------------------------|
| reflexivity. | 0 subgoals |
| (* | |
| 2 of 2 sub-goals complete | All goals completed. |
| *) | |
|----------------------------+--------------------------------------------------------------------------|
So, the whole proof in copy-pastable form is:
Theorem compile_correct : forall (e : exp) (p : prog) (s : stack),
progDenote ((compile e) ++ p) s = progDenote p ((expDenote e)::s).
Proof.
induction e.
- intros.
unfold compile.
simpl.
reflexivity.
- intros.
unfold compile.
fold compile.
unfold expDenote.
fold expDenote.
rewrite app_assoc_reverse.
rewrite IHe1.
rewrite app_assoc_reverse.
rewrite IHe2.
unfold progDenote at 1.
simpl.
fold progDenote.
reflexivity.
Qed.