%{

First we define the multiset type. Each multiset is either
the empty multiset or was constructed from other multiset by
inserting an eleement into it

}%




%% NATURAL NUMBERS

nat: type.
z: nat.
s: nat -> nat.
%freeze nat.


% define false

false : type.
%freeze false.

 

%% equality
eq-nat	    : nat -> nat -> type.
eq-nat/refl : eq-nat N N.

%% less than
lt : nat -> nat -> type.
lt/z : lt z (s N).
lt/s : lt (s N1) (s N2)
	    <- lt N1 N2.

%% less than or equal
lte : nat -> nat -> type.
lte/z : lte z N.
lte/s : lte (s N1) (s N2)
	    <- lte N1 N2.



%% not equal
neq-nat : nat -> nat -> type.
neq-nat/gt : neq-nat N1 N2
	      <- lt N2 N1.
neq-nat/lt : neq-nat N1 N2
	      <- lt N1 N2.


% lemma 
% if N1 =< N2 => N1 =< s N2. 

lte-n-succ: lte N1 N2 -> lte N1 (s N2) -> type.
%mode lte-n-succ +LTE1 -LTE2.


- : lte-n-succ
     (lte/z : lte z N)
     (lte/z : lte z (s N)).

- : lte-n-succ
     (lte/s LTE1' : lte (s N1) (s N2)) 
     (lte/s LTE2' : lte (s N1) (s (s N2)))
     <- lte-n-succ
	 (LTE1' : lte N1 N2) 
	 (LTE2' : lte N1 (s N2)).

%worlds () (lte-n-succ _ _).
%total LTE1 (lte-n-succ LTE1 _).



%% if two numbers are (not) equal, so are their succesors  

eq-nat-s : 
  eq-nat N1 N2 -> eq-nat (s N1) (s N2) -> type.
%mode eq-nat-s +EQN1 -EQN2.

- : eq-nat-s
     (eq-nat/refl : eq-nat N N)
     (eq-nat/refl : eq-nat (s N) (s N)).

%worlds () (eq-nat-s _ _).
%total EQN1 (eq-nat-s EQN1 _).


neq-nat-s : 
  neq-nat N1 N2 -> neq-nat (s N1) (s N2) -> type.
%mode neq-nat-s +NEQ1 -NEQ2.

- : neq-nat-s
     (neq-nat/lt LT: neq-nat N1 N2)
     (neq-nat/lt (lt/s LT): neq-nat (s N1) (s N2)).

- : neq-nat-s
     (neq-nat/gt LT: neq-nat N1 N2)
     (neq-nat/gt (lt/s LT): neq-nat (s N1) (s N2)).

%worlds () (neq-nat-s _ _).
%total NEQ1 (neq-nat-s NEQ1 _).



%% lt is transitive

lt-trans: lt N1 N2 -> lt N2 N3 -> lt N1 N3 -> type.
%mode lt-trans +LT1 +LT2 -LT3.

- : lt-trans
     (lt/z : lt z (s N))
     (LT : lt (s N) (s N2)) 
     (lt/z : lt z (s N2)).


- : lt-trans 
     (lt/s LT1' : lt (s N1') (s N2')) 
     (lt/s LT2' : lt (s N2') (s N3'))
     (lt/s LT3' : lt (s N1') (s N3'))
     <- lt-trans 
	 (LT1' : lt N1' N2') 
	 (LT2' : lt N2' N3') 
	 (LT3' : lt N1' N3').

%worlds () (lt-trans _ _ _).
%total LT1 (lt-trans LT1 _ _).


%% lt is irreflexive 

lt-irrefl : 
  {N} lt N N -> false -> type.
%mode lt-irrefl +N +LT -FALSE.

-/s : lt-irrefl 
       (s N') 
       (lt/s LT' : lt (s N') (s N'))
       FALSE
       <- lt-irrefl N' LT' FALSE.

%worlds () (lt-irrefl _ _ _).  
%total N (lt-irrefl N _ _).  


%% 

lt-lt-cannot: 
  lt N1 N2 -> lt N2 N1 -> false -> type.
%mode lt-lt-cannot +LT1 +LT2 -FALSE.


- : lt-lt-cannot
     (lt/s LT1: lt (s N1) (s N2))
     (lt/s LT2: lt (s N2) (s N1))
     FALSE
     <- lt-lt-cannot
	(LT1: lt N1 N2)
	(LT2: lt N2 N1)
	FALSE.

%worlds () (lt-lt-cannot _ _ _).  
%total LT (lt-lt-cannot LT _ _).


%% N cannot be neq N

not-neq :
  {N} neq-nat N N -> false -> type.
%mode not-neq +N +NEQ -FALSE.

- : not-neq N (neq-nat/lt LT)  FALSE
     <- lt-irrefl N LT FALSE.

- : not-neq N (neq-nat/gt LT)  FALSE
     <- lt-irrefl N LT FALSE.


%worlds () (not-neq _ _ _).  
%total N (not-neq N _ _).  



%% 


not-eq-neq :
  eq-nat N1 N2 -> neq-nat N1 N2 -> false -> type.
%mode not-eq-neq +EQ +NEQ -FALSE.

- : not-eq-neq (eq-nat/refl) NEQ FALSE
    <- not-neq _ NEQ FALSE.

%worlds () (not-eq-neq _ _ _).  
%total N (not-eq-neq N _ _).  


%% zero is different than any other natural number

neq-zero-any: {N:nat} neq-nat z (s N) -> type.
%mode neq-zero-any +N -COMP.

-: neq-zero-any 
    N (neq-nat/lt lt/z).

%worlds () (neq-zero-any _ _).
%total N (neq-zero-any N _).



%% commutativity of being neq

neq-com: neq-nat N1 N2 -> neq-nat N2 N1 -> type.
%mode neq-com +NEQ1 -NEQ2.

-: neq-com
    (neq-nat/lt LT: neq-nat N1 N2)
    (neq-nat/gt LT: neq-nat N2 N1).

-: neq-com
    (neq-nat/gt LT: neq-nat N1 N2)
    (neq-nat/lt LT: neq-nat N2 N1).

%worlds () (neq-com _ _).
%total NEQ (neq-com NEQ _).


% every two natural numbers are comparable

comparable: nat -> nat -> type.
comparable/eq : comparable N1 N2 
		 <- eq-nat N1 N2.
comparable/neq : comparable N1 N2 
		  <- neq-nat N1 N2.


are-comparable-s : 
  comparable N1 N2 -> comparable (s N1) (s N2) -> type.
%mode are-comparable-s +COMP1 -COMP2.

- : are-comparable-s (comparable/eq EQ1)(comparable/eq EQ2)
     <- eq-nat-s EQ1 EQ2.

- : are-comparable-s (comparable/neq NEQ1)(comparable/neq NEQ2)
     <- neq-nat-s NEQ1 NEQ2.

%worlds () (are-comparable-s _ _).
%total CMP1 (are-comparable-s CMP1 _).



are-comparable: {N1}{N2} comparable N1 N2 -> type.
%mode are-comparable +N1 +N2 -COMP.

- : are-comparable z z (comparable/eq eq-nat/refl).

- : are-comparable z (s N) (comparable/neq COMP)
     <- neq-zero-any N COMP.

- : are-comparable (s N) z (comparable/neq NEQ)
     <- neq-zero-any N COM1
	<- neq-com COM1 NEQ.

- : are-comparable (s N1) (s N2) COMP2
     <- are-comparable N1 N2 COMP1
	<- are-comparable-s COMP1 COMP2.


%worlds () (are-comparable _ _ _).
%total N (are-comparable N _ _).




%% addition

add : nat -> nat -> nat -> type.
add/z : add z N N.
add/s : add (s N1) N2 (s N3)
	 <- add N1 N2 N3.


% subtraction

sub : nat -> nat -> nat -> type.

sub/z : sub N N z.
sub/s : sub (s N1) N2 (s N3)
	 <- sub N1 N2 N3.

% some simple properties about subtraction

sub-zero: {N:nat} sub N z N -> type.
%mode sub-zero +N -SUB.

-/z: sub-zero z sub/z.
-/s: sub-zero (s N') (sub/s SUB')
      <- sub-zero N' SUB'.

%worlds () (sub-zero _ _).
%total N (sub-zero N _).


% some simple theorem
% A + B - B = A


stays-thesame : add N1 N2 N3 -> sub N3 N2 N1 -> type.
%mode stays-thesame +ADD -SUB.

- : stays-thesame
     (add/z: add z N N)
     (sub/z: sub N N z).

- : stays-thesame
     (add/s ADD': add (s N1) N2 (s N3))
     (sub/s SUB': sub (s N3) N2 (s N1))
     <- stays-thesame
	(ADD' : add N1 N2 N3)
	(SUB' : sub N3 N2 N1).


%worlds () (stays-thesame _ _).
%total ADD (stays-thesame ADD _).



% another simple lemma about subtraction
% N + 1 - 1 = N


sub-one: {N:nat} sub (s N) (s z) N -> type.
%mode sub-one +N -SUB.

-/z : sub-one z sub/z.
-/s: sub-one (s N') (sub/s SUB')
      <- sub-one N' SUB'.

%worlds () (sub-one _ _).
%total N (sub-one N _).







% MULTISETS

mset: type.

empty: mset.
insert: nat -> mset -> mset.
%freeze mset.



% Now we define the union of two multisets

union: mset -> mset -> mset -> type.

union/e: union empty M M.
union/i: union (insert N M1) M2 (insert N M3)
          <- union M1 M2 M3.


% Now we define the cardinality of a multiset

card: mset -> nat -> type.

card/e: card empty z.
card/i: card (insert _ S) (s N) 
         <- card S N.


% First lemma:
% card (M1 union M2) = card M1 + card M2


union-card :
  union M1 M2 M3 -> card M1 N1 -> card M2 N2 -> card M3 N3 
    -> add N1 N2 N3 -> type.
%mode union-card +UN +CRD1 +CRD2 -CRD3 -ADD.


-: union-card
    (union/e: union empty M M)
    (card/e: card empty z)
    (CRD2: card M N)
    (CRD2: card M N)
    (add/z: add z N N).


-: union-card
    (union/i UN' : union (insert E M1) M2 (insert E M3))
    (card/i CDR1' : card (insert E M1) (s N1) )
    (CDR2' : card M2 N2 )
    (card/i CDR3': card (insert E M3) (s N3))
    (add/s ADD':  add (s N1) N2 (s N3))
    <- union-card
       (UN': union M1 M2 M3)
       (CDR1': card M1 N1)
       (CDR2': card M2 N2)
       (CDR3': card M3 N3)
       (ADD': add N1 N2 N3).


%worlds () (union-card _ _ _ _ _).
%total APP (union-card APP _ _ _ _).


vc-insert :
  card E (s z) -> union L E M -> card L N1 -> card M N2 
    -> add N1 (s z) N2 -> type.
%mode vc-insert +CRD1 +UN +CRD2 -CRD3 -ADD.

-: vc-insert
    CRD1 UN CRD2 CRD3 ADD 
    <- union-card UN CRD2 CRD1 CRD3 ADD.

%worlds () (vc-insert _ _ _ _ _).
%total CRD1 (vc-insert CRD1 _ _ _ _).



% testing membership

isMember: nat -> mset -> type.

isMember/i: isMember N1 (insert N2 M) <- eq-nat N1 N2.
isMember/r: isMember N1 (insert N2 M) <- isMember N1 M <- neq-nat N1 N2.


notMember: nat -> mset -> type.

notMember/i: notMember E empty.
notMember/r: notMember E1 (insert E2 M) <- neq-nat E1 E2 <- notMember E1 M.



% deleting an element from multiset

del: nat -> mset -> mset -> type.

del/last: del N1 (insert N2 M) M <- eq-nat N1 N2.

del/notlast: del N2 (insert N1 M) (insert N1 M2)
		 <- del N2 M M2
		    <- neq-nat N1 N2.



false-implies-card : false -> card M1 N1 -> type.
%mode false-implies-card +FALSE -CARD.
%worlds () (false-implies-card _ _).
%total FALSE (false-implies-card FALSE _).




false-implies-sub : {N1} {N2} false -> sub N1 N2 N3 -> type.
%mode false-implies-sub +N1 +N2 +FALSE -SUB.
%worlds () (false-implies-sub _ _ _ _).
%total FALSE (false-implies-sub _ _ FALSE _).




lemma-cd-2 : card M N1 -> card M N2 -> eq-nat N1 N2 -> type.
%mode lemma-cd-2 +CR1 +CR2 -EQ.

-: lemma-cd-2
    (card/e: card empty z)
    (card/e: card empty z)
    (eq-nat/refl: eq-nat z z).

-: lemma-cd-2
    (card/i CR1: card (insert E M) (s N1))
    (card/i CR2: card (insert E M) (s N2))
    EQ1
    <- lemma-cd-2
       (CR1: card M N1)
       (CR2: card M N2)
       (EQ: eq-nat N1 N2)
    <- eq-nat-s EQ EQ1.

%worlds () (lemma-cd-2 _ _ _).
%total CR1 (lemma-cd-2 CR1 _ _).




lemma-cd-3 :
  eq-nat N1 N2 -> sub N1 (s z) N -> sub N2 (s z) N -> type.
%mode lemma-cd-3 +EQ +SUB1 -SUB2.

-: lemma-cd-3
     (eq-nat/refl) (sub/z) (sub/z).

-: lemma-cd-3
     (eq-nat/refl) % : eq-nat (s N1) (s N2))
     (sub/s SUB1 : sub (s N) (s z) (s N'))
     (sub/s SUB2 : sub (s N) (s z) (s N'))
     <- lemma-cd-3
        (eq-nat/refl)
        (SUB1: sub N (s z) N')
        (SUB2: sub N (s z) N').

%worlds () (lemma-cd-3 _ _ _).
%total SUB1 (lemma-cd-3 _ SUB1 _).




lemma-cd-4 : 
   {E1} {E2} card (insert E1 M) N1 -> card (insert E2 M) N2 -> eq-nat N1 N2 -> type.
%mode lemma-cd-4 +E1 +E2 +CRD1 +CRD2 -EQ.

-: lemma-cd-4 
    _ _ (card/i card/e) (card/i card/e) (eq-nat/refl).


-: lemma-cd-4
    _ _ 
    (card/i CRD1: card (insert _ (insert _ M)) (s N1))
    (card/i CRD2: card (insert _ (insert _ M)) (s N2))
    (EQ1: eq-nat (s N1) (s N2))
    <- lemma-cd-4
       _ _
       (CRD1: card (insert _ M) N1)
       (CRD2: card (insert _ M) N2)
       (EQ: eq-nat N1 N2)
    <- eq-nat-s EQ EQ1.


%worlds () (lemma-cd-4 _ _ _ _ _).
%total CRD1 (lemma-cd-4 _ _ CRD1 _ _).


lemma-cd-1 : {N} {N1} {E} card M N -> card (insert E M) N1 ->
   sub N1 (s z) N -> type.
%mode lemma-cd-1 +N +N1 +E +CR1 +CR2 -SUB.

-: lemma-cd-1  N N1 E CR1 CR2 SUB
    <- sub-one N SUB1
    <- lemma-cd-4 E _ (card/i CR1) CR2 EQ
    <- lemma-cd-3 EQ SUB1 SUB.



%worlds () (lemma-cd-1 _ _ _ _ _ _ ).
%total CR1 (lemma-cd-1 _ _ _ CR1 _ _).

%{

del-card :
  isMember E M -> del E M M1 -> card M N -> card M1 N1 -> 
   sub N (s z) N1 -> type.
%mode del-card +MEM +DEL +CRD1 +CRD2 -SUB.


-: del-card
    (isMember/i EQ1: isMember E (insert E M))
    (del/last EQ2: del E (insert E M) M)
    (card/i CRD: card (insert E M) (s N))
    (CRD: card M N) 
    (SUB: sub (s N) (s z) N)
      <- sub-one N SUB.

-:  del-card
    (isMember/r DIFF1 MEM': isMember E (insert E1 M))
    (del/notlast DIFF2 DEL': del E (insert E1 M) (insert E1 M1))
    (card/i CRD1': card (insert E1 M) (s N))
    (card/i CRD2': card (insert E1 M1) (s N1))
    (sub/s SUB': sub (s N) (s z) (s N1))
    <- del-card
       (MEM': isMember E M)
       (DEL': del E M M1)
       (CRD1': card M N)
       (CRD2': card M1 N1)
       (SUB': sub N (s z) N1).


-: del-card
    (isMember/r NEQ MEM)
    (del/last EQ)
    CARD1
    CARD2
    SUB
    <- not-eq-neq EQ NEQ FALSE
    <- false-implies-card _ _ FALSE CARD1
    <- false-implies-card _ _ FALSE CARD2
    <- false-implies-sub _ _ FALSE SUB.


-: del-card
    (isMember/i EQ)
    (del/notlast NEQ DEL)
    CARD1
    CARD2
    SUB
    <- not-eq-neq EQ NEQ FALSE
    <- false-implies-card _ _ FALSE CARD1
    <- false-implies-card _ _ FALSE CARD2
    <- false-implies-sub _ _ FALSE SUB.


-: del-card
    (isMember/r (neq-nat/gt LT2) MEM)
    (del/notlast (neq-nat/gt LT1) DEL)
    CARD1
    CARD2
    SUB
    <- lt-lt-cannot LT1 LT2 FALSE
    <- false-implies-card _ _ FALSE CARD1
    <- false-implies-card _ _ FALSE CARD2
    <- false-implies-sub _ _ FALSE SUB.


-: del-card
    (isMember/r (neq-nat/lt LT2) MEM)
    (del/notlast (neq-nat/lt LT1) DEL)
    CARD1
    CARD2
    SUB
    <- lt-lt-cannot LT1 LT2 FALSE
    <- false-implies-card _ _ FALSE CARD1
    <- false-implies-card _ _ FALSE CARD2
    <- false-implies-sub _ _ FALSE SUB.

-: del-card
    (isMember/i EQ1: isMember E (insert E M))
    (del/last EQ2: del E (insert E M) M)
    (card/i CRD: card (insert E M) (s N))
    (CRD: card M N) 
    (SUB: sub (s N) (s z) N)
      <- sub-one N SUB.


-:  del-card
    (isMember/i EQ1: isMember E1 (insert E2 M))
    (del/last EQ2: del E1 (insert E2 M) M)
    (CRD1: card (insert E2 M) N1)
    (CRD2: card M N)
    (SUB: sub N1 (s z) N)
    <- lemma-cd-1 N N1 E2 CRD2 CRD1 SUB.





%worlds () (del-card _ _ _ _ _).
%total DEL (del-card _ DEL  _ _ _).

}%




del-card : isMember E M -> del E M M' -> card M (s N) -> card M' N -> type.
%mode del-card +MEM +DEL +CRD1 -CRD2.



-: del-card
    (isMember/i EQ1: isMember E (insert E M))
    (del/last EQ2: del E (insert E M) M)
    (card/i CRD: card (insert E M) (s N))
    (CRD: card M N).


-:  del-card
    (isMember/r DIFF1 MEM': isMember E (insert E1 M))
    (del/notlast DIFF2 DEL': del E (insert E1 M) (insert E1 M1))
    (card/i CRD1': card (insert E1 M) (s (s N)))
    (card/i CRD2': card (insert E1 M1) (s N))
    <- del-card
       (MEM': isMember E M)
       (DEL': del E M M1)
       (CRD1': card M (s N))
       (CRD2': card M1 N).



-: del-card
    (isMember/r NEQ MEM)
    (del/last EQ)
    _ 
    CARD2
    <- not-eq-neq EQ NEQ FALSE
%%    <- false-implies-card FALSE CARD1
    <- false-implies-card FALSE CARD2.




-: del-card
    (isMember/i EQ)
    (del/notlast NEQ DEL)
    _
    CARD2
    <- not-eq-neq EQ NEQ FALSE
%    <- false-implies-card FALSE CARD1
    <- false-implies-card FALSE CARD2.




%worlds () (del-card _ _ _ _).
%total DEL (del-card _ DEL  _ _).


%.


occurs : nat -> mset -> nat -> type.

occurs/e : occurs E empty z.
occurs/i : occurs E1 (insert E2 M) (s N)
	    <- occurs E1 M N
	       <- eq-nat E1 E2.
occurs/i/d : occurs E1 (insert E2 M) N
	    <- occurs E1 M N
	       <- neq-nat E1 E2.

 
% define subset

subset: mset -> mset -> type.

subset/e: subset empty M.
subset/i/r: subset M1 (insert _ M2)
	     <- subset M1 M2.
subset/i/l: subset (insert E M1) M2
	     <- subset M1 M2
	     <- occurs E M1 N1
	     <- occurs E M2 N2
	     <- lt N1 N2.



%% theorem about subsets

% lemma 2

lemma2-sc: 
  occurs E M1 L1 -> occurs E M2 L2 -> lt L1 L2
   -> card M1 N1 -> card M2 N2 -> lt N1 N2 -> type.
%mode lemma2-sc +OC1 +OC2 +LT +CR1 +CR2 -LT.



- : lemma2-sc
     (occurs/e: occurs E empty z)
     (OC: occurs E M (s L))
     (lt/z: lt z (s L))
     (card/e: card empty z)
     (CR: card M (s N))
     (lt/z: lt z (s N) ).


- : lemma2-sc
     (occurs/i EQ1 OC1: occurs E1 (insert E2 M1) (s L1))
     (occurs/i EQ2 OC2: occurs E1 (insert E2 M2) (s L2))
     (lt/s LT1: lt (s L1) (s L2))
     (card/i CRD1: card (insert E2 M1) (s N1))
     (card/i CRD2: card (insert E2 M2) (s N2))
     (lt/s LT2L lt (s N1) (s N2))
     <- lemma2-sc
	(OC1: occurs E M1 L1)
	(OC2: occurs E M2 L2)
	(LT1: lt L1 L2)
	(CRD1: card M1 N1)
	(CRD2: card M2 N2)
	(LT2: lt N1 N2).



%worlds () (lemma2-sc _ _ _ _ _ _).
% total OC (lemma2-sc OC _ _ _ _ _ _).







% lemma 3

lemma3-sc: 
  lt N1 N2 -> lte (s N1) N2 -> type.
%mode lemma3-sc +LT -LTE.

- : lemma3-sc
     (lt/z : lt z (s N))
     (lte/s lte/z : lte (s z) (s N)).

- : lemma3-sc
     (lt/s LT : lt (s N1) (s N2)) 
     (lte/s LTE : lte (s (s N1)) (s N2))
     <- lemma3-sc
	 (LT : lt N1 N2) 
	 (LTE : lte (s N1) N2).

%worlds () (lemma3-sc _ _).
%total LT (lemma3-sc LT _).



% lemma 1

lemma1-sc: 
  occurs E M1 L1 -> occurs E M2 L2 -> lt L1 L2
   -> card M1 N1 -> card M2 N2 -> lte (s N1) N2 -> type.
%mode lemma1-sc +OC1 +OC2 +LT +CR1 +CR2 -LTE.

-: lemma1-sc OC1 OC2 LT CR1 CR2 LTE
    <- lemma3-sc LT LTE
    <- lemma2-sc OC1 OC2 LT CR1 CR2 LT.


%worlds () (lemma1-sc _ _ _ _ _ _).
%total OC (lemma1-sc OC _ _ _ _ _).


subset-card: 
  subset M1 M2 -> card M1 N1 -> card M2 N2 -> lte N1 N2 -> type.
%mode subset-card +SUB +CR1 +CR2 -LTE.

-: subset-card
    (subset/e: subset empty M)
    (card/e: card empty z)
    (CR: card M N)
    (lte/z : lte z N).

-: subset-card
    (subset/i/r SUB': subset M1 (insert E M2))
    (CRD1': card M1 N1)
    (card/i CRD2': card (insert E M2) (s N2))
    (LTE2: lte N1 (s N2))
    <- subset-card
       (SUB': subset M1 M2)
       (CRD1': card M1 N1)
       (CRD2': card M2 N2)
       (LTE': lte N1 N2)
       <- lte-n-succ LTE' LTE2.



-: subset-card
    (subset/i/l LT OC2 OC1 SUB': subset (insert E M1) M2)
    (card/i CRD1': card (insert E M1) (s N1))
    (CRD2': card M2 N2)
    (LTE: lte (s N1) N2)
    <- subset-card
       (SUB': subset M1 M2)
       (CRD1': card M1 N1)
       (CRD2': card M2 N2)
       (LTE': lte N1 N2)
       <- lemma1-sc OC1 OC2 LT CRD1' CRD2' LTE.



%worlds () (subset-card _ _ _ _).
%total SUB (subset-card SUB _ _ _).


% %query * 2 isMember E (insert F(insert E empty)).

% %query * 1 card (insert E (insert F empty)) N.
 

% %query * 1 occurs E (insert F (insert F (insert F (insert G (insert E empty)))))  N.

% %query * 1 subset (insert A (insert B empty)) (insert B (insert A empty)).