Skip to content

Commit

Permalink
Reformatted.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Feb 27, 2024
1 parent f237c8a commit d5030c8
Show file tree
Hide file tree
Showing 63 changed files with 507 additions and 507 deletions.
8 changes: 4 additions & 4 deletions src/predicate/existential/existential-1.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ import org.sireum.justification.natded.pred._
//@formatter:off
(human(Socrates), mortal(Socrates)) ⊢ ∃{(x: T) => human(x) & mortal(x)}
Proof(
1 (human(Socrates)) by Premise,
2 (mortal(Socrates)) by Premise,
3 (human(Socrates) & mortal(Socrates)) by AndI(1, 2),
4 (∃{(x: T) => human(x) & mortal(x)}) by ExistsI[T](3)
1 ( human(Socrates) ) by Premise,
2 ( mortal(Socrates) ) by Premise,
3 ( human(Socrates) & mortal(Socrates) ) by AndI(1, 2),
4 ( ∃{(x: T) => human(x) & mortal(x)} ) by ExistsI[T](3)
)
//@formatter:on
)
Expand Down
10 changes: 5 additions & 5 deletions src/predicate/existential/existential-2.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,11 @@ import org.sireum.justification.natded.pred._
//@formatter:off
(vowel(e), holds(square(1, 4), e)) ⊢ ∃{(y: C) => vowel(y) & ∃{(x: C) => holds(x, y)}}
Proof(
1 (vowel(e)) by Premise,
2 (holds(square(1, 4), e)) by Premise,
3 (∃{(x: C) => holds(x, e)}) by ExistsI[C](2),
4 (vowel(e) & ∃{(x: C) => holds(x, e)}) by AndI(1, 3),
5 (∃{(y: C) => vowel(y) & ∃{(x: C) => holds(x, y)}}) by ExistsI[C](4)
1 ( vowel(e) ) by Premise,
2 ( holds(square(1, 4), e) ) by Premise,
3 ( ∃{(x: C) => holds(x, e)} ) by ExistsI[C](2),
4 ( vowel(e) & ∃{(x: C) => holds(x, e)} ) by AndI(1, 3),
5 ( ∃{(y: C) => vowel(y) & ∃{(x: C) => holds(x, y)}} ) by ExistsI[C](4)
)
//@formatter:on
)
Expand Down
10 changes: 5 additions & 5 deletions src/predicate/existential/existential-3.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ import org.sireum.justification.natded.pred._
//@formatter:off
(vowel(e), holds(square(1, 4), e)) ⊢ ∃{(y: C, x: C) => vowel(y) & holds(x, y)}
Proof(
1 (vowel(e)) by Premise,
2 (holds(square(1, 4), e)) by Premise,
3 (vowel(e) & holds(square(1, 4), e)) by AndI(1, 2),
4 (∃{(x: C) => vowel(e) & holds(x, e)}) by ExistsI[C](3),
5 (∃{(y: C, x: C) => vowel(y) & holds(x, y)}) by ExistsI[C](4),
1 ( vowel(e) ) by Premise,
2 ( holds(square(1, 4), e) ) by Premise,
3 ( vowel(e) & holds(square(1, 4), e) ) by AndI(1, 2),
4 ( ∃{(x: C) => vowel(e) & holds(x, e)} ) by ExistsI[C](3),
5 ( ∃{(y: C, x: C) => vowel(y) & holds(x, y)} ) by ExistsI[C](4),
)
//@formatter:on
)
Expand Down
14 changes: 7 additions & 7 deletions src/predicate/existential/existential-4.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,15 @@ import org.sireum.justification.natded.pred._
∃{(z: T) => mortal(z)}
)
Proof(
1 (∀{(x: T) => human(x) __>: mortal(x)}) by Premise,
2 (∃{(y: T) => human(y)}) by Premise,
1 ( ∀{(x: T) => human(x) __>: mortal(x)} ) by Premise,
2 ( ∃{(y: T) => human(y)} ) by Premise,
3 SubProof {(a: T) => (
4 Assume(human(a)),
5 (human(a) __>: mortal(a)) by AllE[T](1),
6 (mortal(a)) by ImplyE(5, 4),
7 (∃{(z: T) => mortal(z)}) by ExistsI[T](6)
4 Assume( human(a) ),
5 ( human(a) __>: mortal(a) ) by AllE[T](1),
6 ( mortal(a) ) by ImplyE(5, 4),
7 ( ∃{(z: T) => mortal(z)} ) by ExistsI[T](6)
)},
8 #> ∃{(z: T) => mortal(z)} by ExistsE[T](2, 3),
8 ( ∃{(z: T) => mortal(z)} ) by ExistsE[T](2, 3),
)
//@formatter:on
)
Expand Down
14 changes: 7 additions & 7 deletions src/predicate/existential/existential-5.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,15 @@ import org.sireum.justification.natded.pred._
!gameOver
)
Proof(
1 (∃{(s: Z) => covered(s) & ∃{(c: C) => vowel(c) & holds(s, c)}}) by Premise,
2 (∃{(x: Z) => covered(x)} __>: !gameOver) by Premise,
1 ( ∃{(s: Z) => covered(s) & ∃{(c: C) => vowel(c) & holds(s, c)}} ) by Premise,
2 ( ∃{(x: Z) => covered(x)} __>: !gameOver ) by Premise,
3 SubProof {(a: Z) => (
4 Assume(covered(a) & ∃{(c: C) => vowel(c) & holds(a, c)}),
5 (covered(a)) by AndE1(4),
6 (∃{(x: Z) => covered(x)}) by ExistsI[Z](5)
4 Assume( covered(a) & ∃{(c: C) => vowel(c) & holds(a, c)} ),
5 ( covered(a) ) by AndE1(4),
6 ( ∃{(x: Z) => covered(x)} ) by ExistsI[Z](5)
)},
7 (∃{(x: Z) => covered(x)}) by ExistsE[Z](1, 3),
8 (!gameOver) by ImplyE(2, 7),
7 ( ∃{(x: Z) => covered(x)} ) by ExistsE[Z](1, 3),
8 ( !gameOver ) by ImplyE(2, 7),
)
//@formatter:on
)
Expand Down
8 changes: 4 additions & 4 deletions src/predicate/universal/universal-1.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ import org.sireum.justification.natded.pred._
mortal(Socrates)
)
Proof(
1 (∀{(x: T) => human(x) __>: mortal(x)}) by Premise,
2 (human(Socrates)) by Premise,
3 (human(Socrates) __>: mortal(Socrates)) by AllE[T](1),
4 (mortal(Socrates)) by ImplyE(3, 2)
1 ( ∀{(x: T) => human(x) __>: mortal(x)} ) by Premise,
2 ( human(Socrates) ) by Premise,
3 ( human(Socrates) __>: mortal(Socrates) ) by AllE[T](1),
4 ( mortal(Socrates) ) by ImplyE(3, 2)
)
//@formatter:on
)
Expand Down
12 changes: 6 additions & 6 deletions src/predicate/universal/universal-2.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,14 @@ import org.sireum.justification.natded.pred._
∀{(x: T) => gt(inc(x), x) & gt(x, dec(x))}
)
Proof(
1 (∀{(x: T) => gt(inc(x), x)}) by Premise,
2 (∀{(x: T) => gt(x, dec(x))}) by Premise,
1 ( ∀{(x: T) => gt(inc(x), x)} ) by Premise,
2 ( ∀{(x: T) => gt(x, dec(x))} ) by Premise,
3 SubProof {(a: T) => (
4 (gt(inc(a), a)) by AllE[T](1),
5 (gt(a, dec(a))) by AllE[T](2),
6 (gt(inc(a), a) & gt(a, dec(a))) by AndI(4, 5)
4 ( gt(inc(a), a) ) by AllE[T](1),
5 ( gt(a, dec(a)) ) by AllE[T](2),
6 ( gt(inc(a), a) & gt(a, dec(a)) ) by AndI(4, 5)
)},
7 (∀{(x: T) => gt(inc(x), x) & gt(x, dec(x))}) by AllI[T](3)
7 ( ∀{(x: T) => gt(inc(x), x) & gt(x, dec(x))} ) by AllI[T](3)
)
//@formatter:on
)
Expand Down
18 changes: 9 additions & 9 deletions src/predicate/universal/universal-3.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,19 +15,19 @@ import org.sireum.justification.natded.pred._
∀{(x: T) => human(x) __>: soul(x)}
)
Proof(
1 (∀{(x: T) => human(x) __>: mortal(x)}) by Premise,
2 (∀{(y: T) => mortal(y) __>: soul(y)}) by Premise,
1 ( ∀{(x: T) => human(x) __>: mortal(x)} ) by Premise,
2 ( ∀{(y: T) => mortal(y) __>: soul(y)} ) by Premise,
3 SubProof {(a: T) => (
4 SubProof(
5 Assume(human(a)),
6 (human(a) __>: mortal(a)) by AllE[T](1),
7 (mortal(a)) by ImplyE(6, 5),
8 (mortal(a) __>: soul(a)) by AllE[T](2),
9 (soul(a)) by ImplyE(8, 7)
5 Assume( human(a) ),
6 ( human(a) __>: mortal(a) ) by AllE[T](1),
7 ( mortal(a) ) by ImplyE(6, 5),
8 ( mortal(a) __>: soul(a) ) by AllE[T](2),
9 ( soul(a) ) by ImplyE(8, 7)
),
10 (human(a) __>: soul(a)) by ImplyI(4)
10 ( human(a) __>: soul(a) ) by ImplyI(4)
)},
11 (∀{(x: T) => human(x) __>: soul(x)}) by AllI[T](3)
11 ( ∀{(x: T) => human(x) __>: soul(x)} ) by AllI[T](3)
)
//@formatter:on
)
Expand Down
14 changes: 7 additions & 7 deletions src/predicate/universal/universal-4.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,17 +10,17 @@ import org.sireum.justification.natded.pred._
//@formatter:off
∀{(x: T) => healthy(x) __>: happy(x)} ⊢ (∀{(y: T) => healthy(y)} __>: ∀{(x: T) => happy(x)})
Proof(
1 (∀{(x: T) => healthy(x) __>: happy(x)}) by Premise,
1 ( ∀{(x: T) => healthy(x) __>: happy(x)} ) by Premise,
2 SubProof(
3 Assume(∀{(y: T) => healthy(y)}),
3 Assume( ∀{(y: T) => healthy(y)} ),
4 SubProof {(a: T) => (
5 (healthy(a)) by AllE[T](3),
6 (healthy(a) __>: happy(a)) by AllE[T](1),
7 (happy(a)) by ImplyE(6, 5)
5 ( healthy(a) ) by AllE[T](3),
6 ( healthy(a) __>: happy(a) ) by AllE[T](1),
7 ( happy(a) ) by ImplyE(6, 5)
)},
8 (∀{(x: T) => happy(x)}) by AllI[T](4)
8 ( ∀{(x: T) => happy(x)} ) by AllI[T](4)
),
9 (∀{(y: T) => healthy(y)} __>: ∀{(x: T) => happy(x)}) by ImplyI(2)
9 ( ∀{(y: T) => healthy(y)} __>: ∀{(x: T) => happy(x)} ) by ImplyI(2)
)
//@formatter:on
)
Expand Down
18 changes: 9 additions & 9 deletions src/programming/auto/procedure-5.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,21 +19,21 @@ val a: ZS = ZS(1, 2, 3)

