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

Require Export LibHeap.

Module Heap := LibHeap.HeapList.

Section ConcreteExample.

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

Inductive error : Set :=
  | Err
  .

Definition Env := Heap.heap var Val.

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

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

Definition EnvEmpty : Env := 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 aborts : outs → Prop :=
  | aborts_error : ∀ err,
    aborts (outs_error err)
  .

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
  .

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
  .

Inductive prog :=
  | prog_expr : expr → prog
  | prog_ext_expr : ext_expr → prog
  | prog_stat : stat → prog
  | prog_ext_stat : ext_stat → prog
  .

Coercion prog_expr : expr >-> prog.
Coercion prog_ext_expr : ext_expr >-> prog.
Coercion prog_stat : stat >-> prog.
Coercion prog_ext_stat : ext_stat >-> prog.

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
  | _, _ ⇒ 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.

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)
  | _, _ ⇒ 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.

Definition compare_prog p1 p2 :=
  match p1, p2 with
  | prog_expr e1, prog_expr e2 ⇒ decide (e1 = e2)
  | prog_ext_expr e1, prog_ext_expr e2 ⇒ decide (e1 = e2)
  | prog_stat s1, prog_stat s2 ⇒ decide (s1 = s2)
  | prog_ext_stat s1, prog_ext_stat s2 ⇒ decide (s1 = s2)
  | _, _ ⇒ false
  end.

Global Instance prog_Comparable : Comparable prog.
  applys comparable_beq compare_prog. 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_prog : prog → prog → Prop :=
  | sub_prog_expr_expr : ∀ e1 e2,
    sub_expr_expr e1 e2 →
    sub_prog e1 e2
  | sub_prog_expr_ext_expr : ∀ e1 e2,
    sub_expr_ext_expr e1 e2 →
    sub_prog e1 e2
  | sub_prog_expr_stat : ∀ e1 s2,
    sub_expr_stat e1 s2 →
    sub_prog e1 s2
  | sub_prog_expr_ext_stat : ∀ e1 s2,
    sub_expr_ext_stat e1 s2 →
    sub_prog e1 s2
  | sub_prog_stat_stat : ∀ s1 s2,
    sub_stat_stat s1 s2 →
    sub_prog s1 s2
  | sub_prog_stat_ext_stat : ∀ s1 s2,
    sub_stat_ext_stat s1 s2 →
    sub_prog s1 s2
  .

Global Instance sub_prog_Decidable : ∀ t1 t2,
    Decidable (sub_prog 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 sign_name :=
  | name_abort_ext_expr : ext_expr → sign_name
  | name_abort_ext_stat : ext_stat → sign_name
  | name_cst : Val → sign_name
  | name_var : var → sign_name
  | name_varUndef : var → sign_name
  | name_add : expr → expr → sign_name
  | name_add_1 : expr → sign_name
  | name_add_2 : sign_name
  | name_skip : sign_name
  | name_throw : sign_name
  | name_asgn : var → expr → sign_name
  | name_asgn_1 : var → sign_name
  | name_seq : stat → stat → sign_name
  | name_seq_1 : stat → sign_name
  | name_if : expr → stat → stat → sign_name
  | name_if_1_true : stat → stat → sign_name
  | name_if_1_false : stat → stat → sign_name
  | name_while : expr → stat → sign_name
  | name_while_1 : expr → stat → sign_name
  | name_while_2_true : expr → stat → sign_name
  | name_while_2_false : expr → stat → sign_name
  .

Definition sign_struct n : Rule_struct prog :=
  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_varUndef x ⇒ Rule_struct_Ax _
  | name_add e1 e2 ⇒ Rule_struct_R2 (term := prog) e1 (expr_add_1 e2)
  | name_add_1 e2 ⇒ Rule_struct_R2 (term := prog) 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 := prog) e (stat_asgn_1 x)
  | name_asgn_1 x ⇒ Rule_struct_Ax _
  | name_seq s1 s2 ⇒ Rule_struct_R2 (term := prog) s1 (stat_seq_1 s2)
  | name_seq_1 s2 ⇒ Rule_struct_R1 (term := prog) s2
  | name_if e s1 s2 ⇒ Rule_struct_R2 (term := prog) e (stat_if_1 s1 s2)
  | name_if_1_true s1 s2 ⇒ Rule_struct_R1 (term := prog) s1
  | name_if_1_false s1 s2 ⇒ Rule_struct_R1 (term := prog) s2
  | name_while e s ⇒ Rule_struct_R1 (term := prog) (stat_while_1 e s)
  | name_while_1 e s ⇒ Rule_struct_R2 (term := prog) e (stat_while_2 e s)
  | name_while_2_true e s ⇒ Rule_struct_R2 (term := prog) s (stat_while_1 e s)
  | name_while_2_false e s ⇒ Rule_struct_Ax _
  end.

