(****************************************************************
Copyright © 2010-2024 Amy Felty
This file is part of "Two-Level Hybrid in Coq"
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see .
***************************************************************)
(****************************************************************
File: Shapes.v
original: January 2010
updated: March 2014
Apr 2024: Current Coq Version: V8.18.0
Definition of lambda terms, predicates, and judgments plus
proofs of internal adequacy for all judgments
***************************************************************)
From HybridSys Require Export sl.
#[global] Hint Resolve level_CON level_VAR level_BND level_APP level_ABS : hybrid.
#[global] Hint Resolve proper_APP abstr_proper : hybrid.
#[global] Hint Unfold proper: hybrid.
Section encoding.
Hint Rewrite ext_eq_eta : hybrid.
(****************************************************************
Constants for Two Kinds of Terms
****************************************************************)
Inductive Econ: Set := cAPP: Econ | cLAM: Econ | cAPPLY : Econ | cFUN : Econ.
Definition uexp : Set := expr Econ.
Definition Var : var -> uexp := (VAR Econ).
Definition Bnd : bnd -> uexp := (BND Econ).
Definition app : uexp -> uexp -> uexp :=
fun e1:uexp => fun e2:uexp => (APP (APP (CON cAPP) e1) e2).
Definition lam : (uexp -> uexp) -> uexp :=
fun e:uexp->uexp => (APP (CON cLAM) (lambda e)).
Definition apply : uexp -> uexp -> uexp :=
fun e1:uexp => fun e2:uexp => (APP (APP (CON cAPPLY) e1) e2).
Definition fn : (uexp -> uexp) -> uexp :=
fun e:uexp->uexp => (APP (CON cFUN) (lambda e)).
(****************************************************************
Some Properties of Constructors
****************************************************************)
Lemma proper_Var: forall x:var, (proper (Var x)).
Proof.
unfold Var; auto with hybrid.
Qed.
Lemma proper_lam : forall (e:uexp->uexp),
abstr e -> proper (lam e).
Proof.
unfold lam; auto with hybrid.
Qed.
Lemma proper_app : forall e1 e2:uexp,
proper e1 -> proper e2 -> proper (app e1 e2).
Proof.
unfold app; auto with hybrid.
Qed.
Lemma proper_fn : forall (e:uexp->uexp),
abstr e -> proper (fn e).
Proof.
unfold fn; auto with hybrid.
Qed.
Lemma proper_apply : forall e1 e2:uexp,
proper e1 -> proper e2 -> proper (apply e1 e2).
Proof.
unfold apply; auto with hybrid.
Qed.
Hint Resolve proper_Var : hybrid.
(****************************************************************
The atm type and instantiation of oo.
****************************************************************)
Inductive atm : Set :=
is_tm : uexp -> atm
| is_exp : uexp -> atm
| eq_a : uexp -> uexp -> atm
| shape : uexp -> uexp -> atm
| varT : uexp -> atm
| varE : uexp -> atm
| varTOcc : uexp -> nat -> atm
| varEOcc : uexp -> nat -> atm.
Definition oo_ := oo atm Econ.
Definition atom_ : atm -> oo_ := atom Econ.
Definition T_ : oo_ := T atm Econ.
Hint Unfold oo_ atom_ T_: hybrid.
Hint Unfold oo_ atom_ T_: hybrid.
(****************************************************************
Definition of prog
****************************************************************)
Inductive prog : atm -> oo_ -> Prop :=
(* well-formedness of terms (app and lam) *)
| tm_app : forall T1 T2:uexp,
prog (is_tm (app T1 T2))
(Conj (atom_ (is_tm T1)) (atom_ (is_tm T2)))
| tm_lam : forall T:uexp->uexp, abstr T ->
prog (is_tm (lam T))
(All (fun x:uexp =>
(Imp (is_tm x) (atom_ (is_tm (T x))))))
(* well-formedness of expressions (apply and fn) *)
| exp_apply : forall E1 E2:uexp,
prog (is_exp (apply E1 E2))
(Conj (atom_ (is_exp E1)) (atom_ (is_exp E2)))
| exp_fn : forall E:uexp->uexp, abstr E ->
prog (is_exp (fn E))
(All (fun x:uexp =>
(Imp (is_exp x) (atom_ (is_exp (E x))))))
(* algorithmic equality between terms and expressions *)
| eq_lam : forall T E:uexp->uexp, abstr T -> abstr E ->
prog (eq_a (lam T) (fn E))
(All (fun x:uexp =>
(All (fun y:uexp =>
(Imp (eq_a x y) (atom_ (eq_a (T x) (E y))))))))
| eq_app : forall T1 T2 E1 E2:uexp,
prog (eq_a (app T1 T2) (apply E1 E2))
(Conj (atom_ (eq_a T1 E1)) (atom_ (eq_a T2 E2)))
(* same shape for terms and expressions *)
| sh_v : forall T E:uexp,
prog (shape T E)
(Conj (atom_ (varT T)) (atom_ (varE E)))
| sh_lam : forall T E:uexp->uexp, abstr T -> abstr E ->
prog (shape (lam T) (fn E))
(All (fun x:uexp =>
(All (fun y:uexp =>
(Imp (varT x) (Imp (varE y) (atom_ (shape (T x) (E y)))))))))
| sh_app : forall T1 T2 E1 E2:uexp,
prog (shape (app T1 T2) (apply E1 E2))
(Conj (atom_ (shape T1 E1)) (atom_ (shape T2 E2)))
(* counting variables in terms *)
| v_lm : forall T:uexp->uexp, forall N:nat, abstr T ->
prog (varTOcc (lam T) N)
(All (fun x:uexp => (Imp (varT x) (atom_ (varTOcc (T x) N)))))
| v_app : forall T1 T2:uexp, forall N1 N2:nat,
prog (varTOcc (app T1 T2) (N1+N2))
(Conj (atom_ (varTOcc T1 N1)) (atom_ (varTOcc T2 N2)))
| v_varT : forall T:uexp,
prog (varTOcc T 1) (atom_ (varT T))
(* counting variables in expressions *)
| v_fn : forall E:uexp->uexp, forall N:nat, abstr E ->
prog (varEOcc (fn E) N)
(All (fun x:uexp => (Imp (varE x) (atom_ (varEOcc (E x) N)))))
| v_apply : forall E1 E2:uexp, forall N1 N2:nat,
prog (varEOcc (apply E1 E2) (N1+N2))
(Conj (atom_ (varEOcc E1 N1)) (atom_ (varEOcc E2 N2)))
| v_varE : forall E:uexp,
prog (varEOcc E 1) (atom_ (varE E)).
(****************************************************************
Instantiation of seq
****************************************************************)
Definition seq_ : nat -> list atm -> oo_ -> Prop := sl.seq prog.
Definition seq'_ := seq' prog.
Definition seq0 (B : oo_) : Prop := seq'_ nil B.
End encoding.
#[global] Hint Unfold oo_ atom_ T_: hybrid.
#[global] Hint Unfold seq_ seq'_ seq0: hybrid.
#[global] Hint Unfold proper: hybrid.
#[global] Hint Resolve proper_Var : hybrid.
#[global] Hint Resolve tm_app tm_lam exp_apply exp_fn
eq_lam eq_app sh_v sh_lam sh_app
v_lm v_app v_varT v_fn v_apply v_varE : hybrid.
#[global] Hint Unfold seq_ seq'_ seq0: hybrid.
#[global] Hint Resolve proper_Var : hybrid.
(****************************************************************
Specialized Inversion Properties of prog
****************************************************************)
Section prog_inv.
Hint Rewrite ext_eq_eta : hybrid.
Lemma eq_lam_inv :
forall (i:nat) (Psi:list atm) (T E:uexp->uexp),
seq_ i Psi (All (fun x:uexp => All (fun y:uexp =>
Imp (eq_a x y) (atom_ (eq_a (T x) (E y)))))) ->
exists j:nat, (i=j+3 /\
forall (x y:uexp),
proper x -> proper y ->
seq_ j (eq_a x y::Psi) (atom_ (eq_a (T x) (E y)))).
Proof.
intro i; case i.
- intros Psi T E H.
inversion H; clear H; subst.
replace (i0+1) with (S i0) in H0; try lia.
- clear i; intro i; case i.
+ intros Psi T E H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); intro H1.
inversion H1; clear H1; subst.
replace (i1+1+1) with (S (S i1)) in H0; try lia.
+ clear i; intro i; case i.
* intros Psi T E H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); clear H3; intro H1.
inversion H1; clear H1; subst.
generalize (H4 (Var 0) (proper_Var 0)); clear H4; intro H1.
inversion H1; clear H1; subst.
replace (i0+1+1+1) with (S (S (S i0))) in H0; try lia.
* intros n Psi T E h.
exists n; split; try lia.
intros x y H0 H1.
inversion h; clear h; subst.
generalize (H4 x H0); clear H4; intro H4.
inversion H4; clear H4; subst.
generalize (H6 y H1); clear H6; intro H6.
inversion H6; clear H6; subst.
assert (i0 = n); try lia.
subst; auto.
Qed.
Lemma shape_lam_inv :
forall (i:nat) (Psi:list atm) (T E:uexp->uexp),
seq_ i Psi (All (fun x:uexp => All (fun y:uexp =>
Imp (varT x) (Imp (varE y) (atom_ (shape (T x) (E y))))))) ->
exists j:nat, (i=j+4 /\
forall (x y:uexp),
proper x -> proper y ->
seq_ j (varE y::varT x::Psi) (atom_ (shape (T x) (E y)))).
Proof.
intro i; case i.
- intros Psi T E H.
inversion H; clear H; subst.
replace (i0+1) with (S i0) in H0; try lia.
- clear i; intro i; case i.
+ intros Psi T E H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); intro H1.
inversion H1; clear H1; subst.
replace (i1+1+1) with (S (S i1)) in H0; try lia.
+ clear i; intro i; case i.
* intros Psi T E H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); clear H3; intro H1.
inversion H1; clear H1; subst.
generalize (H4 (Var 0) (proper_Var 0)); clear H4; intro H1.
inversion H1; clear H1; subst.
replace (i0+1+1+1) with (S (S (S i0))) in H0; try lia.
* clear i; intro i; case i.
-- intros Psi T E H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); clear H3; intro H1.
inversion H1; clear H1; subst.
generalize (H4 (Var 0) (proper_Var 0)); clear H4; intro H1.
inversion H1; clear H1; subst.
inversion H4; clear H4; subst.
replace (i1+1+1+1+1) with (S (S (S (S i1)))) in H0; try lia.
-- intros n Psi T E h.
exists n; split; try lia.
intros x y H0 H1.
inversion h; clear h; subst.
generalize (H4 x H0); clear H4; intro H4.
inversion H4; clear H4; subst.
generalize (H6 y H1); clear H6; intro H6.
inversion H6; clear H6; subst.
inversion H5; clear H5; subst.
assert (i1 = n); try lia.
subst; auto.
Qed.
Lemma varTOcc_lam_inv :
forall (i N:nat) (Psi:list atm) (T:uexp->uexp),
seq_ i Psi (All (fun x:uexp => Imp (varT x) (atom_ (varTOcc (T x) N)))) ->
exists j:nat, (i=j+2 /\
forall (x:uexp), proper x ->
seq_ j (varT x::Psi) (atom_ (varTOcc (T x) N))).
Proof.
intro i; case i.
- intros N Psi T H.
inversion H; clear H; subst.
replace (i0+1) with (S i0) in H0; try lia.
- clear i; intro i; case i.
+ intros N Psi T H.
inversion H; clear H; subst.
generalize (H3 (Var 0) (proper_Var 0)); intro H1.
inversion H1; clear H1; subst.
replace (i1+1+1) with (S (S i1)) in H0; try lia.
+ intros n N Psi T h.
exists n; split; try lia.
intros x H0.
inversion h; clear h; subst.
generalize (H3 x H0); clear H3; intro H4.
inversion H4; clear H4; subst.
assert (i1 = n); try lia.
subst; auto.
Qed.
End prog_inv.
(****************************************************************
Adequacy
****************************************************************)
Section proper_adeq.
Hint Rewrite ext_eq_eta : hybrid.
Lemma is_tm_proper : forall T:uexp,
seq0 (atom_ (is_tm T)) -> (proper T).
Proof.
intros T [n h1].
generalize T h1; clear h1 T.
generalize
(lt_wf_ind n
(fun n:nat =>
forall T : uexp, seq_ n nil (atom_ (is_tm T)) -> proper T)).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 T h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* app case *)
- inversion H3; clear H3; subst.
apply proper_app; auto.
+ apply h1 with i0; auto; try lia.
+ apply h1 with i0; auto; try lia.
(* lam case *)
- inversion H3; clear H3; subst.
apply proper_lam; auto.
Qed.
Lemma is_exp_proper : forall E:uexp,
seq0 (atom_ (is_exp E)) -> (proper E).
Proof.
intros E [n h1].
generalize E h1; clear h1 E.
generalize
(lt_wf_ind n
(fun n:nat =>
forall E : uexp, seq_ n nil (atom_ (is_exp E)) -> proper E)).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 E h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* apply case *)
- inversion H3; clear H3; subst.
apply proper_apply; auto.
apply h1 with i0; auto; try lia.
apply h1 with i0; auto; try lia.
(* fn case *)
- inversion H3; clear H3; subst.
apply proper_fn; auto.
Qed.
Lemma eq_proper : forall T E:uexp,
seq0 (atom_ (eq_a T E)) -> (proper T /\ proper E).
Proof.
intros T E [n h1].
generalize T E h1; clear h1 T E.
generalize
(lt_wf_ind n
(fun n:nat =>
forall T E : uexp, seq_ n nil (atom_ (eq_a T E)) ->
(proper T /\ proper E))).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 T E h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* fn case *)
- split.
+ apply proper_lam; auto.
+ apply proper_fn; auto.
(* apply case *)
- inversion H3; clear H3; subst.
generalize h1; generalize h1; intros h2 h3.
assert (h4:i0 (proper T /\ proper E).
Proof.
intros T E [n h1].
generalize T E h1; clear h1 T E.
generalize
(lt_wf_ind n
(fun n:nat =>
forall T E : uexp, seq_ n nil (atom_ (shape T E)) ->
(proper T /\ proper E))).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 T E h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* var case *)
- inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
inversion H0; subst; clear H0.
(* fn case *)
- split.
+ apply proper_lam; auto.
+ apply proper_fn; auto.
(* apply case *)
- inversion H3; clear H3; subst.
generalize h1; generalize h1; intros h2 h3.
assert (h4:i0 proper T.
Proof.
intros T n [i h1].
generalize T n h1; clear h1 T n.
generalize
(lt_wf_ind i
(fun i:nat =>
forall T:uexp, forall n:nat, seq_ i nil (atom_ (varTOcc T n)) ->
proper T)).
intro h'.
apply h'; clear h'; auto.
clear i.
intros i h1 T n h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* lam case *)
- apply proper_lam; auto.
(* apply case *)
- inversion H3; clear H3; subst.
generalize h1; generalize h1; intros h2 h3.
assert (h4:i proper E.
Proof.
intros E n [i h1].
generalize E n h1; clear h1 E n.
generalize
(lt_wf_ind i
(fun i:nat =>
forall E:uexp, forall n:nat, seq_ i nil (atom_ (varEOcc E n)) ->
proper E)).
intro h'.
apply h'; clear h'; auto.
clear i.
intros i h1 E n h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
(* lam case *)
- apply proper_fn; auto.
(* apply case *)
- inversion H3; clear H3; subst.
generalize h1; generalize h1; intros h2 h3.
assert (h4:i list atm -> list atm -> Prop :=
| nil_ate: ateR nil nil nil
| cons_ate: forall (Phi Psi Psi':list atm) (x y:uexp), proper x -> proper y ->
ateR Phi Psi Psi' ->
ateR (eq_a x y::Phi) (is_tm x::Psi) (is_exp y::Psi').
Hint Resolve nil_ate cons_ate : hybrid.
Lemma memb_ate : forall (Phi Psi Psi':list atm) (x y:uexp),
ateR Phi Psi Psi' -> In (eq_a x y) Phi ->
(In (is_tm x) Psi /\ In (is_exp y) Psi').
Proof.
intros Phi Psi Psi' x y; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | h2].
- injection h2; intros; subst; simpl; auto.
- simpl; tauto.
Qed.
Lemma eq_adeq :
forall (i:nat) (T E:uexp) (Phi Psi Psi':list atm),
ateR Phi Psi Psi' ->
seq_ i Phi (atom_ (eq_a T E)) ->
seq_ i Psi (atom_ (is_tm T)) /\ seq_ i Psi' (atom_ (is_exp E)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (T E:uexp) (Phi Psi Psi':list atm),
ateR Phi Psi Psi' ->
seq_ i Phi (atom_ (eq_a T E)) ->
seq_ i Psi (atom_ (is_tm T)) /\ seq_ i Psi' (atom_ (is_exp E)))).
intro H'.
apply H'; clear H' i; auto.
intros i h T E Phi Psi Psi' cInv h1.
inversion h1; subst; clear h1.
- inversion H0; subst; clear H0.
(* lam case *)
+ generalize (eq_lam_inv i0 Phi T0 E0 H3); clear H3; intros [j [h1 h2]];
subst.
assert (h':forall (x y:uexp), proper x -> proper y ->
(seq_ j (is_tm x:: Psi) (atom_ (is_tm (T0 x))) /\
seq_ j (is_exp y:: Psi') (atom_ (is_exp (E0 y))))).
{ intros x y h1 h3.
apply h with (eq_a x y::Phi); auto; try lia; eauto with hybrid. }
replace (j+3) with (j+1+1+1); try lia.
split.
* unfold seq_,atom_;
apply s_bc with (All (fun x:uexp => (Imp (is_tm x) (atom_ (is_tm (T0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply seq_mono with j; try lia.
generalize (h' x (Var 0) h5 (proper_Var 0)); tauto.
* unfold seq_,atom_;
apply s_bc with
(All (fun x:uexp => (Imp (is_exp x) (atom_ (is_exp (E0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply seq_mono with j; try lia.
generalize (h' (Var 0) x (proper_Var 0) h5); tauto.
(* app case *)
+ inversion H3; subst; clear H3.
assert (hi:i
(seq0 (atom_ (is_tm T)) /\ seq0 (atom_ (is_exp E))).
Proof.
intros T E [i h1].
generalize nil_ate; intro h2.
specialize eq_adeq with (1:=h2) (2:=h1); intro h.
split; exists i; tauto.
Qed.
End eq_adeq.
Section shape_adeq.
Hint Rewrite ext_eq_eta : hybrid.
Inductive steR: list atm -> list atm -> list atm -> Prop :=
| nil_ste: steR nil nil nil
| cons_ste: forall (Phi Psi Psi':list atm) (x y:uexp), proper x -> proper y ->
steR Phi Psi Psi' ->
steR (varE y::varT x::Phi) (is_tm x::Psi) (is_exp y::Psi').
Hint Resolve nil_ste cons_ste : hybrid.
Lemma memb_ste1: forall (Phi Psi Psi':list atm) (x y:uexp),
steR Phi Psi Psi' -> ~(In (shape x y) Phi).
Proof.
intros Phi Psi Psi' x y; induction 1; eauto with hybrid.
simpl; intros [h1 | [h1 | h1]]; try discriminate h1; try tauto.
Qed.
Lemma memb_ste2 : forall (Phi Psi Psi':list atm) (x:uexp),
steR Phi Psi Psi' -> In (varT x) Phi -> In (is_tm x) Psi.
Proof.
intros Phi Psi Psi' x; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | [h2 | h2]].
- discriminate h2.
- injection h2; intros; subst; simpl; auto.
- simpl; tauto.
Qed.
Lemma memb_ste3 : forall (Phi Psi Psi':list atm) (x:uexp),
steR Phi Psi Psi' -> In (varE x) Phi -> In (is_exp x) Psi'.
Proof.
intros Phi Psi Psi' x; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | [h2 | h2]].
- injection h2; intros; subst; simpl; auto.
- discriminate h2.
- simpl; tauto.
Qed.
Lemma shape_adeq :
forall (i:nat) (T E:uexp) (Phi Psi Psi':list atm),
steR Phi Psi Psi' ->
seq_ i Phi (atom_ (shape T E)) ->
seq_ i Psi (atom_ (is_tm T)) /\ seq_ i Psi' (atom_ (is_exp E)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (T E:uexp) (Phi Psi Psi':list atm),
steR Phi Psi Psi' ->
seq_ i Phi (atom_ (shape T E)) ->
seq_ i Psi (atom_ (is_tm T)) /\ seq_ i Psi' (atom_ (is_exp E)))).
intro H'.
apply H'; clear H' i; auto.
intros i h T E Phi Psi Psi' cInv h1.
inversion h1; subst; clear h1.
- inversion H0; subst; clear H0.
(* var case *)
+ inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
* inversion H0; subst; clear H0.
* specialize memb_ste2 with (1:=cInv) (2:=H2); case Psi.
-- simpl; tauto.
-- intros a Phi h1.
split.
++ apply s_init; auto with hybrid.
++ inversion H5; subst; clear H5.
** inversion H0; subst; clear H0.
** specialize memb_ste3 with (1:=cInv) (2:=H1); case Psi'.
--- simpl; tauto.
--- intros a' Phi' h1'.
apply s_init; auto with hybrid.
(* lam case *)
+ generalize (shape_lam_inv i0 Phi T0 E0 H3); clear H3; intros [j [h1 h2]];
subst.
assert (h':forall (x y:uexp), proper x -> proper y ->
(seq_ j (is_tm x:: Psi) (atom_ (is_tm (T0 x))) /\
seq_ j (is_exp y:: Psi') (atom_ (is_exp (E0 y))))).
{ intros x y h1 h3.
apply h with (varE y::varT x::Phi); eauto with hybrid; try lia. }
replace (j+4+1) with (j+1+1+1+1+1); try lia.
split.
* unfold seq_,atom_;
apply s_bc with (All (fun x:uexp => (Imp (is_tm x) (atom_ (is_tm (T0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply seq_mono with j; try lia.
generalize (h' x (Var 0) h5 (proper_Var 0)); tauto.
* unfold seq_,atom_;
apply s_bc with (All (fun x:uexp => (Imp (is_exp x) (atom_ (is_exp (E0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply seq_mono with j; try lia.
generalize (h' (Var 0) x (proper_Var 0) h5); tauto.
(* app case *)
+ inversion H3; subst; clear H3.
assert (hi:i
(seq0 (atom_ (is_tm T)) /\ seq0 (atom_ (is_exp E))).
Proof.
intros T E [n h1].
generalize nil_ste; intro h2.
specialize shape_adeq with (1:=h2) (2:=h1); intro h.
split; exists n; tauto.
Qed.
End shape_adeq.
Section varTOcc_adeq.
Hint Rewrite ext_eq_eta : hybrid.
Inductive vtR: list atm -> list atm -> Prop :=
| nil_vt: vtR nil nil
| cons_vt: forall (Phi Psi:list atm) (x:uexp), proper x ->
vtR Phi Psi -> vtR (varT x::Phi) (is_tm x::Psi).
Hint Resolve nil_vt cons_vt : hybrid.
Lemma memb_vt1: forall (Phi Psi:list atm) (x:uexp) (n:nat),
vtR Phi Psi -> ~(In (varTOcc x n) Phi).
Proof.
intros Phi Psi x n; induction 1; eauto with hybrid.
simpl; intros [h1 | h1]; try discriminate h1; try tauto.
Qed.
Lemma memb_vt2 : forall (Phi Psi:list atm) (x:uexp),
vtR Phi Psi -> In (varT x) Phi -> In (is_tm x) Psi.
Proof.
intros Phi Psi x; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | h2].
- injection h2; intros; subst; simpl; auto.
- simpl; tauto.
Qed.
Lemma varTOcc_adeq :
forall (i n:nat) (T:uexp) (Phi Psi:list atm),
vtR Phi Psi ->
seq_ i Phi (atom_ (varTOcc T n)) -> seq_ i Psi (atom_ (is_tm T)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (n:nat) (T:uexp) (Phi Psi:list atm),
vtR Phi Psi ->
seq_ i Phi (atom_ (varTOcc T n)) -> seq_ i Psi (atom_ (is_tm T)))).
intro H'.
apply H'; clear H' i; auto.
intros i h n T Phi Psi cInv h1.
inversion h1; subst; clear h1.
- inversion H0; subst; clear H0.
(* lam case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with (All (fun x:uexp => (Imp (is_tm x) (atom_ (is_tm (T0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
specialize (H2 x h5).
inversion H2; subst; clear H2.
apply s_imp; auto.
apply h with n (varT x::Phi); eauto with hybrid; try lia.
(* app case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with (Conj (atom_ (is_tm T1)) (atom_ (is_tm T2)));
auto with hybrid.
apply s_and; auto.
* apply h with N1 Phi; auto; try lia.
* apply h with N2 Phi; auto; try lia.
(* var case *)
+ inversion H3; subst; clear H3.
inversion H0; subst; clear H0.
specialize memb_vt2 with (1:=cInv) (2:=H2); case Psi.
* simpl; tauto.
* intros a Phi h1.
apply s_init; auto with hybrid.
(* context case *)
- specialize memb_vt1 with (x:=T) (n:=n) (1:=cInv); intro; tauto.
Qed.
Lemma varTOcc_adeq_cor : forall (T:uexp) (n:nat),
seq0 (atom_ (varTOcc T n)) -> seq0 (atom_ (is_tm T)).
Proof.
intros T n [i h].
generalize nil_vt; intro h2.
specialize varTOcc_adeq with (1:=h2) (2:=h); intro; exists i; auto.
Qed.
End varTOcc_adeq.
Section varEOcc_adeq.
Hint Rewrite ext_eq_eta : hybrid.
Inductive veR: list atm -> list atm -> Prop :=
| nil_ve: veR nil nil
| cons_ve: forall (Phi Psi:list atm) (x:uexp), proper x ->
veR Phi Psi -> veR (varE x::Phi) (is_exp x::Psi).
Hint Resolve nil_ve cons_ve : hybrid.
Lemma memb_ve1: forall (Phi Psi:list atm) (x:uexp) (n:nat),
veR Phi Psi -> ~(In (varEOcc x n) Phi).
Proof.
intros Phi Psi x n; induction 1; eauto with hybrid.
simpl; intros [h1 | h1]; try discriminate h1; try tauto.
Qed.
Lemma memb_ve2 : forall (Phi Psi:list atm) (x:uexp),
veR Phi Psi -> In (varE x) Phi -> In (is_exp x) Psi.
Proof.
intros Phi Psi x; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | h2].
injection h2; intros; subst; simpl; auto.
simpl; tauto.
Qed.
Lemma varEOcc_adeq :
forall (i n:nat) (E:uexp) (Phi Psi:list atm),
veR Phi Psi ->
seq_ i Phi (atom_ (varEOcc E n)) -> seq_ i Psi (atom_ (is_exp E)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (n:nat) (E:uexp) (Phi Psi:list atm),
veR Phi Psi ->
seq_ i Phi (atom_ (varEOcc E n)) -> seq_ i Psi (atom_ (is_exp E)))).
intro H'.
apply H'; clear H' i; auto.
intros i h n E Phi Psi cInv h1.
inversion h1; subst; clear h1.
- inversion H0; subst; clear H0.
(* fn case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with (All (fun x:uexp => (Imp (is_exp x) (atom_ (is_exp (E0 x))))));
auto with hybrid.
apply s_all; auto.
intros x h5.
specialize (H2 x h5).
inversion H2; subst; clear H2.
apply s_imp; auto.
apply h with n (varE x::Phi); eauto with hybrid; try lia.
(* app case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_;
apply s_bc with (Conj (atom_ (is_exp E1)) (atom_ (is_exp E2)));
auto with hybrid.
apply s_and; auto.
* apply h with N1 Phi; auto; try lia.
* apply h with N2 Phi; auto; try lia.
(* var case *)
+ inversion H3; subst; clear H3.
* inversion H0; subst; clear H0.
* specialize memb_ve2 with (1:=cInv) (2:=H2); case Psi.
-- simpl; tauto.
-- intros a Phi h1.
apply s_init; auto with hybrid.
(* context case *)
- specialize memb_ve1 with (x:=E) (n:=n) (1:=cInv); intro; tauto.
Qed.
Lemma varEOcc_adeq_cor : forall (E:uexp) (n:nat),
seq0 (atom_ (varEOcc E n)) -> seq0 (atom_ (is_exp E)).
Proof.
intros T n [i h].
generalize nil_ve; intro h2.
specialize varEOcc_adeq with (1:=h2) (2:=h); intro; exists i; auto.
Qed.
End varEOcc_adeq.