Semantics of for loops

The semantics of a little programming language is described with the following declarations :

Require Export ZArith.
 
 
Section little_abstract_semantics.
Variables
   (Var, aExp, bExp, state : Set) (evalA : state -> aExp ->  option Z)
   (evalB : state -> bExp ->  option bool)
   (update : state -> Var -> Z ->  option state).
 
Inductive inst : Set :=
  Skip: inst
 | Assign: Var -> aExp ->  inst
 | Scolon: inst -> inst ->  inst
 | WhileDo: bExp -> inst ->  inst .


(* The semantics of the language is given in chapter 7. *)
 
Inductive exec : state -> inst -> state ->  Prop :=
  execSkip: forall s : state, exec s Skip s
 | execAssign:
     forall (s s1 : state) (v : Var) (n : Z) (a : aExp),
     evalA s a = Some n ->
     update s v n = Some s1 -> exec s (Assign v a) s1
 | execScolon:
     forall (s s1 s2 : state) (i1 i2 : inst),
     exec s i1 s1 -> exec s1 i2 s2 -> exec s (Scolon i1 i2) s2
 | execWhileFalse:
     forall (s : state) (i : inst) (e : bExp),
     evalB s e = Some false -> exec s (WhileDo e i) s
 | execWhileTrue:
     forall (s s1 s2 : state) (i : inst) (e : bExp),
     evalB s e = Some true ->
     exec s i s1 -> exec s1 (WhileDo e i) s2 -> exec s (WhileDo e i) s2.

We use the predicate forLoops to characterize a subset of programs for which execution is guaranteed to terminate (if there are no execution errors).

(* We need to use the evaluation functions as if they were total.  extract_optio
n
   makes them total by adding a default value. *)
 
Definition extract_option : forall A : Set, option A -> A ->  A :=
   fun A x def => match x with None => def | Some v => v end.
Implicits extract_option [1].
(* When a while loop contains a variable that is decreased at each
  step and tested against a bound, it is obvious that this loop will
  terminate.  We consider such loops are "for" loops.*)
 
Inductive forLoops : inst ->  Prop :=
  aForLoop:
    forall (e : bExp) (i : inst) (variant : aExp),
    (forall s, s' : state,
     evalB s e = Some true ->
     exec s i s' ->
      Zwf
       ZERO (extract_option (evalA s' variant) ZERO)
       (extract_option (evalA s variant) ZERO)) ->
    forLoops i ->  forLoops (WhileDo e i)
 | assignFor: forall (v : Var) (e : aExp), forLoops (Assign v e)
 | skipFor: forLoops Skip
 | scolonFor:
     forall i1 i2 : inst,
     forLoops i1 -> forLoops i2 -> forLoops (Scolon i1 i2).

Define a function with the following type :

 forall (s : state) (i : inst),
 forLoops i ->
   {s' : state | exec s i s'}+{forall s' : state, ~ exec s i s'}.

Solution

Here is a hint: look at the files from the Coq standard library where well-founded appears.

Follow this link