(* Correctness proof of a (very) simple compiler *)

Require Import Omega.
Require Import List.

(* syntax of the source language *)

Parameter string : Set.  (* the abstract type of variable names *)

Inductive expr : Set := 
  (* TO BE COMPLETED (Q1) *)
.

(* semantics of the source language *)

Definition state := string -> nat.

Fixpoint E (s : state) (e : expr) {struct e} : nat :=
  (* TO BE COMPLETED (Q2) *)
.

(* syntax of the target language *)

Inductive instr : Set :=
  (* TO BE COMPLETED (Q3) *)
.

(* semantics of the target language *)

Inductive cell : Set := (* memory cells *)
  (* TO BE COMPLETED (Q4) *)
.

Definition store := cell -> nat.

Lemma cell_eq_dec : forall c1 c2 : cell, {c1 = c2} + {c1 <> c2}.
  (* TO BE COMPLETED (Q5) *)
.

Definition update (s : store) (c : cell) (v : nat) : store :=
  (* TO BE COMPLETED (Q5) *)
.
 
Definition Si (s : store) (i : instr) : store :=
  (* TO BE COMPLETED (Q6) *)
.
 
Fixpoint Sl (s : store) (l : list instr) {struct l} : store :=
  (* TO BE COMPLETED (Q6) *)
.
 
(* the compiler *)

Definition symt := string -> nat.

Fixpoint C (m : symt) (r : nat) (e : expr) {struct e} : 
  (* TO BE COMPLETED (Q7) *)
.

(* correctness *)

Lemma Sl_append :
 forall (l1 l2 : list instr) (s : store), Sl s (l1 ++ l2) = Sl (Sl s l1) l2.
Proof.
  (* TO BE COMPLETED (Q9) *)
Qed.

Lemma Sl_invariant :
 forall (m : symt) (e : expr) (r r' : nat),
 r' < r -> forall s : store, Sl s (C m r e) (Reg r') = s (Reg r').
Proof.
  (* TO BE COMPLETED (Q9) *)
Qed.

Theorem correctness :
  (* TO BE COMPLETED (Q8) *)
.
Proof.
  (* TO BE COMPLETED (Q9) *)
Qed.