--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
projects / coq-hetmet.git / blobdiff