-- Exercise 1:
mod* GROUP { 
[Group]
op 0 : -> Group
op _+_ : Group Group -> Group
op -_ : Group -> Group
vars X Y Z : Group
eq [lid] : 0 + X = X .
eq [linv] : (- X) + X = 0 .
eq [assoc] : X + (Y + Z) = (X + Y) + Z . 
}

open GROUP + EQL
op a : -> Group .
start a + (- a) = 0 .
apply -.lid with X = a + (- a) at (1) .
**> result 0 + (a + (- a)) = 0 : Bool
apply -.linv with X = - a at (1 1) .
**> result (- (- a) + (- a)) + (a + (- a)) = 0 : Bool
apply assoc at (1) .
**> ((- (- a) + (- a)) + a) + (- a) = 0 : Bool
apply -.assoc at (1 1) .
**> result (- (- a) + (- a + a)) + (- a) = 0 : Bool
apply -.assoc at (1) .
**> result - (- a) + ((- a + a) + (- a)) = 0 : Bool
apply red at term .
**> result true : Bool
close

-- --------------------------------------------------------------------
-- Exercise 2:

mod* SPEC { 
[Elt]
ops a b : -> Elt
op _=_ : Elt Elt -> Bool
vars X Y : Elt
eq [equal] : (X = X) = true .
ceq [cequal] : X = Y if (X = Y) .
}

-- {equal,cequal,a=b} |= (a=b)=true
open SPEC
eq [m-level] : a = b .   -- the meta-level equality
-- we prove object-level equality
red a = b .  
**> result true: Bool
close

-- {equal,cequal,(a=b)=true} |= a=b
open SPEC
eq [o-level] : (a = b) = true .
-- we prove meta-level equality
start a .
apply cequal with X = a , Y = b at term .
apply o-level at term .
**> result b : Elt
close 

-- --------------------------------------------------------------------
-- Execise 3:

mod* QUEUE(D :: SPEC){ 
[Queue]
op nil : -> Queue {constr}
op _@_ : Elt Queue -> Queue {constr}
op _in_ : Elt Queue -> Bool
op empty? : Queue -> Bool
var Q : Queue
vars X Y : Elt
eq [i-1] : X in nil = false .
eq [i-2] : X in (X @ Q) = true .
ceq [i-3]: X in (Y @ Q) = X in Q if not(X = Y) .
eq [e-1]: empty?(nil) = true .
eq [e-2]: empty?(X @ Q) = false . }

mod* QUEUE-I{
using(QUEUE)
op q : -> Queue .
eq [a-q-nil]: a @ q = nil . 
}

-- It suffices to prove that QUEUE-I is inconsistent 
-- QUEUE-I |=^c  true = false 
open QUEUE-I + EQL
-- we prove true = false
start true .
apply  -.e-1 at term .
**> result empty?(nil) : Bool
apply -.a-q-nil at (1) .
**> result empty?(a @ q) : Bool
apply red at term .
**> result false : Bool
close
-- --------------------------------------------------------------------
-- Exercise 4:
mod* SPEC-CA{ 
[Elt]
op a : -> Elt {constr}
op b : -> Elt
}

-- By Case analysis we need to prove
-- SPEC-CA + b = a
open SPEC-CA
eq b = a .
red b .
**> result a : Elt 
-- which shows that SPEC-CA + {b = a} |=^c a = b and  
-- by Case analysis SPEC-CA |=^c a = b
close

-- --------------------------------------------------------------------
-- Exercise 5:

mod* QUEUE={ 
using(QUEUE)
eq [ab]: a @ nil = b @ nil . 
}

-- QUEUE= + {(a = b) = true} |=^c a = b 
open QUEUE=
eq a = b .
red a = b .
close

-- QUEUE= + {(a = b) = false} |=^c  a = b
   -- It suffices to prove that QUEUE= + {(a = b) = false}    
   -- is inconsistent  
open QUEUE= 
eq (a = b) = false . 
-- we prove true = false
start true .
apply -.i-2 with X = a , Q = nil at term .
**> result (a in (a @ nil)) : Bool
apply ab at (2) .
**> result (a in (b @ nil)) : Bool
apply red at term .
** result false : Bool
close 
-- --------------------------------------------------------------------