Deduce(
//@formatter:off
1 (a ≡ ZS(1, 2, 3)) by Premise,
2 (a.size > 1) by Auto
1 ( a ≡ ZS(1, 2, 3) ) by Premise,
2 ( a.size > 1 ) by Auto
//@formatter:on
)

zero2(a)

Deduce(
//@formatter:off
1 (a.size == Old(a).size) by Premise,
2 (a ≡ Old(a)(0 ~> 0)(1 ~> 0)) by Premise,
3 (Old(a) ≡ ZS(1, 2, 3)) by Premise,
4 (a(0) == 0) by Auto* (2, 3),
5 (a(0) == 0) by Auto* (2, 3),
6 (a(2) == 3) by Auto* (2, 3),
7 (a == ZS(0, 0, 3)) by Auto* (2, 3)
1 ( a.size == Old(a).size ) by Premise,
2 ( a ≡ Old(a)(0 ~> 0)(1 ~> 0) ) by Premise,
3 ( Old(a) ≡ ZS(1, 2, 3) ) by Premise,
4 ( a(0) == 0 ) by Auto* (2, 3),
5 ( a(0) == 0 ) by Auto* (2, 3),
6 ( a(2) == 3 ) by Auto* (2, 3),
7 ( a == ZS(0, 0, 3) ) by Auto* (2, 3)
//@formatter:on
)
4 changes: 2 additions & 2 deletions src/programming/auto/procedure-6.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ val zs: ZS = ZS(1, 2, 3)

