src/NaturalDeductionCategory.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeductionCategory:                                                                                                     *)
   3 (*                                                                                                                               *)
   4 (*   Natural Deduction proofs form a category (under mild assumptions, see below)                                                *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12
  13 Require Import Algebras_ch4.
  14 Require Import Categories_ch1_3.
  15 Require Import Functors_ch1_4.
  16 Require Import Isomorphisms_ch1_5.
  17 Require Import ProductCategories_ch1_6_1.
  18 Require Import OppositeCategories_ch1_6_2.
  19 Require Import Enrichment_ch2_8.
  20 Require Import Subcategories_ch7_1.
  21 Require Import NaturalTransformations_ch7_4.
  22 Require Import NaturalIsomorphisms_ch7_5.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25
  26 Open Scope nd_scope.
  27 Open Scope pf_scope.
  28
  29 (* proofs form a category, with judgment-trees as the objects *)
  30 Section Judgments_Category.
  31
  32   Context {Judgment : Type}.
  33   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
  34   Context (nd_eqv   : @ND_Relation Judgment Rule).
  35
  36   (* actually you can use any type as the objects, so long as you give a mapping from that type to judgments *)
  37   Context {Ob       : Type}.
  38   Context (ob2judgment : Ob -> Judgment).
  39   Coercion ob2judgment : Ob >-> Judgment.
  40
  41   Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
  42
  43   Instance Judgments_Category
  44     : Category (Tree ??Ob) (fun h c => (mapOptionTree ob2judgment h) /⋯⋯/ (mapOptionTree ob2judgment c)) :=
  45   { id   := fun h          => nd_id _
  46   ; comp := fun a b c f g  => f ;; g
  47   ; eqv  := fun a b f g    => f === g
  48   }.
  49   intros; apply Build_Equivalence;
  50     [ unfold Reflexive; intros; reflexivity
  51     | unfold Symmetric; intros; symmetry; auto
  52     | unfold Transitive; intros; transitivity y; auto ].
  53   unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
  54   intros; apply ndr_comp_left_identity.
  55   intros; apply ndr_comp_right_identity.
  56   intros; apply ndr_comp_associativity.
  57   Defined.
  58
  59   Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
  60     (fun xy =>
  61      match xy with
  62      | pair_obj x y => T_Branch x y
  63      end).
  64   Definition Judgments_Category_monoidal_endofunctor_fmor :
  65            forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
  66            ((Judgments_Category_monoidal_endofunctor_fobj a)
  67            ~~{Judgments_Category}~~>
  68            (Judgments_Category_monoidal_endofunctor_fobj b)).
  69      intros.
  70      destruct a.
  71      destruct b.
  72      destruct X.
  73      exact (h**h0).
  74      Defined.
  75   Definition Judgments_Category_monoidal_endofunctor
  76   : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj.
  77     refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl.
  78     abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto).
  79     abstract (destruct a; simpl in *; reflexivity).
  80     abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp).
  81     Defined.
  82
  83   Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
  84     apply (@Build_Isomorphic _ _ Judgments_Category _ _
  85       (@nd_assoc _ Rule  (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
  86         : (a,, b),, c ~~{Judgments_Category}~~> a,, (b,, c))
  87       (@nd_cossa _ Rule  (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c)
  88         : a,, (b,, c) ~~{Judgments_Category}~~> (a,, b),, c)); simpl; auto.
  89     Defined.
  90   Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
  91     apply (@Build_Isomorphic _ _ Judgments_Category _ _
  92       (@nd_cancelr _ Rule (mapOptionTree ob2judgment a) : a,,[] ~~{Judgments_Category}~~> a)
  93       (@nd_rlecnac _ Rule (mapOptionTree ob2judgment a) : a     ~~{Judgments_Category}~~> a,,[])); simpl; auto.
  94     Defined.
  95   Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
  96     apply (@Build_Isomorphic _ _ Judgments_Category _ _
  97       (@nd_cancell _ Rule (mapOptionTree ob2judgment a) : [],,a ~~{Judgments_Category}~~> a)
  98       (@nd_llecnac _ Rule (mapOptionTree ob2judgment a) : a     ~~{Judgments_Category}~~> [],,a)); simpl; auto.
  99     Defined.
 100
 101   Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
 102     refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
 103     setoid_rewrite (ndr_prod_right_identity f).
 104     repeat setoid_rewrite ndr_comp_associativity.
 105     apply ndr_comp_respects; try reflexivity.
 106     symmetry.
 107     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 108     apply ndr_comp_respects; try reflexivity; simpl; auto.
 109     Defined.
 110   Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
 111     eapply Build_NaturalIsomorphism.
 112     instantiate (1:=fun x => jud_cancell_iso x).
 113     intros; simpl.
 114     setoid_rewrite (ndr_prod_left_identity f).
 115     repeat setoid_rewrite ndr_comp_associativity.
 116     apply ndr_comp_respects; try reflexivity.
 117     symmetry.
 118     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 119     apply ndr_comp_respects; try reflexivity; simpl; auto.
 120     Defined.
 121   Definition jud_mon_assoc_iso :
 122     forall X,
 123       (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) X) ≅
 124   (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor))) X.
 125     intros.
 126     destruct X as [a c].
 127     destruct a as [a b].
 128     apply (jud_assoc_iso a b c).
 129     Defined.
 130   Definition jud_mon_assoc   :
 131     ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
 132     <~~~>
 133     func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
 134     refine {| ni_iso := jud_mon_assoc_iso |}.
 135     intros.
 136     destruct A as [a1 a3]. destruct a1 as [a1 a2].
 137     destruct B as [b1 b3]. destruct b1 as [b1 b2].
 138     destruct f as [f1 f3]. destruct f1 as [f1 f2].
 139     simpl.
 140     setoid_rewrite ndr_prod_associativity.
 141     setoid_rewrite ndr_comp_associativity.
 142     setoid_rewrite ndr_comp_associativity.
 143     apply ndr_comp_respects; try reflexivity.
 144     symmetry.
 145     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 146     apply ndr_comp_respects; try reflexivity; simpl; auto.
 147     Defined.
 148
 149   Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] :=
 150   { mon_cancelr := jud_mon_cancelr
 151   ; mon_cancell := jud_mon_cancell
 152   ; mon_assoc   := jud_mon_assoc   }.
 153     apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto.
 154     apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto.
 155     Defined.
 156
 157   Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
 158     admit.
 159     Defined.
 160
 161   (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
 162    * this asserts that we have sensible structural rules with respect
 163    * to that mapping.  Doing all of this "with respect to a mapping"
 164    * lets us avoid duplicating code for both the antecedent and
 165    * succedent of sequent deductions. *)
 166   Class TreeStructuralRules  {T:Type}(rep:Tree ??T -> Judgment) :=
 167   { tsr_eqv           : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
 168   ; tsr_ant_assoc     : forall {a b c}, Rule [rep ((a,,b),,c)]     [rep ((a,,(b,,c)))]
 169   ; tsr_ant_cossa     : forall {a b c}, Rule [rep (a,,(b,,c))]     [rep (((a,,b),,c))]
 170   ; tsr_ant_cancell   : forall {a    }, Rule [rep (  [],,a  )]     [rep (        a  )]
 171   ; tsr_ant_cancelr   : forall {a    }, Rule [rep (a,,[]    )]     [rep (        a  )]
 172   ; tsr_ant_llecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  [],,a    )]
 173   ; tsr_ant_rlecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  a,,[]    )]
 174   }.
 175
 176
 177   (* Structure ExpressionAlgebra (sig:Signature) := *)
 178
 179 End Judgments_Category.
 180
 181 Close Scope pf_scope.
 182 Close Scope nd_scope.