re-arrange NaturalDeduction

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2b65a18..61993a1 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -34,12 +34,13 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
+Require Import ProgrammingLanguage.
+
 Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
-Require Import ProgrammingLanguage.
 *)
+Require Import ReificationsEquivalentToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index f246567..bf7743b 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -22,14 +22,14 @@ Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 
-Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) :=
+Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
 { 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 ].
+Implicit Arguments GeneralizedArrow    [ [ce] ].
+Implicit Arguments ga_functor_obj      [ K ce C ].
+Implicit Arguments ga_functor          [ K ce C ].
+Implicit Arguments ga_functor_monoidal [ K ce C ].

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index cd43282..d98f85a 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -9,6 +9,21 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+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 GeneralizedArrow.
+
+Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow.
+  admit.
+  Qed.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 6aeaace..e6d3cbd 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -26,7 +26,7 @@ Require Import GeneralizedArrow.
 
 Section GArrowFromReification.
 
-  Context  (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)).
+  Context  `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)).
 
   Fixpoint garrow_fobj_ vk : C :=
     match vk with
@@ -35,13 +35,13 @@ Section GArrowFromReification.
     | 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 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.
+    set (se_decomp _ K  vk) as sevk.
     destruct sevk.
     simpl in *.
     rewrite e.

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 855b66a..06b6efe 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -333,11 +333,56 @@ Section Natural_Deduction.
   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
   end.
 
+  Section Sequents.
+    Context {S:Type}.   (* type of sequent components *)
+    Context (sequent:S->S->Judgment).
+    Context (ndr:ND_Relation).
+    Notation "a |= b" := (sequent a b).
+    Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
+
+    Class SequentCalculus :=
+    { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
+    }.
+    
+    Class CutRule :=
+    { nd_cutrule_seq       :> SequentCalculus
+    ; nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
+    ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
+    ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
+    ; nd_cut_associativity :  forall {a b c d},
+      (nd_cut a b c ** nd_id1 (c|=d)) ;; (nd_cut a c d) === nd_assoc ;; (nd_id1 (a|=b) ** nd_cut b c d) ;; nd_cut a b d
+    }.
+
+  End Sequents.
+
+  Section SequentsOfTrees.
+    Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}(sc:SequentCalculus sequent).
+    Context (ndr:ND_Relation).
+    Notation "a |= b" := (sequent a b).
+    Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
+
+    Class TreeStructuralRules :=
+    { tsr_ant_assoc     : forall {x a b c}, Rule [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x]
+    ; tsr_ant_cossa     : forall {x a b c}, Rule [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x]
+    ; tsr_ant_cancell   : forall {x a    }, Rule [  [],,a     |= x]     [        a   |= x]
+    ; tsr_ant_cancelr   : forall {x a    }, Rule [a,,[]       |= x]     [        a   |= x]
+    ; tsr_ant_llecnac   : forall {x a    }, Rule [      a     |= x]     [    [],,a   |= x]
+    ; tsr_ant_rlecnac   : forall {x a    }, Rule [      a     |= x]     [    a,,[]   |= x]
+    }.
+
+    Class SequentExpansion :=
+    { se_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
+    ; se_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
+    }.
+  End SequentsOfTrees.
+
   Close Scope nd_scope.
   Open Scope pf_scope.
 
 End Natural_Deduction.
 
+Coercion nd_cut : CutRule >-> Funclass.
+
 Implicit Arguments ND [ Judgment ].
 Hint Constructors Structural.
 Hint Extern 1 => apply nd_id_structural.

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 5e3432b..b64ac4b 100644 (file)
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -201,41 +201,6 @@ Section Judgments_Category.
     apply nd_structural_cancelr; 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,,[]    )]
-  }.
-
-  Section Sequents.
-    Context {S:Type}.   (* type of sequent components *)
-    Context (sequent:S->S->Judgment).
-    Notation "a |= b" := (sequent a b).
-
-    Class SequentCalculus :=
-    { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ]
-    }.
-    
-    Class CutRule :=
-    { nd_cutrule_seq       :> SequentCalculus
-    ; nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
-    ; nd_cut_associativity :  forall {a b c d},
-      ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d)
-        ===
-        nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d))
-    ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
-    ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
-    }.
-  End Sequents.
 
   (* Structure ExpressionAlgebra (sig:Signature) := *)
 

diff --git a/src/Preamble.v b/src/Preamble.v
index f83d9a1..453027a 100644 (file)
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -16,8 +16,11 @@ Export Coq.Setoids.Setoid.
 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
 Generalizable All Variables.
 
+Reserved Notation "a ** b"                      (at level 40).
+Reserved Notation "a ;; b"                      (at level 45).
+
 Reserved Notation "a -~- b"                     (at level 10).
-Reserved Notation "a ** b"                      (at level 10).
+Reserved Notation "pf1 === pf2"                 (at level 80).
 Reserved Notation "?? x"                        (at level 1).
 Reserved Notation "a ,, b"                      (at level 50).
 Reserved Notation "!! f"                        (at level 3).
@@ -52,7 +55,6 @@ Reserved Notation "A ⋊ f"                       (at level 40).
 Reserved Notation "- ⋉ A"                       (at level 40).
 Reserved Notation "A ⋊ -"                       (at level 40).
 Reserved Notation "a *** b"                     (at level 40).
-Reserved Notation "a ;; b"                      (at level 45).
 Reserved Notation "[# f #]"                     (at level 2).
 Reserved Notation "a ---> b"                    (at level 11, right associativity).
 Reserved Notation "a <- b"                      (at level 100, only parsing).
@@ -69,7 +71,6 @@ Reserved Notation "f ○ g"                       (at level 100).
 Reserved Notation "a ==[ n ]==> b"              (at level 20).
 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
-Reserved Notation "pf1 === pf2"                 (at level 80).
 Reserved Notation "a |== b @@ c"                (at level 100).
 Reserved Notation "f >>>> g"                    (at level 45).
 Reserved Notation "a >>[ n ]<< b"               (at level 100).

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index b00d1ad..7630440 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Categories_ch1_3.
+Require Import InitialTerminal_ch2_2.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import ProductCategories_ch1_6_1.
@@ -21,15 +22,17 @@ Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
+Require Import FunctorCategories_ch7_7.
+
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
-Require Import Reification.
+
 Require Import FreydCategories.
-Require Import InitialTerminal_ch2_2.
-Require Import FunctorCategories_ch7_7.
-Require Import GeneralizedArrowFromReification.
-Require Import GeneralizedArrow.
 
+Require Import Reification.
+Require Import GeneralizedArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.
 
 (*
  *  Everything in the rest of this section is just groundwork meant to
@@ -42,7 +45,6 @@ Require Import GeneralizedArrow.
  *)   
 Section Programming_Language.
 
-  (* Formalized Definition 4.1.1, production $\tau$ *)
   Context {T    : Type}.               (* types of the language *)
 
   Context (Judg : Type).
@@ -63,7 +65,7 @@ Section Programming_Language.
   Open Scope nd_scope.
   Open Scope al_scope.
 
-  (* Formalized Definition 4.1
+  (*
    *
    * Note that from this abstract interface, the terms (expressions)
    * in the proof are not accessible at all; they don't need to be --
@@ -82,145 +84,21 @@ Section Programming_Language.
    * This also means that we don't need an explicit proof obligation for 4.1.2.
    *)
   Class ProgrammingLanguage :=
-
-  (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
-  { al_eqv                   : @ND_Relation Judg Rule
-                                     where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
-
-  (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
-   * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
-   * to generate the rest *)
-  ; al_reflexive_seq         : forall t, Rule [] [t|=t]
-
-  (* these can all be absorbed into a separate "sequent calculus" presentation *)
-  ; al_ant_assoc     : forall {a b c d}, Rule [(a,,b),,c|=d]     [(a,,(b,,c))|=d]
-  ; al_ant_cossa     : forall {a b c d}, Rule [a,,(b,,c)|=d]     [((a,,b),,c)|=d]
-  ; al_ant_cancell   : forall {a b    }, Rule [  [],,a  |=b]     [        a  |=b]
-  ; al_ant_cancelr   : forall {a b    }, Rule [a,,[]    |=b]     [        a  |=b]
-  ; al_ant_llecnac   : forall {a b    }, Rule [      a  |=b]     [  [],,a    |=b]
-  ; al_ant_rlecnac   : forall {a b    }, Rule [      a  |=b]     [  a,,[]    |=b]
-  ; al_suc_assoc     : forall {a b c d}, Rule [d|=(a,,b),,c]     [d|=(a,,(b,,c))]
-  ; al_suc_cossa     : forall {a b c d}, Rule [d|=a,,(b,,c)]     [d|=((a,,b),,c)]
-  ; al_suc_cancell   : forall {a b    }, Rule [a|=[],,b    ]     [a|=      b    ]
-  ; al_suc_cancelr   : forall {a b    }, Rule [a|=b,,[]    ]     [a|=      b    ]
-  ; al_suc_llecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=[],,b      ]
-  ; al_suc_rlecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=b,,[]      ]
-
-  ; al_horiz_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
-  ; al_horiz_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
-
-  (* these are essentially one way of formalizing
-   * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
-  ; al_horiz_expand_left_reflexive  : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left  a#]===[#al_reflexive_seq (a,,b)#]
-  ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
-  ; al_horiz_expand_right_then_cancel : forall a,
-    ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
-
-  ; al_vert_expand_ant_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [x,,a   |=   b   ]/⋯⋯/[x,,c   |=   d   ]
-  ; al_vert_expand_ant_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a,,x|=   b   ]/⋯⋯/[   c,,x|=   d   ]
-  ; al_vert_expand_suc_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=x,,b   ]/⋯⋯/[   c   |=x,,d   ]
-  ; al_vert_expand_suc_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=   b,,x]/⋯⋯/[   c   |=   d,,x]
-  ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-      f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left  x g
-  ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_ant_right  x f === al_vert_expand_ant_right x g
-  ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_suc_left   x f === al_vert_expand_suc_left  x g
-  ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
-    f===g -> al_vert_expand_suc_right  x f === al_vert_expand_suc_right x g
-  ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left   x (nd_id [a|=b]) === nd_id [x,,a|=b]
-  ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right  x (nd_id [a|=b]) === nd_id [a,,x|=b]
-  ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left   x (nd_id [a|=b]) === nd_id [a|=x,,b]
-  ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right  x (nd_id [a|=b]) === nd_id [a|=b,,x]
-  ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
-  ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
-  ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
-  ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
-    (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
-
-  ; al_subst                 : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
-  ; al_subst_associativity : forall {a b c d},
-      ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
-      (al_subst a c d)
-      ===
-      nd_assoc ;;
-      ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
-      (al_subst a b d))
-  ; al_subst_associativity' : forall {a b c d},
-      nd_cossa ;;
-      ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
-      (al_subst a c d)
-      ===
-      ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
-      (al_subst a b d))
-
-  ; al_subst_left_identity  : forall a b, ((    [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell
-  ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#]    );; al_subst b _ _) === nd_cancelr
-  ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
-    [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
-    === al_subst a b c;; [#al_horiz_expand_left d#]
-  ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
-    [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
-    === al_subst a b c;; [#al_horiz_expand_right d#]
-  ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
-   (((nd_rlecnac;;
-      ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
-        (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
-     (nd_id [t1 |= t0]) **
-     ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
-       (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));; 
-    al_subst t1 t0 t2)
-   ===
-    ((([#al_reflexive_seq (t1,, [])#];;
-          (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
-           al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));; 
-         (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
+  { al_eqv                : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
+  ; al_tsr                : TreeStructuralRules
+  ; al_subst              : CutRule
+  ; al_sequent_join       : SequentJoin
   }.
-
   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
-  Open Scope temporary_scope3.
-
-  Lemma al_subst_respects {PL:ProgrammingLanguage} :
-    forall {a b c},
-      forall
-      (f  : [] /⋯⋯/ [a |= b])
-      (f' : [] /⋯⋯/ [a |= b])
-      (g  : [] /⋯⋯/ [b |= c])
-      (g' : [] /⋯⋯/ [b |= c]),
-      (f === f') ->
-      (g === g') ->
-      (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
-    intros.
-    setoid_rewrite H.
-    setoid_rewrite H0.
-    reflexivity.
-    Defined.
-
-  (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
-  Class ProgrammingLanguageWithUnrestrictedSubstructuralRules :=
-  { alwusr_al :> ProgrammingLanguage
-  ; al_contr  : forall a b,     Rule [a,,a |= b ]  [    a |= b]
-  ; al_exch   : forall a b c,   Rule [a,,b |= c ]  [(b,,a)|= c]
-  ; al_weak   : forall a b,     Rule [[] |= b ]  [    a |= b]
-  }.
-  Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
-
-  (* languages with a fixpoint operator *)
-  Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) :=
-  { alwfpo_al := al
-  ; al_fix    : forall a b x,   Rule [a,,x |= b,,x]  [a |= b]
-  }.
-  Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage.
 
   Section LanguageCategory.
 
     Context (PL:ProgrammingLanguage).
 
     (* category of judgments in a fixed type/coercion context *)
-    Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv.
+    Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule al_eqv.
+
+    Definition JudgmentsL          := Judgments_cartesian.
 
     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
       unfold hom; simpl.
@@ -233,7 +111,7 @@ Section Programming_Language.
       apply al_subst.
       Defined.
 
-    Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
+    Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
       refine
       {| eid   := identityProof
        ; ecomp := cutProof
@@ -248,98 +126,107 @@ Section Programming_Language.
       apply al_subst_associativity'.
       Defined.
 
-    Definition TypesEnrichedInJudgments : Enrichment.
-      refine {| enr_c := TypesLFC |}.
-      Defined.
-
-    Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
-(*
+    Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
+      (*
       eapply Build_EFunctor; intros.
       eapply MonoidalCat_all_central.
       unfold eqv.
       simpl.
-*)
+      *)
       admit.
       Defined.
 
-    Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
+    Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x ).
       admit.
       Defined.
 
-    Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _).
+    Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
       refine
-        {| bin_first  := TypesL_first
-         ; bin_second := TypesL_second
+        {| bin_first  := Types_first
+         ; bin_second := Types_second
          |}.
       Defined.
 
-    Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal.
-      admit.
-      Defined.
-    Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing.
-      admit.
-      Defined.
-    Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor [].
-      admit.
-      Defined.
+    Definition TypesL_binoidal : BinoidalCat TypesL (@T_Branch _).
+    admit.
+    Defined.
 
-    Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
-      refine {| se_enr := TypesLEnrichedInJudgments0 |}.
-      simpl.
-      admit.
-      Defined.
+    Definition Types_PreMonoidal : PreMonoidalCat TypesL_binoidal [].
+    admit.
+    Defined.
 
-    Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
-      refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
-      simpl.
-      admit.
+    Definition TypesEnrichedInJudgments : Enrichment.
+      refine {| enr_c := TypesL |}.
       Defined.
 
-    Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
-      refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
-      admit.
-      admit.
+    Structure HasProductTypes :=
+    {
+    }.
+
+    (* need to prove that if we have cartesian tuples we have cartesian contexts *)
+    Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
       admit.
       Defined.
 
   End LanguageCategory.
-   
-  (*
-  Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) :=
-    FreydCategory (TypesL L) (TypesL L).
+
+  Structure ProgrammingLanguageSMME :=
+  { plsmme_pl   : ProgrammingLanguage
+  ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments plsmme_pl)
+  }.
+  Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
+
+  Section ArrowInLanguage.
+    Context  (Host:ProgrammingLanguageSMME).
+    Context `(CC:CartesianCat (me_mon Host)).
+    Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
+    Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
+      (* FIXME *)
+      (*
+      Definition ArrowInProgrammingLanguage := 
+        @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
+        *)
+  End ArrowInLanguage.
+
+  Section GArrowInLanguage.
+    Context (Guest:ProgrammingLanguageSMME).
+    Context (Host :ProgrammingLanguageSMME).
+    Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
+
+    (* FIXME
+    Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
     *)
