Require Import ZArith List String Recdef. (* This is the description of a simple programming language. *) (* Arithmetic expressions. *) Inductive aexpr : Type := avar (s : string) | anum (n :Z) | aplus (a1 a2:aexpr). Inductive bexpr : Type := blt (_ _ : aexpr). Inductive instr : Type := assign (_ : string) (_ : aexpr) | sequence (_ _: instr) | while (_ :bexpr)(_ : instr) | skip. Definition env := list (string * Z). (* Write functions that evaluate an arithmetic expression in a given environment of type env, which provides the value for all variables in the expression. *) (* The result should be of type option Z. When a variable from the arithmetic expression is missing in the environment, the result is None. *) (* Write functions that execute an instruction. This function has a numeric argument that states how many times each loop can be unfolded. The result has type option env. When a loop requires more than the allowed number of unfoldings or when a variable is not declared in the initial environment, the result is None. *) (* Here is the semantics of the programming language described as inductive predicates. In particular, exec e i e' means "from the starting environment, executing the instruction i terminates and returns the final environment e'. *) Inductive aeval : env -> aexpr -> Z -> Prop := ae_int : forall r n, aeval r (anum n) n | ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v | ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' -> aeval ((y,v)::r) (avar x) v' | ae_plus : forall r e1 e2 v1 v2, aeval r e1 v1 -> aeval r e2 v2 -> aeval r (aplus e1 e2) (v1 + v2). Inductive beval : env -> bexpr -> bool -> Prop := | be_lt1 : forall r e1 e2 v1 v2, aeval r e1 v1 -> aeval r e2 v2 -> v1 < v2 -> beval r (blt e1 e2) true | be_lt2 : forall r e1 e2 v1 v2, aeval r e1 v1 -> aeval r e2 v2 -> v2 <= v1 -> beval r (blt e1 e2) false. Inductive s_update : env->string->Z->env->Prop := | s_up1 : forall r x v v', s_update ((x,v)::r) x v' ((x,v')::r) | s_up2 : forall r r' x y v v', s_update r x v' r' -> x <> y -> s_update ((y,v)::r) x v' ((y,v)::r'). Inductive exec : env->instr->env->Prop := | SN1 : forall r, exec r skip r | SN2 : forall r r' x e v, aeval r e v -> s_update r x v r' -> exec r (assign x e) r' | SN3 : forall r r' r'' i1 i2, exec r i1 r' -> exec r' i2 r'' -> exec r (sequence i1 i2) r'' | SN4 : forall r r' r'' b i, beval r b true -> exec r i r' -> exec r' (while b i) r'' -> exec r (while b i) r'' | SN5 : forall r b i, beval r b false -> exec r (while b i) r. (* If "fexec" is the name of the function you defined above for executing instructions, you should be able to prove the following statements. *) Lemma fexec_sound : forall n e i e', fexec n e i = Some e' -> exec e i e'. Qed. Lemma fexec_complete : forall e i e', exec e i e' -> exists n, fexec n e i = Some e'. Qed. (* These can take a few days to prove. *)