ladder-calculus/coq/equiv.v

424 lines
9.7 KiB
Coq
Raw Normal View History

2024-07-24 11:19:05 +02:00
(* 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.
*)
2024-07-24 11:19:05 +02:00
Require Import terms.
2024-08-18 10:47:35 +02:00
Require Import subst.
2024-07-24 11:19:05 +02:00
From Coq Require Import Strings.String.
2024-08-18 10:47:35 +02:00
(** Alpha conversion in types *)
Reserved Notation "S '--->α' T" (at level 40).
2024-08-18 10:47:35 +02:00
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).
2024-08-18 10:47:35 +02:00
(** Alpha conversion is symmetric *)
2024-08-18 10:47:35 +02:00
Lemma type_alpha_symm :
forall σ τ,
(σ --->α τ) -> (τ --->α σ).
2024-08-18 10:47:35 +02:00
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.
2024-08-18 10:47:35 +02:00
Admitted.
2024-08-07 15:59:03 +02:00
(** Define all rewrite steps $\label{coq:type-dist}$ *)
2024-07-24 11:19:05 +02:00
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'> >]
2024-07-24 11:19:05 +02:00
-->distribute-ladder
[< <x y>~<x y'> >]
2024-07-24 11:19:05 +02:00
| L_DistributeOverFun1 : forall x x' y,
[< (x~x' -> y) >]
2024-07-24 11:19:05 +02:00
-->distribute-ladder
[< (x -> y) ~ (x' -> y) >]
2024-07-24 11:19:05 +02:00
| L_DistributeOverFun2 : forall x y y',
[< (x -> y~y') >]
2024-07-24 11:19:05 +02:00
-->distribute-ladder
[< (x -> y) ~ (x -> y') >]
2024-07-24 11:19:05 +02:00
| 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'))
2024-07-24 11:19:05 +02:00
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'> >]
2024-07-24 11:19:05 +02:00
-->condense-ladder
[< <x y~y'> >]
2024-07-24 11:19:05 +02:00
| L_CondenseOverFun1 : forall x x' y,
[< (x -> y) ~ (x' -> y) >]
2024-07-24 11:19:05 +02:00
-->condense-ladder
[< (x~x') -> y >]
2024-07-24 11:19:05 +02:00
| L_CondenseOverFun2 : forall x y y',
[< (x -> y) ~ (x -> y') >]
2024-07-24 11:19:05 +02:00
-->condense-ladder
[< (x -> y~y') >]
2024-07-24 11:19:05 +02:00
| 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') >]
2024-07-24 11:19:05 +02:00
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.
2024-07-24 11:19:05 +02:00
apply L_CondenseOverFun1.
apply L_CondenseOverFun2.
apply L_CondenseOverMorph1.
apply L_CondenseOverMorph2.
2024-07-24 11:19:05 +02:00
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.
2024-07-24 11:19:05 +02:00
apply L_DistributeOverFun1.
apply L_DistributeOverFun2.
apply L_DistributeOverMorph1.
apply L_DistributeOverMorph2.
2024-07-24 11:19:05 +02:00
Qed.
2024-08-07 15:59:03 +02:00
(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
2024-07-24 11:19:05 +02:00
Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : type_term -> type_term -> Prop :=
| TEq_Refl : forall x,
2024-07-24 11:19:05 +02:00
x === x
| TEq_Trans : forall x y z,
2024-07-24 11:19:05 +02:00
x === y ->
y === z ->
x === z
2024-09-19 01:41:51 +02:00
| 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 ->
2024-08-18 10:47:35 +02:00
x === y
| TEq_Distribute : forall x y,
2024-07-24 11:19:05 +02:00
x -->distribute-ladder y ->
x === y
| TEq_Condense : forall x y,
2024-07-24 11:19:05 +02:00
x -->condense-ladder y ->
x === y
where "S '===' T" := (type_eq S T).
(** Symmetry of === *)
Lemma TEq_Symm :
2024-07-24 11:19:05 +02:00
forall x y,
(x === y) -> (y === x).
Proof.
intros.
induction H.
apply TEq_Refl.
apply TEq_Trans with (y:=y).
2024-07-24 11:19:05 +02:00
apply IHtype_eq2.
apply IHtype_eq1.
2024-09-19 01:41:51 +02:00
apply TEq_SubFun.
auto. auto.
apply TEq_SubMorph.
auto. auto.
apply TEq_LadderAssocRL.
apply TEq_LadderAssocLR.
2024-08-18 10:47:35 +02:00
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.
2024-08-18 10:47:35 +02:00
apply H.
2024-07-24 11:19:05 +02:00
Qed.
2024-08-07 15:59:03 +02:00
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
2024-07-24 11:19:05 +02:00
| 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))
2024-07-24 11:19:05 +02:00
| 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))
2024-07-24 11:19:05 +02:00
.
(** 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))
2024-07-24 11:19:05 +02:00
-> (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))
2024-07-24 11:19:05 +02:00
-> (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)))
2024-07-24 11:19:05 +02:00
.
Proof.
intros τ H.
induction τ.
2024-07-24 11:19:05 +02:00
left.
apply FlatId.
left.
apply FlatVar.
(*
2024-07-24 11:19:05 +02:00
left.
apply IHτ1 in H.
apply FlatFun.
apply H.
destruct H.
destruct H.
apply IHτ1.
*)
2024-07-24 11:19:05 +02:00
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.
2024-07-24 11:19:05 +02:00
apply LNF.
admit.
admit.
admit.
exists (type_univ s t).
split.
apply TEq_Refl.
2024-07-24 11:19:05 +02:00
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"$> >].
2024-07-24 11:19:05 +02:00
Proof.
apply FlatApp.
apply FlatId.
2024-08-21 16:10:15 +02:00
apply FlatId.
2024-07-24 11:19:05 +02:00
Qed.
Example example_lnf_type :
type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >].
2024-07-24 11:19:05 +02:00
Proof.
Admitted.
Example example_type_eq :
[< [$"Char"$ ~ $"Byte"$] >]
2024-07-24 11:19:05 +02:00
===
[< [$"Char"$] ~ [$"Byte"$] >]
.
2024-07-24 11:19:05 +02:00
Proof.
apply TEq_Distribute.
apply L_DistributeOverSpec2.
2024-07-24 11:19:05 +02:00
Qed.