Expr.v
Require MyList.
Require Termes.
Require Export Names.
(* external level *)
Inductive
expr: Set :=
SRT: sort -> expr
| REF: name -> expr
| ABS: name -> expr -> expr -> expr
| APP: expr -> expr -> expr
| PROD: name -> expr -> expr -> expr.
Inductive
expr_vars [x:name]: expr->Prop :=
ev_ref: (expr_vars x (REF x))
| ev_abs_l: (y:name)(T,M:expr)(expr_vars x T) -> (expr_vars x (ABS y T M))
| ev_abs_r: (y:name)(T,M:expr) ~x=y -> (expr_vars x M)
-> (expr_vars x (ABS y T M))
| ev_app_l: (u,v:expr)(expr_vars x u) -> (expr_vars x (APP u v))
| ev_app_r: (u,v:expr)(expr_vars x v) -> (expr_vars x (APP u v))
| ev_prod_l: (y:name)(T,U:expr)(expr_vars x T) -> (expr_vars x (PROD y T U))
| ev_prod_r: (y:name)(T,U:expr) ~x=y -> (expr_vars x U)
-> (expr_vars x (PROD y T U)).
Hint ev_ref ev_abs_l ev_abs_r ev_app_l ev_app_r ev_prod_l ev_prod_r.
Lemma
is_free_var: (x:name)(e:expr){(expr_vars x e)}+{~(expr_vars x e)}.
Realizer Fix is_free_var { is_free_var/2: name->expr->sumbool :=
[x,e]Cases e of
(SRT _) => right
| (REF y) => (name_dec x y)
| (ABS y t u) => if (is_free_var x t) then left
else if (name_dec x y) then right
else (is_free_var x u)
| (APP u v) => if (is_free_var x u) then left
else (is_free_var x v)
| (PROD y t u) => if (is_free_var x t) then left
else if (name_dec x y) then right
else (is_free_var x u)
end}.
Program_all.
(Red; Intros).
Inversion H.
(Elim e0; Auto).
(Red; Intros; Apply n).
(Inversion H; Auto).
(Red; Intros; Apply n).
(Inversion_clear H; Auto).
(Elim H0; Auto).
(Red; Intros).
(Inversion H; Auto).
(Red; Intros).
(Inversion H; Auto).
(Red; Intros).
Apply n.
(Inversion H; Auto).
(Elim H2; Auto).
(Red; Intros).
(Inversion H; Auto).
Save.
Inductive
transl_name: (list name)->name->(list name)->name->Prop :=
tr_nil: (x:name)(transl_name (nil name) x (nil name) x)
| tr_hd: (x,y:name)(l1,l2:(list name))
(transl_name (cons ? x l1) x (cons ? y l2) y)
| tr_tl: (x,x0,y,y0:name)(l1,l2:(list name))~x=x0->~y=y0
->(transl_name l1 x l2 y)
->(transl_name (cons ? x0 l1) x (cons ? y0 l2) y).
Inductive
alpha: (list name)->expr->(list name)->expr->Prop :=
alp_srt: (l1,l2:(list name))(s:sort)(alpha l1 (SRT s) l2 (SRT s))
| alp_ref: (l1,l2:(list name))(x,y:name)
(transl_name l1 x l2 y)
->(alpha l1 (REF x) l2 (REF y))
| alp_abs: (l1,l2:(list name))(x,y:name)(A,A',M,M':expr)
(alpha l1 A l2 A')
->(alpha (cons ? x l1) M (cons ? y l2) M')
->(alpha l1 (ABS x A M) l2(ABS y A' M'))
| alp_app: (l1,l2:(list name))(A,A',M,M':expr)
(alpha l1 A l2 A')
->(alpha l1 M l2 M')
->(alpha l1 (APP A M) l2 (APP A' M'))
| alp_prod: (l1,l2:(list name))(x,y:name)(A,A',M,M':expr)
(alpha l1 A l2 A')
->(alpha (cons ? x l1) M (cons ? y l2) M')
->(alpha l1 (PROD x A M) l2 (PROD y A' M')).
(* conversion *)
Inductive
term_expr_equiv: prt_names->term->expr->Prop :=
eqv_srt: (l:prt_names)(s:sort)(term_expr_equiv l (Srt s) (SRT s))
| eqv_ref: (l:prt_names)(x:name)(n:nat)(first_item ? x l n)
->(term_expr_equiv l (Ref n) (REF x))
| eqv_abs: (l:prt_names)(A,M:term)(B,N:expr)(x:name)(term_expr_equiv l A B)
-> (term_expr_equiv (cons ? x l) M N)
-> (term_expr_equiv l (Abs A M) (ABS x B N))
| eqv_app: (l:prt_names)(u,v:term)(a,b:expr)(term_expr_equiv l u a)
-> (term_expr_equiv l v b)
-> (term_expr_equiv l (App u v) (APP a b))
| eqv_prod: (l:prt_names)(A,M:term)(B,N:expr)(x:name)(term_expr_equiv l A B)
-> (term_expr_equiv (cons ? x l) M N)
-> (term_expr_equiv l (Prod A M) (PROD x B N)).
Lemma
equiv_free_db: (l:prt_names)(t:term)(e:expr)(term_expr_equiv l t e)
-> (free_db (length ? l) t).
(Induction 1; Simpl; Intros; Auto).
Apply db_ref.
(Elim H0; Simpl; Auto).
Save.
Lemma
equiv_unique: (l:prt_names)(t:term)(e:expr)(term_expr_equiv l t e)
-> (u:term)(term_expr_equiv l u e) -> t=u.
(Induction 1; Intros).
(Inversion_clear H0; Auto).
Inversion_clear H1.
(Elim first_item_unique with name x l0 n n0; Auto).
Inversion_clear H4.
(Elim H1 with A0; Auto).
(Elim H3 with M0; Auto).
Inversion_clear H4.
(Elim H1 with u1; Auto).
(Elim H3 with v0; Auto).
Inversion_clear H4.
(Elim H1 with A0; Auto).
(Elim H3 with M0; Auto).
Save.
Lemma
unique_alpha: (l1:prt_names)(t:term)(e:expr)(term_expr_equiv l1 t e)
->(l2:prt_names)(f:expr)(term_expr_equiv l2 t f)
->(alpha l1 e l2 f).
(Induction 1; Intros).
Inversion_clear H0.
Apply alp_srt.
Inversion_clear H1.
Apply alp_ref.
Generalize l2 H2 .
(Elim H0; Intros).
Inversion_clear H1.
Apply tr_hd.
Inversion_clear H5.
(Apply tr_tl; Auto).
Inversion_clear H4.
(Apply alp_abs; Auto).
Inversion_clear H4.
(Apply alp_app; Auto).
Inversion_clear H4.
(Apply alp_prod; Auto).
Save.
Theorem
expr_of_term: (t:term)(l:prt_names)(name_unique l)
->(free_db (length ? l) t)
->{e:expr| (term_expr_equiv l t e)}.
(Induction t; Intros).
Exists (SRT s).
Apply eqv_srt.
(Elim (list_item ? l n); Intros).
Inversion_clear y.
Exists (REF x).
Apply eqv_ref.
(Apply name_unique_first; Auto).
ElimType False.
Inversion_clear H0.
Generalize n y H1 .
(Elim l; Simpl).
Intros.
Inversion_clear H0.
(Destruct n; Intros).
(Elim y0 with a; Auto).
(Apply H0 with n1; Auto).
(Red; Intros).
(Elim y0 with t0; Auto).
(Elim H with l; Intros; Auto).
(Elim find_free_var with l; Intros).
(Elim H0 with (cons ? x0 l); Intros).
Exists (ABS x0 x x1).
(Apply eqv_abs; Auto).
(Apply fv_ext; Auto).
(Inversion_clear H2; Auto).
(Inversion_clear H2; Auto).
(Elim H with l; Intros; Auto).
(Elim H0 with l; Intros; Auto).
Exists (APP x x0).
(Apply eqv_app; Auto).
(Inversion_clear H2; Auto).
(Inversion_clear H2; Auto).
(Elim H with l; Intros; Auto).
(Elim find_free_var with l; Intros).
(Elim H0 with (cons ? x0 l); Intros).
Exists (PROD x0 x x1).
(Apply eqv_prod; Auto).
(Apply fv_ext; Auto).
(Inversion_clear H2; Auto).
(Inversion_clear H2; Auto).
Save.
Definition
undef_vars: expr->prt_names->prt_names->Prop :=
[e,def,undef] (list_disjoint ? def undef)
/\(x:name)(In ? x undef)->(expr_vars x e).
Lemma
undef_vars_incl: (e:expr)(l,u1,u2:prt_names)
(incl ? u1 u2)
->(undef_vars e l u2)
->(undef_vars e l u1).
(Unfold undef_vars; Split).
Inversion_clear H0.
(Red; Intros).
(Apply H1 with x; Auto).
Inversion_clear H0;Auto.
Save.
Lemma
undef_vars_abs: (x:name)(e1,e2:expr)(l,u1,u2:prt_names)
(undef_vars e1 l u1)
->(undef_vars e2 (cons ? x l) u2)
->(undef_vars (ABS x e1 e2) l u1^u2).
(Split; Intros).
Inversion_clear H.
Inversion_clear H0.
(Red; Intros).
(Elim In_app with name x0 u1 u2; Intros; Auto).
(Apply H1 with x0; Auto).
(Apply H with x0; Auto).
Inversion_clear H.
Inversion_clear H0.
(Elim In_app with name x0 u1 u2; Intros; Auto).
(Apply ev_abs_r; Auto).
(Red; Intros).
(Apply H with x0; Auto).
(Rewrite -> H5; Auto).
Save.
Lemma
undef_vars_app: (e1,e2:expr)(l,u1,u2:prt_names)
(undef_vars e1 l u1)
->(undef_vars e2 l u2)
->(undef_vars (APP e1 e2) l u1^u2).
(Split; Intros).
Inversion_clear H.
Inversion_clear H0.
(Red; Intros).
(Elim In_app with name x u1 u2; Intros; Auto).
(Apply H1 with x; Auto).
(Apply H with x; Auto).
Inversion_clear H.
Inversion_clear H0.
(Elim In_app with name x u1 u2; Intros; Auto).
Save.
Lemma
undef_vars_prod: (x:name)(e1,e2:expr)(l,u1,u2:prt_names)
(undef_vars e1 l u1)
->(undef_vars e2 (cons ? x l) u2)
->(undef_vars (PROD x e1 e2) l u1^u2).
(Split; Intros).
Inversion_clear H.
Inversion_clear H0.
(Red; Intros).
(Elim In_app with name x0 u1 u2; Intros; Auto).
(Apply H1 with x0; Auto).
(Apply H with x0; Auto).
Inversion_clear H.
Inversion_clear H0.
(Elim In_app with name x0 u1 u2; Intros; Auto).
(Apply ev_prod_r; Auto).
(Red; Intros).
(Apply H with x0; Auto).
(Rewrite -> H5; Auto).
Save.
Lemma
equiv_no_undef: (l:prt_names)(t:term)(e:expr)
(term_expr_equiv l t e)
->(undef:prt_names)(undef_vars e l undef)
->undef=(nil ?).
(Induction 1; Destruct undef; Intros; Auto).
Inversion_clear H0.
(Cut (expr_vars n (SRT s)); Intros; Auto).
Inversion_clear H0.
Inversion_clear H1.
(Elim H2 with n0; Auto).
(Cut (expr_vars n0 (REF x)); Intros; Auto).
Inversion_clear H1.
(Elim H0; Auto).
Inversion_clear H4.
(Cut (expr_vars n (ABS x B N)); Intros; Auto).
(Cut (cons ? n (nil ?))=(nil name); Intros).
Discriminate H7.
Inversion_clear H4.
Apply H1.
(Split; Intros).
(Red; Intros).
(Elim H5 with n; Auto).
Generalize H4 .
(Inversion_clear H8; Auto).
Inversion H9.
Generalize H7 .
(Inversion_clear H4; Auto).
Inversion H8.
Apply H3.
(Split; Intros).
(Red; Intros).
Inversion H4.
Apply H7.
Elim H11.
(Inversion_clear H9; Auto).
Inversion H10.
(Elim H5 with x0; Auto).
(Inversion_clear H9; Auto).
Inversion H13.
Generalize H8 .
(Inversion_clear H4; Auto).
Inversion H9.
Inversion_clear H4.
(Cut (expr_vars n (APP a b)); Intros; Auto).
(Cut (cons ? n (nil ?))=(nil name); Intros).
Discriminate H7.
Inversion_clear H4.
Apply H1.
(Split; Intros).
(Red; Intros).
(Elim H5 with n; Auto).
Generalize H4 .
(Inversion_clear H8; Auto).
Inversion H9.
Generalize H7 .
(Inversion_clear H4; Auto).
Inversion H8.
Apply H3.
(Split; Intros).
(Red; Intros).
(Elim H5 with n; Auto).
Generalize H4 .
(Inversion_clear H8; Auto).
Inversion H9.
Generalize H7 .
(Inversion_clear H4; Auto).
Inversion H8.
Inversion_clear H4.
(Cut (expr_vars n (PROD x B N)); Intros; Auto).
(Cut (cons ? n (nil ?))=(nil name); Intros).
Discriminate H7.
Inversion_clear H4.
Apply H1.
(Split; Intros).
(Red; Intros).
(Elim H5 with n; Auto).
Generalize H4 .
(Inversion_clear H8; Auto).
Inversion H9.
Generalize H7 .
(Inversion_clear H4; Auto).
Inversion H8.
Apply H3.
(Split; Intros).
(Red; Intros).
Inversion H4.
Apply H7.
Elim H11.
(Inversion_clear H9; Auto).
Inversion H10.
(Elim H5 with x0; Auto).
(Inversion_clear H9; Auto).
Inversion H13.
Generalize H8 .
(Inversion_clear H4; Auto).
Inversion H9.
Save.
Theorem
term_of_expr: (e:expr)(l:prt_names)
{t:term| (term_expr_equiv l t e)}
+ {undef:prt_names | (undef_vars e l undef) & ~undef=(nil ?)}.
(*Realizer Fix term_of_expr
{term_of_expr/1: expr->prt_names->(sum term prt_names) :=
[e:expr][l:prt_names]Cases e of
(SRT s) => (inl term prt_names (Srt s))
| (REF x) => Cases (list_index name name_dec x l) of
(inleft n) => (inl term prt_names (Ref n))
| inright => (inr term prt_names (cons ? x (nil name)))
end
| (ABS x e1 e2) =>
Cases (term_of_expr e1 l) (term_of_expr e2 (cons ? x l)) of
(inl a) (inl m) => (inl term prt_names (Abs a m))
| (inr u1) (inr u2) => (inr term prt_names u1^u2)
| (inr u) _ => (inr term prt_names u)
| _ (inr u) => (inr term prt_names u)
end
| (APP e1 e2) =>
Cases (term_of_expr e1 l) (term_of_expr e2 l) of
(inl u) (inl v) => (inl term prt_names (App u v))
| (inr u1) (inr u2) => (inr term prt_names u1^u2)
| (inr u) _ => (inr term prt_names u)
| _ (inr u) => (inr term prt_names u)
end
| (PROD x e1 e2) =>
Cases (term_of_expr e1 l) (term_of_expr e2 (cons ? x l)) of
(inl a) (inl b) => (inl term prt_names (Prod a b))
| (inr u1) (inr u2) => (inr term prt_names u1^u2)
| (inr u) _ => (inr term prt_names u)
| _ (inr u) => (inr term prt_names u)
end
end}.
*)
(Induction e; Intros).
Left.
Exists (Srt s).
Apply eqv_srt.
(Elim (list_index ? name_dec n l); Intros).
Left.
Inversion_clear y.
Exists (Ref x).
(Apply eqv_ref; Auto).
Right.
Exists (cons ? n (nil name)).
Split.
(Red; Intros).
Generalize H .
Inversion_clear H0.
Intros.
Generalize y .
(Elim H0; Intros; Auto).
Inversion_clear H1.
Intros.
Inversion_clear H.
Apply ev_ref.
Inversion_clear H0.
Discriminate.
(Elim H with l; Intros).
(Elim H0 with (cons ? n l); Intros).
Left.
Inversion_clear y.
Inversion_clear y0.
Exists (Abs x x0).
(Apply eqv_abs; Auto).
Inversion_clear y0.
Right.
Exists x.
(Replace x with ((nil ?)^x); Auto).
(Apply undef_vars_abs; Auto).
(Split; Intros).
(Red; Intros).
Inversion_clear H4.
Inversion_clear H3.
Auto.
Inversion_clear y.
(Elim H0 with (cons ? n l); Intros).
Right.
(Exists x; Auto).
Apply undef_vars_incl with (x^(nil ?)).
(Red; Intros).
(Elim H3; Simpl; Auto).
(Apply undef_vars_abs; Auto).
(Split; Intros).
(Red; Intros).
Inversion_clear H4.
Inversion_clear H3.
Inversion_clear y.
Right.
(Exists (x^x0); Intros).
(Apply undef_vars_abs; Auto).
Generalize H2 .
(Case x; Simpl; Intros).
(Elim H5; Auto).
Discriminate.
(Elim H with l; Intros).
(Elim H0 with l; Intros).
Left.
Inversion_clear y.
Inversion_clear y0.
Exists (App x x0).
(Apply eqv_app; Auto).
Inversion_clear y0.
Right.
Exists x.
(Replace x with ((nil ?)^x); Auto).
(Apply undef_vars_app; Auto).
(Split; Intros).
(Red; Intros).
Inversion H4.
Inversion H3.
Auto.
Inversion_clear y.
(Elim H0 with l; Intros).
Right.
(Exists x; Auto).
Apply undef_vars_incl with (x^(nil ?)).
(Red; Intros).
(Elim H3; Simpl; Auto).
(Apply undef_vars_app; Auto).
(Split; Intros).
(Red; Intros).
Inversion_clear H4.
Inversion_clear H3.
Inversion_clear y.
Right.
(Exists (x^x0); Intros).
(Apply undef_vars_app; Auto).
Generalize H2 .
(Case x; Simpl; Intros).
(Elim H5; Auto).
Discriminate.
(Elim H with l; Intros).
(Elim H0 with (cons ? n l); Intros).
Left.
Inversion_clear y.
Inversion_clear y0.
Exists (Prod x x0).
(Apply eqv_prod; Auto).
Inversion_clear y0.
Right.
Exists x.
(Replace x with ((nil ?)^x); Auto).
(Apply undef_vars_prod; Auto).
(Split; Intros).
(Red; Intros).
Inversion H4.
Inversion H3.
Auto.
Inversion_clear y.
(Elim H0 with (cons ? n l); Intros).
Right.
(Exists x; Auto).
Apply undef_vars_incl with (x^(nil ?)).
(Red; Intros).
(Elim H3; Simpl; Auto).
(Apply undef_vars_prod; Auto).
(Split; Intros).
(Red; Intros).
Inversion H4.
Inversion H3.
Inversion_clear y.
Right.
(Exists (x^x0); Intros).
(Apply undef_vars_prod; Auto).
Generalize H2 .
(Case x; Simpl; Intros).
(Elim H5; Auto).
Discriminate.
Save.
18/02/97, 12:21