Set Implicit Arguments.
Require Export Utf8.
Require Export PrettyBigStep.

Require Export LibHeap.

Module Heap := LibHeap.HeapList.

Section ConcreteExample.

Definition var := string.
Definition proc := string.
Definition Val := int.

Inductive expr :=
  | expr_cst : Val → expr
  | expr_var : var → expr
  | expr_add : expr → expr → expr
  .

Inductive ext_expr :=
  | expr_add_1 : expr → ext_expr
  | expr_add_2 : ext_expr
  .

Inductive stat :=
  | stat_skip : stat
  | stat_asgn : var → expr → stat
  | stat_seq : stat → stat → stat
  | stat_if : expr → stat → stat → stat
  | stat_while : expr → stat → stat
  | stat_throw : stat
  | stat_proc_call : proc → expr → stat
  .

Inductive ext_stat :=
  | stat_asgn_1 : var → ext_stat
  | stat_seq_1 : stat → ext_stat
  | stat_if_1 : stat → stat → ext_stat
  | stat_while_1 : expr → stat → ext_stat
  | stat_while_2 : expr → stat → ext_stat
  | stat_proc_call_1 : proc → ext_stat
  .

Inductive prog :=
  | prog_proc_decl : proc → var → stat → prog → prog
  | prog_stat : stat → prog
  .

Inductive terms :=
  | terms_expr : expr → terms
  | terms_ext_expr : ext_expr → terms
  | terms_stat : stat → terms
  | terms_ext_stat : ext_stat → terms
  | terms_prog : prog → terms
  .

Coercion terms_expr : expr >-> terms.
Coercion terms_ext_expr : ext_expr >-> terms.
Coercion terms_stat : stat >-> terms.
Coercion terms_ext_stat : ext_stat >-> terms.
Coercion terms_prog : prog >-> terms.

Fixpoint compare_expr e1 e2 :=
  match e1, e2 with
  | expr_cst c1, expr_cst c2 ⇒ decide (c1 = c2)
  | expr_var x1, expr_var x2 ⇒ decide (x1 = x2)
  | expr_add e11 e21, expr_add e12 e22 ⇒
    compare_expr e11 e12 && compare_expr e21 e22
  | _, _ ⇒ false
  end.

Global Instance expr_Comparable : Comparable expr.
  applys comparable_beq compare_expr. intros x y. iff H.
   gen y; induction x; intros; destruct y; simpls; rew_refl in *; tryfalse; substs*; fequals×.
   substs~; induction y; simpls; rew_refl¬.
Defined.

Fixpoint compare_stat s1 s2 :=
  match s1, s2 with
  | stat_skip, stat_skip ⇒ true
  | stat_asgn x1 e1, stat_asgn x2 e2 ⇒ decide (x1 = x2 ∧ e1 = e2)
  | stat_seq s11 s12, stat_seq s21 s22 ⇒
    compare_stat s11 s21 && compare_stat s12 s22
  | stat_if e1 s11 s12, stat_if e2 s21 s22 ⇒
    decide (e1 = e2) && compare_stat s11 s21 && compare_stat s12 s22
  | stat_while e1 s1, stat_while e2 s2 ⇒
    decide (e1 = e2) && compare_stat s1 s2
  | stat_throw, stat_throw ⇒ true
  | stat_proc_call f1 e1, stat_proc_call f2 e2 ⇒ decide (f1 = f2 ∧ e1 = e2)
  | _, _ ⇒ false
  end.

Global Instance stat_Comparable : Comparable stat.
  applys comparable_beq compare_stat. intros x y. iff H.
   gen y; induction x; intros; destruct y; simpls~; tryfalse;
     try rewrite <- and_andb in *; rew_refl in *; substs*; fequals×.
   substs~; induction y; simpls; try rewrite <- and_andb; rew_refl¬.
Defined.

Global Instance stat_Inhab : Inhab stat.
  apply prove_Inhab. constructors¬.
Defined.

Definition compare_ext_expr e1 e2 :=
  match e1, e2 with
  | expr_add_1 e1, expr_add_1 e2 ⇒ decide (e1 = e2)
  | expr_add_2, expr_add_2 ⇒ true
  | _, _ ⇒ false
  end.

Global Instance ext_expr_Comparable : Comparable ext_expr.
  applys comparable_beq compare_ext_expr. intros x y.
  destruct x; destruct y; simpl; rew_refl; iff H; tryfalse; try congruence; auto.
Defined.

Definition compare_ext_stat s1 s2 :=
  match s1, s2 with
  | stat_asgn_1 x1, stat_asgn_1 x2 ⇒ decide (x1 = x2)
  | stat_seq_1 s1, stat_seq_1 s2 ⇒ decide (s1 = s2)
  | stat_if_1 s11 s21, stat_if_1 s12 s22 ⇒ decide (s11 = s12 ∧ s21 = s22)
  | stat_while_1 e1 s1, stat_while_1 e2 s2 ⇒ decide (e1 = e2 ∧ s1 = s2)
  | stat_while_2 e1 s1, stat_while_2 e2 s2 ⇒ decide (e1 = e2 ∧ s1 = s2)
  | stat_proc_call_1 f1, stat_proc_call_1 f2 ⇒ decide (f1 = f2)
  | _, _ ⇒ false
  end.

Global Instance ext_stat_Comparable : Comparable ext_stat.
  applys comparable_beq compare_ext_stat. intros x y.
  destruct x; destruct y; simpl; rew_refl; iff H; tryfalse; (fequals× || inverts× H).
Defined.

Fixpoint compare_prog p1 p2 : bool :=
  match p1, p2 with
  | prog_proc_decl f1 x1 s1 p1, prog_proc_decl f2 x2 s2 p2 ⇒
    decide (f1 = f2 ∧ x1 = x2 ∧ s1 = s2 ∧ compare_prog p1 p2)
  | prog_stat s1, prog_stat s2 ⇒ decide (s1 = s2)
  | _, _ ⇒ false
  end.