Definition sign_left n : prog :=
  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_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_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
  end.

Definition sign_str := {|

    term := prog;
    name := sign_name;

    rule_struct := sign_struct;

    left := sign_left

  |}.

Inductive sign_res : Type :=
  | sign_res_expr : oute → sign_res
  | sign_res_stat : outs → sign_res
  .

Coercion sign_res_expr : oute >-> sign_res.
Coercion sign_res_stat : outs >-> sign_res.

Inductive abort_res : sign_res → Prop :=
  | abort_res_expr : abort_res (sign_res_expr Err)
  | abort_res_stat : abort_res (sign_res_stat Err)
  .

Inductive sign_st : Type :=
  | sign_st_prog : Env → sign_st
  | sign_st_add_1 : Env → sign_res → sign_st
  | sign_st_add_2 : Val → sign_res → sign_st
  | sign_st_asgn_1 : Env → sign_res → sign_st
  | sign_st_seq_1 : sign_res → sign_st
  | sign_st_if_1 : Env → sign_res → sign_st
  | sign_st_while_1 : sign_res → sign_st
  | sign_st_while_2 : Env → sign_res → sign_st
  .

Inductive abort_st : sign_st → Prop :=
  | abort_st_add_1 : ∀ E r,
    abort_res r →
    abort_st (sign_st_add_1 E r)
  | abort_st_add_2 : ∀ v r,
    abort_res r →
    abort_st (sign_st_add_2 v r)
  | abort_st_asgn_1 : ∀ E r,
    abort_res r →
    abort_st (sign_st_asgn_1 E r)
  | abort_st_seq_1 : ∀ r,
    abort_res r →
    abort_st (sign_st_seq_1 r)
  | abort_st_if_1 : ∀ E r,
    abort_res r →
    abort_st (sign_st_if_1 E r)
  | abort_st_while_1 : ∀ r,
    abort_res r →
    abort_st (sign_st_while_1 r)
  | abort_st_while_2 : ∀ E r,
    abort_res r →
    abort_st (sign_st_while_2 E r)
  .

Definition sign_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, sign_st_prog E ⇒
      True
  | name_var x, sign_st_prog E ⇒
      indom E x
  | name_varUndef x, sign_st_prog E ⇒
      ¬ indom E x
  | name_add e1 e2, sign_st_prog E ⇒
      True
  | name_add_1 e2, sign_st_add_1 E r ⇒
      ∃ o, r = sign_res_expr o ∧ is_val o
  | name_add_2, sign_st_add_2 v r ⇒
      ∃ o, r = sign_res_expr o ∧ is_val o
  | name_skip, sign_st_prog E ⇒
      True
  | name_throw, sign_st_prog E ⇒
      True
  | name_asgn x e, sign_st_prog E ⇒
      True
  | name_asgn_1 x, sign_st_asgn_1 E r ⇒
      ∃ o, r = sign_res_expr o ∧ is_val o
  | name_seq s1 s2, sign_st_prog E ⇒
      True
  | name_seq_1 s2, sign_st_seq_1 r ⇒
      ∃ o, r = sign_res_stat o ∧ is_env o
  | name_if e s1 s2, sign_st_prog E ⇒
      True
  | name_if_1_true s1 s2, sign_st_if_1 E o ⇒
      ∃ v, v ≠ 0 ∧ o = oute_val v
  | name_if_1_false s1 s2, sign_st_if_1 E o ⇒
      o = oute_val 0
  | name_while e s, sign_st_prog E ⇒
      True
  | name_while_1 e s, sign_st_while_1 r ⇒
      ∃ o, r = sign_res_stat o ∧ is_env o
  | name_while_2_true e s, sign_st_while_2 E o ⇒
      ∃ v, v ≠ 0 ∧ o = oute_val v
  | name_while_2_false e s, sign_st_while_2 E o ⇒
      o = oute_val 0
  | _, _ ⇒
      False
  end.

