coq: equivalence of type-terms

This commit is contained in:
Michael Sippel 2024-07-24 11:19:05 +02:00
parent 7be0e3fa2f
commit a6939b3a40

308
coq/equiv.v Normal file
View file

@ -0,0 +1,308 @@
(* 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 *)
Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : ladder_type -> ladder_type -> Prop :=
| L_DistributeOverApp : forall x y y',
(type_app x (type_rung y y'))
-->distribute-ladder
(type_rung (type_app x y) (type_app x y'))
| L_DistributeOverFun1 : forall x x' y,
(type_fun (type_rung x x') y)
-->distribute-ladder
(type_rung (type_fun x y) (type_fun x' y))
| L_DistributeOverFun2 : forall x y y',
(type_fun x (type_rung y y'))
-->distribute-ladder
(type_rung (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 : ladder_type -> ladder_type -> Prop :=
| L_CondenseOverApp : forall x y y',
(type_rung (type_app x y) (type_app x y'))
-->condense-ladder
(type_app x (type_rung y y'))
| L_CondenseOverFun1 : forall x x' y,
(type_rung (type_fun x y) (type_fun x' y))
-->condense-ladder
(type_fun (type_rung x x') y)
| L_CondenseOverFun2 : forall x y y',
(type_rung (type_fun x y) (type_fun x y'))
-->condense-ladder
(type_fun x (type_rung 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. *)
Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : ladder_type -> ladder_type -> 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 *)
Inductive type_is_flat : ladder_type -> 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_app 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_abs v x))
.
(** Ladder Normal Form:
exhaustive application of -->distribute-ladder
*)
Inductive type_is_lnf : ladder_type -> Prop :=
| LNF : forall x : ladder_type,
(not (exists y:ladder_type, x -->distribute-ladder y))
-> (type_is_lnf x)
.
(** Parameter Normal Form:
exhaustive application of -->condense-ladder
*)
Inductive type_is_pnf : ladder_type -> Prop :=
| PNF : forall x : ladder_type,
(not (exists y:ladder_type, 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 τ:ladder_type,
(type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_rung τ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.
exists (type_abs 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_app (type_id "PosInt") (type_num 10))).
Proof.
apply FlatApp.
apply FlatId.
apply FlatNum.
Qed.
Example example_lnf_type :
(type_is_lnf
(type_rung (type_app (type_id "Seq") (type_id "Char"))
(type_app (type_id "Seq") (type_id "Byte")))).
Proof.
Admitted.
Example example_type_eq :
(type_app (type_id "Seq") (type_rung (type_id "Char") (type_id "Byte")))
===
(type_rung (type_app (type_id "Seq") (type_id "Char"))
(type_app (type_id "Seq") (type_id "Byte"))).
Proof.
apply L_Distribute.
apply L_DistributeOverApp.
Qed.
End Equiv.