Compare commits

..

No commits in common. "dbfe0cf4def7f6d26de00631f0cacb737ea868b7" and "633843d9c7faf9014150a10f55174fe136fd1abf" have entirely different histories.

10 changed files with 296 additions and 786 deletions

View file

@ -1,6 +1,5 @@
-R . LadderTypes -R . LadderTypes
terms.v terms.v
terms_debruijn.v
equiv.v equiv.v
subst.v subst.v
subtype.v subtype.v

View file

@ -4,101 +4,77 @@ Require Import terms.
Require Import subst. Require Import subst.
Require Import smallstep. Require Import smallstep.
Include Terms.
Include Subst.
Include Smallstep.
Open Scope ladder_type_scope. Open Scope ladder_type_scope.
Open Scope ladder_expr_scope. Open Scope ladder_expr_scope.
(* let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
Definition bb_zero : expr_term := [{ * α.(α->α)->α->α
(Λ"α"
λ"s",(%"α"% -> %"α"%)
λ"z",(%"α"%)
%"z"%)
as $""$~$"BBNat"$
}].
Definition bb_one : expr_term := [{
(Λ"α"
λ"s",(%"α"% -> %"α"%)
λ"z",(%"α"%)
(%"s"% %"z"%))
as $""$~$"BBNat"$
}].
Definition bb_two : expr_term := [{
(Λ"α"
λ"s",(%"α"% -> %"α"%)
λ"z",(%"α"%)
(%"s"% (%"s"% %"z"%)))
as $""$~$"BBNat"$
}].
Definition bb_succ : expr_term := [{
λ"n",$""$
~$"BBNat"$
~("β",(%"β'"%->%"β"%)->%"β"%->%"β"%)
((Λ"α"
λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%)
λ"z",%"α"%
(%"s"% ((%"n"% # %"α"%) %"s"% %"z"%)))
as $""$~$"BBNat"$)
}].
Example example_reduction :
(expr_app bb_succ bb_one) -->β* bb_two
.
Proof.
apply Multi_Step with (y:=[{
(λ"n",$""$
~$"BBNat"$
~("β",(%"β'"%->%"β"%)->%"β"%->%"β"%)
((Λ"α"
λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%)
λ"z",%"α"%
(%"s"% ((%"n"% # %"α"%) %"s"% %"z"%)))
as $""$~$"BBNat"$))
(Λ"β"
λ"s",(%"β"% -> %"β"%)
λ"z",(%"β"%)
(%"s"% %"z"%))
as $""$~$"BBNat"$
}]).
Admitted.
(*
apply E_Alpha.
apply E_App2.
apply EAlpha_Rename.
apply Multi_Step with (y:=[{
(Λ"α"
λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%)
λ"z",%"α"%
(%"s"% (
(((Λ"β"
λ"s",(%"β"% -> %"β"%)
λ"z",(%"β"%)
(%"s"% %"z"%)) as $""$~$"BBNat"$)
# %"α"%) %"s"% %"z"%)))
as $""$~$"BBNat"$ }]).
apply E_AppLam.
apply Multi_Step with (y:=[{
(Λ"α"
λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%)
λ"z",%"α"%
(%"s"% (
(((Λ"α'"
λ"s",(%"α'"% -> %"α'"%)
λ"z",(%"α'"%)
(%"s"% %"z"%)) as $""$~$"BBNat"$)
# %"α"%) %"s"% %"z"%)))
as $""$~$"BBNat"$ }]).
}].
Qed.
*) *)
Definition bb_zero : expr_term :=
(expr_ty_abs "α"
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_abs "z" (type_var "α")
(expr_var "z")))).
(* let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
*)
Definition bb_one : expr_term :=
(expr_ty_abs "α"
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_abs "z" (type_var "α")
(expr_app (expr_var "s") (expr_var "z"))))).
(* let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
*)
Definition bb_two : expr_term :=
(expr_ty_abs "α"
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_abs "z" (type_var "α")
(expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
Definition bb_succ : expr_term :=
(expr_abs "n" (type_ladder (type_id "")
(type_ladder (type_id "BBNat")
(type_univ "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
(type_fun (type_var "α") (type_var "α"))))))
(expr_ascend (type_ladder (type_id "") (type_id "BBNat"))
(expr_ty_abs "α"
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_abs "z" (type_var "α")
(expr_app (expr_var "s")
(expr_app (expr_app
(expr_ty_app (expr_var "n") (type_var "α"))
(expr_var "s"))
(expr_var "z")))))))).
Definition e1 : expr_term :=
(expr_let "bb-zero" bb_zero
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
).
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
Compute (expr_subst "x"
(expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
bb_one
).
Example example_let_reduction :
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
Proof.
apply E_Let.
Qed.
Compute (expr_app bb_succ bb_zero) -->β bb_one. Compute (expr_app bb_succ bb_zero) -->β bb_one.
Example example_succ :
(expr_app bb_succ bb_zero) -->β bb_one.
Proof.
Admitted.

View file

@ -38,44 +38,46 @@ From Coq Require Import Strings.String.
Reserved Notation "S '--->α' T" (at level 40). Reserved Notation "S '--->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop := Inductive type_conv_alpha : type_term -> type_term -> Prop :=
| TAlpha_Rename : forall x y t, | TAlpha_Rename : forall x y t t',
(type_univ x t) --->α (type_univ y (type_subst x (type_var y) t))
(type_subst1 x (type_var y) t t') ->
(type_univ x t) --->α (type_univ y t')
| TAlpha_SubUniv : forall x τ τ', | TAlpha_SubUniv : forall x τ τ',
(τ --->α τ') -> (τ --->α τ') ->
[< x,τ >] --->α [< x,τ' >] (type_univ x τ) --->α (type_univ x τ')
| TAlpha_SubSpec1 : forall τ1 τ1' τ2, | TAlpha_SubSpec1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') -> (τ1 --->α τ1') ->
[< <τ1 τ2> >] --->α [< <τ1' τ2> >] (type_spec τ1 τ2) --->α (type_spec τ1' τ2)
| TAlpha_SubSpec2 : forall τ1 τ2 τ2', | TAlpha_SubSpec2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') -> (τ2 --->α τ2') ->
[< <τ1 τ2> >] --->α [< <τ1 τ2'> >] (type_spec τ1 τ2) --->α (type_spec τ1 τ2')
| TAlpha_SubFun1 : forall τ1 τ1' τ2, | TAlpha_SubFun1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') -> (τ1 --->α τ1') ->
[< τ1 -> τ2 >] --->α [< τ1' -> τ2 >] (type_fun τ1 τ2) --->α (type_fun τ1' τ2)
| TAlpha_SubFun2 : forall τ1 τ2 τ2', | TAlpha_SubFun2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') -> (τ2 --->α τ2') ->
[< τ1 -> τ2 >] --->α [< τ1 -> τ2' >] (type_fun τ1 τ2) --->α (type_fun τ1 τ2')
| TAlpha_SubMorph1 : forall τ1 τ1' τ2, | TAlpha_SubMorph1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') -> (τ1 --->α τ1') ->
[< τ1 ->morph τ2 >] --->α [< τ1' ->morph τ2 >] (type_morph τ1 τ2) --->α (type_morph τ1' τ2)
| TAlpha_SubMorph2 : forall τ1 τ2 τ2', | TAlpha_SubMorph2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') -> (τ2 --->α τ2') ->
[< τ1 ->morph τ2 >] --->α [< τ1 ->morph τ2' >] (type_morph τ1 τ2) --->α (type_morph τ1 τ2')
| TAlpha_SubLadder1 : forall τ1 τ1' τ2, | TAlpha_SubLadder1 : forall τ1 τ1' τ2,
(τ1 --->α τ1') -> (τ1 --->α τ1') ->
[< τ1 ~ τ2 >] --->α [< τ1' ~ τ2 >] (type_ladder τ1 τ2) --->α (type_ladder τ1' τ2)
| TAlpha_SubLadder2 : forall τ1 τ2 τ2', | TAlpha_SubLadder2 : forall τ1 τ2 τ2',
(τ2 --->α τ2') -> (τ2 --->α τ2') ->
[< τ1 ~ τ2 >] --->α [< τ1 ~ τ2' >] (type_ladder τ1 τ2) --->α (type_ladder τ1 τ2')
where "S '--->α' T" := (type_conv_alpha S T). where "S '--->α' T" := (type_conv_alpha S T).
@ -84,48 +86,38 @@ Lemma type_alpha_symm :
forall σ τ, forall σ τ,
(σ --->α τ) -> (τ --->α σ). (σ --->α τ) -> (τ --->α σ).
Proof. Proof.
intros. (* TODO *)
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. Admitted.
(** Define all rewrite steps $\label{coq:type-dist}$ *) (** Define all rewrite steps $\label{coq:type-dist}$ *)
Reserved Notation "S '-->distribute-ladder' T" (at level 40). Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_term -> type_term -> Prop := Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
| L_DistributeOverSpec1 : forall x x' y, | L_DistributeOverSpec1 : forall x x' y,
[< <x~x' y> >] (type_spec (type_ladder x x') y)
-->distribute-ladder -->distribute-ladder
[< <x y>~<x' y> >] (type_ladder (type_spec x y) (type_spec x' y))
| L_DistributeOverSpec2 : forall x y y', | L_DistributeOverSpec2 : forall x y y',
[< <x y~y'> >] (type_spec x (type_ladder y y'))
-->distribute-ladder -->distribute-ladder
[< <x y>~<x y'> >] (type_ladder (type_spec x y) (type_spec x y'))
| L_DistributeOverFun1 : forall x x' y, | L_DistributeOverFun1 : forall x x' y,
[< (x~x' -> y) >] (type_fun (type_ladder x x') y)
-->distribute-ladder -->distribute-ladder
[< (x -> y) ~ (x' -> y) >] (type_ladder (type_fun x y) (type_fun x' y))
| L_DistributeOverFun2 : forall x y y', | L_DistributeOverFun2 : forall x y y',
[< (x -> y~y') >] (type_fun x (type_ladder y y'))
-->distribute-ladder -->distribute-ladder
[< (x -> y) ~ (x -> y') >] (type_ladder (type_fun x y) (type_fun x y'))
| L_DistributeOverMorph1 : forall x x' y, | L_DistributeOverMorph1 : forall x x' y,
[< (x~x' ->morph y) >] (type_morph (type_ladder x x') y)
-->distribute-ladder -->distribute-ladder
[< (x ->morph y) ~ (x' ->morph y) >] (type_ladder (type_morph x y) (type_morph x' y))
| L_DistributeOverMorph2 : forall x y y', | L_DistributeOverMorph2 : forall x y y',
(type_morph x (type_ladder y y')) (type_morph x (type_ladder y y'))
@ -139,34 +131,34 @@ where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
Reserved Notation "S '-->condense-ladder' T" (at level 40). Reserved Notation "S '-->condense-ladder' T" (at level 40).
Inductive type_condense_ladder : type_term -> type_term -> Prop := Inductive type_condense_ladder : type_term -> type_term -> Prop :=
| L_CondenseOverSpec1 : forall x x' y, | L_CondenseOverSpec1 : forall x x' y,
[< <x y>~<x' y> >] (type_ladder (type_spec x y) (type_spec x' y))
-->condense-ladder -->condense-ladder
[< <x~x' y> >] (type_spec (type_ladder x x') y)
| L_CondenseOverSpec2 : forall x y y', | L_CondenseOverSpec2 : forall x y y',
[< <x y>~<x y'> >] (type_ladder (type_spec x y) (type_spec x y'))
-->condense-ladder -->condense-ladder
[< <x y~y'> >] (type_spec x (type_ladder y y'))
| L_CondenseOverFun1 : forall x x' y, | L_CondenseOverFun1 : forall x x' y,
[< (x -> y) ~ (x' -> y) >] (type_ladder (type_fun x y) (type_fun x' y))
-->condense-ladder -->condense-ladder
[< (x~x') -> y >] (type_fun (type_ladder x x') y)
| L_CondenseOverFun2 : forall x y y', | L_CondenseOverFun2 : forall x y y',
[< (x -> y) ~ (x -> y') >] (type_ladder (type_fun x y) (type_fun x y'))
-->condense-ladder -->condense-ladder
[< (x -> y~y') >] (type_fun x (type_ladder y y'))
| L_CondenseOverMorph1 : forall x x' y, | L_CondenseOverMorph1 : forall x x' y,
[< (x ->morph y) ~ (x' ->morph y) >] (type_ladder (type_morph x y) (type_morph x' y))
-->condense-ladder -->condense-ladder
[< (x~x' ->morph y) >] (type_morph (type_ladder x x') y)
| L_CondenseOverMorph2 : forall x y y', | L_CondenseOverMorph2 : forall x y y',
[< (x ->morph y) ~ (x ->morph y') >] (type_ladder (type_morph x y) (type_morph x y'))
-->condense-ladder -->condense-ladder
[< (x ->morph y~y') >] (type_morph x (type_ladder y y'))
where "S '-->condense-ladder' T" := (type_condense_ladder S T). where "S '-->condense-ladder' T" := (type_condense_ladder S T).
@ -220,25 +212,15 @@ Inductive type_eq : type_term -> type_term -> Prop :=
y === z -> y === z ->
x === 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, | TEq_LadderAssocLR : forall x y z,
[< (x~y)~z >] (type_ladder (type_ladder x y) z)
=== ===
[< x~(y~z) >] (type_ladder x (type_ladder y z))
| TEq_LadderAssocRL : forall x y z, | TEq_LadderAssocRL : forall x y z,
[< x~(y~z) >] (type_ladder x (type_ladder y z))
=== ===
[< (x~y)~z >] (type_ladder (type_ladder x y) z)
| TEq_Alpha : forall x y, | TEq_Alpha : forall x y,
x --->α y -> x --->α y ->
@ -269,11 +251,7 @@ Proof.
apply TEq_Trans with (y:=y). apply TEq_Trans with (y:=y).
apply IHtype_eq2. apply IHtype_eq2.
apply IHtype_eq1. apply IHtype_eq1.
apply TEq_SubFun.
auto. auto.
apply TEq_SubMorph.
auto. auto.
apply TEq_LadderAssocRL. apply TEq_LadderAssocRL.
apply TEq_LadderAssocLR. apply TEq_LadderAssocLR.
@ -400,7 +378,7 @@ Admitted.
*) *)
Example example_flat_type : Example example_flat_type :
type_is_flat [< <$"PosInt"$ $"10"$> >]. (type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
Proof. Proof.
apply FlatApp. apply FlatApp.
apply FlatId. apply FlatId.
@ -408,15 +386,17 @@ Proof.
Qed. Qed.
Example example_lnf_type : Example example_lnf_type :
type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >]. (type_is_lnf
(type_ladder (type_spec (type_id "Seq") (type_id "Char"))
(type_spec (type_id "Seq") (type_id "Byte")))).
Proof. Proof.
Admitted. Admitted.
Example example_type_eq : Example example_type_eq :
[< [$"Char"$ ~ $"Byte"$] >] (type_spec (type_id "Seq") (type_ladder (type_id "Char") (type_id "Byte")))
=== ===
[< [$"Char"$] ~ [$"Byte"$] >] (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
. (type_spec (type_id "Seq") (type_id "Byte"))).
Proof. Proof.
apply TEq_Distribute. apply TEq_Distribute.
apply L_DistributeOverSpec2. apply L_DistributeOverSpec2.

View file

@ -8,15 +8,13 @@ Require Import context.
(* Given a context, there is a morphism path from τ to τ' *) (* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level). 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 := Inductive morphism_path : context -> type_term -> type_term -> Prop :=
| M_Sub : forall Γ τ τ', | M_Sub : forall Γ τ τ',
(τ :<= τ') -> (τ :<= τ') ->
(Γ |- τ ~> τ') (Γ |- τ ~> τ')
| M_Single : forall Γ h τ τ', | M_Single : forall Γ h τ τ',
(context_contains Γ h [< τ ->morph τ' >]) -> (context_contains Γ h (type_morph τ τ')) ->
(Γ |- τ ~> τ') (Γ |- τ ~> τ')
| M_Chain : forall Γ τ τ' τ'', | M_Chain : forall Γ τ τ' τ'',
@ -26,57 +24,58 @@ Inductive morphism_path : context -> type_term -> type_term -> Prop :=
| M_Lift : forall Γ σ τ τ', | M_Lift : forall Γ σ τ τ',
(Γ |- τ ~> τ') -> (Γ |- τ ~> τ') ->
(Γ |- [< σ ~ τ >] ~> [< σ ~ τ' >]) (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
| M_MapSeq : forall Γ τ τ', | M_MapSeq : forall Γ τ τ',
(Γ |- τ ~> τ') -> (Γ |- τ ~> τ') ->
(Γ |- [< [τ] >] ~> [< [τ'] >]) (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
where "Γ '|-' s '~>' t" := (morphism_path Γ s t). 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 := Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
| Translate_Descend : forall Γ τ τ', | Translate_Subtype : forall Γ τ τ',
(τ :<= τ') -> (τ :<= τ') ->
(translate_morphism_path Γ τ τ' (translate_morphism_path Γ τ τ'
(expr_morph "x" τ [{ %"x"% des τ' }])) (expr_morph "x" τ (expr_var "x")))
| Translate_Lift : forall Γ σ τ τ' m, | Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~> τ') -> (Γ |- τ ~> τ') ->
(translate_morphism_path Γ τ τ' m) -> (translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ [< σ ~ τ >] [< σ ~ τ' >] (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
(expr_morph "x" [< σ ~ τ >] [{ (m (%"x"% des τ)) as σ }])) (expr_morph "x" (type_ladder σ τ)
(expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
| Translate_Single : forall Γ h τ τ', | Translate_Single : forall Γ h τ τ',
(context_contains Γ h [< τ ->morph τ' >]) -> (context_contains Γ h (type_morph τ τ')) ->
(translate_morphism_path Γ τ τ' [{ %h% }]) (translate_morphism_path Γ τ τ' (expr_var h))
| Translate_Chain : forall Γ τ τ' τ'' m1 m2, | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(translate_morphism_path Γ τ τ' m1) -> (translate_morphism_path Γ τ τ' m1) ->
(translate_morphism_path Γ τ' τ'' m2) -> (translate_morphism_path Γ τ' τ'' m2) ->
(translate_morphism_path Γ τ τ'' (translate_morphism_path Γ τ τ''
(expr_morph "x" τ [{ m2 (m1 %"x"%) }])) (expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
| Translate_MapSeq : forall Γ τ τ' m, | Translate_MapSeq : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) -> (translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ [< [τ] >] [< [τ'] >] (translate_morphism_path Γ
[{ (type_spec (type_id "Seq") τ)
λ"xs",[τ] morph (%"map"% # τ # τ' m %"xs"%) (type_spec (type_id "Seq") τ')
}]) (expr_morph "xs"
(type_spec (type_id "Seq") τ)
(expr_app (expr_app (expr_ty_app (expr_ty_app
(expr_var "map") τ) τ') m)
(expr_var "xs"))))
. .
Example morphism_paths : Example morphism_paths :
(ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$""$ ->morph $"Angle"$~$"Turns"$~$""$ >] (ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$""$ ->morph $"Angle"$~$"Turns"$~$""$ >]
(ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$""$ ->morph $"Angle"$~$"Radians"$~$""$ >] (ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$""$ ->morph $"Angle"$~$"Radians"$~$""$ >]
ctx_empty)) ctx_empty))
|- [< [ $"Hue"$~$"Angle"$~$"Degrees"$~$""$ ] >] |- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$""$> >]
~> [< [ $"Hue"$~$"Angle"$~$"Radians"$~$""$ ] >] ~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$""$> >]
. .
Proof. Proof.
intros. intros.

View file

@ -16,19 +16,19 @@ Inductive expr_alpha : expr_term -> expr_term -> Prop :=
| EAlpha_SubAbs : forall x τ e e', | EAlpha_SubAbs : forall x τ e e',
(e -->α e') -> (e -->α e') ->
[{ λ x , τ e }] -->α [{ λ x , τ e' }] (expr_abs x τ e) -->α (expr_abs x τ e')
| EAlpha_SubTyAbs : forall α e e', | EAlpha_SubTyAbs : forall α e e',
(e -->α e') -> (e -->α e') ->
[{ Λ α e }] -->α [{ Λ α e' }] (expr_ty_abs α e) -->α (expr_ty_abs α e')
| EAlpha_SubApp1 : forall e1 e1' e2, | EAlpha_SubApp1 : forall e1 e1' e2,
(e1 -->α e1') -> (e1 -->α e1') ->
[{ e1 e2 }] -->α [{ e1' e2 }] (expr_app e1 e2) -->α (expr_app e1' e2)
| EAlpha_SubApp2 : forall e1 e2 e2', | EAlpha_SubApp2 : forall e1 e2 e2',
(e2 -->α e2') -> (e2 -->α e2') ->
[{ e1 e2 }] -->α [{ e1 e2' }] (expr_app e1 e2) -->α (expr_app e1 e2')
where "s '-->α' t" := (expr_alpha s t). where "s '-->α' t" := (expr_alpha s t).
@ -45,45 +45,45 @@ Qed.
Inductive beta_step : expr_term -> expr_term -> Prop := Inductive beta_step : expr_term -> expr_term -> Prop :=
| E_App1 : forall e1 e1' e2, | E_App1 : forall e1 e1' e2,
e1 -->β e1' -> e1 -->β e1' ->
[{ e1 e2 }] -->β [{ e1' e2 }] (expr_app e1 e2) -->β (expr_app e1' e2)
| E_App2 : forall v1 e2 e2', | E_App2 : forall v1 e2 e2',
(is_value v1) -> (is_value v1) ->
e2 -->β e2' -> e2 -->β e2' ->
[{ v1 e2 }] -->β [{ v1 e2' }] (expr_app v1 e2) -->β (expr_app v1 e2')
| E_TypApp : forall e e' τ, | E_TypApp : forall e e' τ,
e -->β e' -> e -->β e' ->
[{ Λ τ e }] -->β [{ Λ τ e' }] (expr_ty_app e τ) -->β (expr_ty_app e' τ)
| E_TypAppLam : forall α e τ, | E_TypAppLam : forall α e τ,
[{ (Λ α e) # τ }] -->β (expr_specialize α τ e) (expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
| E_AppLam : forall x τ e a, | E_AppLam : forall x τ e a,
[{ (λ x , τ e) a }] -->β (expr_subst x a e) (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
| E_AppMorph : forall x τ e a, | E_AppMorph : forall x τ e a,
[{ (λ x , τ morph e) a }] -->β (expr_subst x a e) (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
| E_Let : forall x e a, | E_Let : forall x e a,
[{ let x := a in e }] -->β (expr_subst x a e) (expr_let x a e) -->β (expr_subst x a e)
| E_StripAscend : forall τ e, | E_StripAscend : forall τ e,
[{ e as τ }] -->β e (expr_ascend τ e) -->β e
| E_StripDescend : forall τ e, | E_StripDescend : forall τ e,
[{ e des τ }] -->β e (expr_descend τ e) -->β e
| E_Ascend : forall τ e e', | E_Ascend : forall τ e e',
(e -->β e') -> (e -->β e') ->
[{ e as τ }] -->β [{ e' as τ }] (expr_ascend τ e) -->β (expr_ascend τ e')
| E_AscendCollapse : forall τ' τ e, | E_AscendCollapse : forall τ' τ e,
[{ (e as τ) as τ' }] -->β [{ e as (τ'~τ) }] (expr_ascend τ' (expr_ascend τ e)) -->β (expr_ascend (type_ladder τ' τ) e)
| E_DescendCollapse : forall τ' τ e, | E_DescendCollapse : forall τ' τ e,
(τ':<=τ) -> (τ':<=τ) ->
[{ (e des τ') des τ }] -->β [{ e des τ }] (expr_descend τ (expr_descend τ' e)) -->β (expr_descend τ e)
where "s '-->β' t" := (beta_step s t). where "s '-->β' t" := (beta_step s t).
@ -102,7 +102,7 @@ Notation " s -->β* t " := (multi beta_step s t) (at level 40).
Example reduce1 : Example reduce1 :
[{ [{
let "deg2turns" := let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$""$ (λ"x" $"Angle"$~$"Degrees"$~$""$
morph ((%"/"% (%"x"% des $""$) %"360"%) as $"Angle"$~$"Turns"$)) morph ((%"/"% (%"x"% des $""$) %"360"%) as $"Angle"$~$"Turns"$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) ) in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
}] }]
@ -111,7 +111,7 @@ Example reduce1 :
((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$ ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
}]. }].
Proof. Proof.
apply Multi_Step with (y:=[{ (λ"x",$"Angle"$~$"Degrees"$~$""$ apply Multi_Step with (y:=[{ (λ"x" $"Angle"$~$"Degrees"$~$""$
morph (((%"/"% (%"x"% des $""$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]). morph (((%"/"% (%"x"% des $""$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
apply E_Let. apply E_Let.

View file

@ -8,6 +8,7 @@ Require Import morph.
Require Import smallstep. Require Import smallstep.
Require Import typing. Require Import typing.
Lemma typing_weakening : forall Γ e τ x σ, Lemma typing_weakening : forall Γ e τ x σ,
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
((ctx_assign x σ Γ) |- e \is τ) ((ctx_assign x σ Γ) |- e \is τ)
@ -16,22 +17,17 @@ Proof.
intros. intros.
induction H. induction H.
- apply T_Var. apply T_Var.
apply C_shuffle. apply C_shuffle.
apply H. apply H.
- apply T_Let with (σ:=σ0). apply T_Let with (σ:=σ0).
apply IHexpr_type1. apply IHexpr_type1.
admit.
admit.
Admitted.
Lemma map_type : forall Γ,
Γ |- [{ %"map"% }] \is [<
"σ","τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%]
>].
Proof.
Admitted. Admitted.
Lemma morphism_path_solves_type : forall Γ τ τ' m, Lemma morphism_path_solves_type : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) -> (translate_morphism_path Γ τ τ' m) ->
Γ |- m \is (type_morph τ τ') Γ |- m \is (type_morph τ τ')
@ -42,7 +38,7 @@ Proof.
(* Sub *) (* Sub *)
apply T_MorphAbs. apply T_MorphAbs.
apply T_Descend with (τ:=τ). apply T_DescendImplicit with (τ:=τ).
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply H. apply H.
@ -58,7 +54,7 @@ Proof.
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl. apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
apply id_morphism_path. apply M_Sub, TSubRepr_Refl, TEq_Refl.
(* Single *) (* Single *)
apply T_Var. apply T_Var.
@ -70,7 +66,7 @@ Proof.
apply T_MorphFun. apply T_MorphFun.
apply typing_weakening. apply typing_weakening.
apply IHtranslate_morphism_path2. apply IHtranslate_morphism_path2.
apply T_App with (σ':=τ) (σ:=τ) (τ:=τ'). apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
apply T_MorphFun. apply T_MorphFun.
apply typing_weakening. apply typing_weakening.
@ -78,30 +74,15 @@ Proof.
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply id_morphism_path. apply M_Sub, TSubRepr_Refl, TEq_Refl.
apply id_morphism_path. apply M_Sub, TSubRepr_Refl, TEq_Refl.
(* Map Sequence *) (* Map Sequence *)
apply T_MorphAbs. apply T_MorphAbs.
apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)). apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')). apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
set (k:=[< (%"σ"% -> %"τ"%) -> <$"Seq"$ %"σ"%> -> <$"Seq"$ %"τ"%> >]).
set (k1:=[< (τ -> %"τ"%) -> <$"Seq"$ τ> -> <$"Seq"$ %"τ"%> >]).
set (k2:=[< (τ -> τ') -> <$"Seq"$ τ> -> <$"Seq"$ τ'> >]).
set (P:=(type_subst "τ" τ' k1) = k2).
(* apply T_TypeApp with (α:="τ"%string) (τ:=k2).*)
(* apply T_TypeApp with (α:="τ"%string) (τ:=(type_subst "τ" τ' k1)).*)
(*
apply map_type.
apply TSubst_UnivReplace.
admit. admit.
admit.
apply TSubst_UnivReplace.
apply T_MorphFun. apply T_MorphFun.
apply typing_weakening. apply typing_weakening.
@ -111,7 +92,6 @@ Proof.
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply M_Sub, TSubRepr_Refl, TEq_Refl. apply M_Sub, TSubRepr_Refl, TEq_Refl.
*)
Admitted. Admitted.
(* reduction step preserves well-typedness *) (* reduction step preserves well-typedness *)
@ -206,7 +186,7 @@ Proof.
apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ'). apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
apply T_MorphFun. apply T_MorphFun.
apply T_MorphAbs. apply T_MorphAbs.
apply T_Descend with (τ:=τ0). apply T_DescendImplicit with (τ:=τ0).
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply H3. apply H3.
@ -324,7 +304,7 @@ Proof.
apply H0. apply H0.
(* e is Desecension *) (* e is Desecension *)
apply T_Descend with (τ:=τ). apply T_DescendImplicit with (τ:=τ).
apply IHtranslate_typing. apply IHtranslate_typing.
apply H0. apply H0.
apply H1. apply H1.

View file

@ -1,34 +1,60 @@
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import terms. Require Import terms.
(* Type Variable "x" is a free variable in type *)
Inductive type_var_free (x:string) : type_term -> Prop :=
| TFree_Var :
(type_var_free x (type_var x))
| TFree_Ladder : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_ladder τ1 τ2))
| TFree_Fun : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_fun τ1 τ2))
| TFree_Morph : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_morph τ1 τ2))
| TFree_Spec : forall τ1 τ2,
(type_var_free x τ1) ->
(type_var_free x τ2) ->
(type_var_free x (type_spec τ1 τ2))
| TFree_Univ : forall y τ,
~(y = x) ->
(type_var_free x τ) ->
(type_var_free x (type_univ y τ))
.
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. Open Scope ladder_type_scope.
Example ex_type_fv1 : Example ex_type_free_var1 :
(In "T"%string (type_fv [< "U",%"T"% >])) (type_var_free "T" (type_univ "U" (type_var "T")))
. .
Proof. simpl. left. auto. Qed. Proof.
apply TFree_Univ.
easy.
apply TFree_Var.
Qed.
Open Scope ladder_type_scope. Open Scope ladder_type_scope.
Example ex_type_fv2 : Example ex_type_free_var2 :
~(In "T"%string (type_fv [< "T",%"T"% >])) ~(type_var_free "T" (type_univ "T" (type_var "T")))
. .
Proof. simpl. auto. Qed. Proof.
intro H.
inversion H.
contradiction.
Qed.
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *) (* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : type_term := Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
match t0 with match t0 with
| type_var name => if (eqb v name) then n else t0 | 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_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
@ -38,14 +64,12 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : type_term :=
| t => t | t => t
end. end.
(*
Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop := Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop :=
| TSubst_VarReplace : | TSubst_VarReplace :
(type_subst1 x σ (type_var x) σ) (type_subst1 x σ (type_var x) σ)
| TSubst_VarKeep : forall y, | TSubst_VarKeep : forall y,
(x <> y) -> ~(x = y) ->
(type_subst1 x σ (type_var y) (type_var y)) (type_subst1 x σ (type_var y) (type_var y))
| TSubst_UnivReplace : forall y τ τ', | TSubst_UnivReplace : forall y τ τ',
@ -77,56 +101,6 @@ Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop
(type_subst1 x σ τ2 τ2') -> (type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ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 *) (* scoped variable substitution, replaces free occurences of v with n in expression e *)
Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) := Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=

View file

@ -64,66 +64,58 @@ Declare Custom Entry ladder_type.
Declare Custom Entry ladder_expr. Declare Custom Entry ladder_expr.
Notation "[< t >]" := t Notation "[< t >]" := t
(t custom ladder_type at level 99) : ladder_type_scope. (t custom ladder_type at level 80) : ladder_type_scope.
Notation "t" := t Notation "t" := t
(in custom ladder_type at level 0, t ident) : ladder_type_scope. (in custom ladder_type at level 0, t ident) : ladder_type_scope.
Notation "'∀' x ',' t" := (type_univ x t) Notation "'∀' x ',' t" := (type_univ x t)
(t custom ladder_type at level 80, in custom ladder_type at level 80, x constr). (t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
Notation "'<' σ τ '>'" := (type_spec σ τ) Notation "'<' σ τ '>'" := (type_spec σ τ)
(in custom ladder_type at level 80, left associativity) : ladder_type_scope. (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
Notation "'[' τ ']'" := (type_spec (type_id "Seq") τ)
(in custom ladder_type at level 70) : ladder_type_scope.
Notation "'(' τ ')'" := τ Notation "'(' τ ')'" := τ
(in custom ladder_type at level 5) : ladder_type_scope. (in custom ladder_type at level 70) : ladder_type_scope.
Notation "σ '->' τ" := (type_fun σ τ) Notation "σ '->' τ" := (type_fun σ τ)
(in custom ladder_type at level 75, right associativity) : ladder_type_scope. (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '->morph' τ" := (type_morph σ τ) Notation "σ '->morph' τ" := (type_morph σ τ)
(in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope. (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
Notation "σ '~' τ" := (type_ladder σ τ) Notation "σ '~' τ" := (type_ladder σ τ)
(in custom ladder_type at level 20, right associativity) : ladder_type_scope. (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
Notation "'$' x '$'" := (type_id x%string) Notation "'$' x '$'" := (type_id x%string)
(in custom ladder_type at level 10, x constr) : ladder_type_scope. (in custom ladder_type at level 0, x constr) : ladder_type_scope.
Notation "'%' x '%'" := (type_var x%string) Notation "'%' x '%'" := (type_var x%string)
(in custom ladder_type at level 10, x constr) : ladder_type_scope. (in custom ladder_type at level 0, x constr) : ladder_type_scope.
Notation "[{ e }]" := e Notation "[{ e }]" := e
(e custom ladder_expr at level 99) : ladder_expr_scope. (e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "e" := e Notation "e" := e
(in custom ladder_expr at level 0, e ident) : ladder_expr_scope. (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
Notation "'%' x '%'" := (expr_var x%string) Notation "'%' x '%'" := (expr_var x%string)
(in custom ladder_expr at level 10, x constr) : ladder_expr_scope. (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
Notation "'Λ' t '↦' e" := (expr_ty_abs t e) Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
(in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope. (in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'λ' x ',' τ '↦' e" := (expr_abs x τ e) Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
(in custom ladder_expr at level 70, x constr, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope. (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'λ' x ',' τ '↦morph' e" := (expr_morph x τ e) Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
(in custom ladder_expr at level 70, x constr, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope. (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'let' x ':=' e 'in' t" := (expr_let x e t) Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
(in custom ladder_expr at level 60, x constr, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope. (in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
Notation "e 'as' τ" := (expr_ascend τ e) Notation "e 'as' τ" := (expr_ascend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope. (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e 'des' τ" := (expr_descend τ e) Notation "e 'des' τ" := (expr_descend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope. (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e1 e2" := (expr_app e1 e2) Notation "e1 e2" := (expr_app e1 e2)
(in custom ladder_expr at level 90, e2 custom ladder_expr at next level) : ladder_expr_scope. (in custom ladder_expr at level 50) : ladder_expr_scope.
Notation "e '#' τ" := (expr_ty_app e τ)
(in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
Notation "'(' e ')'" := e Notation "'(' e ')'" := e
(in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope. (in custom ladder_expr at level 0) : ladder_expr_scope.
Print Grammar constr.
(* EXAMPLES *) (* EXAMPLES *)
Open Scope ladder_type_scope. Open Scope ladder_type_scope.
Open Scope ladder_expr_scope. Open Scope ladder_expr_scope.
Check [< "α", [%"α"%] ~ <$"List"$ %"α"%> >]. Check [< "α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" λ"x"%"T"% (%"x"%) }].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" λ"x",%"T"% (%"x"%) }]. Definition polymorphic_identity2 : expr_term := [{ Λ"T" λ"y"%"T"% %"y"% }].
Definition polymorphic_identity2 : expr_term := [{ Λ"T" λ"y",%"T"% %"y"% }].
Compute polymorphic_identity1. Compute polymorphic_identity1.

View file

@ -1,281 +0,0 @@
From Coq Require Import Strings.String.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import terms.
Inductive type_DeBruijn : Type :=
| ty_id : string -> type_DeBruijn
| ty_fvar : string -> type_DeBruijn
| ty_bvar : nat -> type_DeBruijn
| ty_univ : type_DeBruijn -> type_DeBruijn
| ty_spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
| ty_func : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
| ty_morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
| ty_ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
.
Inductive expr_DeBruijn : Type :=
| ex_var : nat -> expr_DeBruijn
| ex_ty_abs : expr_DeBruijn -> expr_DeBruijn
| ex_ty_app : expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn
| ex_abs : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| varlet : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
.
(* get the list of all free variables in a type term *)
Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : (list string) :=
match τ with
| ty_id s => []
| ty_fvar α => [α]
| ty_bvar x => []
| ty_univ τ => (type_fv τ)
| ty_spec σ τ => (type_fv σ) ++ (type_fv τ)
| ty_func σ τ => (type_fv σ) ++ (type_fv τ)
| ty_morph σ τ => (type_fv σ) ++ (type_fv τ)
| ty_ladder σ τ => (type_fv σ) ++ (type_fv τ)
end.
(* substitute free variable x with type σ in τ *)
Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
match τ with
| ty_id s => ty_id s
| ty_fvar s => if eqb x s then σ else τ
| ty_bvar y => ty_bvar y
| ty_univ τ => ty_univ (subst_type x σ τ)
| ty_spec τ1 τ2 => ty_spec (subst_type x σ τ1) (subst_type x σ τ2)
| ty_func τ1 τ2 => ty_func (subst_type x σ τ1) (subst_type x σ τ2)
| ty_morph τ1 τ2 => ty_morph (subst_type x σ τ1) (subst_type x σ τ2)
| ty_ladder τ1 τ2 => ty_ladder (subst_type x σ τ1) (subst_type x σ τ2)
end.
(* replace a free variable with a new (dangling) bound variable *)
Fixpoint type_bind_fvar (x:string) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
match τ with
| ty_id s => ty_id s
| ty_fvar s => if eqb x s then ty_bvar n else τ
| ty_bvar n => ty_bvar n
| ty_univ τ1 => ty_univ (type_bind_fvar x (S n) τ1)
| ty_spec τ1 τ2 => ty_spec (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
| ty_func τ1 τ2 => ty_func (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
| ty_morph τ1 τ2 => ty_morph (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
| ty_ladder τ1 τ2 => ty_ladder (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
end.
(* replace (dangling) index with another type *)
Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
match τ with
| ty_id s => ty_id s
| ty_fvar s => ty_fvar s
| ty_bvar i => if Nat.eqb k i then σ else τ
| ty_univ τ1 => ty_univ (type_open_rec (S k) σ τ1)
| ty_spec τ1 τ2 => ty_spec (type_open_rec k σ τ1) (type_open_rec k σ τ2)
| ty_func τ1 τ2 => ty_func (type_open_rec k σ τ1) (type_open_rec k σ τ2)
| ty_morph τ1 τ2 => ty_morph (type_open_rec k σ τ1) (type_open_rec k σ τ2)
| ty_ladder τ1 τ2 => ty_ladder (type_open_rec k σ τ1) (type_open_rec k σ τ2)
end.
Notation "'[' z '~>' u ']' e" := (subst_type z u e) (at level 68).
Notation "'{' k '~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
Definition type_open σ τ := type_open_rec 0 σ τ.
(* is the type locally closed ? *)
Inductive type_lc : type_DeBruijn -> Prop :=
| Tlc_Id : forall s, type_lc (ty_id s)
| Tlc_Var : forall s, type_lc (ty_fvar s)
| Tlc_Univ : forall τ1 L,
(forall x, ~ (In x L) -> type_lc (type_open (ty_fvar x) τ1)) ->
type_lc (ty_univ τ1)
| Tlc_Spec : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_spec τ1 τ2)
| Tlc_Func : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_func τ1 τ2)
| Tlc_Morph : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_morph τ1 τ2)
| Tlc_Ladder : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_ladder τ1 τ2)
.
(* number of abstractions *)
Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
match τ with
| ty_id s => 0
| ty_fvar s => 0
| ty_bvar x => 0
| ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
| ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
| ty_univ t => (1 + (type_debruijn_depth t))
| ty_spec s t => ((type_debruijn_depth s) - 1)
| ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
end.
Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
match τ with
| type_id s => ty_id s
| type_var s => ty_fvar s
| type_univ x t => let t':=(type_named2debruijn t) in (ty_univ (type_bind_fvar x 0 t'))
| type_spec s t => ty_spec (type_named2debruijn s) (type_named2debruijn t)
| type_fun s t => ty_func (type_named2debruijn s) (type_named2debruijn t)
| type_morph s t => ty_morph (type_named2debruijn s) (type_named2debruijn t)
| type_ladder s t => ty_ladder (type_named2debruijn s) (type_named2debruijn t)
end.
Coercion type_named2debruijn : type_term >-> type_DeBruijn.
Lemma list_in_tail : forall x (E:list string) f,
In x E ->
In x (cons f E).
Proof.
intros.
simpl.
right.
apply H.
Qed.
Lemma list_in_concatA : forall x (E:list string) (F:list string),
In x E ->
In x (E ++ F).
Proof.
Admitted.
Lemma list_in_concatB : forall x (E:list string) (F:list string),
In x F ->
In x (E ++ F).
Proof.
intros.
induction E.
auto.
apply list_in_tail.
Admitted.
Lemma list_notin_singleton : forall (x:string) (y:string),
((eqb x y) = false) -> ~ In x [ y ].
Proof.
Admitted.
Lemma list_elim_notin_singleton : forall (x:string) (y:string),
~ In x [y] -> ((eqb x y) = false).
Proof.
Admitted.
Lemma subst_fresh_type : forall (x : string) (τ:type_DeBruijn) (σ:type_DeBruijn),
~(In x (type_fv τ)) ->
(subst_type x σ τ) = τ
.
Proof.
intros.
induction τ.
- reflexivity.
- unfold type_fv in H.
apply list_elim_notin_singleton in H.
simpl.
case_eq (x =? s)%string.
congruence.
reflexivity.
- reflexivity.
- simpl. rewrite IHτ.
reflexivity.
apply H.
- simpl. rewrite IHτ1, IHτ2.
reflexivity.
simpl type_fv in H.
contradict H. apply list_in_concatB, H.
contradict H. apply list_in_concatA, H.
- simpl. rewrite IHτ1, IHτ2.
reflexivity.
contradict H. apply list_in_concatB, H.
contradict H. apply list_in_concatA, H.
- simpl. rewrite IHτ1, IHτ2.
reflexivity.
contradict H. apply list_in_concatB, H.
contradict H. apply list_in_concatA, H.
- simpl. rewrite IHτ1, IHτ2.
reflexivity.
contradict H. apply list_in_concatB, H.
contradict H. apply list_in_concatA, H.
Qed.
Lemma open_rec_lc_core : forall τ j σ1 i σ2,
i <> j ->
{j ~> σ1} τ = {i ~> σ2} ({j ~> σ1} τ) ->
τ = {i ~> σ1} τ.
Proof with (eauto with *).
induction τ;
intros j v i u Neq H;
simpl in *; try solve [inversion H; f_equal; eauto].
(* case (ty_bvar).*)
destruct (Nat.eqb j n)...
destruct (Nat.eqb i n)...
Admitted.
Lemma type_open_rec_lc : forall k σ τ,
type_lc τ ->
{ k ~> σ } τ = τ.
Proof.
intros.
generalize dependent k.
induction H.
- auto.
- auto.
- intro k.
unfold type_open in *.
(*
pick fresh x for L.
apply open_rec_lc_core with (i := S k) (j := 0) (u := u) (v := x). auto. auto.
*)
admit.
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
Admitted.
Lemma type_subst_open_rec : forall τ1 τ2 σ x k,
type_lc σ ->
[x ~> σ] ({k ~> τ2} τ1) = {k ~> [x ~> σ] τ2} ([x ~> σ] τ1).
Proof.
intros.
induction τ1.
(* id *)
- auto.
(* free var *)
- simpl.
case_eq (eqb x s).
intro.
apply eq_sym.
apply type_open_rec_lc, H.
auto.
(* bound var *)
- simpl.
case_eq (Nat.eqb k n).
auto.
auto.
(* univ *)
- simpl.
admit.
- simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
- simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
- simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
- simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
Admitted.

View file

@ -11,42 +11,40 @@ Require Import morph.
(** Typing Derivation *) (** 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). 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 := Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ, | T_Var : forall Γ x τ,
context_contains Γ x τ -> (context_contains Γ x τ) ->
Γ |- [{ %x% }] \is τ (Γ |- (expr_var x) \is τ)
| T_Let : forall Γ s σ t τ x, | T_Let : forall Γ s σ t τ x,
Γ |- s \is σ -> (Γ |- s \is σ) ->
(ctx_assign x σ Γ) |- t \is τ -> ((ctx_assign x σ Γ) |- t \is τ) ->
Γ |- [{ let x := s in t }] \is τ (Γ |- (expr_let x s t) \is τ)
| T_TypeAbs : forall Γ e τ α, | T_TypeAbs : forall Γ e τ α,
Γ |- e \is τ -> Γ |- e \is τ ->
Γ |- [{ Λ α e }] \is [< α,τ >] Γ |- (expr_ty_abs α e) \is (type_univ α τ)
| T_TypeApp : forall Γ α e σ τ, | T_TypeApp : forall Γ α e σ τ τ',
Γ |- e \is [< α, τ >] -> Γ |- e \is (type_univ α τ) ->
Γ |- [{ e # σ }] \is (type_subst α σ τ) (type_subst1 α σ τ τ') ->
Γ |- (expr_ty_app e σ) \is τ'
| T_Abs : forall Γ x σ t τ, | T_Abs : forall Γ x σ t τ,
(ctx_assign x σ Γ) |- t \is τ -> ((ctx_assign x σ Γ) |- t \is τ) ->
Γ |- [{ λ x , σ t }] \is [< σ -> τ >] (Γ |- (expr_abs x σ t) \is (type_fun σ τ))
| T_MorphAbs : forall Γ x σ t τ, | T_MorphAbs : forall Γ x σ e τ,
(ctx_assign x σ Γ) |- t \is τ -> ((ctx_assign x σ Γ) |- e \is τ) ->
Γ |- [{ λ x , σ morph t }] \is [< σ ->morph τ >] Γ |- (expr_morph x σ e) \is (type_morph σ τ)
| T_App : forall Γ f a σ' σ τ, | T_App : forall Γ f a σ' σ τ,
(Γ |- f \is [< σ -> τ >]) -> (Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') -> (Γ |- a \is σ') ->
(Γ |- σ' ~> σ) -> (Γ |- σ' ~> σ) ->
(Γ |- [{ (f a) }] \is τ) (Γ |- (expr_app f a) \is τ)
| T_MorphFun : forall Γ f σ τ, | T_MorphFun : forall Γ f σ τ,
Γ |- f \is (type_morph σ τ) -> Γ |- f \is (type_morph σ τ) ->
@ -54,7 +52,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Ascend : forall Γ e τ τ', | T_Ascend : forall Γ e τ τ',
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
| T_DescendImplicit : forall Γ x τ τ', | T_DescendImplicit : forall Γ x τ τ',
Γ |- x \is τ -> Γ |- x \is τ ->
@ -64,7 +62,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Descend : forall Γ x τ τ', | T_Descend : forall Γ x τ τ',
Γ |- x \is τ -> Γ |- x \is τ ->
(τ :<= τ') -> (τ :<= τ') ->
Γ |- [{ x des τ' }] \is τ' Γ |- (expr_descend τ' x) \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ). where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
@ -77,85 +75,73 @@ Definition is_well_typed (e:expr_term) : Prop :=
Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop := Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
| Expand_Var : forall Γ x τ, | Expand_Var : forall Γ x τ,
(Γ |- (expr_var x) \is τ) -> (Γ |- (expr_var x) \is τ) ->
(translate_typing Γ [{ %x% }] τ [{ %x% }]) (translate_typing Γ (expr_var x) τ (expr_var x))
| Expand_Let : forall Γ x e e' t t' σ τ, | Expand_Let : forall Γ x e e' t t' σ τ,
(Γ |- e \is σ) -> (Γ |- e \is σ) ->
((ctx_assign x σ Γ) |- t \is τ) -> ((ctx_assign x σ Γ) |- t \is τ) ->
(translate_typing Γ e σ e') -> (translate_typing Γ e σ e') ->
(translate_typing (ctx_assign x σ Γ) t τ t') -> (translate_typing (ctx_assign x σ Γ) t τ t') ->
(translate_typing Γ (translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
[{ let x := e in t }]
τ
[{ let x := e' in t' }])
| Expand_TypeAbs : forall Γ α e e' τ, | Expand_TypeAbs : forall Γ α e e' τ,
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
(translate_typing Γ e τ e') -> (translate_typing Γ e τ e') ->
(translate_typing Γ (translate_typing Γ
[{ Λ α e }] (expr_ty_abs α e)
[< α,τ >] (type_univ α τ)
[{ Λ α e' }]) (expr_ty_abs α e'))
| Expand_TypeApp : forall Γ e e' σ α τ, | Expand_TypeApp : forall Γ e e' σ α τ,
(Γ |- e \is (type_univ α τ)) -> (Γ |- e \is (type_univ α τ)) ->
(translate_typing Γ e τ e') -> (translate_typing Γ e τ e') ->
(translate_typing Γ (translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
[{ e # τ }]
(type_subst α σ τ)
[{ e' # τ }])
| Expand_Abs : forall Γ x σ e e' τ, | Expand_Abs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) -> ((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) -> (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') -> (translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
[{ λ x , σ e }]
[< σ -> τ >]
[{ λ x , σ e' }])
| Expand_MorphAbs : forall Γ x σ e e' τ, | Expand_MorphAbs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) -> ((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) -> (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') -> (translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
[{ λ x , σ morph e }]
[< σ ->morph τ >]
[{ λ x , σ morph e' }])
| Expand_App : forall Γ f f' a a' m σ τ σ', | Expand_App : forall Γ f f' a a' m σ τ σ',
(Γ |- f \is (type_fun σ τ)) -> (Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') -> (Γ |- a \is σ') ->
(Γ |- σ' ~> σ) -> (Γ |- σ' ~> σ) ->
(translate_typing Γ f [< σ -> τ >] f') -> (translate_typing Γ f (type_fun σ τ) f') ->
(translate_typing Γ a σ' a') -> (translate_typing Γ a σ' a') ->
(translate_morphism_path Γ σ' σ m) -> (translate_morphism_path Γ σ' σ m) ->
(translate_typing Γ [{ f a }] τ [{ f' (m a') }]) (translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))
| Expand_MorphFun : forall Γ f f' σ τ, | Expand_MorphFun : forall Γ f f' σ τ,
(Γ |- f \is (type_morph σ τ)) -> (Γ |- f \is (type_morph σ τ)) ->
(Γ |- f \is (type_fun σ τ)) -> (Γ |- f \is (type_fun σ τ)) ->
(translate_typing Γ f [< σ ->morph τ >] f') -> (translate_typing Γ f (type_morph σ τ) f') ->
(translate_typing Γ f [< σ -> τ >] f') (translate_typing Γ f (type_fun σ τ) f')
| Expand_Ascend : forall Γ e e' τ τ', | Expand_Ascend : forall Γ e e' τ τ',
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) -> (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
(translate_typing Γ e τ e') -> (translate_typing Γ e τ e') ->
(translate_typing Γ [{ e as τ' }] [< τ' ~ τ >] [{ e' as τ' }]) (translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
| Expand_Descend : forall Γ e e' τ τ', | Expand_Descend : forall Γ e e' τ τ',
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
(τ :<= τ') -> (τ :<= τ') ->
(Γ |- [{ e des τ' }] \is τ') -> (Γ |- e \is τ') ->
(translate_typing Γ e τ e') -> (translate_typing Γ e τ e') ->
(translate_typing Γ e τ' [{ e' des τ' }]) (translate_typing Γ e τ' e')
. .
(* Examples *) (* Examples *)
Example typing1 : Example typing1 :
ctx_empty |- [{ Λ"T" λ "x",%"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >]. ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
Proof. Proof.
intros. intros.
apply T_TypeAbs. apply T_TypeAbs.
@ -165,7 +151,7 @@ Proof.
Qed. Qed.
Example typing2 : Example typing2 :
ctx_empty |- [{ Λ"T" λ "x",%"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >]. ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
Proof. Proof.
intros. intros.
apply T_DescendImplicit with (τ:=[< "T",(%"T"% -> %"T"%) >]). apply T_DescendImplicit with (τ:=[< "T",(%"T"% -> %"T"%) >]).
@ -177,11 +163,14 @@ Proof.
apply TSubRepr_Refl. apply TSubRepr_Refl.
apply TEq_Alpha. apply TEq_Alpha.
apply TAlpha_Rename. apply TAlpha_Rename.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_VarReplace.
Qed. Qed.
Example typing3 : Example typing3 :
ctx_empty |- [{ ctx_empty |- [{
Λ"T" Λ"U" λ"x",%"T"% λ"y",%"U"% %"y"% Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"%
}] \is [< }] \is [<
"S","T",(%"S"%->%"T"%->%"T"%) "S","T",(%"S"%->%"T"%->%"T"%)
>]. >].
@ -197,14 +186,26 @@ Proof.
apply TEq_Trans with (y:= [< "S","U",(%"S"%->%"U"%->%"U"%) >] ). apply TEq_Trans with (y:= [< "S","U",(%"S"%->%"U"%->%"U"%) >] ).
apply TEq_Alpha. apply TEq_Alpha.
apply TAlpha_Rename. apply TAlpha_Rename.
apply TSubst_UnivReplace. discriminate.
easy.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_Fun.
apply TSubst_VarKeep. discriminate.
apply TSubst_VarKeep. discriminate.
apply TEq_Alpha. apply TEq_Alpha.
apply TAlpha_SubUniv. apply TAlpha_SubUniv.
apply TAlpha_Rename. apply TAlpha_Rename.
apply TSubst_Fun.
apply TSubst_VarKeep. discriminate.
apply TSubst_Fun.
apply TSubst_VarReplace.
apply TSubst_VarReplace.
Qed. Qed.
Example typing4 : (is_well_typed Example typing4 : (is_well_typed
[{ Λ"T" Λ"U" λ"x",%"T"% λ"y",%"U"% %"x"% }] [{ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% }]
). ).
Proof. Proof.
unfold is_well_typed. unfold is_well_typed.
@ -217,6 +218,8 @@ Proof.
apply C_shuffle, C_take. apply C_shuffle, C_take.
Qed. Qed.
Open Scope ladder_expr_scope.
Example typing5 : Example typing5 :
(ctx_assign "60" [< $""$ >] (ctx_assign "60" [< $""$ >]
(ctx_assign "360" [< $""$ >] (ctx_assign "360" [< $""$ >]
@ -225,7 +228,7 @@ Example typing5 :
|- |-
[{ [{
let "deg2turns" := let "deg2turns" :=
(λ"x",$"Angle"$~$"Degrees"$~$""$ (λ"x" $"Angle"$~$"Degrees"$~$""$
morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$)) morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) ) in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
}] }]
@ -268,116 +271,4 @@ Proof.
apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl. apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
Qed. Qed.
End Typing.
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.