Definition if_st_prog A (f : _ → option A) sigma :=
  match sigma with
  | sign_st_prog E ⇒ f E
  | _ ⇒ None
  end.

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

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

Definition sign_rule n : Rule sign_st sign_res :=
  match n with
  | name_abort_ext_expr e ⇒
    let ax _ := Some (sign_res_expr Err) in
    Rule_Ax ax
  | name_abort_ext_stat s ⇒
    let ax _ := Some (sign_res_stat Err) in
    Rule_Ax ax
  | name_cst c ⇒
    let ax _ := Some (oute_val c : sign_res) in
    Rule_Ax ax
  | name_var x ⇒
    let ax :=
      if_st_prog (fun E ⇒
        option_map (oute_val : _ → sign_res) (read_option E x)) in
    Rule_Ax ax
  | name_varUndef x ⇒
    let ax _ := Some (Err : sign_res) in
    Rule_Ax ax
  | name_add e1 e2 ⇒
    let up :=
      if_st_prog (fun E ⇒
        Some (sign_st_prog E)) in
    let next E o :=
      if_st_prog (fun E ⇒
        Some (sign_st_add_1 E o)) E in
    Rule_R2 up next
  | name_add_1 e2 ⇒
    let up sigma :=
      match sigma with
      | sign_st_add_1 E o ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    let next sigma r :=
      match sigma with
      | sign_st_add_1 E (oute_val v) ⇒ Some (sign_st_add_2 v r)
      | _ ⇒ None
      end in
    Rule_R2 up next
  | name_add_2 ⇒
    let ax sigma :=
      match sigma with
      | sign_st_add_2 v1 (oute_val v2) ⇒ Some (oute_val (v1 + v2) : sign_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  | name_skip ⇒
    let ax :=
      if_st_prog (fun E ⇒
        Some (outs_normal E : sign_res)) in
    Rule_Ax ax
  | name_throw ⇒
    let ax _ := Some (sign_res_stat Err) in
    Rule_Ax ax
  | name_asgn x e ⇒
    let up :=
      if_st_prog (fun E ⇒
        Some (sign_st_prog E)) in
    let next E r :=
      if_st_prog (fun E ⇒
        Some (sign_st_asgn_1 E r)) E in
    Rule_R2 up next
  | name_asgn_1 x ⇒
    let ax sigma :=
      match sigma with
      | sign_st_asgn_1 E (oute_val v) ⇒ Some (outs_normal (write E x v) : sign_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  | name_seq s1 s2 ⇒
    let up :=
      if_st_prog (fun E ⇒
        Some (sign_st_prog E)) in
    let next E r :=
      if_st_prog (fun E ⇒
        Some (sign_st_seq_1 r)) E in
    Rule_R2 up next
  | name_seq_1 s2 ⇒
    let up sigma :=
      match sigma with
      | sign_st_seq_1 (outs_normal E) ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_if e s1 s2 ⇒
    let up :=
      if_st_prog (fun E ⇒
        Some (sign_st_prog E)) in
    let next E r :=
      if_st_prog (fun E ⇒
        Some (sign_st_if_1 E r)) E in
    Rule_R2 up next
  | name_if_1_true s1 s2 ⇒
    let up sigma :=
      match sigma with
      | sign_st_if_1 E o ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_if_1_false s1 s2 ⇒
    let up sigma :=
      match sigma with
      | sign_st_if_1 E o ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    Rule_R1 _ up
  | name_while e s ⇒
    let up :=
      if_st_prog (fun E ⇒
        Some (sign_st_while_1 (outs_normal E))) in
    Rule_R1 _ up
  | name_while_1 e s ⇒
    let up sigma :=
      match sigma with
      | sign_st_while_1 (sign_res_stat (outs_normal E)) ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    let next sigma r :=
      match sigma with
      | sign_st_while_1 (sign_res_stat (outs_normal E)) ⇒ Some (sign_st_while_2 E r)
      | _ ⇒ None
      end in
    Rule_R2 up next
  | name_while_2_true e s ⇒
    let up sigma :=
      match sigma with
      | sign_st_while_2 E r ⇒ Some (sign_st_prog E)
      | _ ⇒ None
      end in
    let next sigma r := Some (sign_st_while_1 r) in
    Rule_R2 up next
  | name_while_2_false e s ⇒
    let ax sigma :=
      match sigma with
      | sign_st_while_2 E o ⇒ Some (outs_normal E : sign_res)
      | _ ⇒ None
      end in
    Rule_Ax ax
  end.

Definition sign_sem :=
  make_semantics sign_str sign_cond sign_rule.

Lemma sign_rule_format_correct : rule_format_correct_all sign_sem.
Proof. intro n. destruct n; constructors. Qed.

Lemma sign_semantics_full : semantics_full sign_sem.
Proof.
  introv C. simpls. destruct n; destruct sigma; simpls; tryfalse; try solve [ constructors¬ ].
   constructors¬. simpl. rewrite read_option_def. cases_if; simpls¬. false¬ C.
   constructors¬.
    simpls¬.
    introv. eexists. reflexivity.
   constructors¬.
    introv. lets (o&E&V): C. rewrite E. destruct o as [v|]; tryfalse. eexists. reflexivity.
   lets (o&E&V): C. rewrite E. destruct o as [v2|]; tryfalse. constructors¬.
   constructors¬. reflexivity.
   constructors¬.
    simpls¬.
    introv. eexists. reflexivity.
   lets (o&E&V): C. rewrite E. destruct o as [v2|]; tryfalse. constructors¬.
   constructors¬.
    simpls¬.
    introv. eexists. reflexivity.
   lets (o&Eq&V): C. rewrite Eq. destruct o as [E|]; tryfalse. constructors¬.
   constructors¬.
    simpls¬.
    introv. eexists. reflexivity.
   constructors¬. simpls¬.
   lets (o&Eq&V): C. rewrite Eq. destruct o as [E|]; tryfalse. constructors¬.
    introv. eexists. reflexivity.
   lets (o&Nz&Eq): C. rewrite Eq. constructors¬.
    introv. eexists. reflexivity.
Qed.

Definition prog_test0 : prog :=
  
    (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 : prog :=
  stat_asgn "x"%string (expr_cst 42).

Definition prog_test2 : prog :=
  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 : prog :=
  stat_while (expr_var "x"%string)
    (stat_asgn "x"%string (expr_add (expr_var "x"%string) (expr_cst 1))).

Definition prog_test4 : prog :=
  stat_while (expr_cst 0)
    (stat_asgn "x"%string (expr_cst 42)).

Definition prog_test5 : prog :=
  stat_while (expr_cst 1)
    (stat_asgn "x"%string (expr_cst 42)).

Definition prog_test6 : prog :=
  stat_asgn "x"%string (expr_add (expr_cst 42) (expr_add (expr_cst 18) (expr_cst 17))).

Definition prog_test7 : prog :=
  (stat_seq
    (stat_asgn "x" (expr_cst 1))
    (stat_while (expr_var "x")
      (stat_asgn "x" (expr_cst 0))))%string.

Definition prog_test8 : prog :=
  (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_test9 : prog :=
  stat_if (expr_var "x"%string) stat_throw stat_skip.

Definition prog_test10 : prog :=
  (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_test11 : prog :=
  (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_test12 : prog :=
  (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.

Lemma prog_test1_effect :
  eval sign_sem prog_test1
    (sign_st_prog EnvEmpty)
    (outs_normal (write EnvEmpty "x"%string 42)).
Proof.
  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.
      eexists. splits¬. exact I.
    apply× apply_Ax.
Qed.

Lemma prog_test4_effect :
  eval sign_sem prog_test4
    (sign_st_prog EnvEmpty)
    (sign_res_stat (outs_normal EnvEmpty)).
Proof.
  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.