Commit 2acfe358 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Cleaned up local language modules.

parent 8f217412
......@@ -209,28 +209,6 @@ Module LambdaCalc <: LocalLang.
intro n; unfold ExprUpSubst; unfold ExprUpRename; destruct n; cbn; auto.
Qed.
(* Lemma ExprSubstRenameFusion : forall e σ ξ, *)
(* (e [e|σ]) e| ξ⟩ = e[e| fun n => (σ n) e|ξ⟩]. *)
(* Proof using. *)
(* intro e; induction e; intros σ ξ; cbn; auto. *)
(* all: try (rewrite IHe; auto). 1,2: rewrite IHe1; rewrite IHe2; auto. *)
(* rewrite IHe3; reflexivity. *)
(* rewrite ExprSubstExt with (σ2 := ExprUpSubst (fun n => (σ n) e|ξ⟩)); auto. *)
(* intro n; unfold ExprUpSubst; unfold ExprUpRename; destruct n; cbn; auto. *)
(* repeat rewrite ExprRenameFusion; auto. *)
(* Qed. *)
(* Lemma ExprSubstFusion : forall e σ1 σ2, *)
(* (e [e|σ1]) [e|σ2] = e [e| fun n => (σ1 n) [e|σ2]]. *)
(* Proof using. *)
(* intro e; induction e; intros σ1 σ2; cbn; auto. *)
(* all: try (rewrite IHe; auto). 1,2: rewrite IHe1; rewrite IHe2; auto. *)
(* rewrite IHe3; reflexivity. *)
(* erewrite ExprSubstExt; eauto. *)
(* intro n; unfold ExprUpSubst; destruct n; cbn; auto. *)
(* rewrite ExprRenameSubstFusion. rewrite ExprSubstRenameFusion. reflexivity. *)
(* Qed. *)
Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n.
Lemma ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e.
......
......@@ -121,40 +121,5 @@ Module Type TypedLocalLang (Import E : LocalLang).
Proof.
unfold ExprSubstTyping; intros Γ n; unfold ExprIdSubst; apply ExprVarTyping.
Qed.
(* Lemma ExprSubstLWeakening : forall (Γ Δ1 Δ2 : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), *)
(* (forall n, Δ1 n = Δ2 (ξ n)) -> *)
(* Γ es σ Δ1 -> *)
(* Γ es fun n => (σ n) e|ξ⟩ Δ2. *)
(* Proof. *)
(* intros Γ Δ1 Δ2 σ ξ subΔ typing. *)
(* unfold ExprSubstTyping in *; intro n. *)
(* eapply ExprWeakening; eauto. *)
(* Qed. *)
(* Lemma ExprSubstRWeakening : forall (Γ1 Γ2 Δ : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), *)
(* (forall n, Γ1 (ξ n) = Γ2 n) -> *)
(* Γ1 es σ Δ -> *)
(* Γ2 es fun n => σ (ξ n) Δ. *)
(* Proof. *)
(* intros Γ1 Γ2 Δ σ ξ subΓ typing. *)
(* unfold ExprSubstTyping in *; intro n. *)
(* rewrite <- subΓ. apply typing. *)
(* Qed. *)
(* Lemma ExprSubstTypeExpand : forall (Γ Δ : nat -> ExprTyp) (σ : nat -> Expr), *)
(* Γ es σ Δ -> *)
(* forall τ : ExprTyp, ExprSubstTyping (fun n => match n with | 0 => τ | S n => Γ n end) *)
(* (ExprUpSubst σ) *)
(* (fun n => match n with |0 => τ | S n => Δ n end). *)
(* Proof. *)
(* intros Γ Δ σ typing τ. *)
(* unfold ExprUpSubst. *)
(* unfold ExprSubstTyping in *. *)
(* intro m. *)
(* unfold ExprUpSubst. destruct m; simpl. *)
(* apply ExprVarTyping. *)
(* apply ExprWeakening with (Γ := Δ); auto. *)
(* Qed. *)
End TypedLocalLang.
Supports Markdown
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