1 (*********************************************************************************************************************************)
2 (* NaturalDeductionCategory: *)
4 (* Natural Deduction proofs form a category (under mild assumptions, see below) *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
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.
30 (* proofs form a category, with judgment-trees as the objects *)
31 Section Judgments_Category.
33 Context {Judgment : Type}.
34 Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
35 Context (nd_eqv : @ND_Relation Judgment Rule).
37 Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2).
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
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.
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)).
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).
76 Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)).
78 {| iso_forward := nd_assoc
79 ; iso_backward := nd_cossa |};
80 abstract (simpl; auto).
82 Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a.
84 {| iso_forward := nd_cancelr
85 ; iso_backward := nd_rlecnac |};
86 abstract (simpl; auto).
88 Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a.
90 {| iso_forward := nd_cancell
91 ; iso_backward := nd_llecnac |};
92 abstract (simpl; auto).
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;
101 eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
102 apply ndr_comp_respects; try reflexivity; simpl; auto).
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;
112 eapply transitivity; [ idtac | apply ndr_comp_right_identity ];
113 apply ndr_comp_respects; try reflexivity; simpl; auto).
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.
123 exact (jud_assoc_iso a b c).
125 Definition jud_mon_assoc :
126 ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor)
128 func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)).
129 refine {| ni_iso := jud_mon_assoc_iso |}.
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 *.
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.
144 apply ndr_comp_right_identity.
145 apply ndr_comp_respects; try reflexivity.
146 apply ndr_structural_indistinguishable; auto.
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 }.
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).
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).
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).
166 Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal.
167 apply Build_DiagonalCat.
168 intros; unfold bin_obj; simpl; unfold hom; simpl; apply nd_copy.
171 Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal.
172 refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal
173 ; car_one := iso_id [] |}
174 ; intros; unfold hom; simpl
175 ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl.
177 apply ndr_structural_indistinguishable; auto.
178 apply nd_structural_comp; auto.
179 apply nd_structural_comp; auto.
180 apply nd_structural_copy; auto.
181 apply nd_structural_prod; auto.
182 apply nd_structural_comp; auto.
183 apply weak'_structural.
184 apply nd_structural_id0; auto.
185 apply nd_structural_cancell; auto.
187 apply ndr_structural_indistinguishable; auto.
188 apply nd_structural_comp; auto.
189 apply nd_structural_comp; auto.
190 apply nd_structural_copy; auto.
191 apply nd_structural_prod; auto.
192 apply nd_structural_comp; auto.
193 apply weak'_structural.
194 apply nd_structural_id0; auto.
195 apply nd_structural_cancelr; auto.
198 (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment,
199 * this asserts that we have sensible structural rules with respect
200 * to that mapping. Doing all of this "with respect to a mapping"
201 * lets us avoid duplicating code for both the antecedent and
202 * succedent of sequent deductions. *)
203 Class TreeStructuralRules {T:Type}(rep:Tree ??T -> Judgment) :=
204 { tsr_eqv : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2)
205 ; tsr_ant_assoc : forall {a b c}, Rule [rep ((a,,b),,c)] [rep ((a,,(b,,c)))]
206 ; tsr_ant_cossa : forall {a b c}, Rule [rep (a,,(b,,c))] [rep (((a,,b),,c))]
207 ; tsr_ant_cancell : forall {a }, Rule [rep ( [],,a )] [rep ( a )]
208 ; tsr_ant_cancelr : forall {a }, Rule [rep (a,,[] )] [rep ( a )]
209 ; tsr_ant_llecnac : forall {a }, Rule [rep ( a )] [rep ( [],,a )]
210 ; tsr_ant_rlecnac : forall {a }, Rule [rep ( a )] [rep ( a,,[] )]
214 Context {S:Type}. (* type of sequent components *)
215 Context (sequent:S->S->Judgment).
216 Notation "a |= b" := (sequent a b).
218 Class SequentCalculus :=
219 { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ]
223 { nd_cutrule_seq :> SequentCalculus
224 ; nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
225 ; nd_cut_associativity : forall {a b c d},
226 ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d)
228 nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d))
229 ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
230 ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr
234 (* Structure ExpressionAlgebra (sig:Signature) := *)
236 End Judgments_Category.
238 Close Scope pf_scope.
239 Close Scope nd_scope.