<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* generated by Ott 0.10.14 from: ../tests/test8.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.

(** syntax *)
Definition value_name := nat.
Lemma eq_value_name: forall (x y : value_name), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_value_name : ott_coq_equality.

Definition ident := nat.
Definition integer_literal := nat.
Definition index := nat.

Inductive 
typeconstr : Set := 
   TC_unit : typeconstr
 | TC_bool : typeconstr
 | TC_int : typeconstr
.

Inductive 
typvar : Set := 
   TV_ident : ident -> typvar
.

Inductive 
typexpr : Set := 
   TE_var : typvar -> typexpr
 | TE_arrow : typexpr -> typexpr -> typexpr
 | TE_constr0 : typeconstr -> typexpr
.

Inductive 
list_typvar : Set := 
   Nil_list_typvar : list_typvar
 | Cons_list_typvar : typvar -> list_typvar -> list_typvar
.

Inductive 
constant : Set := 
   CONST_int : integer_literal -> constant
 | CONST_false : constant
 | CONST_true : constant
 | CONST_unit : constant
 | CONST_and : constant
 | CONST_not : constant
.

Inductive 
typscheme : Set := 
   TS_ts : list_typvar -> typexpr -> typscheme
.

Inductive 
expr : Set := 
   E_ident : value_name -> expr
 | E_constant : constant -> expr
 | E_apply : expr -> expr -> expr
 | E_function : value_name -> expr -> expr
 | E_let : value_name -> expr -> expr -> expr
.

Inductive 
G : Set := 
   G_em : G
 | G_vn : G -> value_name -> typscheme -> G
.
Lemma eq_typvar: forall (x y : typvar), {x = y} + {x <> y}.
Proof.
decide equality. apply eq_value_name.
Defined.
Hint Resolve eq_typvar : ott_coq_equality.


(** auxiliary functions on the new list types *)
Fixpoint map_list_typvar (A:Set) (f:typvar->A) (l:list_typvar) {struct l} : list A :=
  match l with
  | Nil_list_typvar => nil
  | Cons_list_typvar h tl_ => cons (f h) (map_list_typvar A f tl_)
  end.
Implicit Arguments map_list_typvar.

Fixpoint make_list_typvar (l:list typvar) : list_typvar :=
  match l with
  | nil  => Nil_list_typvar
  | cons h tl_ => Cons_list_typvar h (make_list_typvar tl_)
  end.

Fixpoint unmake_list_typvar (l:list_typvar) :  list typvar :=
  match l with
  | Nil_list_typvar => nil
  | Cons_list_typvar h tl_ =>  cons h (unmake_list_typvar tl_)
  end.

Fixpoint nth_list_typvar (n:nat) (l:list_typvar) {struct n} : option typvar :=
  match n,l with
  | 0, Cons_list_typvar h tl_ => Some h
  | 0, other => None
  | S m, Nil_list_typvar => None
  | S m, Cons_list_typvar h tl_ => nth_list_typvar m tl_
  end.
Implicit Arguments nth_list_typvar.

Fixpoint app_list_typvar (l m:list_typvar) {struct l} : list_typvar :=
  match l with
  | Nil_list_typvar => m
  | Cons_list_typvar h tl_ => Cons_list_typvar h (app_list_typvar tl_ m)
  end.


(** library functions *)
Fixpoint list_mem (A:Set) (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list A) {struct l} : bool :=
  match l with
  | nil => false
  | cons h t => if eq h x then true else list_mem A eq x t
end.
Implicit Arguments list_mem.

Fixpoint list_assoc (A B:Set) (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list (A*B)) {struct l} : option B :=
  match l with
  | nil => None
  | cons (a,b) t => if (eq a x) then Some b else list_assoc A B eq x t
end.
Implicit Arguments list_assoc.

Fixpoint list_filter (A B:Set) (f:(A*B)->bool) (l:list (A*B)) {struct l} : list (A*B) :=
  match l with
  | nil => nil
  | cons h t => if (f h) then cons h (list_filter A B f t) else (list_filter A B f t)
end.
Implicit Arguments list_filter.

Fixpoint list_minus (A:Set) (eq:forall a b:A,{a=b}+{a<>b}) (l1:list A) (l2:list A) {struct l1} : list A :=
  match l1 with
  | nil => nil
  | cons h t => if (list_mem (A:=A) eq h l2) then list_minus A eq t l2 else cons h (list_minus A eq t l2)
