% Copyright (c) 2004 Princeton University
%	$Id: logic.elf,v 1.17 2005/02/10 15:21:23 richards Exp $

tp     : type.
tm     : tp -> type.

form   : tp.
tform  : type = tm form.

pf     : tform -> type.


% constructors:

_forall : {T : tp} (tm T -> tform) -> tform.

_forall_i : {T : tp}{A : tm T -> tform}
  ({X : tm T} pf (A X)) ->
  pf (_forall T A).

% def without type signature (needs abstraction)

_forall2 : {T1 : tp}{T2 : tp}{f : tm T1 -> tm T2 -> tform} tform
  = [T1 : tp][T2 : tp][f : tm T1 -> tm T2 -> tform]
    _forall T1 [x : tm T1]
      _forall T2 (f x).

% defs with type signature

forall : {T:tp} (tm T -> tform) -> tform
  = [T:tp] [x3:tm T -> tform]
      _forall T ([x4:tm T] x3 x4).

forall2 : {T1:tp} {T2:tp} (tm T1 -> tm T2 -> tform) -> tform
  = [T1:tp] [T2:tp] [x3:tm T1 -> tm T2 -> tform]
      _forall2 T1 T2 ([x4:tm T1] [x5:tm T2] x3 x4 x5).

forall_i : {T:tp} {F:tm T -> tform}
  ({a:tm T} pf (F a)) ->
  pf (forall T ([x3:tm T] F x3))
  = [T:tp] [F:tm T -> tform] [x3:{a:tm T} pf (F a)]
      _forall_i T ([x4:tm T] F x4) ([a:tm T] x3 a).

forall2_i : {X1:tp} {X2:tp} {F:tm X1 -> tm X2 -> tform}
  ({a:tm X1} {b:tm X2} pf (F a b)) ->

  pf (forall2 X1 X2 ([x3:tm X1] [x4:tm X2] F x3 x4))

  = [X1:tp] [X2:tp] [F:tm X1 -> tm X2 -> tform]
    [p1:{a:tm X1} {b:tm X2} pf (F a b)]

    forall_i X1 ([x3:tm X1] forall X2 ([x4:tm X2] F x3 x4))
      ([x3:tm X1] forall_i X2 ([x4:tm X2] F x3 x4) ([a:tm X2] p1 x3 a)).

%{
  inferring type of

    forall_i X1 ([x3 : tm X1] forall X2 ([x4 : tm X2] F x3 x4))
      ([x3 : tm X1] forall_i X2 ([x4 : tm X2] F x3 x4) ([a : tm X2] p1 x3 a))


  forall_i =>  {T:tp} {F:tm T -> tform}
                 ({a:tm T} pf (F a)) -> pf (forall T ([x3:tm T] F x3))

  forall_i X1 =>  {F:tm X1 -> tform}
                 ({a:tm X1} pf (F a)) -> pf (forall X1 ([x3:tm X1] F x3))

  forall_i X1 ([x3 : tm X1] forall X2 ([x4 : tm X2] F x3 x4)) =>
            [ ([x3 : tm X1] forall X2 ([x4 : tm X2] F x3 x4)) / F ]
                 ({a:tm X1} pf (F a)) -> pf (forall X1 ([x3:tm X1] F x3))


  checking

    [x3 : tm X1] forall_i X2 ([x4 : tm X2] F x3 x4) ([a : tm X2] p1 x3 a)
  against
    {a : tm X1} pf (forall X2 ([x4] F x4 x4))

  checking

    forall_i X2 ([x4 : tm X2] F x3 x4) ([a : tm X2] p1 x3 a)

  against

    pf (forall X2 ([x4] F x4 x4))

  checking wether

    pf (forall X2 ([x3'] F x3 x3'))
  equals
    pf (forall X2 ([x4] F x4 x4))

  head mismatch x3 !=
}%