Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
sig Element {}
one sig Ring{
elements: set Element,
zero: one elements,
un: one elements,
add: elements -> elements -> one elements,
mult: elements -> elements -> one elements,
neg: elements -> one elements
}
fact NoRedundantElements{
all e: Element | e in Ring.elements
}
fact AddZero{
all a: Ring.elements | Ring.add [a] [Ring.zero] = a
all a: Ring.elements | Ring.add [Ring.zero] [a] = a
}
fact AddAssociative{
all a, b, c: Ring.elements | Ring.add [a] [Ring.add [b] [c]] = Ring.add [Ring.add [a] [b]] [c]
}
fact AddCommutative{
all a, b: Ring.elements | Ring.add [a] [b] = Ring.add [b] [a]
}
fact Neg{
all a: Ring.elements | Ring.add [a] [Ring.neg [a]] = Ring.zero
}
fact MultAssociative{
all a, b, c: Ring.elements | Ring.mult [a] [Ring.mult [b] [c]] = Ring.mult [Ring.mult [a] [b]] [c]
}
// Commutative Ring!
fact MultCommutative{
all a, b: Ring.elements | Ring.mult [a] [b] = Ring.mult [b] [a]
}
fact MultDistributive{
all a, b, c: Ring.elements | Ring.mult [a] [Ring.add [b] [c]] = Ring.add [Ring.mult [a] [b]] [Ring.mult [a] [c]]
}
fact MultUn{
all a: Ring.elements | Ring.mult [a] [Ring.un] = a
}
// run {}
pred isIdeal(i: set Element){
Ring.zero in i
all a, b: i | Ring.add [a] [b] in i
all a:i , c: Ring.elements | Ring.mult [c] [a] in i
}
//run {some i: set Element | isIdeal [i]}
assert main{
all i: set Element, a: set Element, b: set Element |
((i in a+b) and
isIdeal[i] and
isIdeal[a] and
isIdeal[b]) implies
((i in a) or (i in b))
}
//check main for 10 //valid
assert main2{
all i: set Element, a: set Element, b: set Element, c: set Element |
((i in a+b+c) and
isIdeal[i] and
isIdeal[a] and
isIdeal[b] and
isIdeal[c]) implies
((i in a) or (i in b) or (i in c))
}
//check main2 for 8
pred isMultClosed(i: set Element){
Ring.un in i
all a, b: i | Ring.mult [a] [b] in i
}
//run {some i: set Element | isMultClosed [i] }
pred pEquiv(a, s, b, t: Element){ //pseudo equivalent
Ring.mult [a] [t] = Ring.mult [b] [s]
}
/* run {some m: set Element, a, b, s, t: Element |
s in m and
t in m and
pEquiv [a] [s] [b] [t]
} */
assert main3{
all mc: set Element, a, b, c, s, t, u: Element |
(isMultClosed [mc] and
s in mc and
t in mc and
u in mc and
pEquiv [a] [s] [b] [t] and
pEquiv [b] [t] [c] [u]) implies
pEquiv [a] [s] [c] [u]
}
// check main3
assert main4{
all mc: set Element, a, b, c, s, t, u: Element |
(isMultClosed [mc] and
s in mc and
t in mc and
u in mc and
pEquiv [a] [s] [b] [t] and
pEquiv [b] [t] [c] [u] and
not Ring.zero in mc) implies
pEquiv [a] [s] [c] [u]
}
check main4 for 4
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment