syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

organize coq sources in subdirectories

Browse source
This commit is contained in:
Michael Sippel 2024-09-21 13:00:57 +02:00
parent 30fe571a39
commit d690d6dcdc
Signed by: senvas
GPG key ID: F96CF119C34B64A6
25 changed files with 32 additions and 1698 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
coq/_CoqProject
View file

@ -1,28 +1,17 @@
-R . LadderTypes
AdditionalTactics.v
ListFacts.v
FiniteSets.v
FSetNotin.v
Atom.v
Metatheory.v
metatheory/AdditionalTactics.v
metatheory/ListFacts.v
metatheory/FiniteSets.v
metatheory/FSetNotin.v
metatheory/Atom.v
metatheory/Metatheory.v
terms_debruijn.v
equiv_debruijn.v
subtype_debruijn.v
context_debruijn.v
morph_debruijn.v
typing_debruijn.v
eval_debruijn.v
subst_lemmas_debruijn.v
terms/debruijn.v
terms/equiv.v
terms/eval.v
typing/context.v
typing/subtype.v
typing/morph.v
typing/typing.v
lemmas/subst_lemmas.v
terms.v
equiv.v
subst.v
subtype.v
context.v
morph.v
typing.v
smallstep.v
soundness.v
bbencode.v

15
coq/context.v
View file

@ -1,15 +0,0 @@
From Coq Require Import Strings.String.
Require Import terms.
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
Inductive context_contains : context -> string -> type_term -> Prop :=
| C_take : forall (x:string) (X:type_term) (Γ:context),
(context_contains (ctx_assign x X Γ) x X)
| C_shuffle : forall x X y Y Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).

423
coq/equiv.v
View file

@ -1,423 +0,0 @@
(* This module defines an equivalence relation
* on type-terms.
*
* In general, we want distributivity of ladders
* over all other type constructors, e.g. type-
* specializations or function-types.
*
* Formally, we define two rewrite rules that
* shall define how we are able to rewrite type-terms
* such that they remain equivalent.
*
* (1) `-->distribute-ladder` which distributes
* ladder types over other type constructors, e.g.
* <S T~U> -->distribute-ladder <S T> ~ <S U>.
*
* (2) `-->condense-ladder` which does the
* inverse operation, e.g.
* <S T> ~ <S U> -->condense-ladder <S T~U>
*
* When applied exhaustively, each rewrite rule yields
* a normal form, namely *Ladder Normal Form (LNF)*, which
* is reached by exhaustive application of `-->distribute-ladder`,
* and *Parameter Normal Form (PNF)*, which is reached by exhaustive
* application of `-->condense-ladder`.
*
* The equivalence relation `===` over type-terms is then defined
* as the reflexive and transitive hull over `-->distribute-ladder`
* and `-->condense-ladder`. Since the latter two are the inverse
* rewrite-step of each other, `===` is symmetric and thus `===`
* satisfies all properties required of an equivalence relation.
*)
Require Import terms.
Require Import subst.
From Coq Require Import Strings.String.
(** Alpha conversion in types *)
Reserved Notation "S '--->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop :=
| TAlpha_Rename : forall x y t,
(type_univ x t) --->α (type_univ y (type_subst x (type_var y) t))
| TAlpha_SubUniv : forall x τ τ',
(τ --->α τ') ->
[< ∀x,τ >] --->α [< ∀x,τ' >]
| TAlpha_SubSpec1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
[< <τ1 τ2> >] --->α [< <τ1' τ2> >]
| TAlpha_SubSpec2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
[< <τ1 τ2> >] --->α [< <τ1 τ2'> >]
| TAlpha_SubFun1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
[< τ1 -> τ2 >] --->α [< τ1' -> τ2 >]
| TAlpha_SubFun2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
[< τ1 -> τ2 >] --->α [< τ1 -> τ2' >]
| TAlpha_SubMorph1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
[< τ1 ->morph τ2 >] --->α [< τ1' ->morph τ2 >]
| TAlpha_SubMorph2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
[< τ1 ->morph τ2 >] --->α [< τ1 ->morph τ2' >]
| TAlpha_SubLadder1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') ->
[< τ1 ~ τ2 >] --->α [< τ1' ~ τ2 >]
| TAlpha_SubLadder2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') ->
[< τ1 ~ τ2 >] --->α [< τ1 ~ τ2' >]
where "S '--->α' T" := (type_conv_alpha S T).
(** Alpha conversion is symmetric *)
Lemma type_alpha_symm :
forall σ τ,
(σ --->α τ) -> (τ --->α σ).
Proof.
intros.
induction H.
- admit.
- auto using TAlpha_Rename,type_subst,type_subst_symm, TAlpha_SubUniv.
- auto using TAlpha_SubSpec1.
- auto using TAlpha_SubSpec2.
- auto using TAlpha_SubFun1.
- auto using TAlpha_SubFun2.
- auto using TAlpha_SubMorph1.
- auto using TAlpha_SubMorph2.
- auto using TAlpha_SubLadder1.
- auto using TAlpha_SubLadder2.
Admitted.
(** Define all rewrite steps $\label{coq:type-dist}$ *)
Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
| L_DistributeOverSpec1 : forall x x' y,
[< <x~x' y> >]
-->distribute-ladder
[< <x y>~<x' y> >]
| L_DistributeOverSpec2 : forall x y y',
[< <x y~y'> >]
-->distribute-ladder
[< <x y>~<x y'> >]
| L_DistributeOverFun1 : forall x x' y,
[< (x~x' -> y) >]
-->distribute-ladder
[< (x -> y) ~ (x' -> y) >]
| L_DistributeOverFun2 : forall x y y',
[< (x -> y~y') >]
-->distribute-ladder
[< (x -> y) ~ (x -> y') >]
| L_DistributeOverMorph1 : forall x x' y,
[< (x~x' ->morph y) >]
-->distribute-ladder
[< (x ->morph y) ~ (x' ->morph y) >]
| L_DistributeOverMorph2 : forall x y y',
(type_morph x (type_ladder y y'))
-->distribute-ladder
(type_ladder (type_morph x y) (type_morph x y'))
where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
Reserved Notation "S '-->condense-ladder' T" (at level 40).
Inductive type_condense_ladder : type_term -> type_term -> Prop :=
| L_CondenseOverSpec1 : forall x x' y,
[< <x y>~<x' y> >]
-->condense-ladder
[< <x~x' y> >]
| L_CondenseOverSpec2 : forall x y y',
[< <x y>~<x y'> >]
-->condense-ladder
[< <x y~y'> >]
| L_CondenseOverFun1 : forall x x' y,
[< (x -> y) ~ (x' -> y) >]
-->condense-ladder
[< (x~x') -> y >]
| L_CondenseOverFun2 : forall x y y',
[< (x -> y) ~ (x -> y') >]
-->condense-ladder
[< (x -> y~y') >]
| L_CondenseOverMorph1 : forall x x' y,
[< (x ->morph y) ~ (x' ->morph y) >]
-->condense-ladder
[< (x~x' ->morph y) >]
| L_CondenseOverMorph2 : forall x y y',
[< (x ->morph y) ~ (x ->morph y') >]
-->condense-ladder
[< (x ->morph y~y') >]
where "S '-->condense-ladder' T" := (type_condense_ladder S T).
(** Inversion Lemma:
`-->distribute-ladder` is the inverse of `-->condense-ladder
*)
Lemma distribute_inverse :
forall x y,
x -->distribute-ladder y ->
y -->condense-ladder x.
Proof.
intros.
destruct H.
apply L_CondenseOverSpec1.
apply L_CondenseOverSpec2.
apply L_CondenseOverFun1.
apply L_CondenseOverFun2.
apply L_CondenseOverMorph1.
apply L_CondenseOverMorph2.
Qed.
(** Inversion Lemma:
`-->condense-ladder` is the inverse of `-->distribute-ladder`
*)
Lemma condense_inverse :
forall x y,
x -->condense-ladder y ->
y -->distribute-ladder x.
Proof.
intros.
destruct H.
apply L_DistributeOverSpec1.
apply L_DistributeOverSpec2.
apply L_DistributeOverFun1.
apply L_DistributeOverFun2.
apply L_DistributeOverMorph1.
apply L_DistributeOverMorph2.
Qed.
(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : type_term -> type_term -> Prop :=
| TEq_Refl : forall x,
x === x
| TEq_Trans : forall x y z,
x === y ->
y === z ->
x === z
| TEq_SubFun : forall x x' y y',
x === x' ->
y === y' ->
[< x -> y >] === [< x' -> y' >]
| TEq_SubMorph : forall x x' y y',
x === x' ->
y === y' ->
[< x ->morph y >] === [< x' ->morph y' >]
| TEq_LadderAssocLR : forall x y z,
[< (x~y)~z >]
===
[< x~(y~z) >]
| TEq_LadderAssocRL : forall x y z,
[< x~(y~z) >]
===
[< (x~y)~z >]
| TEq_Alpha : forall x y,
x --->α y ->
x === y
| TEq_Distribute : forall x y,
x -->distribute-ladder y ->
x === y
| TEq_Condense : forall x y,
x -->condense-ladder y ->
x === y
where "S '===' T" := (type_eq S T).
(** Symmetry of === *)
Lemma TEq_Symm :
forall x y,
(x === y) -> (y === x).
Proof.
intros.
induction H.
apply TEq_Refl.
apply TEq_Trans with (y:=y).
apply IHtype_eq2.
apply IHtype_eq1.
apply TEq_SubFun.
auto. auto.
apply TEq_SubMorph.
auto. auto.
apply TEq_LadderAssocRL.
apply TEq_LadderAssocLR.
apply type_alpha_symm in H.
apply TEq_Alpha.
apply H.
apply TEq_Condense.
apply distribute_inverse.
apply H.
apply TEq_Distribute.
apply condense_inverse.
apply H.
Qed.
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
| FlatVar : forall x, (type_is_flat (type_var x))
| FlatId : forall x, (type_is_flat (type_id x))
| FlatApp : forall x y,
(type_is_flat x) ->
(type_is_flat y) ->
(type_is_flat (type_spec x y))
| FlatFun : forall x y,
(type_is_flat x) ->
(type_is_flat y) ->
(type_is_flat (type_fun x y))
| FlatSub : forall x v,
(type_is_flat x) ->
(type_is_flat (type_univ v x))
.
(** Ladder Normal Form:
exhaustive application of -->distribute-ladder
*)
Inductive type_is_lnf : type_term -> Prop :=
| LNF : forall x : type_term,
(not (exists y:type_term, x -->distribute-ladder y))
-> (type_is_lnf x)
.
(** Parameter Normal Form:
exhaustive application of -->condense-ladder
*)
Inductive type_is_pnf : type_term -> Prop :=
| PNF : forall x : type_term,
(not (exists y:type_term, x -->condense-ladder y))
-> (type_is_pnf x)
.
(** Any term in LNF either is flat, or is a ladder T1~T2 where T1 is flat and T2 is in LNF *)
Lemma lnf_shape :
forall τ:type_term,
(type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_ladder τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2)))
.
Proof.
intros τ H.
induction τ.
left.
apply FlatId.
left.
apply FlatVar.
(*
left.
apply IHτ1 in H.
apply FlatFun.
apply H.
destruct H.
destruct H.
apply IHτ1.
*)
admit.
admit.
admit.
admit.
Admitted.
(** every type has an equivalent LNF *)
Lemma lnf_normalizing :
forall t, exists t', (t === t') /\ (type_is_lnf t').
Proof.
intros.
destruct t.
exists (type_id s).
split. apply TEq_Refl.
apply LNF.
admit.
admit.
admit.
exists (type_univ s t).
split.
apply TEq_Refl.
apply LNF.
Admitted.
(** every type has an equivalent PNF *)
Lemma pnf_normalizing :
forall t, exists t', (t === t') /\ (type_is_pnf t').
Proof.
Admitted.
Lemma lnf_uniqueness :
forall t t' t'',
(t === t') /\ (type_is_lnf t') /\ (t === t'') /\ (type_is_lnf t'')
-> t = t'.
Proof.
Admitted.
(**
* Examples
*)
Example example_flat_type :
type_is_flat [< <$"PosInt"$ $"10"$> >].
Proof.
apply FlatApp.
apply FlatId.
apply FlatId.
Qed.
Example example_lnf_type :
type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >].
Proof.
Admitted.
Example example_type_eq :
[< [$"Char"$ ~ $"Byte"$] >]
===
[< [$"Char"$] ~ [$"Byte"$] >]
.
Proof.
apply TEq_Distribute.
apply L_DistributeOverSpec2.
Qed.

0
coq/bbencode.v → coq/examples/bbencode.v
View file

2
coq/subst_lemmas_debruijn.v → coq/lemmas/subst_lemmas.v
View file

@ -1,7 +1,7 @@
Require Import terms_debruijn.
Require Import Atom.
Require Import Metatheory.
Require Import FSetNotin.
Require Import debruijn.
(*
* Substitution has no effect if the variable is not free

0
coq/AdditionalTactics.v → coq/metatheory/AdditionalTactics.v
View file

0
coq/Atom.v → coq/metatheory/Atom.v
View file

0
coq/FSetNotin.v → coq/metatheory/FSetNotin.v
View file

0
coq/FiniteSets.v → coq/metatheory/FiniteSets.v
View file

0
coq/ListFacts.v → coq/metatheory/ListFacts.v
View file

0
coq/Metatheory.v → coq/metatheory/Metatheory.v
View file

92
coq/morph.v
View file

@ -1,92 +0,0 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
Open Scope ladder_expr_scope.
Inductive morphism_path : context -> type_term -> type_term -> Prop :=
| M_Sub : forall Γ τ τ',
(τ :<= τ') ->
(Γ |- τ ~> τ')
| M_Single : forall Γ h τ τ',
(context_contains Γ h [< τ ->morph τ' >]) ->
(Γ |- τ ~> τ')
| M_Chain : forall Γ τ τ' τ'',
(Γ |- τ ~> τ') ->
(Γ |- τ' ~> τ'') ->
(Γ |- τ ~> τ'')
| M_Lift : forall Γ σ τ τ',
(Γ |- τ ~> τ') ->
(Γ |- [< σ ~ τ >] ~> [< σ ~ τ' >])
| M_MapSeq : forall Γ τ τ',
(Γ |- τ ~> τ') ->
(Γ |- [< [τ] >] ~> [< [τ'] >])
where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
Lemma id_morphism_path : forall Γ τ, Γ |- τ ~> τ.
Proof.
intros.
apply M_Sub, TSubRepr_Refl, TEq_Refl.
Qed.
Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
| Translate_Descend : forall Γ τ τ',
(τ :<= τ') ->
(translate_morphism_path Γ τ τ'
(expr_morph "x" τ [{ %"x"% des τ' }]))
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~> τ') ->
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ [< σ ~ τ >] [< σ ~ τ' >]
(expr_morph "x" [< σ ~ τ >] [{ (m (%"x"% des τ)) as σ }]))
| Translate_Single : forall Γ h τ τ',
(context_contains Γ h [< τ ->morph τ' >]) ->
(translate_morphism_path Γ τ τ' [{ %h% }])
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(translate_morphism_path Γ τ τ' m1) ->
(translate_morphism_path Γ τ' τ'' m2) ->
(translate_morphism_path Γ τ τ''
(expr_morph "x" τ [{ m2 (m1 %"x"%) }]))
| Translate_MapSeq : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ [< [τ] >] [< [τ'] >]
[{
λ"xs",[τ] ↦morph (%"map"% # τ # τ' m %"xs"%)
}])
.
Example morphism_paths :
(ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]
(ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >]
ctx_empty))
|- [< [ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$ ] >]
~> [< [ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$ ] >]
.
Proof.
intros.
apply M_MapSeq.
apply M_Lift.
apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
apply M_Single with (h:="degrees-to-turns"%string).
apply C_take.
apply M_Single with (h:="turns-to-radians"%string).
apply C_shuffle.
apply C_take.
Qed.

137
coq/smallstep.v
View file

@ -1,137 +0,0 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import subtype.
Require Import typing.
Reserved Notation " s '-->α' t " (at level 40).
Reserved Notation " s '-->β' t " (at level 40).
Inductive expr_alpha : expr_term -> expr_term -> Prop :=
| EAlpha_Rename : forall x x' τ e,
(expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
| EAlpha_TyRename : forall α α' e,
(expr_ty_abs α e) -->α (expr_ty_abs α' (expr_specialize α (type_var α') e))
| EAlpha_SubAbs : forall x τ e e',
(e -->α e') ->
[{ λ x , τ ↦ e }] -->α [{ λ x , τ ↦ e' }]
| EAlpha_SubTyAbs : forall α e e',
(e -->α e') ->
[{ Λ α ↦ e }] -->α [{ Λ α ↦ e' }]
| EAlpha_SubApp1 : forall e1 e1' e2,
(e1 -->α e1') ->
[{ e1 e2 }] -->α [{ e1' e2 }]
| EAlpha_SubApp2 : forall e1 e2 e2',
(e2 -->α e2') ->
[{ e1 e2 }] -->α [{ e1 e2' }]
where "s '-->α' t" := (expr_alpha s t).
Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
Proof.
unfold polymorphic_identity1.
unfold polymorphic_identity2.
apply EAlpha_SubTyAbs.
apply EAlpha_Rename.
Qed.
Inductive beta_step : expr_term -> expr_term -> Prop :=
| E_App1 : forall e1 e1' e2,
e1 -->β e1' ->
[{ e1 e2 }] -->β [{ e1' e2 }]
| E_App2 : forall v1 e2 e2',
(is_value v1) ->
e2 -->β e2' ->
[{ v1 e2 }] -->β [{ v1 e2' }]
| E_TypApp : forall e e' τ,
e -->β e' ->
[{ Λ τ ↦ e }] -->β [{ Λ τ ↦ e' }]
| E_TypAppLam : forall α e τ,
[{ (Λ α ↦ e) # τ }] -->β (expr_specialize α τ e)
| E_AppLam : forall x τ e a,
[{ (λ x , τ ↦ e) a }] -->β (expr_subst x a e)
| E_AppMorph : forall x τ e a,
[{ (λ x , τ ↦morph e) a }] -->β (expr_subst x a e)
| E_Let : forall x e a,
[{ let x := a in e }] -->β (expr_subst x a e)
| E_StripAscend : forall τ e,
[{ e as τ }] -->β e
| E_StripDescend : forall τ e,
[{ e des τ }] -->β e
| E_Ascend : forall τ e e',
(e -->β e') ->
[{ e as τ }] -->β [{ e' as τ }]
| E_AscendCollapse : forall τ' τ e,
[{ (e as τ) as τ' }] -->β [{ e as (τ'~τ) }]
| E_DescendCollapse : forall τ' τ e,
(τ':<=τ) ->
[{ (e des τ') des τ }] -->β [{ e des τ }]
where "s '-->β' t" := (beta_step s t).
Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
| Multi_Refl : forall (x : X), multi R x x
| Multi_Step : forall (x y z : X),
R x y ->
multi R y z ->
multi R x z.
Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
Notation " s -->β* t " := (multi beta_step s t) (at level 40).
Example reduce1 :
[{
let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
}]
-->β*
[{
((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
}].
Proof.
apply Multi_Step with (y:=[{ (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
apply E_Let.
apply Multi_Step with (y:=(expr_subst "x" [{%"60"% as $"Angle"$~$"Degrees"$}] [{ (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$) }])).
apply E_AppMorph.
simpl.
apply Multi_Step with (y:=[{ ((%"/"% (%"60"% as $"Angle"$~$"Degrees"$)) %"360"%) as $"Angle"$~$"Turns"$ }]).
apply E_Ascend.
apply E_App1.
apply E_App2.
apply V_Abs, VAbs_Var.
apply E_StripDescend.
apply Multi_Step with (y:=[{ (%"/"% %"60"% %"360"%) as $"Angle"$~$"Turns"$ }]).
apply E_Ascend.
apply E_App1.
apply E_App2.
apply V_Abs, VAbs_Var.
apply E_StripAscend.
apply Multi_Refl.
Qed.

359
coq/soundness.v
View file

@ -1,359 +0,0 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import morph.
Require Import smallstep.
Require Import typing.
Lemma typing_weakening : forall Γ e τ x σ,
(Γ |- e \is τ) ->
((ctx_assign x σ Γ) |- e \is τ)
.
Proof.
intros.
induction H.
- apply T_Var.
apply C_shuffle.
apply H.
- apply T_Let with (σ:=σ0).
apply IHexpr_type1.
admit.
Admitted.
Lemma typing_subst : forall Γ x σ s e τ,
(ctx_assign x σ Γ) |- e \is τ ->
Γ |- s \is σ ->
Γ |- (expr_subst x s e) \is τ.
Proof.
Admitted.
Lemma typing_tsubst : forall Γ α σ e τ,
Γ |- e \is τ ->
Γ |- (expr_specialize α σ e) \is (type_subst α σ τ).
Proof.
Admitted.
Lemma map_type : forall Γ,
Γ |- [{ %"map"% }] \is [<
∀"σ",∀"τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%]
>].
Proof.
Admitted.
Lemma specialized_map_type : forall Γ τ τ',
Γ |- [{ %"map"% # τ # τ' }] \is [<
(τ -> τ') -> [τ] -> [τ']
>].
Proof.
Admitted.
(* morphism has valid typing *)
Lemma morphism_path_solves_type : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) ->
Γ |- m \is (type_morph τ τ')
.
Proof.
intros.
induction H.
(* Sub *)
apply T_MorphAbs.
apply T_Descend with (τ:=τ).
apply T_Var.
apply C_take.
apply H.
(* Lift *)
apply T_MorphAbs.
apply T_Ascend.
apply T_App with (σ':=τ) (σ:=τ).
apply T_MorphFun.
apply typing_weakening.
apply IHtranslate_morphism_path.
apply T_Descend with (τ:=(type_ladder σ τ)).
apply T_Var.
apply C_take.
apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
apply id_morphism_path.
(* Single *)
apply T_Var.
apply H.
(* Chain *)
apply T_MorphAbs.
apply T_App with (σ':=τ') (σ:=τ') (τ:=τ'').
apply T_MorphFun.
apply typing_weakening.
apply IHtranslate_morphism_path2.
apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
apply T_MorphFun.
apply typing_weakening.
apply IHtranslate_morphism_path1.
apply T_Var.
apply C_take.
apply id_morphism_path.
apply id_morphism_path.
(* Map Sequence *)
apply T_MorphAbs.
apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
apply specialized_map_type.
apply typing_weakening.
apply T_MorphFun.
apply IHtranslate_morphism_path.
apply id_morphism_path.
auto using T_Var, C_take.
apply id_morphism_path.
Qed.
(* reduction step preserves well-typedness *)
Lemma preservation : forall Γ e e' τ,
(Γ |- e \is τ) ->
(e -->β e') ->
(Γ |- e' \is τ)
.
Proof.
intros Γ e e' τ Typ Red.
generalize dependent e'.
induction Typ; intros e' Red.
(* `e` is Variable *)
- inversion Red.
(* `e` is Let *)
- inversion Red.
subst.
apply typing_subst with (σ:=σ).
auto.
auto.
(* `e` is Type-Abstraction *)
- inversion Red.
subst.
apply T_TypeAbs.
auto.
(* `e` is Type-Application *)
- inversion Red.
admit.
(*
apply typing_tsubst.
admit.
*)
(* `e` is abstraction *)
- inversion Red.
(* `e` is morphism *)
- inversion Red.
(* `e` is Application *)
- inversion Red.
* apply T_App with (σ':=σ') (σ:=σ).
apply IHTyp1.
auto. auto. auto.
* apply T_App with (σ':=σ') (σ:=σ).
auto using IHTyp2.
auto. auto.
* apply typing_subst with (σ:=σ').
subst.
admit.
auto.
* apply typing_subst with (σ:=σ').
admit.
auto.
(* `e` is Morphism *)
- auto using T_MorphFun.
(* `e` is Ascend *)
- admit.
(*
apply IHexpr_type.
inversion Red.
*)
(* `e` is Descension *)
- intros.
apply T_DescendImplicit with (τ:=τ).
auto. auto.
(* `e` is descension *)
- apply T_DescendImplicit with (τ:=τ).
apply IHTyp.
admit.
auto.
Admitted.
(* translation of expression preserves typing *)
Lemma translation_preservation : forall Γ e e' τ,
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
(Γ |- e' \is τ)
.
Proof.
intros Γ e e' τ Typ Transl.
generalize dependent e'.
intros e' Transl.
induction Transl.
(* e is Variable *)
- apply H.
(* e is Let-Binding *)
- apply T_Let with (τ:=τ) (σ:=σ).
auto. auto.
- auto using T_TypeAbs.
(* e is Type-Application *)
- apply T_TypeApp.
admit.
- auto using T_Abs.
- auto using T_MorphAbs.
(* e is Application *)
- apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
auto.
apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
apply T_MorphFun.
apply morphism_path_solves_type.
auto. auto.
apply id_morphism_path.
apply id_morphism_path.
(* e is Morphism *)
- auto using T_MorphFun.
(* e is Ascension *)
- auto using T_Ascend.
(* e is Desecension *)
- apply T_Descend with (τ:=τ).
auto. auto.
Admitted.
(* e is stuck when it is neither a value, nor can it be reduced *)
Definition is_stuck (e:expr_term) : Prop :=
~(is_value e) ->
~(exists e', e -->β e')
.
(* the translation any well typed term is not stuck *)
Lemma progress :
forall Γ e τ e',
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
~(is_stuck e')
.
Proof.
Admitted.
(* every well-typed expression is translated,
* such that it be reduced to a value
*)
Theorem soundness :
forall Γ e e' τ,
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
(exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ))
.
Proof.
intros.
induction H0.
(* `e` is Variable *)
- exists (expr_var x).
split. apply Multi_Refl.
split. apply V_Abs,VAbs_Var.
apply H.
(* `e` is Let-Binding *)
- exists (expr_subst x e' t').
split.
apply Multi_Step with (y:=(expr_subst x e' t')).
apply E_Let with (x:=x) (a:=e') (e:=t').
apply Multi_Refl.
admit.
(*
split.
unfold expr_subst.
induction t'.
exists (expr_subst x e' (expr_var s)).
split.
unfold expr_subst.
apply E_Let.
*)
(* `e` is Type-Abstraction *)
- exists (expr_ty_abs α e').
split.
apply Multi_Refl.
split.
apply V_Abs, VAbs_TypAbs.
apply T_TypeAbs.
apply translation_preservation with (e:=e).
apply H0.
apply H1.
(* `e` is Type-Application *)
- admit.
(* `e`is Abstraction *)
- exists (expr_abs x σ e').
split. apply Multi_Refl.
split. apply V_Abs, VAbs_Abs.
apply T_Abs.
apply translation_preservation with (e:=e).
apply H0.
apply H2.
(* `e` is Morphism Abstraction *)
- exists (expr_morph x σ e').
split. apply Multi_Refl.
split. apply V_Abs, VAbs_Morph.
apply T_MorphAbs.
apply translation_preservation with (e:=e).
apply H0.
apply H2.
(* `e` is Application *)
- admit.
(* `e` is morphism *)
- admit.
(* `e` is Ascension *)
- admit.
(* `e` is Descension *)
- admit.
Admitted.

152
coq/subst.v
View file

@ -1,152 +0,0 @@
From Coq Require Import Strings.String.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import terms.
Fixpoint type_fv (τ : type_term) {struct τ} : (list string) :=
match τ with
| type_id s => []
| type_var α => [α]
| type_univ α τ => (remove string_dec α (type_fv τ))
| type_spec σ τ => (type_fv σ) ++ (type_fv τ)
| type_fun σ τ => (type_fv σ) ++ (type_fv τ)
| type_morph σ τ => (type_fv σ) ++ (type_fv τ)
| type_ladder σ τ => (type_fv σ) ++ (type_fv τ)
end.
Open Scope ladder_type_scope.
Example ex_type_fv1 :
(In "T"%string (type_fv [< ∀"U",%"T"% >]))
.
Proof. simpl. left. auto. Qed.
Open Scope ladder_type_scope.
Example ex_type_fv2 :
~(In "T"%string (type_fv [< ∀"T",%"T"% >]))
.
Proof. simpl. auto. Qed.
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : type_term :=
match t0 with
| type_var name => if (eqb v name) then n else t0
| type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
| type_univ x t => if (eqb v x) then t0 else type_univ x (type_subst v n t)
| type_spec t1 t2 => (type_spec (type_subst v n t1) (type_subst v n t2))
| type_ladder t1 t2 => (type_ladder (type_subst v n t1) (type_subst v n t2))
| t => t
end.
(*
Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop :=
| TSubst_VarReplace :
(type_subst1 x σ (type_var x) σ)
| TSubst_VarKeep : forall y,
(x <> y) ->
(type_subst1 x σ (type_var y) (type_var y))
| TSubst_UnivReplace : forall y τ τ',
~(x = y) ->
~(type_var_free y σ) ->
(type_subst1 x σ τ τ') ->
(type_subst1 x σ (type_univ y τ) (type_univ y τ'))
| TSubst_Id : forall n,
(type_subst1 x σ (type_id n) (type_id n))
| TSubst_Spec : forall τ1 τ2 τ1' τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_spec τ1 τ2) (type_spec τ1' τ2'))
| TSubst_Fun : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_fun τ1 τ2) (type_fun τ1' τ2'))
| TSubst_Morph : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_morph τ1 τ2) (type_morph τ1' τ2'))
| TSubst_Ladder : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2'))
.
*)
Lemma type_subst_symm :
forall x y τ τ',
((type_subst x (type_var y) τ) = τ') ->
((type_subst y (type_var x) τ') = τ)
.
Proof.
intros.
induction H.
unfold type_subst.
induction τ.
reflexivity.
Admitted.
Lemma type_subst_fresh :
forall α τ u,
~ (In α (type_fv τ))
-> (type_subst α u τ) = τ
.
Proof.
intros.
unfold type_subst.
induction τ.
reflexivity.
unfold eqb.
admit.
(*
apply TSubst_Id.
apply TSubst_VarKeep.
contradict H.
rewrite H.
apply TFree_Var.
apply TSubst_Fun.
apply IHτ1.
contradict H.
apply TFree_Fun.
apply H.
apply
*)
Admitted.
(* scoped variable substitution, replaces free occurences of v with n in expression e *)
Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
match e0 with
| expr_var name => if (eqb v name) then n else e0
| expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
| expr_ty_app e t => expr_ty_app (expr_subst v n e) t
| expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
| expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
| expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
| expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e)
| expr_ascend t e => expr_ascend t (expr_subst v n e)
| expr_descend t e => expr_descend t (expr_subst v n e)
end.
(* replace only type variables in expression *)
Fixpoint expr_specialize (v:string) (n:type_term) (e0:expr_term) :=
match e0 with
| expr_ty_app e t => expr_ty_app (expr_specialize v n e) (type_subst v n t)
| expr_ascend t e => expr_ascend (type_subst v n t) (expr_specialize v n e)
| expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e)
| e => e
end.

94
coq/subtype.v
View file

@ -1,94 +0,0 @@
(*
* This module defines the subtype relationship
*
* We distinguish between *representational* subtypes,
* where any high-level type is a subtype of its underlying
* representation type and *convertible* subtypes that
* are compatible at high level, but have a different representation
* that requires a conversion.
*)
From Coq Require Import Strings.String.
Require Import terms.
Require Import equiv.
(** Subtyping *)
Reserved Notation "s ':<=' t" (at level 50).
Reserved Notation "s '~<=' t" (at level 50).
(* Representational Subtype *)
Inductive is_repr_subtype : type_term -> type_term -> Prop :=
| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')
| TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
| TSubRepr_Ladder : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y)
where "s ':<=' t" := (is_repr_subtype s t).
(* Convertible Subtype *)
Inductive is_conv_subtype : type_term -> type_term -> Prop :=
| TSubConv_Refl : forall t t', (t === t') -> (t ~<= t')
| TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z)
| TSubConv_Ladder : forall x' x y, (x ~<= y) -> ((type_ladder x' x) ~<= y)
| TSubConv_Morph : forall x y y', (type_ladder x y) ~<= (type_ladder x y')
where "s '~<=' t" := (is_conv_subtype s t).
(* Every Representational Subtype is a Convertible Subtype *)
Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y).
Proof.
intros.
induction H.
apply TSubConv_Refl.
apply H.
apply TSubConv_Trans with (x:=x) (y:=y) (z:=z).
apply IHis_repr_subtype1.
apply IHis_repr_subtype2.
apply TSubConv_Ladder.
apply IHis_repr_subtype.
Qed.
(* EXAMPLES *)
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Example sub0 :
[<
< $"Seq"$ < $"Digit"$ $"10"$ > >
~ < $"Seq"$ $"Char"$ >
>]
:<=
[<
< $"Seq"$ $"Char"$ >
>]
.
Proof.
apply TSubRepr_Ladder.
apply TSubRepr_Refl.
apply TEq_Refl.
Qed.
Example sub1 :
[< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >]
:<= [< < $"Seq"$ $"Char"$ > >]
.
Proof.
set [< < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > >].
set [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >].
set [< < $"Seq"$ $"Char"$ > >].
set (t0 === t).
set (t :<= t0).
set (t :<= t1).
apply TSubRepr_Trans with t.
apply TSubRepr_Refl.
apply TEq_Distribute.
apply L_DistributeOverSpec2.
apply TSubRepr_Ladder.
apply TSubRepr_Refl.
apply TEq_Refl.
Qed.

0
coq/terms_debruijn.v → coq/terms/debruijn.v
View file

2
coq/equiv_debruijn.v → coq/terms/equiv.v
View file

@ -1,4 +1,4 @@
Require Import terms_debruijn.
Require Import debruijn.
Local Open Scope ladder_type_scope.
Local Open Scope ladder_expr_scope.

10
coq/eval_debruijn.v → coq/terms/eval.v
View file

@ -1,11 +1,11 @@
From Coq Require Import Lists.List.
Import ListNotations.
Require Import Atom.
Require Import terms_debruijn.
Require Import subtype_debruijn.
Require Import context_debruijn.
Require Import morph_debruijn.
Require Import typing_debruijn.
Require Import debruijn.
Require Import subtype.
Require Import context.
Require Import morph.
Require Import typing.
Open Scope ladder_expr_scope.

0
coq/terms.v → coq/terms/named.v
View file

383
coq/typing.v
View file

@ -1,383 +0,0 @@
(* This module defines the typing relation
* where each expression is assigned a type.
*)
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import morph.
(** Typing Derivation *)
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0).
Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ,
context_contains Γ x τ ->
Γ |- [{ %x% }] \is τ
| T_Let : forall Γ s σ t τ x,
Γ |- s \is σ ->
(ctx_assign x σ Γ) |- t \is τ ->
Γ |- [{ let x := s in t }] \is τ
| T_TypeAbs : forall Γ e τ α,
Γ |- e \is τ ->
Γ |- [{ Λ α ↦ e }] \is [< ∀α,τ >]
| T_TypeApp : forall Γ α e σ τ,
Γ |- e \is [< ∀α, τ >] ->
Γ |- [{ e # σ }] \is (type_subst α σ τ)
| T_Abs : forall Γ x σ t τ,
(ctx_assign x σ Γ) |- t \is τ ->
Γ |- [{ λ x , σ ↦ t }] \is [< σ -> τ >]
| T_MorphAbs : forall Γ x σ t τ,
(ctx_assign x σ Γ) |- t \is τ ->
Γ |- [{ λ x , σ ↦morph t }] \is [< σ ->morph τ >]
| T_App : forall Γ f a σ' σ τ,
(Γ |- f \is [< σ -> τ >]) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(Γ |- [{ (f a) }] \is τ)
| T_MorphFun : forall Γ f σ τ,
Γ |- f \is (type_morph σ τ) ->
Γ |- f \is (type_fun σ τ)
| T_Ascend : forall Γ e τ τ',
(Γ |- e \is τ) ->
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >])
| T_DescendImplicit : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
| T_Descend : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- [{ x des τ' }] \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Definition is_well_typed (e:expr_term) : Prop :=
forall Γ,
exists τ,
Γ |- e \is τ
.
Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
| Expand_Var : forall Γ x τ,
(Γ |- (expr_var x) \is τ) ->
(translate_typing Γ [{ %x% }] τ [{ %x% }])
| Expand_Let : forall Γ x e e' t t' σ τ,
(Γ |- e \is σ) ->
((ctx_assign x σ Γ) |- t \is τ) ->
(translate_typing Γ e σ e') ->
(translate_typing (ctx_assign x σ Γ) t τ t') ->
(translate_typing Γ
[{ let x := e in t }]
τ
[{ let x := e' in t' }])
| Expand_TypeAbs : forall Γ α e e' τ,
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ
[{ Λ α ↦ e }]
[< ∀ α,τ >]
[{ Λ α ↦ e' }])
| Expand_TypeApp : forall Γ e e' σ α τ,
(Γ |- e \is (type_univ α τ)) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ
[{ e # σ }]
(type_subst α σ τ)
[{ e' # σ }])
| Expand_Abs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ
[{ λ x , σ ↦ e }]
[< σ -> τ >]
[{ λ x , σ ↦ e' }])
| Expand_MorphAbs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ
[{ λ x , σ ↦morph e }]
[< σ ->morph τ >]
[{ λ x , σ ↦morph e' }])
| Expand_App : forall Γ f f' a a' m σ τ σ',
(Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(translate_typing Γ f [< σ -> τ >] f') ->
(translate_typing Γ a σ' a') ->
(translate_morphism_path Γ σ' σ m) ->
(translate_typing Γ [{ f a }] τ [{ f' (m a') }])
| Expand_MorphFun : forall Γ f f' σ τ,
(Γ |- f \is (type_morph σ τ)) ->
(Γ |- f \is (type_fun σ τ)) ->
(translate_typing Γ f [< σ ->morph τ >] f') ->
(translate_typing Γ f [< σ -> τ >] f')
| Expand_Ascend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ [{ e as τ' }] [< τ' ~ τ >] [{ e' as τ' }])
| Expand_Descend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(τ :<= τ') ->
(Γ |- [{ e des τ' }] \is τ') ->
(translate_typing Γ e τ e') ->
(translate_typing Γ e τ' [{ e' des τ' }])
.
(* Examples *)
Example typing1 :
ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
Proof.
intros.
apply T_TypeAbs.
apply T_Abs.
apply T_Var.
apply C_take.
Qed.
Example typing2 :
ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
Proof.
intros.
apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs.
apply T_Abs.
apply T_Var.
apply C_take.
apply TSubRepr_Refl.
apply TEq_Alpha.
apply TAlpha_Rename.
Qed.
Example typing3 :
ctx_empty |- [{
Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"y"%
}] \is [<
∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
>].
Proof.
intros.
apply T_DescendImplicit with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
apply T_TypeAbs, T_TypeAbs, T_Abs.
apply T_Abs.
apply T_Var.
apply C_take.
apply TSubRepr_Refl.
apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
apply TEq_Alpha.
apply TAlpha_Rename.
apply TEq_Alpha.
apply TAlpha_SubUniv.
apply TAlpha_Rename.
Qed.
Example typing4 : (is_well_typed
[{ Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"x"% }]
).
Proof.
unfold is_well_typed.
exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
apply T_TypeAbs.
apply T_TypeAbs.
apply T_Abs.
apply T_Abs.
apply T_Var.
apply C_shuffle, C_take.
Qed.
Example typing5 :
(ctx_assign "60" [< $"ℝ"$ >]
(ctx_assign "360" [< $"ℝ"$ >]
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
ctx_empty)))
|-
[{
let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
}]
\is
[<
$"Angle"$~$"Turns"$~$"ℝ"$
>]
.
Proof.
apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
apply T_MorphAbs.
apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])).
2: apply TSubRepr_Refl, TEq_LadderAssocLR.
apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
apply T_Var.
apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]).
apply T_Var.
apply C_take.
apply TSubRepr_Ladder. apply TSubRepr_Ladder.
apply TSubRepr_Refl. apply TEq_Refl.
apply M_Sub.
apply TSubRepr_Refl. apply TEq_Refl.
apply T_Var.
apply C_shuffle, C_shuffle, C_take.
apply M_Sub.
apply TSubRepr_Refl.
apply TEq_Refl.
apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
apply T_MorphFun.
apply T_Var.
apply C_take.
apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])).
2: apply TSubRepr_Refl, TEq_LadderAssocLR.
apply T_Ascend.
apply T_Var.
apply C_shuffle. apply C_take.
apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
Qed.
Ltac var_typing := auto using T_Var, C_shuffle, C_take.
Ltac repr_subtype := auto using TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl, TEq_LadderAssocLR.
Example expand1 :
(translate_typing
(ctx_assign "60" [< $"ℝ"$ >]
(ctx_assign "360" [< $"ℝ"$ >]
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
ctx_empty)))
[{
let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in
let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in
( %"sin"% (%"60"% as $"Angle"$~$"Degrees"$) )
}]
[<
$"ℝ"$
>]
[{
let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in
let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in
(%"sin"% (%"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$)))
}])
.
Proof.
apply Expand_Let with (σ:=[< ($"Angle"$~$"Degrees"$)~$"ℝ"$ ->morph ($"Angle"$~$"Turns"$)~$"ℝ"$ >]).
- apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$ ~ $"ℝ"$ >]).
2: {
apply TSubRepr_Refl.
apply TEq_SubMorph.
apply TEq_LadderAssocRL.
apply TEq_LadderAssocRL.
}
apply T_MorphAbs.
apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
2: {
apply TSubRepr_Refl.
apply TEq_LadderAssocLR.
}
apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
var_typing.
var_typing.
apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
repr_subtype.
var_typing.
repr_subtype.
apply id_morphism_path.
var_typing.
apply id_morphism_path.
- apply T_Let with (σ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]).
apply T_Abs.
* apply T_Descend with (τ:=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
2: repr_subtype.
var_typing.
* apply T_App with (σ':=[<($"Angle"$~$"Degrees"$)~$"ℝ"$>]) (σ:=[<($"Angle"$~$"Turns"$)~$"ℝ"$>]) (τ:=[<$"ℝ"$>]).
apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]).
2: {
apply TSubRepr_Refl.
apply TEq_SubFun.
apply TEq_LadderAssocRL.
apply TEq_Refl.
}
var_typing.
apply T_Ascend with (τ':=[<$"Angle"$~$"Degrees"$>]) (τ:=[<$"ℝ"$>]).
var_typing.
apply M_Single with (h:="deg2turns"%string).
var_typing.
- admit.
(*
- apply Expand_MorphAbs.
* apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
2: repr_subtype.
apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]).
apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]).
apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]).
auto using T_Var, C_shuffle, C_take.
apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
2: repr_subtype.
var_typing.
apply id_morphism_path.
var_typing.
apply id_morphism_path.
* apply T_Abs.
apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
2: repr_subtype.
apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]).
apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
var_typing.
apply T_Descend with [<$"Angle"$~$"Degrees"$~$"ℝ"$>].
2: repr_subtype.
var_typing.
apply id_morphism_path.
var_typing.
apply id_morphism_path.
* apply Expand_Ascend.
*)
- admit.
Admitted.

2
coq/context_debruijn.v → coq/typing/context.v
View file

@ -1,4 +1,4 @@
Require Import Atom.
Require Import terms_debruijn.
Require Import debruijn.
Definition context : Type := (list (atom * type_DeBruijn)).

8
coq/morph_debruijn.v → coq/typing/morph.v
View file

@ -1,7 +1,7 @@
Require Import terms_debruijn.
Require Import equiv_debruijn.
Require Import subtype_debruijn.
Require Import context_debruijn.
Require Import debruijn.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import Atom.
Import AtomImpl.
From Coq Require Import Lists.List.

4
coq/subtype_debruijn.v → coq/typing/subtype.v
View file

@ -8,8 +8,8 @@
* that requires a conversion.
*)
Require Import terms_debruijn.
Require Import equiv_debruijn.
Require Import debruijn.
Require Import equiv.
(** Subtyping *)

8
coq/typing_debruijn.v → coq/typing/typing.v
View file

@ -2,10 +2,10 @@ From Coq Require Import Lists.List.
Import ListNotations.
Require Import Metatheory.
Require Import Atom.
Require Import terms_debruijn.
Require Import subtype_debruijn.
Require Import context_debruijn.
Require Import morph_debruijn.
Require Import debruijn.
Require Import subtype.
Require Import context.
Require Import morph.
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.