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 Require Import InitialTerminal_ch2_2.
  26
  27 Open Scope nd_scope.
  28 Open Scope pf_scope.
  29
  30 (* proofs form a category, with judgment-trees as the objects *)
  31 Section Judgments_Category.
  32
  33   Context {Judgment : Type}.
  34   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
  35   Context (nd_eqv   : @ND_Relation Judgment Rule).
  36
  37   Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
  38
  39   Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) :=
  40   { id   := fun h          => nd_id _
  41   ; comp := fun a b c f g  => f ;; g
  42   ; eqv  := fun a b f g    => f === g
  43   }.
  44   intros; apply Build_Equivalence;
  45     [ unfold Reflexive; intros; reflexivity
  46     | unfold Symmetric; intros; symmetry; auto
  47     | unfold Transitive; intros; transitivity y; auto ].
  48   unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
  49   intros; apply ndr_comp_left_identity.
  50   intros; apply ndr_comp_right_identity.
  51   intros; apply ndr_comp_associativity.
  52   Defined.
  53
  54   Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category :=
  55     fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy).
  56   Definition Judgments_Category_monoidal_endofunctor_fmor :
  57            forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) ->
  58            ((Judgments_Category_monoidal_endofunctor_fobj a)
  59            ~~{Judgments_Category}~~>
  60            (Judgments_Category_monoidal_endofunctor_fobj b)).
  61      intros.
  62      destruct a.
  63      destruct b.
  64      destruct X.
  65      simpl in *.
  66      exact (h**h0).
  67      Defined.
  68   Definition Judgments_Category_monoidal_endofunctor
  69   : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj.
  70     refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl.
  71     abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto).
  72     abstract (destruct a; simpl in *; reflexivity).
  73     abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp).
  74     Defined.
  75
  76   Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
  77     refine
  78     {| iso_forward  := nd_assoc
  79      ; iso_backward := nd_cossa |};
  80     abstract (simpl; auto).
  81     Defined.
  82   Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
  83     refine
  84     {| iso_forward  := nd_cancelr
  85      ; iso_backward := nd_rlecnac |};
  86     abstract (simpl; auto).
  87     Defined.
  88   Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
  89     refine
  90     {| iso_forward  := nd_cancell
  91      ; iso_backward := nd_llecnac |};
  92     abstract (simpl; auto).
  93     Defined.
  94
  95   Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
  96     refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl.
  97     abstract (setoid_rewrite (ndr_prod_right_identity f);
  98               repeat setoid_rewrite ndr_comp_associativity;
  99               apply ndr_comp_respects; try reflexivity;
 100               symmetry;
 101               eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
 102               apply ndr_comp_respects; try reflexivity; simpl; auto).
 103     Defined.
 104   Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category.
 105     eapply Build_NaturalIsomorphism.
 106     instantiate (1:=fun x => jud_cancell_iso x).
 107     abstract (intros; simpl;
 108               setoid_rewrite (ndr_prod_left_identity f);
 109               repeat setoid_rewrite ndr_comp_associativity;
 110               apply ndr_comp_respects; try reflexivity;
 111               symmetry;
 112               eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
 113               apply ndr_comp_respects; try reflexivity; simpl; auto).
 114     Defined.
 115   Definition jud_mon_assoc_iso : forall X,
 116       (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>>
 117         Judgments_Category_monoidal_endofunctor) X) ≅
 118        (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>>
 119          Judgments_Category_monoidal_endofunctor))) X.
 120     intros.
 121     destruct X as [a c].
 122     destruct a as [a b].
 123     exact (jud_assoc_iso a b c).
 124     Defined.
 125   Definition jud_mon_assoc   :
 126     ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
 127     <~~~>
 128     func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
 129     refine {| ni_iso := jud_mon_assoc_iso |}.
 130     intros.
 131     unfold hom in *.
 132     destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *.
 133     destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *.
 134     destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *.
 135     unfold hom in *.
 136     unfold ob in *.
 137     unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
 138     setoid_rewrite ndr_prod_associativity.
 139     setoid_rewrite ndr_comp_associativity.
 140     setoid_rewrite ndr_comp_associativity.
 141     apply ndr_comp_respects; try reflexivity.
 142     etransitivity.
 143     symmetry.
 144     apply ndr_comp_right_identity.
 145     apply ndr_comp_respects; try reflexivity.
 146     apply ndr_structural_indistinguishable; 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     abstract
 154       (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
 155         apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto).
 156     abstract
 157       (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl;
 158         apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto).
 159     Defined.
 160
 161   Instance Judgments_Category_Terminal : Terminal Judgments_Category.
 162     refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}.
 163       abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant).
 164     Defined.
 165
 166   Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
 167     refine {| copy_nt := _ |}.
 168     intros.
 169     refine {| nt_component := nd_copy |}.
 170     intros.
 171     unfold hom in *; unfold ob in *; unfold eqv.
 172     simpl.
 173     rewrite ndr_prod_preserves_copy; auto.
 174     reflexivity.
 175     Defined.
 176
 177   Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
 178     refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
 179       ; car_one := iso_id [] |}
 180       ; intros; unfold hom; simpl
 181       ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
 182
 183     apply ndr_structural_indistinguishable; auto.
 184     apply nd_structural_comp; auto.
 185     apply nd_structural_comp; auto.
 186     unfold copy; simpl; apply nd_structural_copy; auto.
 187     apply nd_structural_prod; auto.
 188     apply nd_structural_comp; auto.
 189     apply weak'_structural.
 190     apply nd_structural_id0; auto.
 191     apply nd_structural_cancell; auto.
 192
 193     apply ndr_structural_indistinguishable; auto.
 194     apply nd_structural_comp; auto.
 195     apply nd_structural_comp; auto.
 196     unfold copy; simpl; apply nd_structural_copy; auto.
 197     apply nd_structural_prod; auto.
 198     apply nd_structural_comp; auto.
 199     apply weak'_structural.
 200     apply nd_structural_id0; auto.
 201     apply nd_structural_cancelr; auto.
 202     Defined.
 203
 204   (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
 205    * this asserts that we have sensible structural rules with respect
 206    * to that mapping.  Doing all of this "with respect to a mapping"
 207    * lets us avoid duplicating code for both the antecedent and
 208    * succedent of sequent deductions. *)
 209   Class TreeStructuralRules  {T:Type}(rep:Tree ??T -> Judgment) :=
 210   { tsr_eqv           : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
 211   ; tsr_ant_assoc     : forall {a b c}, Rule [rep ((a,,b),,c)]     [rep ((a,,(b,,c)))]
 212   ; tsr_ant_cossa     : forall {a b c}, Rule [rep (a,,(b,,c))]     [rep (((a,,b),,c))]
 213   ; tsr_ant_cancell   : forall {a    }, Rule [rep (  [],,a  )]     [rep (        a  )]
 214   ; tsr_ant_cancelr   : forall {a    }, Rule [rep (a,,[]    )]     [rep (        a  )]
 215   ; tsr_ant_llecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  [],,a    )]
 216   ; tsr_ant_rlecnac   : forall {a    }, Rule [rep (      a  )]     [rep (  a,,[]    )]
 217   }.
 218
 219   Section Sequents.
 220     Context {S:Type}.   (* type of sequent components *)
 221     Context (sequent:S->S->Judgment).
 222     Notation "a |= b" := (sequent a b).
 223
 224     Class SequentCalculus :=
 225     { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ]
 226     }.
 227
 228     Class CutRule :=
 229     { nd_cutrule_seq       :> SequentCalculus
 230     ; nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
 231     ; nd_cut_associativity :  forall {a b c d},
 232       ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d)
 233         ===
 234         nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d))
 235     ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
 236     ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
 237     }.
 238   End Sequents.
 239
 240   (* Structure ExpressionAlgebra (sig:Signature) := *)
 241
 242 End Judgments_Category.
 243
 244 Close Scope pf_scope.
 245 Close Scope nd_scope.