Global Instance prog_Comparable : Comparable prog.
  applys comparable_beq compare_prog.
  induction x; induction y; simpl; rew_refl; iff H; tryfalse; (fequals× || inverts× H).
   repeat inverts H as H. apply¬ IHx.
   splits¬. apply¬ IHx.
Defined.

Definition compare_terms p1 p2 :=
  match p1, p2 with
  | terms_expr e1, terms_expr e2 ⇒ decide (e1 = e2)
  | terms_ext_expr e1, terms_ext_expr e2 ⇒ decide (e1 = e2)
  | terms_stat s1, terms_stat s2 ⇒ decide (s1 = s2)
  | terms_ext_stat s1, terms_ext_stat s2 ⇒ decide (s1 = s2)
  | terms_prog p1, terms_prog p2 ⇒ decide (p1 = p2)
  | _, _ ⇒ false
  end.

Global Instance terms_Comparable : Comparable terms.
  applys comparable_beq compare_terms. intros x y.
  destruct x; destruct y; simpl; rew_refl; iff H; tryfalse; (fequals× || inverts× H).
Defined.


Inductive sub_expr_expr : expr → expr → Prop :=
  | sub_expr_expr_add_1 : ∀ e1 e2,
    sub_expr_expr e1 (expr_add e1 e2)
  | sub_expr_expr_add_2 : ∀ e1 e2,
    sub_expr_expr e2 (expr_add e1 e2)
  .

