Commit ab81157d authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Cleaned up example language modules.

parent 2acfe358
......@@ -98,10 +98,6 @@ Module NatLang <: LocalLang.
(e e| ξ1) e| ξ2 = e e| fun n => ξ2 (ξ1 n).
Proof using. intro e; induction e; intros ξ1 ξ2; cbn; try rewrite IHe; reflexivity. Qed.
(* Theorem ExprSubstFusion : forall (e : Expr) (σ1 σ2 : nat -> Expr), *)
(* (e [e| σ1]) [e|σ2] = e [e| fun n => σ1 n [e| σ2]]. *)
(* Proof using. intro e; induction e; intros σ1 σ2; cbn; try rewrite IHe; reflexivity. Qed. *)
Definition ExprUpSubst : (nat -> Expr) -> nat -> Expr :=
fun σ n =>
match n with
......
......@@ -139,40 +139,5 @@ Module STLC <: (TypedLocalLang LambdaCalc).
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 STLC.
......@@ -104,40 +104,5 @@ Module TypedNatLang <: (TypedLocalLang NatLang).
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 TypedNatLang.
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