The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Dear coq-admin,
  I obtained a message of the form 

Error while reading /tmp/coqc0.v :
File "./categories1.v", line 272, characters 0-50
Search error.
If this is in user-written tactic code, then it needs to be modified.
If this is in system code, then it needs to be reported.

Thus, I am reporting this. In fact we were only able to install an
old system:
 Welcome to Coq V6.2.1 (July 1998)
so whatever the problem is it has probably been fixed since then,
in which case I'm sorry to bother you with this. 

THe file in question is attached, called categories1.v

On another register the question I posted to coq-club the other day
was motivated by the following type of problem which I suppose you know
about but again just in case, here it is: the ambiguity in indexing Type
can cause the following problem: you might be able to prove a result
in one file and might want to transpose it to another file as an axiom;
but this can cause an inconsistency if the word Type occurs two or more
times in the proposition in question. I have an example in 
the other file called problem.v (the example is incomplete because
it needs a proof of Russell's paradox but I suppose that this exists).
Try compiling it two times, one with line AAA commented out and the other
with line AAA included.

There is no hurry for these questions because I will not be here next week
(vacation).

Sincerely,
 Carlos Simpson
(working with Andre' Hirschowitz, trying to learn Coq...)




Definition Type2 := Type.
Definition Type1 : Type2 := Type.


Definition DOESNT_EXIST := [A:Type][P:A-> Prop] (a:A) ((P a) -> False).

(* Here is existence *)
Definition EXISTS : (A:Type)(P:A->Prop)Prop 
        := [A:Type][P:A->Prop](DOESNT_EXIST A P)-> False.
        
(* Here is the type of thing which illustrates how to obtain a problem
if you don't use the above type indexing convention *)

        
Definition strange_prop : Prop := (A : Type) (EXISTS Type ([B:Type] (A == B)) 
).

Section now_we_prove_it_locally.

Variable A : Type.
Local Q: Type -> Prop := ([B:Type] (A == B)).
Variable hyp : (DOESNT_EXIST Type Q).
Local hyp2 : (a: Type) ((Q a) -> False) := hyp.
Local step1 : ((Q A) -> False) := (hyp2 A).
Local step2 : (Q A) := (refl_eqT Type A).
Definition step3 : False := (step1 step2).

End now_we_prove_it_locally.

(* The following line is denoted AAA below 
---if you remove the comments then it compiles, saying that
strange_prop can be proved   *)
(*
Definition strange_prop_proof : strange_prop := step3. 
*)


Axiom strange_axiom : strange_prop.


Definition p :(EXISTS Type ([B:Type]Type1==B)) := (strange_axiom Type1).



(* it seems to me that one can prove the following 
statement using Russell's paradox if excluded middle is assumed *)
(* of course my example isnt complete until I furnish this proof! *)
(* Note however that following Werner's principle the projection of this
statement into ZFC_2 is certainly consistent...*)


Parameter contra : (DOESNT_EXIST Type1 ([B:Type1]Type1==B)  ).

(* If line AAA is commented out then the following line goes through;
however if line AAA is put in then the following line generates
a UI.  *)

Local strange_conclusion : False := (p contra).



(* The following trick was suggested by Alexandre Miquel
Alexandre.Miquel AT inria.fr
  on the coq-club mailing list *)

Definition Type4 := Type.
Definition Type3 : Type4 := Type.
Definition Type2 : Type3 := Type.
Definition Type1 : Type2 := Type.


Definition EQ  :=
[A:Type4] [a,b:A] (P: A-> Prop) (P a) -> (P b).

Definition not := [P:Prop] P -> False. 

Axiom excluded_middle : (P: Prop) (not (not P)) -> P.


Definition DOESNT_EXIST := [A:Type4][P:A-> Prop] (a:A) ((P a) -> False).

(* Here is existence *)
Definition EXISTS : (A:Type4)(P:A->Prop)Prop 
        := [A:Type4][P:A->Prop] (DOESNT_EXIST A P)-> False.
        
(* now we take as an axiom a universal choice function *)


Axiom CHOICE : (A:Type4)(P: A->Prop)(h:(EXISTS A P))A.
Axiom CHOICE_pr : (A:Type4)(P: A->Prop)(h:(EXISTS A P))(P (CHOICE A P h)).

(* syntax example : given a type A, a property P and proof h of *)
(* nonempty_property A P, then we obtain the construction b:= (CHOICE A P h) 
: A, *)
(* together with CHOICE_pr : (P b).   *)




(* aaaLemma_EQ_symmetric : we prove that (A: Type4) (a,b : A) (EQ A a b) -> 
(EQ A b a). *)

Section aaa1.
Variable A:Type4.
Variable a:A.
Variable b:A.
Variable hyp: (EQ A a b).
        Section aaa1a.
        Variable contra: (EQ A b a ) -> False.
                Section aaa1a1.
                Variable P: A-> Prop.
                Variable hyp2 : (P b).
                Section aaa1a1a.
                        Variable contra2 : (P a)-> False.
                        Local Q := [x:A] (( P x) -> False ).
                        Local Step1 : (Q a) -> (Q b) := (hyp Q).
                        Local Step2 : (Q b) := (Step1 contra2).
                        Definition aaa1a1aOut : False := (Step2 hyp2).
                        End aaa1a1a.
                Local Step3 : ((P a)-> False)-> False := aaa1a1aOut.
                Definition aaa1a1Out : (P a) := (excluded_middle (P a) Step3).
                End aaa1a1.
        Local Step4 : (P: A-> Prop) ((P b) -> (P a)) := aaa1a1Out.
        Definition aaa1aOut : False := (contra Step4).
        End aaa1a.
Definition Step5 : ((EQ A b a) -> False) -> False := aaa1aOut.
Definition aaa1Out: (EQ A b a) := (excluded_middle (EQ A b a) Step5).
End aaa1.
Definition aaaLemma_EQ_symmetric : (A:Type4) (a,b:A) (EQ A a b) -> (EQ A b a) 
:= aaa1Out.


(* aabLemma_EQ_reflexive : we prove that (A: Type4) (a : A) (EQ A a a). *)
(* note that (EQ A a a) = (P: A-> Prop) (P a) -> (P a). *)

Section aab1a.
Variable A:Type4.
Variable a:A.
        Section aab1a1.
        Variable P: A -> Prop.
        Variable hyp : (P a).
        Definition aab1a1Out : (P a) := hyp.
        End aab1a1.
Definition aab1aOut : (EQ A a a) := aab1a1Out.
End aab1a.
Definition aabLemma_EQ_reflexive : (A:Type4) (a:A) (EQ A a a) := aab1aOut.

(* aacLemma_EQ_transitive : we prove that (A: Type4) (a,b,c: A) *)
(* ((EQ A a b) ->(EQ A b c)->(EQ A a c)). *)


Section aac1.
Variable A:Type4.
Variable a:A. Variable b:A. Variable c:A.
Variable hyp1 : (EQ A a b).
Variable hyp2 : (EQ A b c).
        Section aac1a1.
        Variable P: A -> Prop.
        Variable hyp3: (P a).
        Local Step1 : (P b) := (hyp1 P hyp3).
        Definition aac1a1Out : (P c) := ( hyp2 P Step1).
        End aac1a1.
Definition aac1Out : (EQ A a c) := aac1a1Out.
End aac1.
Definition aacLemma_EQ_transitive : (A: Type4) (a,b,c: A) 
((EQ A a b) ->(EQ A b c)->(EQ A a c)) := aac1Out.



(* Injectivity --- for all a,b : A, fa equals fb implies a equals b *)

Definition INJ := [A,B:Type4][f:A-> B] (a,b:A) ( (EQ B (f a) (f b)) -> (EQ A 
a b) ).



(* Surjectivity --- for all b:B there exists a:A with fa equal b *)


Definition SURJ := [A,B:Type4][f:A->B] ((b:B) ( EXISTS A ([a:A](EQ B (f a) 
b))  )).


(* Bijectivity ---injective and surjective NB : ``and'' is written  /\ *)
Definition BIJ := [A,B:Type4][f:A->B] ( (INJ A B f) /\ (SURJ A B f)).

(* Now we define a function SECTION of a surjection, its easier to do *)
(* this using a Section aad. *)

Section aad.
Variable A: Type4. Variable B: Type4. Variable f: A-> B. Variable h: (SURJ A 
B f).
Variable b:B. 
Local ourP :A-> Prop := [a:A](EQ B (f a) b).
Local step1 :  (EXISTS A ourP)  := (h b). 
Definition aadOut1 :A :=  (CHOICE A ourP step1).
Definition aadOut2 : (ourP aadOut1) := (CHOICE_pr A ourP step1).
End aad.

Definition SECTION : (A,B: Type4)(f:A->B)(h:(SURJ A B f))(b:B) A 
        := aadOut1.

Definition SECTION_pr : (A,B: Type4)(f:A->B)(h:(SURJ A B f))(b:B) 
        (EQ B (f (SECTION A B f h b)) b) := aadOut2.
        
(* Syntax: SECTION A B f h b  is an element of a and SECTION_pr is a proof 
        of (EQ B (f (SECTION A B f h b)) b). 
        Note that here, h is a proof of SURJ A B f.  *)



(* The system didnt accept the line 
Record big_category_pre : Type3 := {   *)

(* This may have been what Miquel was refering to in his message
when he said ``This trick does not solve all the problems...'' ??? *)


Record big_category_pre : Type := {
bOb : Type2;
bMor : (X, Y : bOb) Type1;
bComp : (X,Y,Z: bOb)(f: (bMor X Y))(g: (bMor Y Z)) (bMor X Z);
        (* note that composition is in the arrow order rather than the
                usual order *)
bId : (X : bOb) (bMor X X);
        (* the meaning of leftunit and right unit is changed by the
                change in the order of the composition *)
bId_leftunit : (X,Y: bOb)(f: (bMor X Y)) 
        (EQ (bMor X Y) f (bComp X X Y (bId X) f)  );
bId_rightunit : (X,Y: bOb)(f: (bMor X Y)) 
        (EQ (bMor X Y) f (bComp X Y Y f (bId Y) )  );
bComp_assoc : (X,Y,Z,W : bOb) 
        (f: (bMor X Y)) (g: (bMor Y Z)) (h: (bMor Z W))
        (EQ (bMor X W) 
          (bComp X Y W f (bComp Y Z W g h))  (bComp X Z W (bComp X Y Z f g) 
h))
}.

(* Because of the above problem, now we force this to Type3 *)


Definition big_category : Type3 := big_category_pre.
Definition Build_big_category := Build_big_category_pre.

(* now we assign long names to the objects too *)
Definition big_category_Ob := bOb.
Definition big_category_Mor := bMor.
Definition big_category_Comp := bComp.
Definition big_category_Id := bId.
Definition big_category_Id_leftunit := bId_leftunit.
Definition big_category_Id_rightunit := bId_rightunit.
Definition big_category_Comp_assoc := bComp_assoc.


        
Record small_category_pre : Type := {
sOb : Type1;
sMor : (X, Y : sOb) Type1;
sComp : (X,Y,Z: sOb)(f: (sMor X Y))(g: (sMor Y Z)) (sMor X Z);
        (* note that composition is in the arrow order rather than the
                usual order *)
sId : (X : sOb) (sMor X X);
        (* the meaning of leftunit and right unit is changed by the
                change in the order of the composition *)
sId_leftunit : (X,Y: sOb)(f: (sMor X Y)) 
        (EQ (sMor X Y) f (sComp X X Y (sId X) f)  );
sId_rightunit : (X,Y: sOb)(f: (sMor X Y)) 
        (EQ (sMor X Y) f (sComp X Y Y f (sId Y) )  );
sComp_assoc : (X,Y,Z,W : sOb) 
        (f: (sMor X Y)) (g: (sMor Y Z)) (h: (sMor Z W))
        (EQ (sMor X W) 
          (sComp X Y W f (sComp Y Z W g h))  (sComp X Z W (sComp X Y Z f g) 
h))
}.

(* Now we force this to Type2 *)
Definition small_category : Type2 := small_category_pre.
Definition Build_small_category := Build_small_category_pre.

(* now we assign long names to the objects too *)
Definition small_category_Ob := sOb.
Definition small_category_Mor := sMor.
Definition small_category_Comp := sComp.
Definition small_category_Id := sId.
Definition small_category_Id_leftunit := sId_leftunit.
Definition small_category_Id_rightunit := sId_rightunit.
Definition small_category_Comp_assoc := sComp_assoc.


(* Here is an interesting question: is a small category also a big one?
*)
(*
Section is_a_small_category_a_big_one.

Variable C : small_category.
Local C_considered_as_big : big_category := C.

End is_a_small_category_a_big_one.
*)
(* No that didnt work so it was commented out *)


(* Assuming that the answer to the previous question is no, we need
to define a construction small_to_big_category 
for this we assume that the inclusion Type1 in Type2 works ok *)

(* the reader should note that the names of sections have absolutely
        no mathematical content for the machine, they are just chosen
        for the reader's convenience   *)

Section for_definition_of_small_to_big.
Variable C : small_category.
Local ob : Type2 := (sOb C).
Local mor := (sMor C).
Local comp := (sComp C).
Local id := (sId C).
Local id_lu := (sId_leftunit C).
Local id_ru := (sId_rightunit C).
Local assoc := (sComp_assoc C).

Definition small_to_big_Out : big_category := 
        (Build_big_category ob mor comp id id_lu id_ru assoc).

End for_definition_of_small_to_big.

Definition small_to_big_category : (C: small_category) big_category :=
        small_to_big_Out.

(* here it would be good to see how things work such as the fact that
the composition is the same in C and in (small_to_big_category C)   
this might be by strict equality or it might be that we need to prove a 
theorem; to check this out we will do a test section  *)

Section small_to_big_test1.
Variable C : small_category.
Local D := (small_to_big_category C).
Variable X : (sOb C).
Variable Y : (sOb C).
Variable Z : (sOb C).
Variable f: ((sMor C) X Y).
Variable g: ((sMor C) Y Z).
Local h : ((sMor C) X Z) := ((sComp C) X Y Z f g).

(* ------ the above line generated the message 

Error while reading /tmp/coqc0.v :
File "./categories1.v", line 272, characters 0-50
Search error.
If this is in user-written tactic code, then it needs to be modified.
If this is in system code, then it needs to be reported.


------ in particular the rest of the code was not compiled  
and my further comments are not relevant  

-----NOTA  we have an old system --- here is the coqtop prefix   
    
Welcome to Coq V6.2.1 (July 1998)
No .coqrc or .coqrc.6.2.1 found. Skipping rcfile loading.
Coq < 

        
so I suppose that this problem is resolved in the current system. I am sending
the file just in case...

*)

Local X1 : (bOb D) := X.
Local Y1 : (bOb D) := Y.
Local Z1 : (bOb D) := Z.
Local f1 : ((bMor D) X1 Y1) := f.
Local g1 : ((bMor D) Y1 Z1) := g.
Local h1 : ((bMor D) X1 Z1) := ((bComp D) X1 Y1 Z1 f1 g1).
        (* the following line tries to show that we didnt even need to 
redefine
                X1 etc   *)
Local h2 : ((bMor D) X1 Z1) := ((bComp D) X Y Z f g).
Local h3 : ((bMor D) X1 Z1) := h. 

(* Now we demonstrate that h1 equals h2 equals h3 by substituting them
        for each other in an expression; we use a proposition as a test 
        note that this could easily be turned into a proof of 
        (EQ ? h1 h2) and (EQ ? h2 h3) and in fact it shows--I hope--that the
        system considers h1, h2 and h3 (and indeed h) as identical. 
*)

Variable P : ((bMor D) X1 Z1) -> Prop.
Variable pr : (P h1).
Local pr2 : (P h2) := pr.
Local pr3 : (P h3) := pr.
Local pr4 : (P h) := pr. 



End  small_to_big_test1.
        

(* Now we define functors, starting with the case of small categories 
        for convenience we do it in a section *)

(* First, and to illustrate how one can simplify notation, we redefine
        the notation for small categories taking out the prefix s  
        but only locally in a section  ---this also illustrates why
        we did the original redefinition to long names because here
        it becomes more explanational and since we are redefining anyway
        we didnt need the short names *)

Section notational_simplification_for_small_categories.

Local Ob := small_category_Ob.
Local Mor := small_category_Mor.
Local Comp := small_category_Comp.
Local Id := small_category_Id.
Local Id_leftunit := small_category_Id_leftunit.
Local Id_rightunit := small_category_Id_rightunit.
Local Comp_assoc := small_category_Comp_assoc.



Section for_defining_functors_on_small_categories.

Variable A : small_category.
Variable B : small_category. 

Record small_functor : Type1 := {
        ObF : (Ob A) -> (Ob B);
        MorF : (X,Y: (Ob A)) 
                ( ((Mor A) X Y) -> ((Mor B) (ObF X) (ObF Y))  );
        IdF : (X : (Ob A)) 
( EQ ((Mor B) (ObF X) (ObF X))
                ((Id B) (ObF X)) (*equals*) (MorF X X ((Id A) X))  
);

(* NB the comment ``equals'' in the previous line has no
mathematical content and is put in for lisibility  *)

        AssocF : (X,Y,Z: (Ob A))(f: ((Mor A) X Y))(g: ((Mor A) Y Z)
(               
EQ ((Mor B) (ObF X) (ObF Z))
        (MorF (ObF X) (ObF Z) ((Comp A) X Y Z f g)) 
                        (* equals *)
        ((Comp B) (ObF X) (ObF Y) (ObF Z) (MorF X Y f) (MorF Y Z g))  
)
        

}.


End for_defining_functors_on_small_categories.

(* now we should do a notational test to discover the actual type of 
the resulting object small_functor    *)




End notational_simplification_for_small_categories.

(* we should redo a notational test to go back to the original notation
        although here we go back to the original short names sOb etc *)