Global Instance sub_expr_expr_Decidable : ∀ e1 e2,
    Decidable (sub_expr_expr e1 e2).
  introv. destruct e2;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
  applys decidable_make (decide (e1 = e2_1 ∨ e1 = e2_2)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   inverts D as [?|?]; substs; constructors.
   intro A; inverts¬ A.
Defined.

Inductive sub_expr_ext_expr : expr → ext_expr → Prop :=
  | sub_expr_ext_expr_add_1 : ∀ e,
    sub_expr_ext_expr e (expr_add_1 e)
  .

Global Instance sub_expr_ext_expr_Decidable : ∀ e1 e2,
    Decidable (sub_expr_ext_expr e1 e2).
  introv. destruct e2;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
  applys decidable_make (decide (e1 = e)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   constructors.
   intro A; inverts¬ A.
Defined.

Inductive sub_expr_stat : expr → stat → Prop :=
  | sub_expr_stat_asgn : ∀ x e,
    sub_expr_stat e (stat_asgn x e)
  | sub_expr_stat_if : ∀ e s1 s2,
    sub_expr_stat e (stat_if e s1 s2)
  | sub_expr_stat_while : ∀ e s,
    sub_expr_stat e (stat_while e s)
  .

Global Instance sub_expr_stat_Decidable : ∀ e s,
    Decidable (sub_expr_stat e s).
  introv. destruct s;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (e = e0)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
   applys decidable_make (decide (e = e0)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
   applys decidable_make (decide (e = e0)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
Defined.

Inductive sub_stat_stat : stat → stat → Prop :=
  | sub_stat_stat_seq_1 : ∀ s1 s2,
    sub_stat_stat s1 (stat_seq s1 s2)
  | sub_stat_stat_seq_2 : ∀ s1 s2,
    sub_stat_stat s2 (stat_seq s1 s2)
  | sub_stat_stat_if_1 : ∀ e s1 s2,
    sub_stat_stat s1 (stat_if e s1 s2)
  | sub_stat_stat_if_2 : ∀ e s1 s2,
    sub_stat_stat s2 (stat_if e s1 s2)
  | sub_stat_stat_while : ∀ e s,
    sub_stat_stat s (stat_while e s)
  .

Global Instance sub_stat_stat_Decidable : ∀ s1 s2,
    Decidable (sub_stat_stat s1 s2).
  introv. destruct s2;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (s1 = s2_1 ∨ s1 = s2_2)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     inverts D as [?|?]; substs; constructors.
     intro A; inverts¬ A.
   applys decidable_make (decide (s1 = s2_1 ∨ s1 = s2_2)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     inverts D as [?|?]; substs; constructors.
     intro A; inverts¬ A.
   applys decidable_make (decide (s1 = s2)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
Defined.

Inductive sub_expr_ext_stat : expr → ext_stat → Prop :=
  | sub_expr_ext_stat_while_1 : ∀ e s,
    sub_expr_ext_stat e (stat_while_1 e s)
  | sub_expr_ext_stat_while_2 : ∀ e s,
    sub_expr_ext_stat e (stat_while_2 e s)
  .

Global Instance sub_expr_ext_stat_Decidable : ∀ e s,
    Decidable (sub_expr_ext_stat e s).
  introv. destruct s;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (e = e0)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
   applys decidable_make (decide (e = e0)).
    rewrite decide_def. cases_if as D; fold_bool; rew_refl.
     constructors.
     intro A; inverts¬ A.
Defined.

Inductive sub_stat_ext_stat : stat → ext_stat → Prop :=
  | sub_stat_ext_stat_seq_1 : ∀ s,
    sub_stat_ext_stat s (stat_seq_1 s)
  | sub_stat_ext_stat_if_1_1 : ∀ s1 s2,
    sub_stat_ext_stat s1 (stat_if_1 s1 s2)
  | sub_stat_ext_stat_if_1_2 : ∀ s1 s2,
    sub_stat_ext_stat s2 (stat_if_1 s1 s2)
  | sub_stat_ext_stat_while_1 : ∀ e s,
    sub_stat_ext_stat s (stat_while_1 e s)
  | sub_stat_ext_stat_while_2 : ∀ e s,
    sub_stat_ext_stat s (stat_while_2 e s)
  .

Global Instance sub_stat_ext_stat_Decidable : ∀ s1 s2,
    Decidable (sub_stat_ext_stat s1 s2).
  introv. destruct s2;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
  applys decidable_make (decide (s1 = s)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   constructors.
   intro A; inverts¬ A.
  applys decidable_make (decide (s1 = s ∨ s1 = s0)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   inverts D as [?|?]; substs; constructors.
   intro A; inverts¬ A.
  applys decidable_make (decide (s1 = s)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   constructors.
   intro A; inverts¬ A.
  applys decidable_make (decide (s1 = s)).
  rewrite decide_def. cases_if as D; fold_bool; rew_refl.
   constructors.
   intro A; inverts¬ A.
Defined.

Inductive sub_terms : terms → terms → Prop :=
  | sub_terms_expr_expr : ∀ e1 e2,
    sub_expr_expr e1 e2 →
    sub_terms e1 e2
  | sub_terms_expr_ext_expr : ∀ e1 e2,
    sub_expr_ext_expr e1 e2 →
    sub_terms e1 e2
  | sub_terms_expr_stat : ∀ e1 s2,
    sub_expr_stat e1 s2 →
    sub_terms e1 s2
  | sub_terms_expr_ext_stat : ∀ e1 s2,
    sub_expr_ext_stat e1 s2 →
    sub_terms e1 s2
  | sub_terms_stat_stat : ∀ s1 s2,
    sub_stat_stat s1 s2 →
    sub_terms s1 s2
  | sub_terms_stat_ext_stat : ∀ s1 s2,
    sub_stat_ext_stat s1 s2 →
    sub_terms s1 s2
  .

Global Instance sub_terms_Decidable : ∀ t1 t2,
    Decidable (sub_terms t1 t2).
  introv. destruct t1; destruct t2;
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (sub_expr_expr e e0)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
   applys decidable_make (decide (sub_expr_ext_expr e e0)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
   applys decidable_make (decide (sub_expr_stat e s)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
   applys decidable_make (decide (sub_expr_ext_stat e e0)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
   applys decidable_make (decide (sub_stat_stat s s0)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
   applys decidable_make (decide (sub_stat_ext_stat s e)). rew_refl. apply eq_isTrue.
    iff S; [ constructors¬ | inverts¬ S ].
Defined.

Inductive while_name :=
  | name_abort_ext_expr : ext_expr → while_name
  | name_abort_ext_stat : ext_stat → while_name
  | name_cst : Val → while_name
  | name_var : var → while_name
  | name_varCxt : var → while_name
  | name_varUndef : var → while_name
  | name_add : expr → expr → while_name
  | name_add_1 : expr → while_name
  | name_add_2 : while_name
  | name_skip : while_name
  | name_throw : while_name
  | name_asgn : var → expr → while_name
  | name_asgn_1 : var → while_name
  | name_asgn_1_immutable : var → while_name
  | name_seq : stat → stat → while_name
  | name_seq_1 : stat → while_name
  | name_if : expr → stat → stat → while_name
  | name_if_1_true : stat → stat → while_name
  | name_if_1_false : stat → stat → while_name
  | name_while : expr → stat → while_name
  | name_while_1 : expr → stat → while_name
  | name_while_2_true : expr → stat → while_name
  | name_while_2_false : expr → stat → while_name
  | name_proc_call : proc → expr → while_name
  | name_proc_call_1 : proc → var → stat → while_name
  | name_proc_call_1_undef : proc → while_name
  | name_proc_decl : proc → var → stat → prog → while_name
  | name_prog_stat : stat → while_name
  .

Definition while_struct n : Rule_struct terms :=
  match n with
  | name_abort_ext_expr e ⇒ Rule_struct_Ax _
  | name_abort_ext_stat s ⇒ Rule_struct_Ax _
  | name_cst c ⇒ Rule_struct_Ax _
  | name_var x ⇒ Rule_struct_Ax _
  | name_varCxt x ⇒ Rule_struct_Ax _
  | name_varUndef x ⇒ Rule_struct_Ax _
  | name_add e1 e2 ⇒ Rule_struct_R2 (term := terms) e1 (expr_add_1 e2)
  | name_add_1 e2 ⇒ Rule_struct_R2 (term := terms) e2 expr_add_2
  | name_add_2 ⇒ Rule_struct_Ax _
  | name_skip ⇒ Rule_struct_Ax _
  | name_throw ⇒ Rule_struct_Ax _
  | name_asgn x e ⇒ Rule_struct_R2 (term := terms) e (stat_asgn_1 x)
  | name_asgn_1 x ⇒ Rule_struct_Ax _
  | name_asgn_1_immutable x ⇒ Rule_struct_Ax _
  | name_seq s1 s2 ⇒ Rule_struct_R2 (term := terms) s1 (stat_seq_1 s2)
  | name_seq_1 s2 ⇒ Rule_struct_R1 (term := terms) s2
  | name_if e s1 s2 ⇒ Rule_struct_R2 (term := terms) e (stat_if_1 s1 s2)
  | name_if_1_true s1 s2 ⇒ Rule_struct_R1 (term := terms) s1
  | name_if_1_false s1 s2 ⇒ Rule_struct_R1 (term := terms) s2
  | name_while e s ⇒ Rule_struct_R1 (term := terms) (stat_while_1 e s)
  | name_while_1 e s ⇒ Rule_struct_R2 (term := terms) e (stat_while_2 e s)
  | name_while_2_true e s ⇒ Rule_struct_R2 (term := terms) s (stat_while_1 e s)
  | name_while_2_false e s ⇒ Rule_struct_Ax _
  | name_proc_call f e ⇒ Rule_struct_R2 (term := terms) e (stat_proc_call_1 f)
  | name_proc_call_1 f x s ⇒ Rule_struct_R1 (term := terms) s
  | name_proc_call_1_undef f ⇒ Rule_struct_Ax _
  | name_proc_decl f x s p ⇒ Rule_struct_R1 (term := terms) p
  | name_prog_stat s ⇒ Rule_struct_R1 (term := terms) s
  end.

Definition while_left n : terms :=
  match n with
  | name_abort_ext_expr e ⇒ e
  | name_abort_ext_stat s ⇒ s
  | name_cst c ⇒ expr_cst c
  | name_var x ⇒ expr_var x
  | name_varCxt x ⇒ expr_var x
  | name_varUndef x ⇒ expr_var x
  | name_add e1 e2 ⇒ expr_add e1 e2
  | name_add_1 e2 ⇒ expr_add_1 e2
  | name_add_2 ⇒ expr_add_2
  | name_skip ⇒ stat_skip
  | name_throw ⇒ stat_throw
  | name_asgn x e ⇒ stat_asgn x e
  | name_asgn_1 x ⇒ stat_asgn_1 x
  | name_asgn_1_immutable x ⇒ stat_asgn_1 x
  | name_seq s1 s2 ⇒ stat_seq s1 s2
  | name_seq_1 s2 ⇒ stat_seq_1 s2
  | name_if e s1 s2 ⇒ stat_if e s1 s2
  | name_if_1_true s1 s2 ⇒ stat_if_1 s1 s2
  | name_if_1_false s1 s2 ⇒ stat_if_1 s1 s2
  | name_while e s ⇒ stat_while e s
  | name_while_1 e s ⇒ stat_while_1 e s
  | name_while_2_true e s ⇒ stat_while_2 e s
  | name_while_2_false e s ⇒ stat_while_2 e s
  | name_proc_call f e ⇒ stat_proc_call f e
  | name_proc_call_1 f x s ⇒ stat_proc_call_1 f
  | name_proc_call_1_undef f ⇒ stat_proc_call_1 f
  | name_proc_decl f x s p ⇒ prog_proc_decl f x s p
  | name_prog_stat s ⇒ prog_stat s
  end.

Definition while_str := {|

    term := terms;
    name := while_name;

    rule_struct := while_struct;

    left := while_left

  |}.

Inductive error : Set :=
  | Err
  .

Definition CtxEnv := option (var × Val).

Definition Env := Heap.heap var Val.

Definition EnvV := (Env × CtxEnv)%type.

Definition EnvF := Heap.heap proc (var × stat).

Definition indomF (Ef : EnvF) f := Heap.indom Ef f.

Definition indom (E : Env) x := Heap.indom E x.

Definition writeF Ef f x s : EnvF := write Ef f (x, s).

Definition write E x v : Env := write E x v.

Definition EnvEmpty : Env := empty.

Definition EnvVEmpty : EnvV := (EnvEmpty, None).

Definition EnvFEmpty : EnvF := empty.

Inductive oute :=
  | oute_val : Val → oute
  | oute_error : error → oute
  .

Coercion oute_error : error >-> oute.

Definition is_val o :=
  match o with
  | oute_val v ⇒ True
  | oute_error err ⇒ False
  end.

Inductive aborte : oute → Prop :=
  | aborte_error : ∀ err,
    aborte (oute_error err)
  .

Inductive outs :=
  | outs_normal : Env → outs
  | outs_error : error → outs
  .

Coercion outs_error : error >-> outs.

Definition is_env o :=
  match o with
  | outs_normal E ⇒ True
  | outs_error err ⇒ False
  end.

Inductive ctx_ref : CtxEnv → var → Prop :=
  | ctx_ref_cons : ∀ x v,
      ctx_ref (Some (x, v)) x
  .

Inductive aborts : outs → Prop :=
  | aborts_error : ∀ err,
    aborts (outs_error err)
  .

Inductive while_res : Type :=
  | while_res_expr : oute → while_res
  | while_res_stat : outs → while_res
  .

Coercion while_res_expr : oute >-> while_res.
Coercion while_res_stat : outs >-> while_res.

Inductive abort_res : while_res → Prop :=
  | abort_res_expr : abort_res (while_res_expr Err)
  | abort_res_stat : abort_res (while_res_stat Err)
  .

Inductive while_st : Type :=
  | while_st_expr : EnvV → while_st
  | while_st_stat : EnvV → EnvF → while_st
  | while_st_prog : EnvV → EnvF → while_st
  | while_st_add_1 : EnvV → while_res → while_st
  | while_st_add_2 : Val → while_res → while_st
  | while_st_asgn_1 : EnvV → while_res → while_st
  | while_st_seq_1 : CtxEnv → EnvF → while_res → while_st
  | while_st_if_1 : EnvV → EnvF → while_res → while_st
  | while_st_while_1 : CtxEnv → EnvF → while_res → while_st
  | while_st_while_2 : EnvV → EnvF → while_res → while_st
  | while_st_proc_call_1 : EnvV → EnvF → while_res → while_st
  .

Inductive abort_st : while_st → Prop :=
  | abort_st_add_1 : ∀ Ev r,
    abort_res r →
    abort_st (while_st_add_1 Ev r)
  | abort_st_add_2 : ∀ v r,
    abort_res r →
    abort_st (while_st_add_2 v r)
  | abort_st_asgn_1 : ∀ Ev r,
    abort_res r →
    abort_st (while_st_asgn_1 Ev r)
  | abort_st_seq_1 : ∀ C Ef r,
    abort_res r →
    abort_st (while_st_seq_1 C Ef r)
  | abort_st_if_1 : ∀ Ev Ef r,
    abort_res r →
    abort_st (while_st_if_1 Ev Ef r)
  | abort_st_while_1 : ∀ C Ef r,
    abort_res r →
    abort_st (while_st_while_1 C Ef r)
  | abort_st_while_2 : ∀ Ev Ef r,
    abort_res r →
    abort_st (while_st_while_2 Ev Ef r)
  | abort_st_proc_call_1 : ∀ Ev Ef r,
    abort_res r →
    abort_st (while_st_proc_call_1 Ev Ef r)
  .

Definition while_cond n sigma : Prop :=
  match n, sigma with
  | name_abort_ext_expr e, sigma ⇒
      abort_st sigma
  | name_abort_ext_stat s, sigma ⇒
      abort_st sigma
  | name_cst c, while_st_expr Ev ⇒
      True
  | name_var x, while_st_expr (E, C) ⇒
      indom E x
  | name_varCxt x, while_st_expr (E, Some (y, v)) ⇒
      x = y
  | name_varUndef x, while_st_expr (E, C) ⇒
      (∀ v, C ≠ Some (x, v)) ∧
      ¬ indom E x
  | name_add e1 e2, while_st_expr Ev ⇒
      True
  | name_add_1 e2, while_st_add_1 Ev r ⇒
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_add_2, while_st_add_2 v r ⇒
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_skip, while_st_stat Ev Ef ⇒
      True
  | name_throw, while_st_stat Ev Ef ⇒
      True
  | name_asgn x e, while_st_stat Ev Ef ⇒
      True
  | name_asgn_1 x, while_st_asgn_1 (E, C) r ⇒
      ¬ ctx_ref C x ∧
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_asgn_1_immutable x, while_st_asgn_1 (E, C) r ⇒
      ctx_ref C x ∧
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_seq s1 s2, while_st_stat Ev Ef ⇒
      True
  | name_seq_1 s2, while_st_seq_1 C Ef r ⇒
      ∃ o, r = while_res_stat o ∧ is_env o
  | name_if e s1 s2, while_st_stat Ev Ef ⇒
      True
  | name_if_1_true s1 s2, while_st_if_1 Ev Ef o ⇒
      ∃ v, v ≠ 0 ∧ o = oute_val v
  | name_if_1_false s1 s2, while_st_if_1 Ev Ef o ⇒
      o = oute_val 0
  | name_while e s, while_st_stat Ev Ef ⇒
      True
  | name_while_1 e s, while_st_while_1 C Ef r ⇒
      ∃ o, r = while_res_stat o ∧ is_env o
  | name_while_2_true e s, while_st_while_2 Ev Ef o ⇒
      ∃ v, v ≠ 0 ∧ o = oute_val v
  | name_while_2_false e s, while_st_while_2 Ev Ef o ⇒
      o = oute_val 0
  | name_proc_call f e, while_st_stat Ev Ef ⇒
      True
  | name_proc_call_1 f x s, while_st_proc_call_1 Ev Ef r ⇒
      binds Ef f (x, s) ∧
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_proc_call_1_undef f, while_st_proc_call_1 Ev Ef r ⇒
      ¬ indomF Ef f ∧
      ∃ o, r = while_res_expr o ∧ is_val o
  | name_proc_decl f x s p, while_st_prog Ev Ef ⇒
      True
  | name_prog_stat s, while_st_prog Ev Ef ⇒
      True
  | _, _ ⇒
      False
  end.

Definition if_st_expr A (f : _ → _ → option A) sigma :=
  match sigma with
  | while_st_expr (E, C) ⇒ f E C
  | _ ⇒ None
  end.

Definition if_st_stat A (f : _ → _ → option A) sigma :=
  match sigma with
  | while_st_stat Ev Ef ⇒ f Ev Ef
  | _ ⇒ None
  end.

Definition if_st_prog A (f : _ → _ → option A) sigma :=
  match sigma with
  | while_st_prog Ev Ef ⇒ f Ev Ef
  | _ ⇒ None
  end.

Definition if_res_expr A (f : _ → option A) r :=
  match r with
  | while_res_expr o ⇒ f o
  | _ ⇒ None
  end.

Definition if_res_stat A (f : _ → option A) r :=
  match r with
  | while_res_stat o ⇒ f o
  | _ ⇒ None
  end.

Definition while_rule n : Rule while_st while_res :=
  match n with
  | name_abort_ext_expr e ⇒
    let ax _ := Some (while_res_expr Err) in
    Rule_Ax ax
  | name_abort_ext_stat s ⇒
    let ax _ := Some (while_res_stat Err) in
    Rule_Ax ax
  | name_cst c ⇒
    let ax _ := Some (oute_val c : while_res) in
    Rule_Ax ax
  | name_var x ⇒
    let ax :=
      if_st_expr (fun E C ⇒
        option_map (oute_val : _ → while_res) (read_option E x)) in
    Rule_Ax ax
  | name_varCxt x ⇒
    let ax :=
      if_st_expr (fun E C ⇒
        option_map (fun Cd ⇒ oute_val (snd Cd) : while_res) C) in
    Rule_Ax ax
  | name_varUndef x ⇒
    let ax _ := Some (Err : while_res) in
    Rule_Ax ax
  | name_add e1 e2 ⇒
    let up :=
      if_st_expr (fun E C ⇒
        Some (while_st_expr (E, C))) in
    let next sigma o :=
      if_st_expr (fun E C ⇒
        Some (while_st_add_1 (E, C) o)) sigma in
    Rule_R2 up next
  | name_add_1 e2 ⇒
    let up sigma :=
      match sigma with
      | while_st_add_1 E o ⇒ Some (while_st_expr E)
      | _ ⇒ None
      end in
    let next sigma r :=
      match sigma with
      | while_st_add_1 E (oute_val v) ⇒ Some (while_st_add_2 v r)
      | _ ⇒ None
      end in
    Rule_R2 up next
  | name_add_2 ⇒
    let ax sigma :=
      match sigma with
      | while_st_add_2 v1 (oute_val v2) ⇒ Some (oute_val (v1 + v2) : while_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  | name_skip ⇒
    let ax :=
      if_st_stat (fun Ev Ef ⇒
        Some (outs_normal (fst Ev) : while_res)) in
    Rule_Ax ax
  | name_throw ⇒
    let ax _ := Some (while_res_stat Err) in
    Rule_Ax ax
  | name_asgn x e ⇒
    let up :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_expr Ev)) in
    let next sigma r :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_asgn_1 Ev r)) sigma in
    Rule_R2 up next
  | name_asgn_1 x ⇒
    let ax sigma :=
      match sigma with
      | while_st_asgn_1 (E, C) (oute_val v) ⇒
        Some (outs_normal (write E x v) : while_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  | name_asgn_1_immutable x ⇒
    let ax _ := Some (while_res_stat Err) in
    Rule_Ax ax
  | name_seq s1 s2 ⇒
    let up :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_stat Ev Ef)) in
    let next sigma r :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_seq_1 (snd Ev) Ef r)) sigma in
    Rule_R2 up next
  | name_seq_1 s2 ⇒
    let up sigma :=
      match sigma with
      | while_st_seq_1 C Ef (outs_normal E) ⇒ Some (while_st_stat (E, C) Ef)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_if e s1 s2 ⇒
    let up :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_expr Ev)) in
    let next sigma r :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_if_1 Ev Ef r)) sigma in
    Rule_R2 up next
  | name_if_1_true s1 s2 ⇒
    let up sigma :=
      match sigma with
      | while_st_if_1 Ev Ef o ⇒ Some (while_st_stat Ev Ef)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_if_1_false s1 s2 ⇒
    let up sigma :=
      match sigma with
      | while_st_if_1 Ev Ef o ⇒ Some (while_st_stat Ev Ef)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_while e s ⇒
    let up :=
      if_st_stat (fun Ev Ef ⇒
        let (E, C) := Ev in
        Some (while_st_while_1 C Ef (outs_normal E))) in
    Rule_R1 _ up
  | name_while_1 e s ⇒
    let up sigma :=
      match sigma with
      | while_st_while_1 C Ef (while_res_stat (outs_normal E)) ⇒
        Some (while_st_expr (E, C))
      | _ ⇒ None
      end in
    let next sigma r :=
      match sigma with
      | while_st_while_1 C Ef (while_res_stat (outs_normal E)) ⇒
        Some (while_st_while_2 (E, C) Ef r)
      | _ ⇒ None
      end in
    Rule_R2 up next
  | name_while_2_true e s ⇒
    let up sigma :=
      match sigma with
      | while_st_while_2 Ev Ef r ⇒ Some (while_st_stat Ev Ef)
      | _ ⇒ None
      end in
    let next sigma r :=
      match sigma with
      | while_st_while_2 Ev Ef _ ⇒ Some (while_st_while_1 (snd Ev) Ef r)
      | _ ⇒ None
      end in
    Rule_R2 up next
  | name_while_2_false e s ⇒
    let ax sigma :=
      match sigma with
      | while_st_while_2 (E, C) Ef o ⇒ Some (outs_normal E : while_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  | name_proc_call f e ⇒
    let up :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_expr Ev)) in
    let next sigma r :=
      if_st_stat (fun Ev Ef ⇒
        Some (while_st_proc_call_1 Ev Ef r)) sigma in
    Rule_R2 up next
  | name_proc_call_1 f x s ⇒
    let up sigma :=
      match sigma with
      | while_st_proc_call_1 (E, C) Ef (oute_val v) ⇒
        let C := Some (x, v) in
        Some (while_st_stat (E, C) Ef)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_proc_call_1_undef f ⇒
    let ax _ := Some (while_res_stat Err) in
    Rule_Ax ax
  | name_proc_decl f x s p ⇒
    let up :=
      if_st_prog (fun Ev Ef ⇒
        let Ef := writeF Ef f x s in
        Some (while_st_prog Ev Ef)) in
    Rule_R1 _ up
  | name_prog_stat s ⇒
    let up :=
      if_st_prog (fun Ev Ef ⇒
        Some (while_st_stat Ev Ef)) in
    Rule_R1 _ up
  end.

Definition while_sem :=
  make_semantics while_str while_cond while_rule.

Lemma while_rule_format_correct : rule_format_correct_all while_sem.
Proof. intro n. destruct n; constructors. Qed.

Lemma while_semantics_full : semantics_full while_sem.
Proof.
  introv C. simpls. destruct n; destruct sigma; simpls; tryfalse; try solve [ constructors¬ ].
  destruct e as [E Ct]. constructors¬. simpl. rewrite read_option_def.
  cases_if; simpls¬. false¬ C.
  destruct e as [E Ct]. destruct Ct as [[y va]|]; tryfalse. substs¬.
  constructors¬. simpls¬.
  destruct e1 as [E Ct]. constructors¬.
   simpls¬.
   introv. eexists. reflexivity.
  constructors¬. introv. lets (o&E&V): (rm C). substs.
  destruct o as [v|]; tryfalse. eexists. reflexivity.
  lets (o&E&V): (rm C). substs. destruct o as [v2|]; tryfalse. constructors¬.
  constructors¬. reflexivity.
  constructors¬.
   simpls¬.
   introv. eexists. reflexivity.
  destruct e as [E Ct]. lets (NC&o&Eq&V): (rm C). substs.
  destruct o as [v2|]; tryfalse. constructors¬.
  constructors¬.
   simpls¬.
   introv. eexists. reflexivity.
  lets (o&Eq&V): (rm C). substs. destruct o as [E|]; tryfalse. constructors¬.
  constructors¬.
   simpls¬.
   introv. eexists. reflexivity.
  destruct e0 as [E Ct]. constructors¬. simpls¬.
  lets (o&Eq&V): (rm C). substs. destruct o as [E|]; tryfalse. constructors¬.
  introv. eexists. reflexivity.
  lets (o&Nz&Eq): (rm C). substs. constructors¬.
  introv. eexists. reflexivity.
  destruct e0 as [E Ct]. substs. constructors¬.
  constructors¬.
   simpls¬.
   introv. eexists. reflexivity.
  destruct e as [E Ct]. lets (R&o&Eq&V): (rm C). destruct o as [va|]; tryfalse.
  substs. constructors¬.
  constructors¬. simpls¬.
  constructors¬. reflexivity.
Qed.

Definition prog_test0 : terms :=
  
  (prog_stat
    (stat_seq
      (stat_seq
         (stat_asgn "a" (expr_cst 6))
         (stat_asgn "b" (expr_cst 7)))
      (stat_seq
         (stat_seq
            (stat_asgn "n" (expr_var "a"))
            (stat_asgn "res" (expr_cst 0)))
         (stat_while (expr_var "n")
            (stat_seq
               (stat_asgn "res" (expr_add (expr_var "res") (expr_var "b")))
               (stat_asgn "n" (expr_add (expr_var "n") (expr_cst (0-1)))))))))%string
  .

Definition prog_test1 : terms :=
  prog_stat (stat_asgn "x"%string (expr_cst 42)).

Definition prog_test2 : terms :=
  prog_stat
    (stat_if (expr_add (expr_var "x"%string) (expr_cst 1))
      (stat_asgn "y"%string (expr_cst (-1)%Z))
      (stat_asgn "y"%string (expr_var "x"%string))).

Definition prog_test3 : terms :=
  prog_stat
    (stat_if (expr_var "x"%string)
      (stat_asgn "y"%string (expr_cst 0))
      (stat_asgn "y"%string (expr_var "x"%string))).

Definition prog_test4 : terms :=
  prog_stat
    (stat_if (expr_var "x"%string)
      (stat_asgn "x"%string (expr_cst 0))
      stat_skip).

Definition prog_test5 : terms :=
  prog_stat
    (stat_while (expr_var "x"%string)
      (stat_asgn "x"%string (expr_add (expr_var "x"%string) (expr_cst 1)))).

Definition prog_test6 : terms :=
  prog_stat
    (stat_while (expr_cst 0)
      (stat_asgn "x"%string (expr_cst 42))).

Definition prog_test7 : terms :=
  prog_stat
    (stat_while (expr_cst 1)
       (stat_asgn "x"%string (expr_cst 42))).

Definition prog_test8 : terms :=
  prog_stat
    (stat_asgn "x"%string
       (expr_add (expr_cst 42) (expr_add (expr_cst 18) (expr_cst 17)))).

Definition prog_test9 : terms :=
  prog_stat
    (stat_seq
      (stat_asgn "x" (expr_cst 1))
      (stat_while (expr_var "x")
        (stat_asgn "x" (expr_cst 0))))%string.

Definition prog_test10 : terms :=
  prog_stat
    (stat_seq
      (stat_seq
          (stat_asgn "x" (expr_cst 1))
          (stat_seq
            (stat_asgn "y" (expr_cst 1))
            (stat_asgn "z" (expr_cst 1))))
     (stat_while (expr_var "x")
       (stat_seq
          (stat_asgn "x" (expr_var "y"))
          (stat_seq
            (stat_asgn "y" (expr_var "z"))
            (stat_asgn "z" (expr_cst 0))))))%string.

Definition prog_test11 : terms :=
  prog_stat (stat_if (expr_var "x"%string) stat_throw stat_skip).

Definition prog_test12 : terms :=
  prog_stat
    (stat_seq
      (stat_seq
          (stat_asgn "x" (expr_cst 1))
          (stat_seq
            (stat_asgn "y" (expr_cst 1))
            (stat_asgn "z" (expr_cst 1))))
     (stat_while (expr_var "z")
       (stat_seq
          (stat_if (expr_var "y")
            (stat_asgn "z" (expr_cst 0))
            stat_skip)
        (stat_seq
           (stat_if (expr_var "x")
             (stat_asgn "y" (expr_cst 0))
             stat_skip)
           (stat_asgn "x" (expr_cst 0))))))%string.

Definition prog_test13 : terms :=
  prog_stat
    (stat_seq
      (stat_asgn "a" (expr_cst 5))
      (stat_while (expr_var "a")
        (stat_seq
          (stat_seq
            (stat_asgn "b" (expr_cst 5))
            (stat_while (expr_var "b")
              (stat_seq
                (stat_seq
                  (stat_asgn "c" (expr_cst 5))
                  (stat_while (expr_var "c")
                    (stat_seq
                      (stat_asgn "x" (expr_add (expr_var "x") (expr_var "c")))
                      (stat_asgn "c" (expr_add (expr_var "c") (expr_cst (-1)%Z))))))
                (stat_asgn "b" (expr_add (expr_var "b") (expr_cst (-1)%Z))))))
          (stat_asgn "a" (expr_add (expr_var "a") (expr_cst (-1)%Z))))))%string.

Definition prog_test14 : terms :=
  prog_stat
    (stat_seq
       (stat_seq
          (stat_asgn "y" (expr_cst 0))
          (stat_asgn "x" (expr_cst 18)))
       (stat_while (expr_var "x")
         (stat_seq
           (stat_asgn "x" (expr_add (expr_var "x") (expr_cst (-1)%Z)))
           (stat_asgn "y" (expr_add (expr_var "y") (expr_cst 1))))))%string.

Definition prog_test15 : terms :=
  (prog_proc_decl "f" "x"
    (stat_proc_call "g" (expr_cst 1))
  (prog_proc_decl "g" "x"
    (stat_proc_call "h" (expr_var "x"))
  (prog_proc_decl "h" "y"
    (stat_proc_call "f" (expr_var "x"))
  (prog_stat
    (stat_seq
      (stat_asgn "x" (expr_cst 0))
      (stat_proc_call "g" (expr_cst (-1)%Z)))))))%string.

Definition prog_test16 : terms :=
  (prog_proc_decl "triangle" "x"
    (stat_if (expr_var "x")
      (stat_seq
        (stat_proc_call "triangle" (expr_add (expr_var "x") (expr_cst (-1)%Z)))
        (stat_asgn "res" (expr_add (expr_var "res") (expr_var "x"))))
      (stat_asgn "res" (expr_cst 0)))
  (prog_stat
    (stat_proc_call "triangle" (expr_cst 42))))%string.

Definition prog_test17 : terms :=
  (prog_proc_decl "f" "l"
    (stat_while (expr_var "y")
      (stat_seq
        (stat_asgn "y" (expr_add (expr_var "y") (expr_cst (-1)%Z)))
        (stat_if (expr_var "x")
          (stat_proc_call "f" (expr_cst 42))
          stat_skip)))
  (prog_stat
    (stat_seq
      (stat_asgn "y" (expr_cst 42))
      (stat_proc_call "f" (expr_cst 18)))))%string.

Definition prog_test18 : terms :=
  
  (prog_proc_decl "prod" "n"
    (stat_if (expr_var "n")
      (stat_seq
        (stat_proc_call "prod" (expr_add (expr_var "n") (expr_cst (-1)%Z)))
        (stat_asgn "res" (expr_add (expr_var "res") (expr_var "b"))))
      (stat_asgn "res" (expr_cst 0)))
  (prog_stat
    (stat_seq
      (stat_seq
        (stat_asgn "a" (expr_cst 6))
        (stat_asgn "b" (expr_cst 7)))
      (stat_proc_call "prod" (expr_var "a")))))%string.

Definition prog_test19 : terms :=
  (prog_proc_decl "id" "x"
    (stat_asgn "res" (expr_var "x"))
  (prog_stat
    (stat_seq
      (stat_seq
        (stat_proc_call "id" (expr_cst 42))
        (stat_asgn "r1" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "id" (expr_cst (-1)%Z))
        (stat_asgn "r2" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "id" (expr_cst 0))
        (stat_asgn "r3" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "id" (expr_cst 18))
        (stat_seq
          (stat_proc_call "id" (expr_var "res"))
          (stat_proc_call "id" (expr_var "res"))))
        (stat_asgn "r4" (expr_var "res"))))))))%string.

