Logic

The logic file contains impredicative encodings of ``and'', ``or'' ``exists'', etc. and their introduction and elimination rules, and definitions of some properties of relations (symmetry, reflexivity etc.). It is based on Randy Pollack's logic file. For the convenience of some of our users we have included definitions of ``and'' and ``exists'' which take up to 7 arguments.

 ** Module lib_logic Imports parameters
 ** Config Infix /\ left 3
 ** Config Infix \/ left 2
  cut = ... : {A,B|Prop}A->(A->B)->B
  trueProp = ... : Prop
  Id = ... : {T|SET}T->T
  PropId = ... : {A|Prop}A->A
  Contrapos = ... : {A,B|Prop}(A->B)->{X|Prop}(B->X)->A->X
  compose = ... : {T,S,U|SET}(S->U)->(T->S)->T->U
  permute = ... : {T,S,U|SET}(T->S->U)->S->T->U
  forall_elim = ... :
    {C|Prop}{T|SET}{P:T->Prop}({x:T}P x)->{e:T}((P e)->C)->C
  impl_elim = ... : {A,B,C|Prop}(A->B)->A->(B->C)->C
  and = ... : Prop->Prop->Prop
  or = ... : Prop->Prop->Prop
  or_elim = ... : {A,B,C|Prop}(A \/ B)->(A->C)->(B->C)->C
  pair = ... : {A,B|Prop}A->B->(A /\ B)
  inl = ... : {A,B|Prop}A->(A \/ B)
  inr = ... : {A,B|Prop}B->(A \/ B)
  fst = ... : {A,B|Prop}(A /\ B)->A
  snd = ... : {A,B|Prop}(A /\ B)->B
  iff = ... : Prop->Prop->Prop
  absurd = ... : Prop
  absurd_elim = ... : absurd->{N:Prop}N
  not = ... : Prop->Prop
  All = ... : {T|SET}(T->Prop)->Prop
  Ex = ... : {T|SET}(T->Prop)->Prop
  ExIntro = ... : {T|SET}{wit:T}{P:T->Prop}(P wit)->Ex P
  ExIn = ... :
    {T|SET}{wit:T}{P:T->Prop}(P wit)->{B:Prop}({t:T}(P t)->B)->B
  ExElim = ... : {T|SET}{P|T->Prop}(Ex P)->{N|Prop}({t:T}(P t)->N)->N
  ex = ... : {A|Prop}(A->Prop)->Prop
  ex_intro = ... : {A|Prop}{P:A->Prop}{wit|A}(P wit)->ex P
  witness = ... : {A|Prop}{P|A->Prop}(ex P)->A
  Ex2 = ... : {T,S|SET}(T->S->Prop)->Prop
  Ex2Intro = ... : {T,S|SET}{P:T->S->Prop}{t|T}{s|S}(P t s)->Ex2 P
  Ex2Elim = ... :
    {T,S|SET}{P|T->S->Prop}(Ex2 P)->{N|Prop}({t|T}{s|S}(P t s)->N)->N
  Ex2In = ... : {T,S|SET}{t:T}{s:S}{P:T->S->Prop}(P t s)->Ex2 P
  Ex3 = ... : {T,S,U|SET}(T->S->U->Prop)->Prop
  Ex3In = ... :
    {T,S,U|SET}{t:T}{s:S}{u:U}{P:T->S->U->Prop}(P t s u)->Ex3 P
  Ex3Elim = ... :
    {T,S,U|SET}{P|T->S->U->Prop}(Ex3 P)->{N|Prop}
    ({t|T}{s|S}{u|U}(P t s u)->N)->N
  Ex4 = ... : {T,S,U,V|SET}(T->S->U->V->Prop)->Prop
  Ex4In = ... :
    {T,S,U,V|SET}{t:T}{s:S}{u:U}{v:V}{P:T->S->U->V->Prop}(P t s u v)->
    Ex4 P
  Ex4Elim = ... :
    {T,S,U,V|SET}{P|T->S->U->V->Prop}(Ex4 P)->{N|Prop}
    ({t|T}{s|S}{u|U}{v|V}(P t s u v)->N)->N
  Ex5 = ... : {T,S,U,V,W|SET}(T->S->U->V->W->Prop)->Prop
  Ex5In = ... :
    {T,S,U,V,W|SET}{t:T}{s:S}{u:U}{v:V}{w:W}{P:T->S->U->V->W->Prop}
    (P t s u v w)->Ex5 P
  Ex5Elim = ... :
    {T,S,U,V,W|SET}{P|T->S->U->V->W->Prop}(Ex5 P)->{N|Prop}
    ({t|T}{s|S}{u|U}{v|V}{w|W}(P t s u v w)->N)->N
  Ex6 = ... : {T,S,U,V,W,X|SET}(T->S->U->V->W->X->Prop)->Prop
  Ex6In = ... :
    {T,S,U,V,W,X|SET}{t:T}{s:S}{u:U}{v:V}{w:W}{x:X}
    {P:T->S->U->V->W->X->Prop}(P t s u v w x)->Ex6 P
  Ex6Elim = ... :
    {T,S,U,V,W,X|SET}{P|T->S->U->V->W->X->Prop}(Ex6 P)->{N|Prop}
    ({t|T}{s|S}{u|U}{v|V}{w|W}{x|X}(P t s u v w x)->N)->N
  and3 = ... : Prop->Prop->Prop->Prop
  pair3 = ... : {A,B,C|Prop}A->B->C->and3 A B C
  and3_out1 = ... : {A,B,C|Prop}(and3 A B C)->A
  and3_out2 = ... : {A,B,C|Prop}(and3 A B C)->B
  and3_out3 = ... : {A,B,C|Prop}(and3 A B C)->C
  and4 = ... : Prop->Prop->Prop->Prop->Prop
  pair4 = ... : {A,B,C,D|Prop}A->B->C->D->and4 A B C D
  and4_out1 = ... : {A,B,C,D|Prop}(and4 A B C D)->A
  and4_out2 = ... : {A,B,C,D|Prop}(and4 A B C D)->B
  and4_out3 = ... : {A,B,C,D|Prop}(and4 A B C D)->C
  and4_out4 = ... : {A,B,C,D|Prop}(and4 A B C D)->D
  and5 = ... : Prop->Prop->Prop->Prop->Prop->Prop
  pair5 = ... : {A,B,C,D,E|Prop}A->B->C->D->E->and5 A B C D E
  and5_out1 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->A
  and5_out2 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->B
  and5_out3 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->C
  and5_out4 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->D
  and5_out5 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->E
  and6 = ... : Prop->Prop->Prop->Prop->Prop->Prop->Prop
  pair6 = ... : {A,B,C,D,E,F|Prop}A->B->C->D->E->F->and6 A B C D E F
  and6_out1 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->A
  and6_out2 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->B
  and6_out3 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->C
  and6_out4 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->D
  and6_out5 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->E
  and6_out6 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->F
  and7 = ... : Prop->Prop->Prop->Prop->Prop->Prop->Prop->Prop
  pair7 = ... :
    {A,B,C,D,E,F,G|Prop}A->B->C->D->E->F->G->and7 A B C D E F G
  and7_out1 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->A
  and7_out2 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->B
  and7_out3 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->C
  and7_out4 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->D
  and7_out5 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->E
  and7_out6 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->F
  and7_out7 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->G
  iff3 = ... : Prop->Prop->Prop->Prop
  or3 = ... : Prop->Prop->Prop->Prop
  or3_in1 = ... : {A,B,C|Prop}A->or3 A B C
  or3_in2 = ... : {A,B,C|Prop}B->or3 A B C
  or3_in3 = ... : {A,B,C|Prop}C->or3 A B C
  or3_elim = ... : {A,B,C,X|Prop}(or3 A B C)->(A->X)->(B->X)->(C->X)->X
  refl = ... : {T|SET}(T->T->Prop)->Prop
  sym = ... : {T|SET}(T->T->Prop)->Prop
  trans = ... : {T|SET}(T->T->Prop)->Prop
  Equivalence = ... : {T|SET}(T->T->Prop)->Prop
  respect = ... : {T,S|SET}(T->S)->({X|SET}X->X->Prop)->Prop
  respect2 = ... : {T,S,U|SET}(T->U->S)->({X|SET}X->X->Prop)->Prop