Commit 5f2649fb authored by Amin Timany's avatar Amin Timany
Browse files

Use functions from variables for interpretation of contexts in Fμref

parent 7b4c1c3c
......@@ -31,7 +31,7 @@ Section typed_interp.
--------------------------------------
_) => eapply (@always_intro _ _ _ _)
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
......@@ -39,15 +39,14 @@ Section typed_interp.
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
eapply (@always_intro _ _ _ _);
iIntros {v} Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp Δ Γ vs e τ
......@@ -156,5 +155,5 @@ Section typed_interp.
Unshelve.
cbn; typeclasses eauto.
Qed.
End typed_interp.
\ No newline at end of file
......@@ -7,13 +7,11 @@ Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context {Σ : iFunctor}.
Implicit Types P Q R : iProp lang Σ.
Notation "# v" := (of_val v) (at level 20).
Canonical Structure leibniz_val := leibnizC val.
Canonical Structure leibniz_var := leibnizC var.
Class Val_to_IProp_Persistent (f : leibniz_val -n> iProp lang Σ) :=
val_to_iprop_persistent : v : val, PersistentP ((cofe_mor_car _ _ f) v).
......@@ -31,7 +29,7 @@ Section logrel.
| S x' => f x'
end
|}.
Program Definition extend_context_interp_fun2
(τi : leibniz_val -n> iProp lang Σ) :
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
......@@ -51,7 +49,7 @@ Section logrel.
|}.
Next Obligation.
Proof. intros n g h H Δ x y. destruct x; cbn; auto. Qed.
Program Definition extend_context_interp_apply :
((leibniz_var -n> leibniz_val -n> iProp lang Σ)) -n>
((leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
......@@ -78,7 +76,7 @@ Section logrel.
end.
apply cofe_mor_car_ne; trivial. intros y. cbn.
destruct y; trivial.
Qed.
Qed.
Definition interp_unit : leibniz_val -n> iProp lang Σ :=
{|
......@@ -104,7 +102,7 @@ Section logrel.
repeat intros ?; cbn;
repeat apply exist_ne =>?;
try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
Program Definition interp_sum :
(leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ) -n>
leibniz_val -n> iProp lang Σ :=
......@@ -173,7 +171,7 @@ Section logrel.
apply forall_ne=> P.
apply always_ne, (contractive_ne _), wp_ne => w.
rewrite Hfg; trivial.
Qed.
Qed.
Program Definition interp_rec_pre :
((leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ)) -n>
......@@ -192,7 +190,7 @@ Section logrel.
Next Obligation.
Proof.
intros τi rec_appr n x y Hxy; rewrite Hxy; trivial.
Qed.
Qed.
Next Obligation.
Proof.
intros τi n f g Hfg x. cbn.
......@@ -214,7 +212,7 @@ Section logrel.
apply later_contractive =>i Hi.
rewrite H; trivial.
Qed.
Program Definition interp_rec :
((leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ)) -n>
(leibniz_val -n> iProp lang Σ)
......@@ -224,7 +222,7 @@ Section logrel.
|}.
Next Obligation.
Proof. intros n f g H; apply fixpoint_ne => z; rewrite H; trivial. Qed.
Program Fixpoint interp (τ : type) {struct τ}
: (leibniz_var -n> (leibniz_val -n> iProp lang Σ)) -n> leibniz_val -n> iProp lang Σ
:=
......@@ -255,7 +253,7 @@ Section logrel.
(v : val)
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_Persistent
τ (Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
{HΔ : context_interp_Persistent Δ}
......@@ -375,7 +373,7 @@ Section logrel.
[ |- _ _ _ Δ ?a _ _ _ Δ ?b] => assert (Heq : a = b) by omega; rewrite Heq; trivial
end.
Qed.
Lemma interp_subst_weaken
(m n : nat)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
......@@ -406,7 +404,7 @@ Section logrel.
replace (x + n) with (n + x) by omega.
induction n; cbn; auto with omega.
induction x; cbn; trivial.
}
}
- properness; trivial.
change (up (iter m up (ren (+n)))) with (iter (S m) up (ren (+n))).
rewrite IHτ.
......@@ -425,7 +423,7 @@ Section logrel.
Qed.
Local Opaque eq_nat_dec.
Program Definition context_interp_insert (m : nat) :
(leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
......@@ -452,7 +450,7 @@ Section logrel.
intros m n f g Hfg F Δ x; cbn;
destruct lt_dec; try destruct eq_nat_dec; auto.
Qed.
Lemma extend_context_interp_insert (m : nat)
(τi : leibniz_val -n> iProp lang Σ)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
......@@ -497,8 +495,8 @@ Section logrel.
rewrite IHm.
repeat destruct lt_dec; repeat destruct eq_nat_dec;
asimpl; auto with omega.
Qed.
Qed.
Lemma interp_subst_iter_up
(m : nat)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
......@@ -557,7 +555,7 @@ Section logrel.
destruct vs; cbn; trivial.
apply and_proper.
- apply interp_ren_S.
- apply IHΓ.
- apply IHΓ.
Qed.
End logrel.
\ No newline at end of file
Require Import iris.prelude.base.
Require Import prelude.base.
Require Import F_mu.lang.
Inductive type :=
......
......@@ -10,44 +10,11 @@ Require Import prelude.Vlist.
Import uPred.
Section typed_interp.
Context
{Σ : gFunctors}
`{i : heapG Σ}
`{L : namespace}.
Context {Σ : gFunctors} `{i : heapG Σ} `{L : namespace}.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
(*
Local Ltac ipropsimpl :=
repeat
match goal with
| [|- (_ (_ _))%I] => eapply and_intro
| [|- ( _ _)%I] => apply later_mono
| [|- (_ _, _)%I] => rewrite -exist_intro
| [|- (( _, _) _)%I] => let v := fresh "v" in rewrite exist_elim; [|intros v]
end.
Local Hint Extern 1 => progress ipropsimpl.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) uconstr(t) ident(v) :=
rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_impl_l; apply and_intro; [
apply (@always_intro _ _ _ t), forall_intro=> v /=; apply impl_intro_l| eauto with itauto].
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) :=
rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_mono; eauto; intros v; cbn.
Create HintDb itauto.
Local Hint Extern 3 ((_ _) _)%I => rewrite and_elim_r : itauto.
Local Hint Extern 3 ((_ _) _)%I => rewrite and_elim_l : itauto.
Local Hint Extern 3 (_ (_ _))%I => rewrite -or_intro_l : itauto.
Local Hint Extern 3 (_ (_ _))%I => rewrite -or_intro_r : itauto.
Local Hint Extern 2 (_ _)%I => etransitivity; [|rewrite -later_intro] : itauto.
Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto 2.
*)
Local Hint Extern 1 =>
match goal with
|-
......@@ -64,6 +31,14 @@ Section typed_interp.
_) => iNext
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => eapply (@always_intro _ _ _ _)
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
......@@ -71,42 +46,37 @@ Section typed_interp.
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial];
[apply (always_intro _ _); iIntros {v} Hv|iSplit; trivial]; cbn.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma later_exist_turnstile (M : cmraT) (A : Type) :
Inhabited A Φ : A uPred M, ( ( a : A, Φ a))%I ( a : A, Φ a)%I.
Proof. intros H Φ. rewrite later_exist; trivial. Qed.
Lemma typed_interp N k Δ Γ vs e τ
Lemma typed_interp N Δ Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed k Γ e τ)
(Hctx : closed_ctx k Γ)
(HC : closed_type k τ)
(HΔ : VlistAlwaysStable Δ)
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
: List.length Γ = List.length vs
(heap_ctx N Π∧ zip_with (λ τ v, (@interp Σ i L) k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I
WP (e.[env_subst vs]) @ {{ λ v, (@interp Σ i L) k τ HC Δ v }}.
(heap_ctx N Π∧ zip_with (λ τ v, (@interp Σ i L) τ Δ v) Γ vs)%I
WP (e.[env_subst vs]) @ {{ λ v, (@interp Σ i L) τ Δ v }}.
Proof.
revert Hctx HC HΔ vs.
induction Htyped; intros Hctx HC HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
edestruct (zipwith_Forall_lookup _ Hctx) as [Hτ' Hτ'eq]; eauto.
iApply interp_closed_irrel_turnstile.
iApply big_and_elem_of "HΓ"; eauto.
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
- (* unit *) value_case.
- (* unit *) value_case; trivial.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
......@@ -116,13 +86,11 @@ Section typed_interp.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_fst; eauto using to_of_val; cbn.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_snd; eauto using to_of_val; cbn.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
......@@ -131,31 +99,24 @@ Section typed_interp.
value_case; iRight; auto with itauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "HΓ"; iRevert "Hheap";
iApply exist_elim; eauto; cbn;
iIntros {w} "#[% Hw2] #HΓ #Hheap"; rewrite H; cbn;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl;
[specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (w::vs)) |
specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto;
(iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
iDestruct "Hv" as "[Hv|Hv]";
iDestruct "Hv" as {w} "[% Hw]"; rewrite H;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl;
[specialize (IHHtyped2 Δ HΔ (w::vs)) |
specialize (IHHtyped3 Δ HΔ (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
- (* lam *)
value_case; apply (always_intro _ _); iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC)
HΔ (w :: vs)); cbn; auto.
(iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto with itauto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"; auto with itauto].
intros; apply interp_closed_irrel_turnstile.
iApply wp_mono; [|iApply "Hv"]; auto with itauto.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
......@@ -165,56 +126,44 @@ Section typed_interp.
iIntros "#HΓ #Hheap"; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "HΓ". rewrite zip_with_closed_ctx_list_subst. iIntros "#HΓ"; trivial.
iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
iIntros "#Hheap #HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply exist_elim; [|iExact "Hv"]; cbn.
iIntros {e'} "[% #He']"; rewrite H0.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize "He'" {((interp k τ' H Δ) _)}; cbn.
iSpecialize "He'" {((interp τ' Δ) _)}; cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
intros w; cbn; rewrite -interp_subst; trivial.
iIntros {w} "#H". rewrite -interp_subst; trivial.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]);
iApply wp_impl_l;
iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_impl_l.
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (closed_type_rec HC)); trivial]; cbn.
iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
trivial].
+ iIntros {v} "#Hv".
value_case. rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
eapply (@always_intro _ _ _ _).
iApply exist_intro; iSplit; trivial.
iNext.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply Δ (interp (S k) τ (closed_type_rec HC)))))
with ((@interp _ _ L k (TRec τ) HC) Δ); trivial.
+ iRevert "HΓ"; rewrite zip_with_closed_ctx_list_subst; iIntros "#HΓ";
iSplit; trivial.
value_case.
rewrite fixpoint_unfold; cbn.
auto with itauto.
+ iRevert "Hheap HΓ"; rewrite zip_with_context_interp_subst;
iIntros "#Hheap #HΓ"; auto with itauto.
- (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (typed_closed_type _ _ _ _ Htyped)); trivial];
[|iSplit; trivial]; cbn.
iApply IHHtyped;
auto with itauto].
iIntros {v}.
rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
iIntros "#Hv".
iApply exist_elim; [|iAssumption].
iIntros {w}; cbn.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply
Δ
(interp
(S k) τ
(closed_type_rec
(typed_closed_type k Γ e (TRec τ) Htyped))))))
with ((@interp _ _ L k (TRec τ) (typed_closed_type k Γ e (TRec τ) Htyped)) Δ);
trivial.
iIntros "[% #Hw]"; rewrite H.
cbn [interp interp_rec cofe_mor_car].
rewrite fixpoint_unfold.
iIntros "#Hv"; cbn.
change (fixpoint _) with (@interp _ _ L (TRec τ) Δ).
iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
iApply wp_Fold; cbn; auto using to_of_val.
iRevert "Hw". rewrite -interp_subst. iIntros "#Hw". trivial.
rewrite -interp_subst; auto with itauto.
- (* Alloc *)
smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
......@@ -249,7 +198,7 @@ Section typed_interp.
iIntros "Hl".
iSplitL.
+ iNext. iApply exist_intro; iSplitL; trivial.
+ iApply pvs_intro; iApply interp_closed_irrel_turnstile; trivial.
+ iApply pvs_intro; trivial.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
......@@ -266,17 +215,15 @@ Section typed_interp.
iIntros {u} "[Hl1 #Hl2] #Hheap #Hw".
iApply wp_store;
[rewrite to_of_val; trivial | apply and_elim_r
| | apply and_elim_l | iSplit; trivial].
| | apply and_elim_l | iSplit; trivial].
specialize (HNLdisj l); set_solver_ndisj.
iSplitL; trivial.
iNext. iIntros "Hl".
iSplitL; [|iApply pvs_intro; trivial].
iNext. iApply exist_intro; iSplitL; trivial.
iApply interp_closed_irrel_turnstile; trivial.
(* unshelving *)
Unshelve.
all: cbn; solve [eauto 2 using closed_ctx_map_S_back,
typed_closed_type | try typeclasses eauto].
cbn; typeclasses eauto.
Qed.
End typed_interp.
\ No newline at end of file
This diff is collapsed.
Require Import prelude.base.
Require Import F_mu_ref.lang.
Inductive type :=
......@@ -16,343 +17,84 @@ Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Inductive closed_type (k : nat) : type Prop :=
| CLT_TUnit : closed_type k TUnit
| CLT_TProd t t' : closed_type k t closed_type k t' closed_type k (TProd t t')
| CLT_TSum t t' : closed_type k t closed_type k t' closed_type k (TSum t t')
| CLT_TArrow t t' : closed_type k t closed_type k t' closed_type k (TArrow t t')
| CLT_TRec t : closed_type (S k) t closed_type k (TRec t)
| CLT_TVar n : n < k closed_type k (TVar n)
| CLT_TForall t : closed_type (S k) t closed_type k (TForall t)
| CLT_Tref t : closed_type k t closed_type k (Tref t)
.
Hint Constructors closed_type.
Lemma closed_type_prod_1 {k : nat} {τ1 τ2 : type} :
closed_type k (TProd τ1 τ2) closed_type k τ1.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_prod_2 {k : nat} {τ1 τ2 : type} :
closed_type k (TProd τ1 τ2) closed_type k τ2.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_sum_1 {k : nat} {τ1 τ2 : type} :
closed_type k (TSum τ1 τ2) closed_type k τ1.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_sum_2 {k : nat} {τ1 τ2 : type} :
closed_type k (TSum τ1 τ2) closed_type k τ2.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_arrow_1 {k : nat} {τ1 τ2 : type} :
closed_type k (TArrow τ1 τ2) closed_type k τ1.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_arrow_2 {k : nat} {τ1 τ2 : type} :
closed_type k (TArrow τ1 τ2) closed_type k τ2.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_rec {k : nat} {τ : type} :
closed_type k (TRec τ) closed_type (S k) τ.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_var {k : nat} {v : var} :
closed_type k (TVar v) v < k.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_forall {k : nat} {τ : type} :
closed_type k (TForall τ) closed_type (S k) τ.
Proof. intros H; inversion H; subst; trivial. Qed.
Lemma closed_type_ref {k : nat} {τ : type} :
closed_type k (Tref τ) closed_type k τ.
Proof. intros H; inversion H; subst; trivial. Qed.
Local Hint Resolve closed_type_prod_1 closed_type_prod_2 closed_type_sum_1
closed_type_sum_2 closed_type_arrow_1 closed_type_arrow_2
closed_type_rec closed_type_var closed_type_forall closed_type_ref.
Lemma closed_type_S (k : nat) (τ : type) : closed_type k τ closed_type (S k) τ.
Proof. intros H; induction H; auto using closed_type with omega. Qed.
Lemma closed_type_le (k k' : nat) (τ : type) : k k' closed_type k τ closed_type k' τ.
Proof. intros H; induction H; auto using closed_type, closed_type_S with omega. Qed.
Definition closed_ctx (k : nat) (Γ : list type) := Forall (closed_type k) Γ.
Lemma closed_ctx_S (k : nat) (Γ : list type) : closed_ctx k Γ closed_ctx (S k) Γ.
Proof. intros H. eapply Forall_impl; [| apply closed_type_S]; trivial. Qed.
Lemma closed_ctx_le (k k' : nat) (Γ : list type) : k k' closed_ctx k Γ closed_ctx k' Γ.
Proof. intros H; induction H; auto using closed_type, closed_ctx_S with omega. Qed.
Lemma closed_ctx_closed_type (k : nat) (Γ : list type) (x : var) (τ : type) :
closed_ctx k Γ Γ !! x = Some τ closed_type k τ.
Proof. intros; eapply Forall_lookup; eauto. Qed.
Lemma closed_ctx_map (k k' : nat) (Γ : list type) (f : type type) :
closed_ctx k Γ
( τ, closed_type k τ closed_type k' (f τ))
closed_ctx k' (map f Γ).
Proof.
revert k k' f.
induction Γ; intros k k' f H1 H2; cbn; constructor;
inversion H1; subst; auto.
eapply IHΓ; eauto.
Qed.
Program Fixpoint zipwith_Forall {A : Type} {P : A Prop} (l : list A) (H : Forall P l) :
list ({x : A | P x}) :=
match l as u return Forall P u _ with
| [] => λ _, []
| a :: l' => λ H, (a _) :: (zipwith_Forall l' _)
end H.
Solve Obligations with repeat intros ?; match goal with [H : Forall _ _ |- _] => inversion H; trivial end.
Lemma zipwith_Forall_lookup {A : Type} {P : A Prop} (l : list A) (Hf : Forall P l) (x : A) (n : nat) :
l !! n = Some x {Hx : P x| (zipwith_Forall l Hf) !! n = Some (x Hx)}.
Proof.
revert n.
induction l; intros n H1; cbn in *; [inversion H1|].
destruct n; [cbn in *; inversion H1; subst|]; eauto.
Qed.
Definition closed_ctx_list (k : nat) (Γ : list type) (H : closed_ctx k Γ) :
list ({τ : type | closed_type k τ}) := zipwith_Forall Γ H.
Inductive typed (k : nat) (Γ : list type) : expr type Prop :=
| Var_typed x τ : (closed_ctx k Γ) Γ !! x = Some τ typed k Γ (Var x) τ
| Unit_typed : closed_ctx k Γ typed k Γ Unit TUnit
Inductive typed (Γ : list type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ typed Γ (Var x) τ
| Unit_typed : typed Γ Unit TUnit
| Pair_typed e1 e2 τ1 τ2 :
typed k Γ e1 τ1 typed k Γ e2 τ2 typed k Γ (Pair e1 e2) (TProd τ1 τ2)
| Fst_typed e τ1 τ2 : typed k Γ e (TProd τ1 τ2) typed k Γ (Fst e) τ1
| Snd_typed e τ1 τ2