Definition prog_test20 : terms :=
  (prog_proc_decl "f" "x"
    (stat_if (expr_var "x")
      (stat_asgn "res" (expr_cst 0))
      (stat_asgn "res" (expr_var "x")))
  (prog_stat
    (stat_seq
      (stat_seq
        (stat_proc_call "f" (expr_cst 42))
        (stat_asgn "r1" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "f" (expr_cst (-1)%Z))
        (stat_asgn "r2" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "f" (expr_cst 0))
        (stat_asgn "r3" (expr_var "res")))
    (stat_seq
      (stat_seq
        (stat_proc_call "f" (expr_cst 18))
        (stat_seq
          (stat_proc_call "f" (expr_var "res"))
          (stat_proc_call "f" (expr_var "res"))))
        (stat_asgn "r4" (expr_var "res"))))))))%string.

Definition prog_test21 : terms :=
  (prog_stat
    (stat_proc_call "undefined_proc" (expr_cst 42)))%string.

Definition prog_test22 : terms :=
  (prog_stat
    (stat_seq
      (stat_if (expr_var "x")
        (stat_asgn "y" (expr_cst (-1)%Z))
        (stat_asgn "y" (expr_cst 1)))
    (stat_seq
      (stat_if (expr_var "y")
        (stat_if (expr_var "x")
          (stat_asgn "z" (expr_cst 1))
          (stat_asgn "z" (expr_cst (-1)%Z)))
        stat_throw)
      (stat_if (expr_add (expr_var "y") (expr_var "z"))
        (stat_asgn "a" (expr_cst 1))
        (stat_asgn "a" (expr_cst 0))))))%string.

