From 76f4613eaa5989e29bfd59d716c216ee5386c5f7 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 20 Mar 2011 18:57:32 -0700 Subject: [PATCH] add HaskXXXXCategory, generalized arrows, and reifications --- src/Extraction.v | 11 + src/GeneralizedArrow.v | 35 +++ src/GeneralizedArrowCategory.v | 14 ++ src/GeneralizedArrowFromReification.v | 131 +++++++++++ src/HaskProofCategory.v | 284 +++++++++++++++++++++++ src/HaskStrongCategory.v | 127 ++++++++++ src/NaturalDeductionCategory.v | 178 ++++++++++++++ src/Reification.v | 46 ++++ src/ReificationCategory.v | 14 ++ src/ReificationFromGeneralizedArrow.v | 37 +++ src/ReificationsEquivalentToGeneralizedArrows.v | 86 +++++++ 11 files changed, 963 insertions(+) create mode 100644 src/GeneralizedArrow.v create mode 100644 src/GeneralizedArrowCategory.v create mode 100644 src/GeneralizedArrowFromReification.v create mode 100644 src/HaskProofCategory.v create mode 100644 src/HaskStrongCategory.v create mode 100644 src/NaturalDeductionCategory.v create mode 100644 src/Reification.v create mode 100644 src/ReificationCategory.v create mode 100644 src/ReificationFromGeneralizedArrow.v create mode 100644 src/ReificationsEquivalentToGeneralizedArrows.v diff --git a/src/Extraction.v b/src/Extraction.v index c23d1c5..82b0543 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -1,3 +1,10 @@ +(*********************************************************************************************************************************) +(* Extraction: *) +(* *) +(* This module is the "top level" for extraction *) +(* *) +(*********************************************************************************************************************************) + (* need this or the Haskell extraction fails *) Set Printing Width 1300000. @@ -30,6 +37,10 @@ Require Import HaskStrongToWeak. Require Import HaskWeakToCore. Require Import HaskProofToStrong. +Require Import HaskProofCategory. +Require Import HaskStrongCategory. +Require Import ReificationsEquivalentToGeneralizedArrows. + Open Scope string_scope. Extraction Language Haskell. diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v new file mode 100644 index 0000000..f246567 --- /dev/null +++ b/src/GeneralizedArrow.v @@ -0,0 +1,35 @@ +(*********************************************************************************************************************************) +(* Generalized Arrow: *) +(* *) +(* A generalized arrow is a monoidal functor from an enriching category to an enriched category. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. + +Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) := +{ ga_functor_obj : enr_v_mon K -> C +; ga_functor : Functor (enr_v_mon K) C ga_functor_obj +; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor +}. +Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor. + +Implicit Arguments GeneralizedArrow [ ]. +Implicit Arguments ga_functor_obj [ K C ]. +Implicit Arguments ga_functor [ K C ]. +Implicit Arguments ga_functor_monoidal [ K C ]. diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v new file mode 100644 index 0000000..cd43282 --- /dev/null +++ b/src/GeneralizedArrowCategory.v @@ -0,0 +1,14 @@ +(*********************************************************************************************************************************) +(* CategoryOfGeneralizedArrows: *) +(* *) +(* There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms *) +(* are generalized Arrows *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v new file mode 100644 index 0000000..6aeaace --- /dev/null +++ b/src/GeneralizedArrowFromReification.v @@ -0,0 +1,131 @@ +(*********************************************************************************************************************************) +(* GeneralizedArrowFromReification: *) +(* *) +(* Turn a generalized arrow into a reification *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import Reification. +Require Import GeneralizedArrow. + +Section GArrowFromReification. + + Context (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)). + + Fixpoint garrow_fobj_ vk : C := + match vk with + | T_Leaf None => me_i C + | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end + | t1,,t2 => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2)) + end. + + Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp K vk)). + + Definition homset_tensor_iso + : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk). + intros. + unfold garrow_fobj. + set (se_decomp K vk) as sevk. + destruct sevk. + simpl in *. + rewrite e. + clear e. + induction x; simpl. + + destruct a. + destruct p. + + apply iso_inv. + apply (ni_iso (reification_commutes reification e) e0). + + eapply id_comp. + apply iso_inv. + apply (mf_id (reification_rstar reification)). + apply (mf_id (me_mf C)). + + eapply id_comp. + apply iso_inv. + apply (ni_iso (mf_coherence (reification_rstar reification)) (pair_obj _ _)). + eapply id_comp. + Focus 2. + apply (ni_iso (mf_coherence (me_mf C)) (pair_obj _ _)). + unfold bin_obj. + apply (functors_preserve_isos (enr_v_f C) (a:=(pair_obj _ _))(b:=(pair_obj _ _))). + apply (iso_prod IHx1 IHx2). + Defined. + + Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (RepresentableFunctor C (me_i C)). + exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)). + abstract (exists (garrow_fobj vk); auto). + Defined. + + Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (RepresentableFunctor C (me_i C))}~~>(garrow_fobj' b). + exists (iso_backward (homset_tensor_iso a) + >>> reification_rstar reification \ f + >>> iso_forward (homset_tensor_iso b)). + abstract (auto). + Defined. + + Definition step1_functor : Functor (enr_v_mon K) (FullImage (RepresentableFunctor C (me_i C))) garrow_fobj'. + refine {| fmor := fun a b f => step1_mor f |}. + abstract (intros; unfold step1_mor; simpl; + apply comp_respects; try reflexivity; + apply comp_respects; try reflexivity; + apply fmor_respects; auto). + abstract (intros; unfold step1_mor; simpl; + setoid_rewrite fmor_preserves_id; + setoid_rewrite right_identity; + apply iso_comp2). + abstract (intros; + unfold step1_mor; + simpl; + repeat setoid_rewrite <- associativity; + apply comp_respects; try reflexivity; + repeat setoid_rewrite associativity; + apply comp_respects; try reflexivity; + setoid_rewrite juggle2; + set (iso_comp1 (homset_tensor_iso b)) as qqq; + setoid_rewrite qqq; + clear qqq; + setoid_rewrite right_identity; + apply (fmor_preserves_comp reification)). + Defined. + + Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))). + exists (fun c1 => homset_tensor_iso c1). + abstract (intros; + simpl; + repeat setoid_rewrite <- associativity; + setoid_rewrite iso_comp1; + setoid_rewrite left_identity; + reflexivity). + Qed. + Opaque homset_tensor_iso. + + Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C). + + Definition garrow_functor := step1_functor >>>> step2_functor. + + Definition garrow_from_reification : GeneralizedArrow K C. + refine {| ga_functor := garrow_functor |}. + admit. + Defined. + +End GArrowFromReification. +Opaque homset_tensor_iso. diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v new file mode 100644 index 0000000..e324990 --- /dev/null +++ b/src/HaskProofCategory.v @@ -0,0 +1,284 @@ +(*********************************************************************************************************************************) +(* HaskProofCategory: *) +(* *) +(* Natural Deduction proofs of the well-typedness of a Haskell term form a category *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskKinds. +Require Import HaskCoreTypes. +Require Import HaskLiteralsAndTyCons. +Require Import HaskStrongTypes. +Require Import HaskProof. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. + +Section HaskProofCategory. +(* + + Context (flat_dynamic_semantics : @ND_Relation _ Rule). + Context (ml_dynamic_semantics : @ND_Relation _ Rule). + + Section SystemFC_Category. + Context (encodeTypeTree_reduce : @LeveledHaskType V -> @LeveledHaskType V -> @LeveledHaskType V). + Context (encodeTypeTree_empty : @LeveledHaskType V). + Context (encodeTypeTree_flat_empty : @CoreType V). + Context (encodeTypeTree_flat_reduce : @CoreType V -> @CoreType V -> @CoreType V). + + Definition encodeTypeTree := + @treeReduce _ _ (fun x => match x with None => encodeTypeTree_empty | Some q => q end) encodeTypeTree_reduce. + Definition encodeTypeTree_flat := + @treeReduce _ _ (fun x => match x with None => encodeTypeTree_flat_empty | Some q => q end) encodeTypeTree_flat_reduce. + (* the full category of judgments *) + Definition ob2judgment past := + fun q:Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V) => + let (a,s):=q in (Γ > past : a |- (encodeTypeTree s) ). + Definition SystemFC_Cat past := + @Judgments_Category_monoidal _ Rule + (@ml_dynamic_semantics V) + (Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V)) + (ob2judgment past). + + (* the category of judgments with no variables or succedents in the "future" –- still may have code types *) + (* technically this should be a subcategory of SystemFC_Cat *) + Definition ob2judgment_flat past := + fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) => + let (a,s):=q in (Γ > past : ``a |- `(encodeTypeTree_flat s) ). + Definition SystemFC_Cat_Flat past := + @Judgments_Category_monoidal _ Rule + (@flat_dynamic_semantics V) + (Tree ??(@CoreType V) * Tree ??(@CoreType V)) + (ob2judgment_flat past). + + Section EscBrak_Functor. + Context + (past:@Past V) + (n:V) + (Σ₁:Tree ??(@LeveledHaskType V)). + + Definition EscBrak_Functor_Fobj + : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past + := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) => + let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])). + + Definition append_brak + : forall {c}, ND_ML + (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c ) + (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)). + intros. + unfold ND_ML. + unfold EscBrak_Functor_Fobj. + rewrite mapOptionTree_comp. + simpl in *. + apply nd_replicate. + intro o; destruct o. + apply nd_rule. + apply MLRBrak. + Defined. + + Definition prepend_esc + : forall {h}, ND_ML + (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h)) + (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ). + intros. + unfold ND_ML. + unfold EscBrak_Functor_Fobj. + rewrite mapOptionTree_comp. + simpl in *. + apply nd_replicate. + intro o; destruct o. + apply nd_rule. + apply MLREsc. + Defined. + + Definition EscBrak_Functor_Fmor + : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b), + (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b). + intros. + eapply nd_comp. + apply prepend_esc. + eapply nd_comp. + eapply Flat_to_ML. + apply f. + apply append_brak. + Defined. + + Lemma esc_then_brak_is_id : forall a, + ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak) + (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))). + admit. + Qed. + + Lemma brak_then_esc_is_id : forall a, + ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc) + (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)). + admit. + Qed. + + Instance EscBrak_Functor + : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj := + { fmor := fun a b f => EscBrak_Functor_Fmor a b f }. + intros; unfold EscBrak_Functor_Fmor; simpl in *. + apply ndr_comp_respects; try reflexivity. + apply ndr_comp_respects; try reflexivity. + auto. + intros; unfold EscBrak_Functor_Fmor; simpl in *. + set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q. + setoid_rewrite q. + apply esc_then_brak_is_id. + intros; unfold EscBrak_Functor_Fmor; simpl in *. + set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q. + repeat setoid_rewrite q. + apply ndr_comp_respects; try reflexivity. + apply ndr_comp_respects; try reflexivity. + repeat setoid_rewrite <- q. + apply ndr_comp_respects; try reflexivity. + setoid_rewrite brak_then_esc_is_id. + clear q. + set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q. + setoid_rewrite q. + reflexivity. + Defined. + + End EscBrak_Functor. + + + + Ltac rule_helper_tactic' := + match goal with + | [ H : ?A = ?A |- _ ] => clear H + | [ H : [?A] = [] |- _ ] => inversion H; clear H + | [ H : [] = [?A] |- _ ] => inversion H; clear H + | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H + | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H + | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H + | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H + | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H + | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H +(* | [ H : Sequent T |- _ ] => destruct H *) +(* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*) + | [ H : [?A] = [?B] |- _ ] => inversion H; clear H + | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst + | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl + | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H + end. + + Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2). + admit. + Defined. + + Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c. + admit. + Qed. + + Definition append_brak_to_id : forall {c}, + @ND_FC V + (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c ) + (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)). + admit. + Defined. + + Definition append_brak : forall {h c} + (pf:@ND_FC V + h + (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )), + @ND_FC V + h + (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)). + + refine (fix append_brak h c nd {struct nd} := + ((match nd + as nd' + in @ND _ _ H C + return + (H=h) -> + (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) -> + ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)) + with + | nd_id0 => let case_nd_id0 := tt in _ + | nd_id1 h => let case_nd_id1 := tt in _ + | nd_weak h => let case_nd_weak := tt in _ + | nd_copy h => let case_nd_copy := tt in _ + | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ + | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ + | nd_rule _ _ rule => let case_nd_rule := tt in _ + | nd_cancell _ => let case_nd_cancell := tt in _ + | nd_cancelr _ => let case_nd_cancelr := tt in _ + | nd_llecnac _ => let case_nd_llecnac := tt in _ + | nd_rlecnac _ => let case_nd_rlecnac := tt in _ + | nd_assoc _ _ _ => let case_nd_assoc := tt in _ + | nd_cossa _ _ _ => let case_nd_cossa := tt in _ + end) (refl_equal _) (refl_equal _) + )); + simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *. + destruct case_nd_id0. apply nd_id0. + destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak. + destruct case_nd_weak. apply nd_weak. + + destruct case_nd_copy. + (* + destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'. + inversion H0; subst. + simpl.*) + idtac. + clear H0. + admit. + + destruct case_nd_prod. + eapply nd_prod. + apply (append_brak _ _ lpf). + apply (append_brak _ _ rpf). + + destruct case_nd_comp. + apply append_brak in bot. + apply (nd_comp top bot). + + destruct case_nd_cancell. + eapply nd_comp; [ apply nd_cancell | idtac ]. + apply append_brak_to_id. + + destruct case_nd_cancelr. + eapply nd_comp; [ apply nd_cancelr | idtac ]. + apply append_brak_to_id. + + destruct case_nd_llecnac. + eapply nd_comp; [ idtac | apply nd_llecnac ]. + apply append_brak_to_id. + + destruct case_nd_rlecnac. + eapply nd_comp; [ idtac | apply nd_rlecnac ]. + apply append_brak_to_id. + + destruct case_nd_assoc. + eapply nd_comp; [ apply nd_assoc | idtac ]. + repeat rewrite fixit. + apply append_brak_to_id. + + destruct case_nd_cossa. + eapply nd_comp; [ idtac | apply nd_cossa ]. + repeat rewrite fixit. + apply append_brak_to_id. + + destruct case_nd_rule + + + + Defined. + + Definition append_brak {h c} : forall + pf:@ND_FC V + (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h ) + c, + @ND_FC V + (fixify Γ past (EscBrak_Functor_Fobj h)) + c. + admit. + Defined. +*) +End HaskProofCategory. \ No newline at end of file diff --git a/src/HaskStrongCategory.v b/src/HaskStrongCategory.v new file mode 100644 index 0000000..99772c7 --- /dev/null +++ b/src/HaskStrongCategory.v @@ -0,0 +1,127 @@ +(*********************************************************************************************************************************) +(* HaskStrongCategory: *) +(* *) +(* Well-typed Haskell terms in a specific tyvar/covar context form a category *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskKinds. +Require Import HaskCoreTypes. +Require Import HaskLiteralsAndTyCons. +Require Import HaskStrongTypes. +Require Import HaskStrong. + +(* + (* the category of flat Haskell terms (n-ary) *) + Section HaskFlat. + + Context (past:@Past V). + + Lemma idmor a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)]. + (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*) + admit. + Defined. + + Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)]. + admit. + Defined. + + Definition HaskFlat + : ECategory + (SystemFC_Cat_Flat past) + (Tree ??(@CoreType V)) + (fun a s => [(a,s)]). + refine + {| eid := fun a => idmor a + ; ecomp := fun a b c => compmor a b c + |}; intros; simpl in *; auto. + apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)). + apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)). + admit. + admit. + admit. + Defined. + + Definition HaskFlatEnrichment : SurjectiveEnrichment. + refine {| se_enr := {| enr_c := HaskFlat |} |}. + admit. + Defined. + + End HaskFlat. + + (* the category of multi-level Haskell terms (n-ary) with a given past *) + Section Hask. + Context (past:@Past V). + + Lemma idmor' a : [] ~~{SystemFC_Cat past}~~> [(a,a)]. + (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*) + admit. + Defined. + + Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)]. + admit. + Defined. + + Definition Hask + : ECategory + (SystemFC_Cat past) + (Tree ??(@LeveledHaskType V)) + (fun a s => [(a,s)]). + refine + {| eid := fun a => idmor' a + ; ecomp := fun a b c => compmor' a b c + |}; intros; simpl in *; auto. + apply (MonoidalCat_all_central (SystemFC_Cat past)). + apply (MonoidalCat_all_central (SystemFC_Cat past)). + admit. + admit. + admit. + Defined. + + Definition HaskEnrichmentMonoidal : MonoidalEnrichment. + refine {| me_enr := {| enr_c := Hask |} |}. + Admitted. + + Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment. + refine {| ffme_enr := HaskEnrichmentMonoidal |}. + admit. + admit. + admit. + Defined. + End Hask. + + Section ReificationAndGeneralizedArrow. + Context + (past:list ((Tree ??(@LeveledHaskType V)) * V)) + (Σ:(Tree ??(@LeveledHaskType V))) + (n:V). + + Definition SystemFC_Reification + : Reification + (HaskFlatEnrichment (((Σ,n)::past))) + (HaskEnrichmentMonicMonoidal (*past*)) + (me_i (HaskEnrichmentMonicMonoidal (*past*))). + (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*) + admit. + Defined. +(* + Definition SystemFC_GArrow := + garrow_from_reification + (HaskFlatEnrichment (((Σ,n)::past))) + (HaskEnrichmentMonicMonoidal (*past*)) + SystemFC_Reification. + *) + (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor; + * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory + * of Hask which consists of the (GArrow g => g a b) morphisms *) + + End ReificationAndGeneralizedArrow. +*) + + diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v new file mode 100644 index 0000000..23ddb56 --- /dev/null +++ b/src/NaturalDeductionCategory.v @@ -0,0 +1,178 @@ +(*********************************************************************************************************************************) +(* NaturalDeductionCategory: *) +(* *) +(* Natural Deduction proofs form a category (under mild assumptions, see below) *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. + +Require Import Algebras_ch4. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. + +Open Scope nd_scope. +Open Scope pf_scope. + +(* proofs form a category, with judgment-trees as the objects *) +Section Judgments_Category. + + Context {Judgment : Type}. + Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. + Context (nd_eqv : @ND_Relation Judgment Rule). + + (* actually you can use any type as the objects, so long as you give a mapping from that type to judgments *) + Context {Ob : Type}. + Context (ob2judgment : Ob -> Judgment). + Coercion ob2judgment : Ob >-> Judgment. + + Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2). + + Instance Judgments_Category + : Category (Tree ??Ob) (fun h c => (mapOptionTree ob2judgment h) /⋯⋯/ (mapOptionTree ob2judgment c)) := + { id := fun h => nd_id _ + ; comp := fun a b c f g => f ;; g + ; eqv := fun a b f g => f === g + }. + intros; apply Build_Equivalence; + [ unfold Reflexive; intros; reflexivity + | unfold Symmetric; intros; symmetry; auto + | unfold Transitive; intros; transitivity y; auto ]. + unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto. + intros; apply ndr_comp_left_identity. + intros; apply ndr_comp_right_identity. + intros; apply ndr_comp_associativity. + Defined. + + Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category := + (fun xy => + match xy with + | pair_obj x y => T_Branch x y + end). + Definition Judgments_Category_monoidal_endofunctor_fmor : + forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) -> + ((Judgments_Category_monoidal_endofunctor_fobj a) + ~~{Judgments_Category}~~> + (Judgments_Category_monoidal_endofunctor_fobj b)). + intros. + destruct a. + destruct b. + destruct X. + exact (h**h0). + Defined. + Definition Judgments_Category_monoidal_endofunctor + : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj. + refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl. + abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto). + abstract (destruct a; simpl in *; reflexivity). + abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp). + Defined. + + Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)). + apply (@Build_Isomorphic _ _ Judgments_Category _ _ + (@nd_assoc _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c) + : (a,, b),, c ~~{Judgments_Category}~~> a,, (b,, c)) + (@nd_cossa _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c) + : a,, (b,, c) ~~{Judgments_Category}~~> (a,, b),, c)); simpl; auto. + Defined. + Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a. + apply (@Build_Isomorphic _ _ Judgments_Category _ _ + (@nd_cancelr _ Rule (mapOptionTree ob2judgment a) : a,,[] ~~{Judgments_Category}~~> a) + (@nd_rlecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> a,,[])); simpl; auto. + Defined. + Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a. + apply (@Build_Isomorphic _ _ Judgments_Category _ _ + (@nd_cancell _ Rule (mapOptionTree ob2judgment a) : [],,a ~~{Judgments_Category}~~> a) + (@nd_llecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> [],,a)); simpl; auto. + Defined. + + Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. + refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl. + setoid_rewrite (ndr_prod_right_identity f). + repeat setoid_rewrite ndr_comp_associativity. + apply ndr_comp_respects; try reflexivity. + symmetry. + eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. + apply ndr_comp_respects; try reflexivity; simpl; auto. + Defined. + Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. + eapply Build_NaturalIsomorphism. + instantiate (1:=fun x => jud_cancell_iso x). + intros; simpl. + setoid_rewrite (ndr_prod_left_identity f). + repeat setoid_rewrite ndr_comp_associativity. + apply ndr_comp_respects; try reflexivity. + symmetry. + eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. + apply ndr_comp_respects; try reflexivity; simpl; auto. + Defined. + Definition jud_mon_assoc_iso : + forall X, + (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) X) ≅ + (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor))) X. + intros. + destruct X as [a c]. + destruct a as [a b]. + apply (jud_assoc_iso a b c). + Defined. + Definition jud_mon_assoc : + ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) + <~~~> + func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)). + refine {| ni_iso := jud_mon_assoc_iso |}. + intros. + destruct A as [a1 a3]. destruct a1 as [a1 a2]. + destruct B as [b1 b3]. destruct b1 as [b1 b2]. + destruct f as [f1 f3]. destruct f1 as [f1 f2]. + simpl. + setoid_rewrite ndr_prod_associativity. + setoid_rewrite ndr_comp_associativity. + setoid_rewrite ndr_comp_associativity. + apply ndr_comp_respects; try reflexivity. + symmetry. + eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. + apply ndr_comp_respects; try reflexivity; simpl; auto. + Defined. + + Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] := + { mon_cancelr := jud_mon_cancelr + ; mon_cancell := jud_mon_cancell + ; mon_assoc := jud_mon_assoc }. + apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto. + apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto. + Defined. + + (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment, + * this asserts that we have sensible structural rules with respect + * to that mapping. Doing all of this "with respect to a mapping" + * lets us avoid duplicating code for both the antecedent and + * succedent of sequent deductions. *) + Class TreeStructuralRules {T:Type}(rep:Tree ??T -> Judgment) := + { tsr_eqv : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2) + ; tsr_ant_assoc : forall {a b c}, Rule [rep ((a,,b),,c)] [rep ((a,,(b,,c)))] + ; tsr_ant_cossa : forall {a b c}, Rule [rep (a,,(b,,c))] [rep (((a,,b),,c))] + ; tsr_ant_cancell : forall {a }, Rule [rep ( [],,a )] [rep ( a )] + ; tsr_ant_cancelr : forall {a }, Rule [rep (a,,[] )] [rep ( a )] + ; tsr_ant_llecnac : forall {a }, Rule [rep ( a )] [rep ( [],,a )] + ; tsr_ant_rlecnac : forall {a }, Rule [rep ( a )] [rep ( a,,[] )] + }. + + + (* Structure ExpressionAlgebra (sig:Signature) := *) + +End Judgments_Category. + +Close Scope pf_scope. +Close Scope nd_scope. diff --git a/src/Reification.v b/src/Reification.v new file mode 100644 index 0000000..a56ded8 --- /dev/null +++ b/src/Reification.v @@ -0,0 +1,46 @@ +(*********************************************************************************************************************************) +(* Reification: *) +(* *) +(* A reification is a functor R from one enrichING category A to another enrichING category B which forms a commuting square *) +(* with every pair of hom-functors Hom(X,-):a->A and Hom(Y,-):b->B up to natural isomorphism. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. + +Opaque RepresentableFunctor. +Opaque functor_comp. +Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := +{ reification_r_obj : K -> K -> C +; reification_rstar_obj : enr_v K -> enr_v C +; reification_r : forall k:K, Functor K C (reification_r_obj k) +; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj +; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f +; reification_commutes : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f +}. +Transparent RepresentableFunctor. +Transparent functor_comp. + +Coercion reification_rstar : Reification >-> MonoidalFunctor. +Implicit Arguments Reification [ ]. +Implicit Arguments reification_r_obj [ K C CI ]. +Implicit Arguments reification_r [ K C CI ]. +Implicit Arguments reification_rstar [ K C CI ]. +Implicit Arguments reification_rstar_f [ K C CI ]. +Implicit Arguments reification_commutes [ K C CI ]. +Implicit Arguments reification_rstar_obj [ K C CI ]. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v new file mode 100644 index 0000000..4d83b78 --- /dev/null +++ b/src/ReificationCategory.v @@ -0,0 +1,14 @@ +(*********************************************************************************************************************************) +(* ReificationCategory: *) +(* *) +(* There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms *) +(* are reifications *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v new file mode 100644 index 0000000..ed92c57 --- /dev/null +++ b/src/ReificationFromGeneralizedArrow.v @@ -0,0 +1,37 @@ +(*********************************************************************************************************************************) +(* ReificationFromGeneralizedArrow: *) +(* *) +(* Turn a reification into a generalized arrow *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import Reification. +Require Import GeneralizedArrow. + +Definition reification_from_garrow (K:Enrichment) (C:MonoidalEnrichment) (garrow : GeneralizedArrow K C) + : Reification K C (mon_i C). + refine + {| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow + ; reification_rstar_f := garrow >>>> me_mf C + ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C) + |}. + abstract (intros; set (@ni_associativity) as q; apply q). + Defined. + + diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v new file mode 100644 index 0000000..5b4c5ef --- /dev/null +++ b/src/ReificationsEquivalentToGeneralizedArrows.v @@ -0,0 +1,86 @@ +(*********************************************************************************************************************************) +(* ReificationsEquivalentToGeneralizedArrows: *) +(* *) +(* The category of generalized arrows and the category of reifications are equivalent categories. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import Reification. +Require Import GeneralizedArrow. +Require Import GArrowFromReification. +Require Import ReificationFromGArrow. +Require Import ReificationCategory. +Require Import GeneralizedArrowCategory. + +Section ReificationsEquivalentToGeneralizedArrows. + + Ltac if_transitive := + match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _) + end. + + Lemma roundtrip_lemma' + `{C:Category}`{D:Category}`{E:Category} + {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) : + ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _). + if_transitive. + apply (if_associativity F (ff_functor_section_functor G _ _) G). + apply if_respects. + apply if_id. + if_transitive; [ idtac | apply if_left_identity ]. + apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)). + apply if_inv. + apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))). + apply if_respects. + apply ff_functor_section_splits_niso. + apply if_id. + Qed. + + Definition roundtrip_lemma + (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)) + := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification). + + Lemma roundtrip_reification_to_reification + (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)) + : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification). + simpl. + unfold mon_f. + unfold garrow_functor. + apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))). + apply step1_niso. + apply (if_inv (roundtrip_lemma K C reification)). + Qed. + (* FIXME: show that the R-functors are naturally isomorphic as well; should follow pretty easily from the proof for Rstar *) + + Lemma roundtrip_garrow_to_garrow + (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (garrow : GeneralizedArrow K C) + : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow). + apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)). + apply if_inv. + apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow) + >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))). + unfold mf_f. + unfold garrow_from_reification. + unfold garrow_functor. + unfold step2_functor. + apply roundtrip_lemma. + apply if_inv. + apply (step1_niso K C (reification_from_garrow K C garrow)). + Qed. + +End ReificationsEquivalentToGeneralizedArrows. -- 1.7.10.4