ladder-calculus/coq/equiv.v

423 lines
9.7 KiB
Coq
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

(* 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.