complete type distribute/condense definitions

This commit is contained in:
Michael Sippel 2024-08-18 10:56:06 +02:00
parent 221c017640
commit d08144434c
Signed by: senvas
GPG key ID: 060F22F65102F95C

View file

@ -61,7 +61,12 @@ Admitted.
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_DistributeOverApp : forall x y y', | L_DistributeOverSpec1 : forall x x' y,
(type_spec (type_ladder x x') y)
-->distribute-ladder
(type_ladder (type_spec x y) (type_spec x' y))
| L_DistributeOverSpec2 : forall x y y',
(type_spec x (type_ladder y y')) (type_spec x (type_ladder y y'))
-->distribute-ladder -->distribute-ladder
(type_ladder (type_spec x y) (type_spec x y')) (type_ladder (type_spec x y) (type_spec x y'))
@ -76,13 +81,28 @@ Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
-->distribute-ladder -->distribute-ladder
(type_ladder (type_fun x y) (type_fun x y')) (type_ladder (type_fun x y) (type_fun x y'))
| L_DistributeOverMorph1 : forall x x' y,
(type_morph (type_ladder x x') y)
-->distribute-ladder
(type_ladder (type_morph x y) (type_morph x' 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). 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_CondenseOverApp : forall x y y', | L_CondenseOverSpec1 : forall x x' y,
(type_ladder (type_spec x y) (type_spec x' y))
-->condense-ladder
(type_spec (type_ladder x x') y)
| L_CondenseOverSpec2 : forall x y y',
(type_ladder (type_spec x y) (type_spec x y')) (type_ladder (type_spec x y) (type_spec x y'))
-->condense-ladder -->condense-ladder
(type_spec x (type_ladder y y')) (type_spec x (type_ladder y y'))
@ -97,6 +117,16 @@ Inductive type_condense_ladder : type_term -> type_term -> Prop :=
-->condense-ladder -->condense-ladder
(type_fun x (type_ladder y y')) (type_fun x (type_ladder y y'))
| L_CondenseOverMorph1 : forall x x' y,
(type_ladder (type_morph x y) (type_morph x' y))
-->condense-ladder
(type_morph (type_ladder x x') y)
| L_CondenseOverMorph2 : forall x y y',
(type_ladder (type_morph x y) (type_morph x y'))
-->condense-ladder
(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).
@ -110,9 +140,12 @@ Lemma distribute_inverse :
Proof. Proof.
intros. intros.
destruct H. destruct H.
apply L_CondenseOverApp. apply L_CondenseOverSpec1.
apply L_CondenseOverSpec2.
apply L_CondenseOverFun1. apply L_CondenseOverFun1.
apply L_CondenseOverFun2. apply L_CondenseOverFun2.
apply L_CondenseOverMorph1.
apply L_CondenseOverMorph2.
Qed. Qed.
(** Inversion Lemma: (** Inversion Lemma:
@ -125,9 +158,12 @@ Lemma condense_inverse :
Proof. Proof.
intros. intros.
destruct H. destruct H.
apply L_DistributeOverApp. apply L_DistributeOverSpec1.
apply L_DistributeOverSpec2.
apply L_DistributeOverFun1. apply L_DistributeOverFun1.
apply L_DistributeOverFun2. apply L_DistributeOverFun2.
apply L_DistributeOverMorph1.
apply L_DistributeOverMorph2.
Qed. Qed.
@ -331,7 +367,7 @@ Example example_type_eq :
(type_spec (type_id "Seq") (type_id "Byte"))). (type_spec (type_id "Seq") (type_id "Byte"))).
Proof. Proof.
apply L_Distribute. apply L_Distribute.
apply L_DistributeOverApp. apply L_DistributeOverSpec2.
Qed. Qed.