+    Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
 
-  Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) :=
-    Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)).
+    Context (GuestHost:TwoLevelLanguage).
 
-  Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type :=
-  | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
-  | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
+    Definition FlatObject (x:TypesL Host) :=
+      forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 
-  Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
-    forall n:nat, NLevelLanguage n PL.
+    Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject.
 
-  Section TwoLevelLanguage.
-    Context `(L12:TwoLevelLanguage L1 L2).
+    Section Flattening.
 
-    Definition FlatObject (x:TypesL L2) :=
-      forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
+      Context  (F:Retraction (TypesL Host) FlatSubCategory).
+      Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
+      Lemma FlatteningIsNotDestructive : 
+        FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
+        admit.
+        Qed.
 
-    Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
+    End Flattening.
 
-    Context `(retraction      :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj).
-    Context `(retraction_inv  :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj).
-    Context  (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _).
+  End GArrowInLanguage.
 
-    Definition FlatteningOfReification :=
-      (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
-
-    Lemma FlatteningIsNotDestructive : 
-      FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12.
-      admit.
-      Qed.
+  Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
+  | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
+  | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
+    TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 
-  End TwoLevelLanguage.      
+  Definition OmegaLevelLanguage : Type :=
+    { f : nat -> ProgrammingLanguageSMME
+    & forall n, TwoLevelLanguage (f n) (f (S n)) }.
     
   Close Scope temporary_scope3.
   Close Scope al_scope.
@@ -349,146 +236,3 @@ Section Programming_Language.
 End Programming_Language.
 
 Implicit Arguments ND [ Judgment ].
-
-(*
-Open Scope nd_scope.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_suc_right.
-    intros; apply al_vert_expand_suc_r_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_suc_left.
-    intros; apply al_vert_expand_suc_l_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_ant_right.
-    intros; apply al_vert_expand_ant_r_respects; auto.
-    Defined.
-  Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
-  with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
-    as parametric_morphism_al_vert_expand_ant_left.
-    intros; apply al_vert_expand_ant_l_respects; auto.
-    Defined.
-Close Scope nd_scope.
-
-Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
-(*
-Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R :=
-  match seq with sequentpair a b => pair (f a) (f b) end.
-Implicit Arguments Judg [ ].
-*)
-
-
-(* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
-Section Programming_Language_Facts.
-
-  (* the ambient language about which we are proving facts *)
-  Context `(Lang : @ProgrammingLanguage T Rule).
-
-  (* just for this section *)
-  Open Scope nd_scope.
-  Open Scope al_scope.
-  Open Scope pf_scope.
-  Notation "H /⋯⋯/ C" := (@ND Judg Rule H C)     : temporary_scope4.
-  Notation "a === b"  := (@ndr_eqv _ _ al_eqv _ _ a b)                   : temporary_scope4.
-  Open Scope temporary_scope4.
-
-  Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang).
-  Existing Instance lang_al_eqv.
-
-  Ltac distribute :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?A ** ?B) ;; (?C ** ?D)] => 
-           setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
-      end
-      end.
-
-  Ltac sequentialize_product A B :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-      | context ct [(A ** B)] =>
-          setoid_replace (A ** B)
-        with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
-        (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
-    end end.
-  Ltac sequentialize_product' A B :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-      | context ct [(A ** B)] =>
-          setoid_replace (A ** B)
-        with (((nd_id _) ** B) ;; (A ** (nd_id _)))
-        (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
-    end end.
-  Ltac distribute' :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?A ;; ?B) ** (?C ;; ?D)] => 
-           setoid_rewrite (ndr_prod_preserves_comp A B C D)
-      end
-      end.
-  Ltac distribute_left_product_with_id :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(nd_id ?A) ** (?C ;; ?D)] => 
-           setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
-        [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
-      end
-      end.
-  Ltac distribute_right_product_with_id :=
-    match goal with
-     [ |- ?G ] =>
-      match G with
-        context ct [(?C ;; ?D) ** (nd_id ?A)] => 
-           setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
-        [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
-      end
-      end.
-
-  (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
-  Lemma al_subst_associativity'' : 
-    forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]]) 
-    (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
-    nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
-    nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
-    intros.
-      sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      distribute_right_product_with_id.
-      repeat setoid_rewrite ndr_comp_associativity.
-      set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
-      apply ndr_comp_respects; try reflexivity.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      apply ndr_comp_respects; try reflexivity.
-      sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
-      distribute_left_product_with_id.
-      repeat setoid_rewrite <- ndr_comp_associativity.
-      apply ndr_comp_respects; try reflexivity.
-      setoid_rewrite <- ndr_prod_preserves_comp.
-      repeat setoid_rewrite ndr_comp_left_identity.
-      repeat setoid_rewrite ndr_comp_right_identity.
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-    Qed.
-
-  Close Scope temporary_scope4.
-  Close Scope al_scope.
-  Close Scope nd_scope.
-  Close Scope pf_scope.
-  Close Scope isomorphism_scope.
-End Programming_Language_Facts.
-
-(*Coercion AL_SurjectiveEnrichment    : ProgrammingLanguage >-> SurjectiveEnrichment.*)
-(*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*)
-*)
\ No newline at end of file

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 4d83b78..eb6b5fd 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -9,6 +9,21 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+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.
+
+Instance CategoryOfReifications : Category SMME Reification.
+  admit.
+  Qed.
\ No newline at end of file

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 678de5c..8d94dca 100644 (file)
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -24,7 +24,7 @@ Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
 
-Definition reification_from_garrow (K:Enrichment) (C:MonoidalEnrichment) (garrow : GeneralizedArrow K C)
+Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
  : Reification K C (mon_i C).
   refine
   {| reification_r         := fun k:K => RepresentableFunctor K k >>>> garrow

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index a81c895..1b626a2 100644 (file)
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -83,4 +83,8 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
+  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
+    admit.
+    Qed.
+
 End ReificationsEquivalentToGeneralizedArrows.