Deduce(
//@formatter:off
1 (0 <= 0 & 0 < zs.size) by Auto, // obligation for the 1st swap's requires
2 (0 <= 2 & 2 < zs.size) by Auto // obligation for the 2nd swap's requires
1 ( 0 <= 0 & 0 < zs.size ) by Auto, // obligation for the 1st swap's requires
2 ( 0 <= 2 & 2 < zs.size ) by Auto // obligation for the 2nd swap's requires
//@formatter:on
)

Expand Down
8 changes: 4 additions & 4 deletions src/programming/auto/sequence-3.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ import org.sireum.justification._
// Convenient Notations for ∀ and ∃
def foo(a: ZS): Unit = {
Deduce(
1 #> (∀(0 until a.size)(x => P(x)) ≡ ∀{ (x: Z) => (0 <= x & x < a.size) ___>: P(x) }) by Auto T,
2 #> (∀(0 to a.size - 1)(x => P(x)) ≡ ∀{ (x: Z) => (0 <= x & x <= a.size - 1) ___>: P(x) }) by Auto T,
3 #> (∃(0 until a.size)(x => P(x)) ≡ ∃{ (x: Z) => (0 <= x & x < a.size) && P(x) }) by Auto T,
4 #> (∃(0 to a.size - 1)(x => P(x)) ≡ ∃{ (x: Z) => (0 <= x & x <= a.size - 1) && P(x) }) by Auto T
1 ( ∀(0 until a.size)(x => P(x)) ≡ ∀{ (x: Z) => (0 <= x & x < a.size) ___>: P(x) } ) by Auto T,
2 ( ∀(0 to a.size - 1)(x => P(x)) ≡ ∀{ (x: Z) => (0 <= x & x <= a.size - 1) ___>: P(x) } ) by Auto T,
3 ( ∃(0 until a.size)(x => P(x)) ≡ ∃{ (x: Z) => (0 <= x & x < a.size) && P(x) } ) by Auto T,
4 ( ∃(0 to a.size - 1)(x => P(x)) ≡ ∃{ (x: Z) => (0 <= x & x <= a.size - 1) && P(x) } ) by Auto T
)
}
4 changes: 2 additions & 2 deletions src/programming/auto/termination-1.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@ def mult(m: Z, n: Z): Z = {

Deduce(
//@formatter:off
1 (decreasesPost < decreasesPre) by Auto,
2 ((decreasesPost <= 0) __>: !(i != n)) by Auto
1 ( decreasesPost < decreasesPre ) by Auto,
2 ( (decreasesPost <= 0) __>: !(i != n) ) by Auto
//@formatter:on
)
// or
Expand Down
4 changes: 2 additions & 2 deletions src/programming/auto/termination-2.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,8 @@ def factorial(n: Z): Z = {

Deduce(
//@formatter:off
1 (decreasesPost < decreasesPre) by Auto,
2 ((decreasesPost <= 0) __>: !(i < n)) by Auto
1 ( decreasesPost < decreasesPre ) by Auto,
2 ( (decreasesPost <= 0) __>: !(i < n) ) by Auto
//@formatter:on
)
}
Expand Down
4 changes: 2 additions & 2 deletions src/programming/auto/termination-3.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ def multRec(m: Z, n: Z): Z = {

Deduce(
//@formatter:off
1 (decreasesRec < decreasesEntry) by Auto,
2 (decreasesEntry > 0) by Auto
1 ( decreasesRec < decreasesEntry ) by Auto,
2 ( decreasesEntry > 0 ) by Auto
//@formatter:on
)
// or
Expand Down
4 changes: 2 additions & 2 deletions src/programming/manual/assignment-1.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ assume(hours > 2)

Deduce(
//@formatter:off
1 (hours > 2) by Premise,
(hours > 2) by Premise
1 ( hours > 2 ) by Premise,
( hours > 2 ) by Premise
//@formatter:on
)
8 changes: 4 additions & 4 deletions src/programming/manual/assignment-2.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,17 @@ assume(hours > 2)

Deduce(
//@formatter:off
(hours > 2) by Premise
( hours > 2 ) by Premise
//@formatter:on
)

val minutes: Z = hours * 60

Deduce(
//@formatter:off
1 (hours > 2) by Premise,
2 (minutes == hours * 60) by Premise,
3 (minutes > 120) by Algebra*(1, 2)
1 ( hours > 2 ) by Premise,
2 ( minutes == hours * 60 ) by Premise,
3 ( minutes > 120 ) by Algebra*(1, 2)
//@formatter:off
)

Expand Down
20 changes: 10 additions & 10 deletions src/programming/manual/assignment-3.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,29 +8,29 @@ val y: Z = 5

Deduce(
//@formatter:off
1 (x == 1) by Premise,
2 (y == 5) by Premise
1 ( x == 1 ) by Premise,
2 ( y == 5 ) by Premise
//@formatter:on
)

val q: Z = x + y

Deduce(
//@formatter:off
1 (q == x + y) by Premise,
2 (x == 1) by Premise,
3 (y == 5) by Premise,
4 (q == 1 + y) by Subst_<(2, 1),
5 (q == 1 + 5) by Subst_<(3, 4),
6 (q > 5) by Algebra* 5
1 ( q == x + y ) by Premise,
2 ( x == 1 ) by Premise,
3 ( y == 5 ) by Premise,
4 ( q == 1 + y ) by Subst_<(2, 1),
5 ( q == 1 + 5 ) by Subst_<(3, 4),
6 ( q > 5 ) by Algebra* 5
//@formatter:on
)

assert(q > 5)

Deduce(
//@formatter:off
1 (q > 5) by Premise,
2 (x == 1) by Premise
1 ( q > 5 ) by Premise,
2 ( x == 1 ) by Premise
//@formatter:on
)
12 changes: 6 additions & 6 deletions src/programming/manual/assignment-4.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,23 +5,23 @@ import org.sireum.justification._

var hours: Z = 4

Deduce((hours == 4) by Premise)
Deduce(( hours == 4 ) by Premise)

val minutes: Z = hours * 60

Deduce(
//@formatter:off
1 (hours == 4) by Premise,
2 (minutes == hours * 60) by Premise,
3 (minutes == 240) by Algebra*(1, 2)
1 ( hours == 4 ) by Premise,
2 ( minutes == hours * 60 ) by Premise,
3 ( minutes == 240 ) by Algebra*(1, 2)
//@formatter:on
)

hours = 5

Deduce(
//@formatter:off
1 (hours == 5) by Premise,
2 (minutes == 240) by Premise
1 ( hours == 5 ) by Premise,
2 ( minutes == 240 ) by Premise
//@formatter:on
)
10 changes: 5 additions & 5 deletions src/programming/manual/assignment-5.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,16 @@ var x: Z = Z.prompt("Enter an integer > 0: ")

assume(x > 0)

Deduce((x > 0) by Premise)
Deduce(( x > 0 ) by Premise)

x = x + 1

Deduce(
//@formatter:off
1 (x == Old(x) + 1) by Premise,
2 (Old(x) > 0) by Premise,
3 (Old(x) + 1 > 1) by Algebra* 2,
4 (x > 1) by Subst_>(1, 3)
1 ( x == Old(x) + 1 ) by Premise,
2 ( Old(x) > 0 ) by Premise,
3 ( Old(x) + 1 > 1 ) by Algebra* 2,
4 ( x > 1 ) by Subst_>(1, 3)
//@formatter:on
)

Expand Down
Loading

0 comments on commit d5030c8

Please sign in to comment.