end.
Implicit Arguments list_minus.


(** subrules *)
Definition is_value_of_expr (e5:expr) : Prop :=
  match e5 with
  | (E_ident value_name5) => False
  | (E_constant constant5) => (True)
  | (E_apply expr5 expr') => False
  | (E_function value_name5 expr5) => (True)
  | (E_let value_name5 expr5 expr') => False
end.


(** free variables *)
Fixpoint ftv_typexpr (t5:typexpr) : list typvar :=
  match t5 with
  | (TE_var typvar5) => (cons typvar5 nil)
  | (TE_arrow typexpr5 typexpr') => (app (ftv_typexpr typexpr5) (ftv_typexpr typexpr'))
  | (TE_constr0 typeconstr5) => nil
end.

Definition ftv_typscheme (ts5:typscheme) : list typvar :=
  match ts5 with
  | (TS_ts typvar_list typexpr5) => (app nil (list_minus eq_typvar (ftv_typexpr typexpr5) (unmake_list_typvar typvar_list)))
end.

Fixpoint ftv_G (G_6:G) : list typvar :=
  match G_6 with
  | G_em => nil
  | (G_vn G5 value_name5 typscheme5) => (app (ftv_G G5) (ftv_typscheme typscheme5))
end.


(** substitutions *)
Fixpoint tsubst_typexpr (sub:list (typvar*typexpr)) (t_6:typexpr) {struct t_6} : typexpr :=
  match t_6 with
  | (TE_var typvar5) => (match list_assoc eq_typvar typvar5 sub with None => (TE_var typvar5) | Some t5 => t5 end)
  | (TE_arrow typexpr5 typexpr') => TE_arrow (tsubst_typexpr sub typexpr5) (tsubst_typexpr sub typexpr')
  | (TE_constr0 typeconstr5) => TE_constr0 typeconstr5
end.

Definition tsubst_typscheme (sub:list (typvar*typexpr)) (ts5:typscheme) : typscheme :=
  match ts5 with
  | (TS_ts typvar_list typexpr5) => TS_ts typvar_list (tsubst_typexpr (list_filter (fun (tmp:typvar*typexpr) => match tmp with (tv5,t5) => negb (list_mem eq_typvar tv5 (unmake_list_typvar typvar_list)) end) sub) typexpr5)
end.

Fixpoint subst_expr (e5:expr) (x5:value_name) (e_6:expr) {struct e_6} : expr :=
  match e_6 with
  | (E_ident value_name5) => (if eq_value_name value_name5 x5 then e5 else (E_ident value_name5))
  | (E_constant constant5) => E_constant constant5
  | (E_apply expr5 expr') => E_apply (subst_expr e5 x5 expr5) (subst_expr e5 x5 expr')
  | (E_function value_name5 expr5) => E_function value_name5 (if list_mem eq_value_name x5 (cons value_name5 nil) then expr5 else (subst_expr e5 x5 expr5))
  | (E_let value_name5 expr5 expr') => E_let value_name5 (subst_expr e5 x5 expr5) (if list_mem eq_value_name x5 (cons value_name5 nil) then expr' else (subst_expr e5 x5 expr'))
end.

Fixpoint tsubst_G (sub:list (typvar*typexpr)) (G_6:G) {struct G_6} : G :=
  match G_6 with
  | G_em => G_em 
  | (G_vn G5 value_name5 typscheme5) => G_vn (tsubst_G sub G5) value_name5 (tsubst_typscheme sub typscheme5)
end.

Fixpoint remove_duplicates (l:list_typvar) : list_typvar :=
  match l with
  | Nil_list_typvar => Nil_list_typvar
  | Cons_list_typvar h t => 
    if (list_mem eq_typvar h (unmake_list_typvar t))  
    then remove_duplicates t
    else Cons_list_typvar h (remove_duplicates t)
end. 


(** definitions *)
(* defns Jtype *)

Inductive
(* defn VTSin *)

VTSin : value_name -> typscheme -> G -> Prop :=
 | VTSin_vn1 : forall (value_name5:value_name) (typscheme5:typscheme) (G5:G),
     VTSin value_name5 typscheme5 (G_vn G5 value_name5 typscheme5)
 | VTSin_vn2 : forall (value_name5:value_name) (typscheme5:typscheme) (G5:G) (value_name':value_name) (typscheme':typscheme),
     VTSin value_name5 typscheme5 G5 ->
      not(  value_name5 = value_name'  )  ->
     VTSin value_name5 typscheme5 (G_vn G5 value_name' typscheme')


with
(* defn G_constant *)

G_constant : G -> constant -> typexpr -> Prop :=
 | constant_int : forall (G5:G) (integer_literal5:integer_literal),
     G_constant G5 (CONST_int integer_literal5) (TE_constr0 TC_int)
 | constant_false : forall (G5:G),
     G_constant G5 CONST_false (TE_constr0 TC_bool)
 | constant_true : forall (G5:G),
     G_constant G5 CONST_true (TE_constr0 TC_bool)
 | constant_unit : forall (G5:G),
     G_constant G5 CONST_unit (TE_constr0 TC_unit)
 | constant_and : forall (G5:G),
     G_constant G5 CONST_and (TE_arrow (TE_constr0 TC_bool)  (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool)) )
 | constant_not : forall (G5:G),
     G_constant G5 CONST_not (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool))


with
(* defn Get *)

Get : G -> expr -> typexpr -> Prop :=
 | Get_value_name : forall (G5:G) (x:value_name) (t:typexpr) (typscheme5:typscheme),
     VTSin x typscheme5 G5 ->
      (exists tvs, exists txp, exists s, 
              typscheme5  = TS_ts tvs txp 
             /\ tvs = make_list_typvar
                    (List.map (fun (x:typvar*typexpr) => match x with (x1,x2) => x1 end) 
                              s)  
             /\ tsubst_typexpr s txp =  t )  ->
     Get G5 (E_ident x) t
 | Get_constant : forall (G5:G) (constant5:constant) (t:typexpr),
     G_constant G5 constant5 t ->
     Get G5 (E_constant constant5) t
 | Get_apply : forall (G5:G) (e:expr) (e':expr) (t2:typexpr) (t1:typexpr),
     Get G5 e (TE_arrow t1 t2) ->
     Get G5 e' t1 ->
     Get G5 (E_apply e e') t2
 | Get_lambda : forall (G5:G) (x1:value_name) (e:expr) (t1:typexpr) (t:typexpr),
     Get (G_vn G5 x1 (TS_ts Nil_list_typvar t1)) e t ->
     Get G5 (E_function x1 e) (TE_arrow t1 t)
 | Get_let : forall (G5:G) (x:value_name) (e:expr) (e':expr) (t':typexpr) (t:typexpr) (typscheme5:typscheme),
     Get G5 e t ->
     Get (G_vn G5 x typscheme5) e' t' ->
      typscheme5 =  (TS_ts (remove_duplicates (make_list_typvar (list_minus eq_typvar (ftv_typexpr  t ) (ftv_G  G5 ))))  t )   ->
     Get G5 (E_let x e e') t'

.
(* defns Jop *)

Inductive
(* defn red *)

JO_red : expr -> expr -> Prop :=
 | JO_red_app : forall (x:value_name) (e:expr) (v:expr),
     is_value_of_expr v ->
     JO_red (E_apply  (E_function x e)  v)  (subst_expr  v   x   e ) 
 | JO_red_let : forall (x:value_name) (e:expr) (v:expr),
     is_value_of_expr v ->
     JO_red (E_let x v e)  (subst_expr  v   x   e ) 
 | JO_red_context_app1 : forall (e:expr) (e1:expr) (e':expr),
     JO_red e e' ->
     JO_red (E_apply e e1) (E_apply e' e1)
 | JO_red_context_app2 : forall (v:expr) (e:expr) (e':expr),
     is_value_of_expr v ->
     JO_red e e' ->
     JO_red (E_apply v e) (E_apply v e')
 | JO_red_context_let : forall (x:value_name) (e:expr) (e1:expr) (e':expr),
     JO_red e e' ->
     JO_red (E_let x e e1) (E_let x e' e1)
 | JO_red_not_1 : 
     JO_red (E_apply (E_constant CONST_not) (E_constant CONST_true)) (E_constant CONST_false)
 | JO_red_not_2 : 
     JO_red (E_apply (E_constant CONST_not) (E_constant CONST_false)) (E_constant CONST_true)
 | JO_red_and_1 : forall (e:expr),
     JO_red (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_true))  e) e
 | JO_red_and_2 : forall (e:expr),
     JO_red (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_false))  e) (E_constant CONST_false)

.