Skip to content

GitLab

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

Comments for example languages.

parent 2203b568
Hide whitespace changes
Inline Side-by-side
LambdaCalc.v
View file @ e7cd0f54
......@@ -2,8 +2,21 @@ Require Export LocalLang.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
(*
Call-by-value lambda calculus as a local language. We use module subtyping so that we can
export more than is exported by the LocalLang type.
*)
Module LambdaCalc <: LocalLang.
(*
We have types which are simple types with base types booleans and nats. We introduce
types here so that we can have intensional typing for functions: lambdas have the form
λ x : τ. e
In this module, we ignore the τ.
Equality is easily decidable for these types.
*)
Inductive SimpleType : Set :=
boolType : SimpleType
| natType : SimpleType
......@@ -13,6 +26,11 @@ Module LambdaCalc <: LocalLang.
decide equality.
Qed.
(*
Our λ calculus contains standard λ-calculus constructs along with true, false, zero,
successor, fixpoints and if-then-else. As promised, our abstraction syntax contains a
type for the bound variable.
*)
Inductive LC :=
| var : nat -> LC
| ttLC : LC
......@@ -24,45 +42,57 @@ Module LambdaCalc <: LocalLang.
| app : LC -> LC -> LC
| abs : SimpleType -> LC -> LC.
(*
Due to a Coq quirk, we have to give this sort of definition whenever we want to use an
inductive type for something required by a module type.
*)
Definition Expr := LC.
Definition ExprEqDec : forall e1 e2 : Expr, {e1 = e2} + {e1 <> e2}.
Proof.
decide equality. apply Nat.eq_dec. apply SimpleTypeEqDec.
Qed.
Definition ExprVar : nat -> Expr := var.
Fixpoint LCClosedAbove (n : nat) (e : LC) : Prop :=
(*
A λ-calculus program is closed above n if it does not contain free variables above n.
When moving across an abstraction boundary, we add one to n to account for the fact
that we must count back to another abstraction barrier before getting to free
variables.
*)
Fixpoint ExprClosedAbove (n : nat) (e : LC) : Prop :=
match e with
| var m => if m <? n then True else False
| ttLC => True
| ffLC => True
| zero => True
| succ e' => LCClosedAbove n e'
| fixP e' => LCClosedAbove n e'
| ite b e1 e2 => LCClosedAbove n b /\ LCClosedAbove n e1 /\ LCClosedAbove n e2
| app e1 e2 => LCClosedAbove n e1 /\ LCClosedAbove n e2
| abs τ e' => LCClosedAbove (S n) e'
| succ e' => ExprClosedAbove n e'
| fixP e' => ExprClosedAbove n e'
| ite b e1 e2 => ExprClosedAbove n b /\ ExprClosedAbove n e1 /\ ExprClosedAbove n e2
| app e1 e2 => ExprClosedAbove n e1 /\ ExprClosedAbove n e2
| abs τ e' => ExprClosedAbove (S n) e'
end.
Definition ExprClosedAbove := LCClosedAbove.
(*
Annoyingly, Coq requires that we repeat definitions and lemmas from the module type
into modules of that type.
*)
Definition ExprClosed := ExprClosedAbove 0.
(*
Values are as standard in CBV λ calculus, _except that functions must be closed
in order to be values_.
*)
Inductive LCVal : LC -> Prop :=
| ttVal : LCVal ttLC
| ffVal : LCVal ffLC
| zeroVal : LCVal zero
| succVal : forall e : Expr, LCVal e -> LCVal (succ e)
| AbsVal : forall (τ : SimpleType) (e : LC), LCClosedAbove 1 e -> LCVal (abs τ e).
| AbsVal : forall (τ : SimpleType) (e : LC), ExprClosedAbove 1 e -> LCVal (abs τ e).
Definition ExprVal := LCVal.
(* Inductive LCOpenVal : LC -> Prop := *)
(* | varOVal : forall n, LCOpenVal (var n) *)
(* | ttOVal : LCOpenVal ttLC *)
(* | ffOVal : LCOpenVal ffLC *)
(* | zeroOVal : LCOpenVal zero *)
(* | succOVal : forall e : Expr, LCOpenVal e -> LCOpenVal (succ e) *)
(* | AbsOVal : forall (τ : SimpleType) (e : LC), LCOpenVal (abs τ e). *)
(* Definition ExprOpenVal := LCOpenVal. *)
Lemma ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Proof.
intros v val_v; induction val_v; unfold ExprClosed; simpl; auto.
......@@ -73,7 +103,11 @@ Module LambdaCalc <: LocalLang.
| 0 => 0
| S n' => S (ξ n')
end.
(*
We define renaming separately from substitution. This makes proving several properties
easier. This especiallly applies to the fusion properties.
*)
Fixpoint ExprRename (e : Expr) (ξ : nat -> nat) : Expr :=
match e with
| var n => var (ξ n)
......@@ -142,6 +176,12 @@ Module LambdaCalc <: LocalLang.
intro n; destruct n; simpl; auto.
Qed.
(*
ExprSubstVar is true judgmentally, so we only need to provide eq_refl.
We need to repeat Lemmas in modules, just like definitions. We thus just
copy-and-paste the definition of ExprRenameVar into this file.
*)
Definition ExprSubstVar : forall n σ, (ExprVar n) [e| σ] = σ n := fun n σ => eq_refl.
Lemma ExprRenameVar : forall n ξ, (ExprVar n) ⟨e| ξ ⟩ = ExprVar (ξ n).
Proof.
......@@ -169,27 +209,27 @@ 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 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.
(* 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.
......@@ -223,11 +263,20 @@ Module LambdaCalc <: LocalLang.
intros n; unfold ExprUpRename; destruct n; unfold ExprIdRenaming; reflexivity.
Qed.
(*
As with inductive types, so with constructors. Thus, due to this quirk of Coq, we need
to provide a definition whenever we want to provide a constructor as the definition
of a parameter of the module type.
*)
Definition tt := ttLC.
Definition ff := ffLC.
Lemma ttValue : ExprVal tt. Proof. constructor. Qed.
Lemma ffValue : ExprVal ff. Proof. constructor. Qed.
(*
This substitution represents replacing the first free variable with e, and then
moving every other variable "down one" to make up for that.
*)
Definition LCStepSubst : Expr -> (nat -> Expr) :=
fun e n => match n with
| 0 => e
......@@ -277,6 +326,7 @@ Module LambdaCalc <: LocalLang.
intros k lt; destruct k; auto. apply Lt.lt_S_n in lt.
rewrite static_above; auto.
Qed.
Lemma ExprClosedSubst : forall (e : Expr) (σ : nat -> Expr), ExprClosed e -> e [e|σ] = e.
Proof using.
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedAboveSubst with (n := 0);
......@@ -300,74 +350,6 @@ Module LambdaCalc <: LocalLang.
apply Lt.lt_le_S in l. apply Lt.le_lt_or_eq in l; destruct l; subst; eauto.
Qed.
Fixpoint IsClosedAbove (e : Expr) (n : nat) : bool :=
match e with
| var m => if m <? n then true else false
| ttLC => true
| ffLC => true
| zero => true
| succ e' => IsClosedAbove e' n
| fixP e' => IsClosedAbove e' n
| ite b e1 e2 => IsClosedAbove b n && IsClosedAbove e1 n && IsClosedAbove e2 n
| app e1 e2 => IsClosedAbove e1 n && IsClosedAbove e2 n
| abs τ e' => IsClosedAbove e' (S n)
end.
Lemma IsClosedAboveSpec : forall e n, IsClosedAbove e n = true <-> LCClosedAbove n e.
Proof using.
intro e; induction e; intro m; cbn; split; intro H; auto; try discriminate.
1,2: destruct m; cbn in *;
try match goal with
| [ |-context[?a <=? ?b]] => destruct (a <=? b)
end;
auto; try discriminate.
all: repeat match goal with
| [ H: (andb _ _) = true |- _ ] => apply andb_prop in H
| [ |- andb _ _ = true ] => apply andb_true_intro
| [ H : _ /\ _ |- _ ] => destruct H
| [|- _ /\ _ ] => split
| [IH : forall n, IsClosedAbove ?e n = true <-> LCClosedAbove n ?e,
H : IsClosedAbove ?e ?m = true |- LCClosedAbove ?m ?e ] =>
apply ((proj1 (IH m)) H)
| [IH : forall n, IsClosedAbove ?e n = true <-> LCClosedAbove n ?e,
H : LCClosedAbove ?m ?e |- IsClosedAbove ?e ?m = true ] =>
apply ((proj2 (IH m)) H)
end.
Qed.
Fixpoint IsExprVal (e : Expr) : bool :=
match e with
| var x => false
| ttLC => true
| ffLC => true
| zero => true
| succ e => IsExprVal e
| fixP e => false
| ite e1 e2 e3 => false
| app e1 e2 => false
| abs τ e1 => IsClosedAbove e1 1
end.
Lemma IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true.
Proof using.
intros v val; induction val; cbn; auto.
apply IsClosedAboveSpec; auto.
Qed.
Lemma IsExprValSpec2 : forall v : Expr, IsExprVal v = true -> ExprVal v.
Proof using.
intros v eq; induction v; cbn in *; try discriminate; constructor; auto.
apply IHv; auto. apply IsClosedAboveSpec; auto.
Qed.
Lemma IsExprValSpec3 : forall e : Expr, ~ ExprVal e -> IsExprVal e = false.
Proof using.
intros e nv; destruct (IsExprVal e) eqn:eq; auto.
apply IsExprValSpec2 in eq; exfalso; apply nv; auto.
Qed.
Lemma IsExprValSpec4 : forall e : Expr, IsExprVal e = false -> ~ ExprVal e.
Proof using.
intros e eq val; apply IsExprValSpec1 in val; rewrite val in eq; inversion eq.
Qed.
Theorem NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Proof using.
intros v; induction v; intros val_v e step; inversion val_v; subst;
......@@ -377,66 +359,6 @@ Module LambdaCalc <: LocalLang.
Theorem boolSeperation : tt <> ff. discriminate. Qed.
(* Theorem OpenValRename : forall e ξ, ExprOpenVal e -> ExprOpenVal (e ⟨e|ξ⟩). *)
(* Proof using. *)
(* intro e; induction e; cbn; intros ξ val_e; inversion val_e; subst; *)
(* constructor; auto. *)
(* apply IHe; auto. *)
(* Qed. *)
(* Theorem OpenValSubst : forall e σ, *)
(* ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e| σ]). *)
(* Proof using. *)
(* intro e; induction e; cbn; intros σ val_e val_σ; auto; inversion val_e; subst. *)
(* constructor; apply IHe; auto. *)
(* constructor. *)
(* Qed. *)
(* Theorem OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e. *)
(* Proof using. *)
(* intro e; induction e; cbn; intros σ val; inversion val; subst; constructor. *)
(* eapply IHe; eauto. *)
(* Qed. *)
(* Theorem ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e. *)
(* Proof using. *)
(* intro e; induction e; intro val; inversion val; subst; constructor. *)
(* apply IHe; auto. *)
(* Qed. *)
(* Theorem VarToOpenVal : forall n, ExprOpenVal (ExprVar n). *)
(* Proof using. *)
(* intro n; constructor. *)
(* Qed. *)
(* Theorem NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2. *)
(* Proof using. *)
(* intros e1; induction e1; intros val e2 step; inversion val; subst; *)
(* inversion step; subst. *)
(* apply IHe1 in H1; auto. *)
(* Qed. *)
(* Fixpoint IsOpenVal (e : Expr) : bool := *)
(* match e with *)
(* | var x => true *)
(* | ttLC => true *)
(* | ffLC => true *)
(* | zero => true *)
(* | succ e => IsOpenVal e *)
(* | fixP x => false *)
(* | ite x x0 x1 => false *)
(* | app x x0 => false *)
(* | abs x x0 => true *)
(* end. *)
(* Theorem IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e. *)
(* Proof using. *)
(* intro e; induction e; cbn; split; intro H; auto; try discriminate; try (inversion H; fail). *)
(* all: try (constructor; auto; fail). *)
(* - apply IHe in H; constructor; auto. *)
(* - inversion H; subst. apply IHe in H1; auto. *)
(* Qed. *)
Lemma ExprRenameClosedAbove : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedAbove n e ->
......
NatLang.v
View file @ e7cd0f54
......@@ -2,6 +2,12 @@ Require Export LocalLang.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
(*
A simple language with natural numbers and booleans. This language has no control flow
or evaluation at all. It is inspired by the local language in the Core Choreography
Calculus.
*)
Module NatLang <: LocalLang.
Inductive NL :=
......@@ -13,13 +19,7 @@ Module NatLang <: LocalLang.
Global Hint Constructors NL : NL.
Definition Expr := NL.
Definition ExprEqDec : forall e1 e2 : Expr, {e1 = e2} + {e1 <> e2}.
intros e1; induction e1; intros e2; destruct e2;
try (right; intro eq; inversion eq; fail);
try (left; reflexivity).
- destruct (Nat.eq_dec n n0). left; apply f_equal; auto.
right; intro eq; inversion eq; apply n1; auto.
- destruct (IHe1 e2). left; apply f_equal; auto.
right; intro eq; inversion eq; apply n; auto.
decide equality; apply Nat.eq_dec.
Qed.
Definition ExprVar : nat -> Expr := var.
......@@ -31,6 +31,10 @@ Module NatLang <: LocalLang.
Global Hint Constructors NLVal : NL.
Definition ExprVal : Expr -> Prop := NLVal.
(*
Being closed is a much-simpler property here than in the λ calculus, since we do not
have any binders to worry about.
*)
Fixpoint ExprClosedAbove (n : nat) (e : Expr) : Prop :=
match e with
| var x => x < n
......@@ -40,8 +44,10 @@ Module NatLang <: LocalLang.
| ffalse => True
end.
Definition ExprClosed := ExprClosedAbove 0.
Theorem ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Proof using. intros v val_v; induction val_v; cbn; auto. Qed.
Theorem ExprClosedAboveMono : forall m n e, m < n -> ExprClosedAbove m e -> ExprClosedAbove n e.
Proof using.
intros m n e; revert m n; induction e; try rename n into x;
......@@ -53,6 +59,9 @@ Module NatLang <: LocalLang.
Theorem ExprVarClosed : forall n m, ExprClosedAbove n (ExprVar m) <-> m < n.
Proof using. intros n m; cbn; reflexivity. Qed.
(*
Since we have no binders, we substitution and renaming are very simple.
*)
Fixpoint ExprSubst (e : Expr) (σ : nat -> Expr) : Expr :=
match e with
| var x => σ x
......@@ -89,9 +98,9 @@ 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.
(* 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 =>
......
STLC.v
View file @ e7cd0f54
......@@ -4,6 +4,9 @@ Require Export LambdaCalc.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
(*
Simple typing for the λ calculus defined earlier.
*)
Module STLC <: (TypedLocalLang LambdaCalc).
Include LambdaCalc.
......@@ -126,7 +129,7 @@ Module STLC <: (TypedLocalLang LambdaCalc).
intros Γ; constructor.
Qed.
Definition ExprSubstTyping : (nat -> ExprTyp) -> (nat -> Expr) -> (nat -> ExprTyp) -> Prop :=
Definition ExprSubstTyping : (nat -> ExprTyp) -> (nat -> Expr) -> (nat -> ExprTyp) -> Prop :=
fun Γ σ Δ => forall n : nat, Δ ⊢e (σ n) ::: (Γ n).
Notation "Gamma ⊢es sigma ⊣ Delta" := (ExprSubstTyping Gamma sigma Delta) (at level 30).
Parameter ExprSubstType :
......@@ -137,39 +140,39 @@ Module STLC <: (TypedLocalLang LambdaCalc).
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 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 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.
(* 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.
STLCSound.v
View file @ e7cd0f54
......@@ -4,6 +4,10 @@ Require Export SoundlyTypedLocalLang.
Require Export LambdaCalc.
Require Export STLC.
(*
Type soundness for STLC. The arguments here are very standard.
*)
Module STLCSound <: (SoundlyTypedLocalLang LambdaCalc STLC).
Import LambdaCalc.
Import STLC.
......
TypedNatLang.v
View file @ e7cd0f54
......@@ -4,14 +4,16 @@ Require Export NatLang.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
(*
A very simple type system for a very simple language.
*)
Module TypedNatLang <: (TypedLocalLang NatLang).
Include NatLang.
Inductive UniType := N | B.
Definition ExprTyp := UniType.
Inductive NatLangType := N | B.
Definition ExprTyp := NatLangType.
Definition ExprTypEqDec : forall tau sigma : ExprTyp, {tau = sigma} + {tau <> sigma}.
intros τ σ; destruct τ; destruct σ; try (left; reflexivity);
right; intro eq; inversion eq.
decide equality.
Defined.
Reserved Notation "Γ ⊢e e ::: τ" (at level 30).
......@@ -103,39 +105,39 @@ Module TypedNatLang <: (TypedLocalLang NatLang).
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 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.