Commit 799cda60 authored by Amin Timany's avatar Amin Timany

Merge branch 'wip'

parents f1ae6242 2afabce4
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
-Q . ""
prelude/base.v
prelude/Vlist.v
stlc/lang.v
stlc/typing.v
stlc/rules.v
......@@ -15,4 +14,4 @@ F_mu_ref/lang.v
F_mu_ref/typing.v
F_mu_ref/rules.v
F_mu_ref/logrel.v
F_mu_ref/fundamental.v
F_mu_ref/fundamental.v
\ No newline at end of file
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