Commit 687237f2 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Writing more examples.

parent 83db6873
Require Export Expression.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Module NatLang <: Expression.
Inductive NL :=
| var : nat -> NL
| Z : NL
| Succ : NL -> NL
| ttrue : NL
| ffalse : NL.
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.
Qed.
Definition ExprVar : nat -> Expr := var.
Inductive NLVal : NL -> Prop :=
ZVal : NLVal Z
| SuccVal : forall v, NLVal v -> NLVal (Succ v)
| TTrueVal : NLVal ttrue
| FFalseVal : NLVal ffalse.
Global Hint Constructors NLVal : NL.
Definition ExprVal : Expr -> Prop := NLVal.
Fixpoint ExprClosedBelow (n : nat) (e : Expr) : Prop :=
match e with
| var x => x < n
| Z => True
| Succ e => ExprClosedBelow n e
| ttrue => True
| ffalse => True
end.
Definition ExprClosed := ExprClosedBelow 0.
Theorem ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Proof using. intros v val_v; induction val_v; cbn; auto. Qed.
Theorem ExprClosedBelowMono : forall m n e, m < n -> ExprClosedBelow m e -> ExprClosedBelow n e.
Proof using.
intros m n e; revert m n; induction e; try rename n into x;
intros m n m_lt_n cb; cbn; auto.
- cbn in cb; transitivity m; auto.
- cbn in cb; apply IHe with (m := m); auto.
Qed.
Theorem ExprVarClosed : forall n m, ExprClosedBelow n (ExprVar m) <-> m < n.
Proof using. intros n m; cbn; reflexivity. Qed.
Fixpoint ExprSubst (e : Expr) (σ : nat -> Expr) : Expr :=
match e with
| var x => σ x
| Z => Z
| Succ e => Succ (ExprSubst e σ)
| ttrue => ttrue
| ffalse => ffalse
end.
Fixpoint ExprRename (e : Expr) (ξ : nat -> nat) : Expr :=
match e with
| var x => var (ξ x)
| Z => Z
| Succ e => Succ (ExprRename e ξ)
| ttrue => ttrue
| ffalse => ffalse
end.
Notation "e [e| sigma ]" := (ExprSubst e sigma) (at level 29).
Notation "e ⟨e| xi ⟩" := (ExprRename e xi) (at level 29).
Theorem ExprRenameSpec : forall (e : Expr) (ξ : nat -> nat),
e e| ξ⟩ = e [e| fun n => ExprVar (ξ n)].
Proof using. intro e; induction e; intro ξ; cbn; try rewrite IHe; reflexivity. Qed.
Theorem ExprSubstVar : forall n σ, (ExprVar n ) [e| σ] = σ n.
Proof using. intros n σ; cbn; reflexivity. Qed.
Lemma ExprRenameVar : forall n ξ, (ExprVar n) e| ξ = ExprVar (ξ n).
Proof.
intros n ξ.
rewrite ExprRenameSpec. rewrite ExprSubstVar. reflexivity.
Qed.
Theorem ExprRenameFusion : forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(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
| 0 => ExprVar 0
| S n => (σ n) e| S
end.
Definition ExprUpRename : (nat -> nat) -> nat -> nat :=
fun ξ n =>
match n with
| 0 => 0
| S n => S (ξ n)
end.
Theorem ExprSubstExt : forall (e : Expr) (σ1 σ2 : nat -> Expr),
(forall n, σ1 n = σ2 n) -> e [e| σ1] = e [e| σ2].
Proof using. intros e σ1 σ2 eq; induction e; cbn; auto. apply f_equal; auto. Qed.
Theorem ExprRenameExt :forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(forall n, ξ1 n = ξ2 n) -> e e| ξ1 = e e| ξ2.
Proof using. intros e ξ1 ξ2 eq; induction e; cbn; auto. apply f_equal; auto. Qed.
Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n.
Theorem ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e.
Proof using. intro e; induction e; cbn; auto; rewrite IHe; reflexivity. Qed.
Definition ExprIdRenaming : nat -> nat := fun n => n.
Theorem ExprIdRenamingSpec : forall (e : Expr), e e| ExprIdRenaming = e.
Proof using. intro e; induction e; cbn; auto; rewrite IHe; reflexivity. Qed.
Lemma ExprUpSubstId : forall n, ExprIdSubst n = (ExprUpSubst ExprIdSubst) n.
Proof.
intros n; unfold ExprUpSubst; destruct n.
- unfold ExprIdSubst; reflexivity.
- unfold ExprIdSubst. rewrite ExprRenameVar. reflexivity.
Qed.
Lemma ExprUpRenamingId : forall n, ExprIdRenaming n = ExprUpRename ExprIdRenaming n.
Proof.
intros n; unfold ExprUpRename; destruct n; unfold ExprIdRenaming; reflexivity.
Qed.
Theorem ExprClosedBelowSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
ExprClosedBelow n e -> (forall m, m < n -> σ m = ExprVar m) -> e [e|σ] = e.
Proof using.
intro e; induction e; cbn; intros σ x cb σ_bdd; auto; apply f_equal; eapply IHe; eauto.
Qed.
Lemma ExprClosedSubst : forall (e : Expr) (σ : nat -> Expr), ExprClosed e -> e [e|σ] = e.
Proof using.
intros e σ closed; unfold ExprClosed in closed; apply ExprClosedBelowSubst with (n := 0);
auto.
intros m lt; inversion lt.
Qed.
Definition tt : Expr := ttrue. Definition ff : Expr := ffalse.
Theorem ttValue : ExprVal tt. Proof using. unfold tt; unfold ExprVal; auto with NL. Qed.
Theorem ffValue : ExprVal ff. Proof using. unfold ff; unfold ExprVal; auto with NL. Qed.
Theorem boolSeperation : tt <> ff. Proof using. unfold tt; unfold ff; discriminate. Qed.
Inductive NLStep : Expr -> Expr -> Prop :=.
Definition ExprStep : Expr -> Expr -> Prop := NLStep.
Theorem NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Proof using. intros v _ e step; destruct step. Qed.
Theorem ExprRenameClosedBelow : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e e| ξ⟩).
Proof using.
intros e; induction e; intros x ξ m ξ_bdd cb; cbn in *; auto. eapply IHe; eauto.
Qed.
Theorem ExprSubstClosedBelow : forall e n σ m,
(forall k, k < n -> ExprClosedBelow m (σ k)) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e [e| σ]).
Proof using.
intros e; induction e; intros x σ m σ_bdd cb; cbn in *; auto. eapply IHe; eauto.
Qed.
Theorem ExprClosedAfterStep : forall e1 e2 n,
ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
Proof using. intros e1 e2 n step; destruct step. Qed.
End NatLang.
Require Export Expression.
Require Export TypedExpression.
Require Export SoundlyTypedExpression.
Require Export NatLang.
Require Export TypedNatLang.
Module SoundlyTypedNatLang <: (SoundlyTypedExpression NatLang TypedNatLang).
Include TypedNatLang.
Theorem BoolInversion : forall (Γ : nat -> ExprTyp) (v : Expr),
Γ e v ::: bool ->
ExprVal v ->
{v = tt} + {v = ff}.
Proof using.
intros Γ v typ val_v; destruct v; unfold tt; unfold ff; try (left;reflexivity);
try (right; reflexivity).
all: exfalso; inversion typ; subst. inversion val_v.
Qed.
Theorem ExprPreservation : forall (Γ : nat -> ExprTyp) (e1 e2 : Expr) (τ : ExprTyp),
Γ e e1 ::: τ -> ExprStep e1 e2 -> Γ e e2 ::: τ.
Proof using.
intros Γ e1 e2 τ typ step; destruct step.
Qed.
Theorem ExprProgress : forall (Γ : nat -> ExprTyp) (e1 : Expr) (τ : ExprTyp),
Γ e e1 ::: τ -> ExprClosed e1 -> ExprVal e1 \/ exists e2, ExprStep e1 e2.
Proof using.
intros Γ e1 τ typ; induction typ; cbn; intro clsd;
try (left; unfold ExprVal; auto with NL).
inversion clsd. destruct IHtyp; auto; try (constructor; auto).
destruct H as [e2 step]; destruct step.
Qed.
End SoundlyTypedNatLang.
Require Export Expression.
Require Export TypedExpression.
Require Export NatLang.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Module TypedNatLang <: (TypedExpression NatLang).
Include NatLang.
Inductive UniType := N | B.
Definition ExprTyp := UniType.
Definition ExprTypEqDec : forall tau sigma : ExprTyp, {tau = sigma} + {tau <> sigma}.
intros τ σ; destruct τ; destruct σ; try (left; reflexivity);
right; intro eq; inversion eq.
Defined.
Reserved Notation "Γ ⊢e e ::: τ" (at level 30).
Inductive NLTyping : (nat -> ExprTyp) -> Expr -> ExprTyp -> Prop :=
| VarTyping : forall Γ x, Γ e (var x) ::: (Γ x) (* Requires that variables are in scope *)
| ZTyping : forall Γ, Γ e Z ::: N
| STyping : forall Γ e, Γ e e ::: N -> Γ e (Succ e) ::: N
| ttrueTyping : forall Γ, Γ e ttrue ::: B
| ffalseTyping : forall Γ, Γ e ffalse ::: B
where "Γ ⊢e e ::: τ" := (NLTyping Γ e τ).
Global Hint Constructors NLTyping : NL.
Definition ExprTyping : (nat -> ExprTyp) -> Expr -> ExprTyp -> Prop := NLTyping.
Theorem ExprVarTyping : forall (Γ : nat -> ExprTyp) (n : nat),
Γ e (ExprVar n) ::: (Γ n).
Proof using. intros Γ n; unfold ExprVar; constructor. Qed.
Theorem ExprTypingExt : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ n) ->
Γ e e ::: τ ->
Δ e e ::: τ.
Proof using.
intros Γ Δ e τ eq typ; revert Δ eq; induction typ; intros Δ eq; auto with NL.
rewrite eq; constructor.
Qed.
Theorem ExprTypingUnique : forall (Γ : nat -> ExprTyp) (e : Expr) (τ σ : ExprTyp),
Γ e e ::: τ ->
Γ e e ::: σ ->
τ = σ.
Proof using.
intros Γ e τ σ typ1; revert σ; induction typ1; intros σ typ2; inversion typ2; subst;
reflexivity.
Qed.
Theorem ExprWeakening : forall (Γ Δ : nat -> ExprTyp) (ξ : nat -> nat) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ (ξ n)) ->
Γ e e ::: τ ->
Δ e e e| ξ⟩ ::: τ.
Proof using.
intros Γ Δ ξ e τ eq typ; revert Δ ξ eq; induction typ; intros Δ ξ eq; cbn in *;
auto with NL.
rewrite eq; auto with NL.
Qed.
Theorem ExprClosedBelowTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp) (n : nat),
ExprClosedBelow n e -> (forall m, m < n -> Γ m = Δ m) -> Γ e e ::: τ -> Δ e e ::: τ.
Proof using.
intros Γ Δ e; revert Γ Δ; induction e; intros Γ Δ τ x cb bdd ty; inversion ty;
subst; auto with NL.
- rewrite bdd; auto with NL. - constructor; eapply IHe; eauto.
Qed.
Lemma ExprClosedTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
ExprClosed e -> Γ e e ::: τ -> Δ e e ::: τ.
Proof.
intros Γ Δ e τ H H0. unfold ExprClosed in H.
apply ExprClosedBelowTyping with (Γ := Γ) (n := 0); auto.
intros m H1. inversion H1.
Qed.
Lemma ExprValueTyping : forall (Γ Δ : nat -> ExprTyp) (v : Expr) (τ : ExprTyp),
ExprVal v -> Γ e v ::: τ -> Δ e v ::: τ.
Proof.
intros Γ Δ v τ H H0. apply ExprClosedTyping with (Γ := Γ); auto.
apply ExprValuesClosed; auto.
Qed.
Definition bool : ExprTyp := B.
Theorem TrueTyping : forall (Γ : nat -> ExprTyp), Γ e tt ::: bool.
Proof using. intro Γ; constructor. Qed.
Theorem FalseTyping : forall (Γ : nat -> ExprTyp), Γ e ff ::: bool.
Proof using. intro Γ; constructor. Qed.
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).
Theorem ExprSubstType :
forall (Γ Δ : nat -> ExprTyp) (sigma : nat -> Expr) (e : Expr) (τ : ExprTyp),
Γ es sigma Δ -> Γ e e ::: τ -> Δ e e [e| sigma ] ::: τ.
Proof using.
intros Γ Δ σ e τ σ_ty e_ty; revert Δ σ σ_ty; induction e_ty; intros Δ σ σ_ty; cbn;
try (constructor; auto); apply σ_ty.
Qed.
Lemma ExprIdSubstTyping : forall (Γ : nat -> ExprTyp), Γ es ExprIdSubst Γ.
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.
Require Export Expression.
Require Export TypedExpression.
Require Export LambdaCalc.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Module UnitypedLC <: (TypedExpression LambdaCalc).
Include LambdaCalc.
Inductive UniType := Ast.
Definition ExprTyp := UniType.
Definition ExprTypEqDec : forall tau sigma : ExprTyp, {tau = sigma} + {tau <> sigma}.
intros τ σ; destruct τ; destruct σ; left; reflexivity.
Qed.
Reserved Notation "Γ ⊢e e ::: τ" (at level 30).
Inductive Unityping : (nat -> ExprTyp) -> Expr -> ExprTyp -> Prop :=
| TrivialTyping : forall Γ e, Γ e e ::: Ast
where "Γ ⊢e e ::: τ" := (Unityping Γ e τ).
Global Hint Constructors Unityping : LC.
Definition ExprTyping := Unityping.
Theorem ExprVarTyping : forall (Γ : nat -> ExprTyp) (n : nat),
Γ e (ExprVar n) ::: (Γ n).
Proof using. intros Γ n; destruct (Γ n); apply TrivialTyping. Qed.
Theorem ExprTypingExt : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ n) ->
Γ e e ::: τ ->
Δ e e ::: τ.
Proof using. intros Γ Δ e τ _ _; destruct τ; apply TrivialTyping. Qed.
Theorem ExprTypingUnique : forall (Γ : nat -> ExprTyp) (e : Expr) (τ σ : ExprTyp),
Γ e e ::: τ ->
Γ e e ::: σ ->
τ = σ.
Proof using. intros _ _ τ σ _ _; destruct τ; destruct σ; reflexivity. Qed.
Theorem ExprWeakening : forall (Γ Δ : nat -> ExprTyp) (ξ : nat -> nat) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ (ξ n)) ->
Γ e e ::: τ ->
Δ e e e| ξ⟩ ::: τ.
Proof using. intros _ Δ ξ e τ _ _; destruct τ; auto with LC. Qed.
Theorem ExprClosedBelowTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp) (n : nat),
ExprClosedBelow n e -> (forall m, m < n -> Γ m = Δ m) -> Γ e e ::: τ -> Δ e e ::: τ.
Proof using. intros _ Δ e τ _ _ _ _; destruct τ; auto with LC. Qed.
Lemma ExprClosedTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
ExprClosed e -> Γ e e ::: τ -> Δ e e ::: τ.
Proof.
intros Γ Δ e τ H H0. unfold ExprClosed in H.
apply ExprClosedBelowTyping with (Γ := Γ) (n := 0); auto.
intros m H1. inversion H1.
Qed.
Lemma ExprValueTyping : forall (Γ Δ : nat -> ExprTyp) (v : Expr) (τ : ExprTyp),
ExprVal v -> Γ e v ::: τ -> Δ e v ::: τ.
Proof.
intros Γ Δ v τ H H0. apply ExprClosedTyping with (Γ := Γ); auto.
apply ExprValuesClosed; auto.
Qed.
Definition bool : ExprTyp := Ast.
Theorem TrueTyping : forall (Γ : nat -> ExprTyp),
Γ e tt ::: bool.
Proof using. intro Γ; unfold bool; auto with LC. Qed.
Theorem FalseTyping : forall (Γ : nat -> ExprTyp),
Γ e ff ::: bool.
Proof using. intro Γ; unfold bool; auto with LC. Qed.
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).
Theorem ExprSubstType :
forall (Γ Δ : nat -> ExprTyp) (sigma : nat -> Expr) (e : Expr) (τ : ExprTyp),
Γ es sigma Δ -> Γ e e ::: τ -> Δ e e [e| sigma ] ::: τ.
Proof using. intros _ Δ σ e τ _ _; destruct τ; auto with LC. Qed.
Lemma ExprIdSubstTyping : forall (Γ : nat -> ExprTyp), Γ es ExprIdSubst Γ.
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 UnitypedLC.
......@@ -5,6 +5,10 @@ SoundlyTypedExpression.v
LambdaCalc.v
STLC.v
STLCSound.v
UnitypedLC.v
NatLang.v
TypedNatLang.v
SoundlyTypedNatLang.v
Locations.v
LocationMap.v
FunLMap.v
......
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