Next: Equality Up: Providing logic and equality Previous: Providing logic and equality

## 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
```

Conor McBride
11/13/1998