File 8
Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
From Coq Require Import Strings.String.
From Coq Require Import ZArith.ZArith.
Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c
.
Hint Constructors Rstar.
Lemma RTrans {T : Type} {P : T -> T -> Prop} {a b c : T} : Rstar P a b -> Rstar P b c -> Rstar P a c.
Proof.
elim; eauto.
Qed.
Definition ident := string.
Inductive aexp : Type :=
| CONST (n: Z)
| VAR (x: ident)
| PLUS (a1: aexp) (a2: aexp)
| MINUS (a1: aexp) (a2: aexp). Hint Constructors aexp.
Definition store : Type := ident -> Z.
Fixpoint aeval (s: store) (a: aexp) : Z :=
match a with
| CONST n => n
| VAR x => s x
| PLUS a1 a2 => aeval s a1 + aeval s a2
| MINUS a1 a2 => aeval s a1 - aeval s a2
end.
Fixpoint free_in_aexp (x: ident) (a: aexp) : Prop :=
match a with
| CONST n => False
| VAR y => y = x
| PLUS a1 a2 | MINUS a1 a2 => free_in_aexp x a1 \/ free_in_aexp x a2
end.
Theorem aeval_free:
forall s1 s2 a,
(forall x, free_in_aexp x a -> s1 x = s2 x) ->
aeval s1 a = aeval s2 a.
Admitted.
Inductive bexp : Type :=
| TRUE
| FALSE
| EQUAL (a1: aexp) (a2: aexp)
| LESSEQUAL (a1: aexp) (a2: aexp)
| NOT (b1: bexp)
| AND (b1: bexp) (b2: bexp). Hint Constructors bexp.
Fixpoint beval (s: store) (b: bexp) : bool :=
match b with
| TRUE => true
| FALSE => false
| EQUAL a1 a2 => (aeval s a1 =? aeval s a2)%Z
| LESSEQUAL a1 a2 => (aeval s a1 <=? aeval s a2)%Z
| NOT b1 => negb (beval s b1)
| AND b1 b2 => beval s b1 && beval s b2
end.
Definition NOTEQUAL (a1 a2: aexp) : bexp := NOT (EQUAL a1 a2).
Definition GREATEREQUAL (a1 a2: aexp) : bexp := LESSEQUAL a2 a1.
Definition GREATER (a1 a2: aexp) : bexp := NOT (LESSEQUAL a1 a2).
Definition LESS (a1 a2: aexp) : bexp := GREATER a2 a1.
Definition OR (b1 b2: bexp) : bexp := NOT (AND (NOT b1) (NOT b2)).
Inductive com: Type :=
| SKIP
| ASSIGN (x: ident) (a: aexp)
| SEQ (c1: com) (c2: com)
| IFTHENELSE (b: bexp) (c1: com) (c2: com)
| WHILE (b: bexp) (c1: com). Hint Constructors com.
Infix ";;" := SEQ (at level 80, right associativity).
Definition update (x: ident) (v: Z) (s: store) : store :=
fun y => if string_dec x y then v else s y.
Fail Fixpoint cexec (s: store) (c: com) : store :=
match c with
| SKIP => s
| ASSIGN x a => update x (aeval s a) s
| SEQ c1 c2 => let s' := cexec s c1 in cexec s' c2
| IFTHENELSE b c1 c2 => if beval s b then cexec s c1 else cexec s c2
| WHILE b c1 =>
if beval s b
then (let s' := cexec s c1 in cexec s' (WHILE b c1))
else s
end.
Inductive cexec: store -> com -> store -> Prop :=
| cexec_skip: forall s,
cexec s SKIP s
| cexec_assign: forall s x a,
cexec s (ASSIGN x a) (update x (aeval s a) s)
| cexec_seq: forall c1 c2 s s' s'',
cexec s c1 s' -> cexec s' c2 s'' ->
cexec s (SEQ c1 c2) s''
| cexec_ifthenelse: forall b c1 c2 s s',
cexec s (if beval s b then c1 else c2) s' ->
cexec s (IFTHENELSE b c1 c2) s'
| cexec_while_done: forall b c s,
beval s b = false ->
cexec s (WHILE b c) s
| cexec_while_loop: forall b c s s' s'',
beval s b = true -> cexec s c s' -> cexec s' (WHILE b c) s'' ->
cexec s (WHILE b c) s''.
Hint Constructors cexec.
Fixpoint cexec_bounded (fuel: nat) (s: store) (c: com) : option store :=
match fuel with
| O => None
| S fuel' =>
match c with
| SKIP => Some s
| ASSIGN x a => Some (update x (aeval s a) s)
| SEQ c1 c2 =>
match cexec_bounded fuel' s c1 with
| None => None
| Some s' => cexec_bounded fuel' s' c2
end
| IFTHENELSE b c1 c2 =>
if beval s b then cexec_bounded fuel' s c1 else cexec_bounded fuel' s c2
| WHILE b c1 =>
if beval s b then
match cexec_bounded fuel' s c1 with
| None => None
| Some s' => cexec_bounded fuel' s' (WHILE b c1)
end
else Some s
end
end.
Ltac invert H := inversion H; subst; eauto.
Inductive red: com * store -> com * store -> Prop :=
| red_assign: forall x a s,
red (ASSIGN x a, s) (SKIP, update x (aeval s a) s)
| red_seq_done: forall c s,
red (SEQ SKIP c, s) (c, s)
| red_seq_step: forall c1 c s1 c2 s2,
red (c1, s1) (c2, s2) ->
red (SEQ c1 c, s1) (SEQ c2 c, s2)
| red_ifthenelse: forall b c1 c2 s,
red (IFTHENELSE b c1 c2, s) ((if beval s b then c1 else c2), s)
| red_while_done: forall b c s,
beval s b = false ->
red (WHILE b c, s) (SKIP, s)
| red_while_loop: forall b c s,
beval s b = true ->
red (WHILE b c, s) (SEQ c (WHILE b c), s).
Hint Constructors red.
Tactic Notation "invert" := let x := fresh in move=> x; invert x.
Definition irred {A : Type} (R : A -> A -> Prop) (a : A) := forall b, ~(R a b).
Inductive instr : Type :=
| Iconst (n: Z)
| Ivar (x: ident)
| Isetvar (x: ident)
| Iadd
| Iopp
| Ibranch (d: Z)
| Ibeq (d1: Z) (d0: Z)
| Ible (d1: Z) (d0: Z)
| Ihalt.
Definition code := seq instr.
Definition codelen (c: code) : Z := Z.of_nat (size c).
Definition stack : Type := seq Z.
Definition config : Type := (Z * stack * store)%type.
Fixpoint instr_at (C: code) (pc: Z) : option instr :=
match C with
| nil => None
| i :: C' => if pc =? 0 then Some i else instr_at C' (pc - 1)
end % Z.
Open Scope Z.
Inductive transition (C: code): config -> config -> Prop :=
| trans_const: forall pc stk s n,
instr_at C pc = Some(Iconst n) ->
transition C (pc , stk , s)
(pc + 1, n :: stk, s)
| trans_var: forall pc stk s x,
instr_at C pc = Some(Ivar x) ->
transition C (pc , stk , s)
(pc + 1, s x :: stk, s)
| trans_setvar: forall pc stk s x n,
instr_at C pc = Some(Isetvar x) ->
transition C (pc , n :: stk, s)
(pc + 1, stk , update x n s)
| trans_add: forall pc stk s n1 n2,
instr_at C pc = Some(Iadd) ->
transition C (pc , n2 :: n1 :: stk , s)
(pc + 1, (n1 + n2) :: stk, s)
| trans_opp: forall pc stk s n,
instr_at C pc = Some(Iopp) ->
transition C (pc , n :: stk , s)
(pc + 1, (- n) :: stk, s)
| trans_branch: forall pc stk s d pc',
instr_at C pc = Some(Ibranch d) ->
pc' = pc + 1 + d ->
transition C (pc , stk, s)
(pc', stk, s)
| trans_beq: forall pc stk s d1 d0 n1 n2 pc',
instr_at C pc = Some(Ibeq d1 d0) ->
pc' = pc + 1 + (if n1 =? n2 then d1 else d0) ->
transition C (pc , n2 :: n1 :: stk, s)
(pc', stk , s)
| trans_ble: forall pc stk s d1 d0 n1 n2 pc',
instr_at C pc = Some(Ible d1 d0) ->
pc' = pc + 1 + (if n1 <=? n2 then d1 else d0) ->
transition C (pc , n2 :: n1 :: stk, s)
(pc', stk , s).
Definition transitions (C: code): config -> config -> Prop :=
Rstar (transition C).
Definition machine_terminates (C: code) (s_init: store) (s_final: store) : Prop :=
exists pc, transitions C (0, nil, s_init) (pc, nil, s_final)
/\ instr_at C pc = Some Ihalt.
Inductive machine_result : Type :=
| Timeout
| Stuck
| Terminates (s: store).
Fixpoint mach_interp (C: code) (fuel: nat)
(pc: Z) (stk: stack) (s: store) : machine_result :=
match fuel with
| O => Timeout
| S fuel' =>
match instr_at C pc, stk with
| Some Ihalt, nil => Terminates s
| Some (Iconst n), stk => mach_interp C fuel' (pc + 1) (n :: stk) s
| _, _ => Stuck
end
end.
Fixpoint compile_aexp (a: aexp) : code :=
match a with
| CONST n => Iconst n :: nil
| VAR x => Ivar x :: nil
| PLUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iadd :: nil
| MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iopp :: Iadd :: nil
end.
Fixpoint compile_bexp (b: bexp) (d1: Z) (d0: Z) : code :=
match b with
| TRUE => if d1 =? 0 then nil else Ibranch d1 :: nil
| FALSE => if d0 =? 0 then nil else Ibranch d0 :: nil
| EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ibeq d1 d0 :: nil
| LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ible d1 d0 :: nil
| NOT b1 => compile_bexp b1 d0 d1
| AND b1 b2 =>
let code2 := compile_bexp b2 d1 d0 in
let code1 := compile_bexp b1 0 (codelen code2 + d0) in
code1 ++ code2
end.
Fixpoint compile_com (c: com) : code :=
match c with
| SKIP =>
nil
| ASSIGN x a =>
compile_aexp a ++ Isetvar x :: nil
| SEQ c1 c2 =>
compile_com c1 ++ compile_com c2
| IFTHENELSE b ifso ifnot =>
let code_ifso := compile_com ifso in
let code_ifnot := compile_com ifnot in
compile_bexp b 0 (codelen code_ifso + 1)
++ code_ifso
++ Ibranch (codelen code_ifnot)
:: code_ifnot
| WHILE b body =>
let code_body := compile_com body in
let code_test := compile_bexp b 0 (codelen code_body + 1) in
code_test
++ code_body
++ Ibranch (- (codelen code_test + codelen code_body + 1)) :: nil
end.
Inductive code_at: code -> Z -> code -> Prop :=
| code_at_intro: forall C1 C2 C3 pc,
pc = codelen C1 ->
code_at (C1 ++ C2 ++ C3) pc C2.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
From Coq Require Import Strings.String.
From Coq Require Import ZArith.ZArith.
Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c
.
Hint Constructors Rstar.
Lemma RTrans {T : Type} {P : T -> T -> Prop} {a b c : T} : Rstar P a b -> Rstar P b c -> Rstar P a c.
Proof.
elim; eauto.
Qed.
Definition ident := string.
Inductive aexp : Type :=
| CONST (n: Z)
| VAR (x: ident)
| PLUS (a1: aexp) (a2: aexp)
| MINUS (a1: aexp) (a2: aexp). Hint Constructors aexp.
Definition store : Type := ident -> Z.
Fixpoint aeval (s: store) (a: aexp) : Z :=
match a with
| CONST n => n
| VAR x => s x
| PLUS a1 a2 => aeval s a1 + aeval s a2
| MINUS a1 a2 => aeval s a1 - aeval s a2
end.
Fixpoint free_in_aexp (x: ident) (a: aexp) : Prop :=
match a with
| CONST n => False
| VAR y => y = x
| PLUS a1 a2 | MINUS a1 a2 => free_in_aexp x a1 \/ free_in_aexp x a2
end.
Theorem aeval_free:
forall s1 s2 a,
(forall x, free_in_aexp x a -> s1 x = s2 x) ->
aeval s1 a = aeval s2 a.
Admitted.
Inductive bexp : Type :=
| TRUE
| FALSE
| EQUAL (a1: aexp) (a2: aexp)
| LESSEQUAL (a1: aexp) (a2: aexp)
| NOT (b1: bexp)
| AND (b1: bexp) (b2: bexp). Hint Constructors bexp.
Fixpoint beval (s: store) (b: bexp) : bool :=
match b with
| TRUE => true
| FALSE => false
| EQUAL a1 a2 => (aeval s a1 =? aeval s a2)%Z
| LESSEQUAL a1 a2 => (aeval s a1 <=? aeval s a2)%Z
| NOT b1 => negb (beval s b1)
| AND b1 b2 => beval s b1 && beval s b2
end.
Definition NOTEQUAL (a1 a2: aexp) : bexp := NOT (EQUAL a1 a2).
Definition GREATEREQUAL (a1 a2: aexp) : bexp := LESSEQUAL a2 a1.
Definition GREATER (a1 a2: aexp) : bexp := NOT (LESSEQUAL a1 a2).
Definition LESS (a1 a2: aexp) : bexp := GREATER a2 a1.
Definition OR (b1 b2: bexp) : bexp := NOT (AND (NOT b1) (NOT b2)).
Inductive com: Type :=
| SKIP
| ASSIGN (x: ident) (a: aexp)
| SEQ (c1: com) (c2: com)
| IFTHENELSE (b: bexp) (c1: com) (c2: com)
| WHILE (b: bexp) (c1: com). Hint Constructors com.
Infix ";;" := SEQ (at level 80, right associativity).
Definition update (x: ident) (v: Z) (s: store) : store :=
fun y => if string_dec x y then v else s y.
Fail Fixpoint cexec (s: store) (c: com) : store :=
match c with
| SKIP => s
| ASSIGN x a => update x (aeval s a) s
| SEQ c1 c2 => let s' := cexec s c1 in cexec s' c2
| IFTHENELSE b c1 c2 => if beval s b then cexec s c1 else cexec s c2
| WHILE b c1 =>
if beval s b
then (let s' := cexec s c1 in cexec s' (WHILE b c1))
else s
end.
Inductive cexec: store -> com -> store -> Prop :=
| cexec_skip: forall s,
cexec s SKIP s
| cexec_assign: forall s x a,
cexec s (ASSIGN x a) (update x (aeval s a) s)
| cexec_seq: forall c1 c2 s s' s'',
cexec s c1 s' -> cexec s' c2 s'' ->
cexec s (SEQ c1 c2) s''
| cexec_ifthenelse: forall b c1 c2 s s',
cexec s (if beval s b then c1 else c2) s' ->
cexec s (IFTHENELSE b c1 c2) s'
| cexec_while_done: forall b c s,
beval s b = false ->
cexec s (WHILE b c) s
| cexec_while_loop: forall b c s s' s'',
beval s b = true -> cexec s c s' -> cexec s' (WHILE b c) s'' ->
cexec s (WHILE b c) s''.
Hint Constructors cexec.
Fixpoint cexec_bounded (fuel: nat) (s: store) (c: com) : option store :=
match fuel with
| O => None
| S fuel' =>
match c with
| SKIP => Some s
| ASSIGN x a => Some (update x (aeval s a) s)
| SEQ c1 c2 =>
match cexec_bounded fuel' s c1 with
| None => None
| Some s' => cexec_bounded fuel' s' c2
end
| IFTHENELSE b c1 c2 =>
if beval s b then cexec_bounded fuel' s c1 else cexec_bounded fuel' s c2
| WHILE b c1 =>
if beval s b then
match cexec_bounded fuel' s c1 with
| None => None
| Some s' => cexec_bounded fuel' s' (WHILE b c1)
end
else Some s
end
end.
Ltac invert H := inversion H; subst; eauto.
Inductive red: com * store -> com * store -> Prop :=
| red_assign: forall x a s,
red (ASSIGN x a, s) (SKIP, update x (aeval s a) s)
| red_seq_done: forall c s,
red (SEQ SKIP c, s) (c, s)
| red_seq_step: forall c1 c s1 c2 s2,
red (c1, s1) (c2, s2) ->
red (SEQ c1 c, s1) (SEQ c2 c, s2)
| red_ifthenelse: forall b c1 c2 s,
red (IFTHENELSE b c1 c2, s) ((if beval s b then c1 else c2), s)
| red_while_done: forall b c s,
beval s b = false ->
red (WHILE b c, s) (SKIP, s)
| red_while_loop: forall b c s,
beval s b = true ->
red (WHILE b c, s) (SEQ c (WHILE b c), s).
Hint Constructors red.
Tactic Notation "invert" := let x := fresh in move=> x; invert x.
Definition irred {A : Type} (R : A -> A -> Prop) (a : A) := forall b, ~(R a b).
Inductive instr : Type :=
| Iconst (n: Z)
| Ivar (x: ident)
| Isetvar (x: ident)
| Iadd
| Iopp
| Ibranch (d: Z)
| Ibeq (d1: Z) (d0: Z)
| Ible (d1: Z) (d0: Z)
| Ihalt.
Definition code := seq instr.
Definition codelen (c: code) : Z := Z.of_nat (size c).
Definition stack : Type := seq Z.
Definition config : Type := (Z * stack * store)%type.
Fixpoint instr_at (C: code) (pc: Z) : option instr :=
match C with
| nil => None
| i :: C' => if pc =? 0 then Some i else instr_at C' (pc - 1)
end % Z.
Open Scope Z.
Inductive transition (C: code): config -> config -> Prop :=
| trans_const: forall pc stk s n,
instr_at C pc = Some(Iconst n) ->
transition C (pc , stk , s)
(pc + 1, n :: stk, s)
| trans_var: forall pc stk s x,
instr_at C pc = Some(Ivar x) ->
transition C (pc , stk , s)
(pc + 1, s x :: stk, s)
| trans_setvar: forall pc stk s x n,
instr_at C pc = Some(Isetvar x) ->
transition C (pc , n :: stk, s)
(pc + 1, stk , update x n s)
| trans_add: forall pc stk s n1 n2,
instr_at C pc = Some(Iadd) ->
transition C (pc , n2 :: n1 :: stk , s)
(pc + 1, (n1 + n2) :: stk, s)
| trans_opp: forall pc stk s n,
instr_at C pc = Some(Iopp) ->
transition C (pc , n :: stk , s)
(pc + 1, (- n) :: stk, s)
| trans_branch: forall pc stk s d pc',
instr_at C pc = Some(Ibranch d) ->
pc' = pc + 1 + d ->
transition C (pc , stk, s)
(pc', stk, s)
| trans_beq: forall pc stk s d1 d0 n1 n2 pc',
instr_at C pc = Some(Ibeq d1 d0) ->
pc' = pc + 1 + (if n1 =? n2 then d1 else d0) ->
transition C (pc , n2 :: n1 :: stk, s)
(pc', stk , s)
| trans_ble: forall pc stk s d1 d0 n1 n2 pc',
instr_at C pc = Some(Ible d1 d0) ->
pc' = pc + 1 + (if n1 <=? n2 then d1 else d0) ->
transition C (pc , n2 :: n1 :: stk, s)
(pc', stk , s).
Definition transitions (C: code): config -> config -> Prop :=
Rstar (transition C).
Definition machine_terminates (C: code) (s_init: store) (s_final: store) : Prop :=
exists pc, transitions C (0, nil, s_init) (pc, nil, s_final)
/\ instr_at C pc = Some Ihalt.
Inductive machine_result : Type :=
| Timeout
| Stuck
| Terminates (s: store).
Fixpoint mach_interp (C: code) (fuel: nat)
(pc: Z) (stk: stack) (s: store) : machine_result :=
match fuel with
| O => Timeout
| S fuel' =>
match instr_at C pc, stk with
| Some Ihalt, nil => Terminates s
| Some (Iconst n), stk => mach_interp C fuel' (pc + 1) (n :: stk) s
| _, _ => Stuck
end
end.
Fixpoint compile_aexp (a: aexp) : code :=
match a with
| CONST n => Iconst n :: nil
| VAR x => Ivar x :: nil
| PLUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iadd :: nil
| MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iopp :: Iadd :: nil
end.
Fixpoint compile_bexp (b: bexp) (d1: Z) (d0: Z) : code :=
match b with
| TRUE => if d1 =? 0 then nil else Ibranch d1 :: nil
| FALSE => if d0 =? 0 then nil else Ibranch d0 :: nil
| EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ibeq d1 d0 :: nil
| LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ible d1 d0 :: nil
| NOT b1 => compile_bexp b1 d0 d1
| AND b1 b2 =>
let code2 := compile_bexp b2 d1 d0 in
let code1 := compile_bexp b1 0 (codelen code2 + d0) in
code1 ++ code2
end.
Fixpoint compile_com (c: com) : code :=
match c with
| SKIP =>
nil
| ASSIGN x a =>
compile_aexp a ++ Isetvar x :: nil
| SEQ c1 c2 =>
compile_com c1 ++ compile_com c2
| IFTHENELSE b ifso ifnot =>
let code_ifso := compile_com ifso in
let code_ifnot := compile_com ifnot in
compile_bexp b 0 (codelen code_ifso + 1)
++ code_ifso
++ Ibranch (codelen code_ifnot)
:: code_ifnot
| WHILE b body =>
let code_body := compile_com body in
let code_test := compile_bexp b 0 (codelen code_body + 1) in
code_test
++ code_body
++ Ibranch (- (codelen code_test + codelen code_body + 1)) :: nil
end.
Inductive code_at: code -> Z -> code -> Prop :=
| code_at_intro: forall C1 C2 C3 pc,
pc = codelen C1 ->
code_at (C1 ++ C2 ++ C3) pc C2.
Exercise 1. Prove some basic lemmas.
Lemma codelen_cons:
forall i c, codelen (i :: c) = codelen c + 1.
Proof.
Admitted.
Lemma codelen_app:
forall c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2.
Proof.
Admitted.
Lemma instr_at_app:
forall i c2 c1 pc,
pc = codelen c1 ->
instr_at (c1 ++ i :: c2) pc = Some i.
Proof.
Admitted.
Lemma code_at_head:
forall C pc i C',
code_at C pc (i :: C') ->
instr_at C pc = Some i.
Proof.
Admitted.
Lemma code_at_tail:
forall C pc i C',
code_at C pc (i :: C') ->
code_at C (pc + 1) C'.
Proof.
Admitted.
Lemma code_at_app_left:
forall C pc C1 C2,
code_at C pc (C1 ++ C2) ->
code_at C pc C1.
Proof.
Admitted.
Lemma code_at_app_right:
forall C pc C1 C2,
code_at C pc (C1 ++ C2) ->
code_at C (pc + codelen C1) C2.
Proof.
Admitted.
Lemma code_at_app_right2:
forall C pc C1 C2 C3,
code_at C pc (C1 ++ C2 ++ C3) ->
code_at C (pc + codelen C1) C2.
Proof.
Admitted.
Lemma code_at_nil:
forall C pc C1,
code_at C pc C1 -> code_at C pc nil.
Proof.
Admitted.
Lemma instr_at_code_at_nil:
forall C pc i, instr_at C pc = Some i -> code_at C pc nil.
Proof.
Admitted.
forall i c, codelen (i :: c) = codelen c + 1.
Proof.
Admitted.
Lemma codelen_app:
forall c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2.
Proof.
Admitted.
Lemma instr_at_app:
forall i c2 c1 pc,
pc = codelen c1 ->
instr_at (c1 ++ i :: c2) pc = Some i.
Proof.
Admitted.
Lemma code_at_head:
forall C pc i C',
code_at C pc (i :: C') ->
instr_at C pc = Some i.
Proof.
Admitted.
Lemma code_at_tail:
forall C pc i C',
code_at C pc (i :: C') ->
code_at C (pc + 1) C'.
Proof.
Admitted.
Lemma code_at_app_left:
forall C pc C1 C2,
code_at C pc (C1 ++ C2) ->
code_at C pc C1.
Proof.
Admitted.
Lemma code_at_app_right:
forall C pc C1 C2,
code_at C pc (C1 ++ C2) ->
code_at C (pc + codelen C1) C2.
Proof.
Admitted.
Lemma code_at_app_right2:
forall C pc C1 C2 C3,
code_at C pc (C1 ++ C2 ++ C3) ->
code_at C (pc + codelen C1) C2.
Proof.
Admitted.
Lemma code_at_nil:
forall C pc C1,
code_at C pc C1 -> code_at C pc nil.
Proof.
Admitted.
Lemma instr_at_code_at_nil:
forall C pc i, instr_at C pc = Some i -> code_at C pc nil.
Proof.
Admitted.
Exercise 2. Prove the correctness of compile_aexp
Hint: Prove this by induction over a.
Lemma compile_aexp_correct:
forall C s a pc stk,
code_at C pc (compile_aexp a) ->
transitions C
(pc, stk, s)
(pc + codelen (compile_aexp a), aeval s a :: stk, s).
Proof.
Admitted.
Exercise 3. Prove the correctness of compile_bexp
Hint: Prove this by induction over b.
Lemma compile_bexp_correct:
forall C s b d1 d0 pc stk,
code_at C pc (compile_bexp b d1 d0) ->
transitions C
(pc, stk, s)
(pc + codelen (compile_bexp b d1 d0) + (if beval s b then d1 else d0), stk, s).
Proof.
Admitted.
Exercise 4. Prove the correctness of compile_com, in the case that it terminates
Hint: Prove this by induction over cexec.
Lemma compile_com_correct_terminating:
forall s c s',
cexec s c s' ->
forall C pc stk,
code_at C pc (compile_com c) ->
transitions C
(pc, stk, s)
(pc + codelen (compile_com c), stk, s').
Proof.
Admitted.