Commit 7b4c1c3c authored by Amin Timany's avatar Amin Timany

Cleanup after changing representation of interpretation of context

parent b84a1e85
......@@ -89,16 +89,15 @@ 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Γ";
iApply exist_elim; eauto; cbn;
iIntros {w} "#[% Hw2] #HΓ"; rewrite H; cbn;
[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.
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.
......@@ -119,8 +118,7 @@ Section typed_interp.
iIntros "#HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply exist_elim; [|iExact "Hv"]; cbn.
iIntros {e'} "[% #He']"; rewrite H.
iDestruct "Hv" as {e'} "[% He']"; rewrite H.
iApply wp_TLam.
iSpecialize "He'" {((interp τ' Δ) _)}; cbn.
iApply always_elim. iApply always_mono; [|trivial].
......@@ -150,12 +148,9 @@ Section typed_interp.
cbn [interp interp_rec cofe_mor_car].
rewrite fixpoint_unfold.
iIntros "#Hv"; cbn.
iApply exist_elim; [|iAssumption].
iIntros {w}; hnf.
change (fixpoint _) with (interp (TRec τ) Δ).
iIntros "[% #Hw]"; rewrite H.
iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
iApply wp_Fold; cbn; auto using to_of_val.
change (fixpoint _) with (interp (TRec τ) Δ); trivial.
rewrite -interp_subst; trivial.
(* unshelving *)
Unshelve.
......
This diff is collapsed.
This diff is collapsed.
......@@ -7,8 +7,31 @@ From iris.prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
Require Export Autosubst.Autosubst.
Fixpoint iter (n : nat) `(f : A A) :=
match n with
| O => λ x, x
| S n' => λ x, f (iter n' f x)
end.
Section Autosubst_Lemmas.
Context {term : Type} {Ids_term : Ids term}
{Rename_term : Rename term} {Subst_term : Subst term}
{SubstLemmas_term : SubstLemmas term}.
Lemma iter_up (m x : nat) (f : var term) :
iter m up f x = if lt_dec x m then ids x else rename (+m) (f (x - m)).
Proof.
revert x; induction m; cbn; auto with omega.
intros x; destruct x; cbn; asimpl; trivial.
intros x; destruct x; cbn; asimpl; trivial.
rewrite IHm; repeat destruct lt_dec;
asimpl; auto with omega.
Qed.
End Autosubst_Lemmas.
Section uPred_Lemmas.
Import uPred.
Context {Λ : language} {Σ : iFunctor}.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment