310 lines
7 KiB
Coq
310 lines
7 KiB
Coq
(* 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.
|
|
From Coq Require Import Strings.String.
|
|
|
|
Include Terms.
|
|
|
|
Module Equiv.
|
|
|
|
|
|
(** 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_DistributeOverApp : forall x y y',
|
|
(type_spec x (type_ladder y y'))
|
|
-->distribute-ladder
|
|
(type_ladder (type_spec x y) (type_spec x y'))
|
|
|
|
| L_DistributeOverFun1 : forall x x' y,
|
|
(type_fun (type_ladder x x') y)
|
|
-->distribute-ladder
|
|
(type_ladder (type_fun x y) (type_fun x' y))
|
|
|
|
| L_DistributeOverFun2 : forall x y y',
|
|
(type_fun x (type_ladder y y'))
|
|
-->distribute-ladder
|
|
(type_ladder (type_fun x y) (type_fun 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_CondenseOverApp : forall x y y',
|
|
(type_ladder (type_spec x y) (type_spec x y'))
|
|
-->condense-ladder
|
|
(type_spec x (type_ladder y y'))
|
|
|
|
| L_CondenseOverFun1 : forall x x' y,
|
|
(type_ladder (type_fun x y) (type_fun x' y))
|
|
-->condense-ladder
|
|
(type_fun (type_ladder x x') y)
|
|
|
|
| L_CondenseOverFun2 : forall x y y',
|
|
(type_ladder (type_fun x y) (type_fun x y'))
|
|
-->condense-ladder
|
|
(type_fun x (type_ladder 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_CondenseOverApp.
|
|
apply L_CondenseOverFun1.
|
|
apply L_CondenseOverFun2.
|
|
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_DistributeOverApp.
|
|
apply L_DistributeOverFun1.
|
|
apply L_DistributeOverFun2.
|
|
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 :=
|
|
| L_Refl : forall x,
|
|
x === x
|
|
|
|
| L_Trans : forall x y z,
|
|
x === y ->
|
|
y === z ->
|
|
x === z
|
|
|
|
| L_Distribute : forall x y,
|
|
x -->distribute-ladder y ->
|
|
x === y
|
|
|
|
| L_Condense : forall x y,
|
|
x -->condense-ladder y ->
|
|
x === y
|
|
|
|
where "S '===' T" := (type_eq S T).
|
|
|
|
|
|
|
|
(** Symmetry of === *)
|
|
Lemma type_eq_is_symmetric :
|
|
forall x y,
|
|
(x === y) -> (y === x).
|
|
Proof.
|
|
intros.
|
|
induction H.
|
|
|
|
1:{
|
|
apply L_Refl.
|
|
}
|
|
|
|
2:{
|
|
apply L_Condense.
|
|
apply distribute_inverse.
|
|
apply H.
|
|
}
|
|
2:{
|
|
apply L_Distribute.
|
|
apply condense_inverse.
|
|
apply H.
|
|
}
|
|
|
|
apply L_Trans with (y:=y).
|
|
apply IHtype_eq2.
|
|
apply IHtype_eq1.
|
|
Qed.
|
|
|
|
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
|
|
Inductive type_is_flat : type_term -> Prop :=
|
|
| FlatUnit : (type_is_flat type_unit)
|
|
| FlatVar : forall x, (type_is_flat (type_var x))
|
|
| FlatNum : forall x, (type_is_flat (type_num 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 FlatUnit.
|
|
|
|
left.
|
|
apply FlatId.
|
|
|
|
left.
|
|
apply FlatVar.
|
|
|
|
left.
|
|
apply FlatNum.
|
|
|
|
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_unit.
|
|
split. apply L_Refl.
|
|
apply LNF.
|
|
admit.
|
|
|
|
exists (type_id s).
|
|
split. apply L_Refl.
|
|
apply LNF.
|
|
admit.
|
|
admit.
|
|
|
|
exists (type_num n).
|
|
split. apply L_Refl.
|
|
apply LNF.
|
|
admit.
|
|
|
|
admit.
|
|
|
|
exists (type_univ s t).
|
|
split. apply L_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 (type_spec (type_id "PosInt") (type_num 10))).
|
|
Proof.
|
|
apply FlatApp.
|
|
apply FlatId.
|
|
apply FlatNum.
|
|
Qed.
|
|
|
|
Example example_lnf_type :
|
|
(type_is_lnf
|
|
(type_ladder (type_spec (type_id "Seq") (type_id "Char"))
|
|
(type_spec (type_id "Seq") (type_id "Byte")))).
|
|
Proof.
|
|
Admitted.
|
|
|
|
Example example_type_eq :
|
|
(type_spec (type_id "Seq") (type_ladder (type_id "Char") (type_id "Byte")))
|
|
===
|
|
(type_ladder (type_spec (type_id "Seq") (type_id "Char"))
|
|
(type_spec (type_id "Seq") (type_id "Byte"))).
|
|
Proof.
|
|
apply L_Distribute.
|
|
apply L_DistributeOverApp.
|
|
Qed.
|
|
|
|
|
|
End Equiv.
|