Lemma prog_test1_effect :
  eval while_sem prog_test1
    (while_st_prog EnvVEmpty EnvFEmpty)
    (outs_normal (write EnvEmpty "x"%string 42)).
Proof.
  eapply eval_cons with (n := name_prog_stat _).
    reflexivity.
    exact I.
  apply× apply_R1.
  eapply eval_cons with (n := name_asgn _ _).
    reflexivity.
    exact I.
  apply× apply_R2.
   eapply eval_cons with (n := name_cst _).
    reflexivity.
    exact I.
    apply× apply_Ax.
   eapply eval_cons with (n := name_asgn_1 _).
      reflexivity.
      split.
       intro A. inverts A.
       eexists. splits¬. exact I.
    apply× apply_Ax.
Qed.

Lemma prog_test6_effect :
  eval while_sem prog_test6
    (while_st_prog EnvVEmpty EnvFEmpty)
    (while_res_stat (outs_normal EnvEmpty)).
Proof.
  eapply eval_cons with (n := name_prog_stat _).
    reflexivity.
    exact I.
  apply× apply_R1.
  eapply eval_cons with (n := name_while _ _).
    reflexivity.
    exact I.
  apply× apply_R1.
   eapply eval_cons with (n := name_while_1 _ _).
     reflexivity.
     eexists. splits¬. constructors.
   apply× apply_R2.
    eapply eval_cons with (n := name_cst _).
      reflexivity.
      exact I.
     apply× apply_Ax.
    eapply eval_cons with (n := name_while_2_false _ _).
      reflexivity.
      reflexivity.
     apply× apply_Ax.
Qed.

End ConcreteExample.