Nested Sections not quite working #16

New issue

Closed

opened 2024-12-08 19:25:13 -08:00 by wball · 1 comment

wball commented

2024-12-08 19:25:13 -08:00

Owner

I was starting to formalize some basic category theory using sections, and found a bug in the section mechanism.

Here's the relevant code:

@include logic.pg
section Category
    variable
        (Obj  : *)
        (Hom  : Obj -> Obj -> *)
        (id   : forall (A     : Obj), Hom A A)
        (comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C);

    hypothesis
        (id_l  : forall (A B     : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f)
        (id_r  : forall (A B     : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f)
        (assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D),
            eq (Hom A D)
                (comp A B D f (comp B C D g h))
                (comp A C D (comp A B C f g) h));

    section Inverses
        variable
            (A B : Obj)
            (f : Hom A B)
            (g : Hom B A);

        def inv_l := eq (Hom A A) (comp A B A f g) (id A);
        def inv_r := eq (Hom B B) (comp B A B g f) (id B);

        def inv := and inv_l inv_r;
    end Inverses

    def isomorphic (A B : Obj) :=
        exists (Hom A B) (fun (f : Hom A B) =>
            exists (Hom B A) (fun (g : Hom B A) => 
                inv A B f g));
end Category

The line in question is inv A B f g. This does not type check, though it is supposed to. In order to get it to type check, I have to insert inv Obj Hom id comp A B f g. The problem is that, when exiting a nested section, definitions that depend on section variables from the outer section should not be removed from the SectionContext. This means the saveState function will need to be smarter at least.

I was starting to formalize some basic category theory using sections, and found a bug in the section mechanism. Here's the relevant code: ```perga @include logic.pg section Category variable (Obj : *) (Hom : Obj -> Obj -> *) (id : forall (A : Obj), Hom A A) (comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C); hypothesis (id_l : forall (A B : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f) (id_r : forall (A B : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f) (assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D), eq (Hom A D) (comp A B D f (comp B C D g h)) (comp A C D (comp A B C f g) h)); section Inverses variable (A B : Obj) (f : Hom A B) (g : Hom B A); def inv_l := eq (Hom A A) (comp A B A f g) (id A); def inv_r := eq (Hom B B) (comp B A B g f) (id B); def inv := and inv_l inv_r; end Inverses def isomorphic (A B : Obj) := exists (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (fun (g : Hom B A) => inv A B f g)); end Category ``` The line in question is `inv A B f g`. This does not type check, though it is supposed to. In order to get it to type check, I have to insert `inv Obj Hom id comp A B f g`. The problem is that, when exiting a nested section, definitions that depend on section variables from the outer section should not be removed from the `SectionContext`. This means the `saveState` function will need to be smarter at least.