diff --git a/abstract_syntax.py b/abstract_syntax.py index 3fceb79..740302b 100644 --- a/abstract_syntax.py +++ b/abstract_syntax.py @@ -1831,7 +1831,7 @@ class ImpIntro(Proof): body: Proof def __str__(self): - return 'suppose ' + str(self.label) + ': ' + str(self.premise) + '{' + str(self.body) + '}' + return 'assume ' + str(self.label) + ': ' + str(self.premise) + '{' + str(self.body) + '}' def uniquify(self, env): if self.premise: diff --git a/doc/ProofIntro.md b/doc/ProofIntro.md index 3489362..67028b6 100644 --- a/doc/ProofIntro.md +++ b/doc/ProofIntro.md @@ -622,7 +622,7 @@ proceed by induction as follows. case empty { ? } - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { ? } end @@ -673,7 +673,7 @@ Perhaps we forget the exact definition of `++`, so we can let Deduce tell us the expansion by putting `?` on the right-hand side of the equation. - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { equations node(n,xs') ++ [] = ? by definition operator++ @@ -689,7 +689,7 @@ It has transformed the left-hand side of the equation by expanding the definition of `++`. We copy and paste the `node(n, xs' ++ empty)` to replace the `?`. - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { equations node(n,xs') ++ [] = node(n, xs' ++ []) by definition operator++ @@ -700,7 +700,7 @@ Next, we see that the subterm `xs' ++ []` matches the right-hand side of the induction hypothesis `IH`. We use the `rewrite` statement to apply the `IH` equation to this subterm. - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { equations node(n,xs') ++ [] = node(n, xs' ++ []) by definition operator++ @@ -719,7 +719,7 @@ proof case empty { conclude @[] ++ [] = [] by definition operator++ } - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { equations node(n,xs') ++ [] = node(n, xs' ++ []) by definition operator++ @@ -1004,11 +1004,11 @@ theorem less_max: all x:Nat, y:Nat. x ≤ max'(x,y) proof arbitrary x:Nat, y:Nat switch x ≤ y { - case true suppose x_le_y_true { + case true assume x_le_y_true { suffices x ≤ y by definition max' and rewrite x_le_y_true rewrite x_le_y_true } - case false suppose x_le_y_false { + case false assume x_le_y_false { suffices x ≤ x by definition max' and rewrite x_le_y_false less_equal_refl[x] } @@ -1043,11 +1043,11 @@ Goal: (if length(xs) = 0 then xs = []) ``` -To prove an `if`-`then` formula, we `suppose` the condition and then +To prove an `if`-`then` formula, we `assume` the condition and then prove the conclusion. ``` - suppose len_z: length(xs) = 0 + assume len_z: length(xs) = 0 ``` Deduce adds `len_z` to the givens (similar to `have`). @@ -1067,7 +1067,7 @@ obtain a contradiction. ``` switch xs { case empty { . } - case node(x, xs') suppose xs_xxs: xs = node(x,xs') { + case node(x, xs') assume xs_xxs: xs = node(x,xs') { ? } } @@ -1100,10 +1100,10 @@ theorem list_length_zero_empty: all T:type. all xs:List. proof arbitrary T:type arbitrary xs:List - suppose len_z: length(xs) = 0 + assume len_z: length(xs) = 0 switch xs { case empty { . } - case node(x, xs') suppose xs_xxs: xs = node(x,xs') { + case node(x, xs') assume xs_xxs: xs = node(x,xs') { have len_z2: length(node(x,xs')) = 0 by rewrite xs_xxs in len_z conclude false by apply not_one_add_zero[length(xs')] to definition length in len_z2 @@ -1126,7 +1126,7 @@ theorem length_append_zero_empty: all T:type. all xs:List, ys:List. proof arbitrary T:type arbitrary xs:List, ys:List - suppose len_xs_ys: length(xs ++ ys) = 0 + assume len_xs_ys: length(xs ++ ys) = 0 ? end ``` @@ -1182,7 +1182,7 @@ theorem length_append_zero_empty: all T:type. all xs:List, ys:List. proof arbitrary T:type arbitrary xs:List, ys:List - suppose len_xs_ys: length(xs ++ ys) = 0 + assume len_xs_ys: length(xs ++ ys) = 0 have len_xs_len_ys: length(xs) + length(ys) = 0 by transitive (symmetric length_append[xs][ys]) len_xs_ys have len_xs: length(xs) = 0 by apply add_to_zero to len_xs_len_ys @@ -1196,7 +1196,7 @@ end To summarize this section: * A conditional formula is stated in Deduce using the `if`-`then` syntax. -* To prove an `if`-`then` formula, `suppose` the condition +* To prove an `if`-`then` formula, `assume` the condition and prove the conclusion. * To use a fact that is an `if`-`then` formula, `apply` it `to` a proof of the condition. @@ -1235,7 +1235,7 @@ theorem contra_false: all a:bool, b:bool. if a = b and a = true and b = false then false proof arbitrary a:bool, b:bool - suppose prem: a = b and a = true and b = false + assume prem: a = b and a = true and b = false have a_true: a = true by prem have b_true: b = false by prem conclude false by rewrite a_true | b_true in prem @@ -1273,7 +1273,7 @@ we have a premise that is `false`, it doesn't matter. theorem false_any: all x:bool, y:bool. if false then x = y proof arbitrary x:bool, y:bool - suppose f: false + assume f: false conclude x = y by f end ``` @@ -1299,18 +1299,18 @@ We proceed by induction. case zero { ? } - case suc(x') suppose IH: not (x' < x') { + case suc(x') assume IH: not (x' < x') { ? } Deduce treats `not` as syntactic sugar for a conditional formal with a `false` conclusion. So in the first case, we must prove that `0 < 0` implies `false`. -So we `suppose` the premise `0 < 0` and then conclude `false` by the +So we `assume` the premise `0 < 0` and then conclude `false` by the definitions of `<` and `≤`. case zero { - suppose z_l_z: 0 < 0 + assume z_l_z: 0 < 0 conclude false by definition {operator <, operator ≤} in z_l_z } @@ -1319,7 +1319,7 @@ that `suc(x') < suc(x')` implies `false`. So we assume the premise `suc(x') < suc(x')` from which we can prove that `x' < x'` using the definitions of `<` and `≤`. - suppose sx_l_sx: suc(x') < suc(x') + assume sx_l_sx: suc(x') < suc(x') enable {operator <, operator ≤} have x_l_x: x' < x' by sx_l_sx @@ -1335,11 +1335,11 @@ theorem intro_less_irreflexive: all x:Nat. not (x < x) proof induction Nat case zero { - suppose z_l_z: 0 < 0 + assume z_l_z: 0 < 0 conclude false by definition {operator <, operator ≤} in z_l_z } - case suc(x') suppose IH: not (x' < x') { - suppose sx_l_sx: suc(x') < suc(x') + case suc(x') assume IH: not (x' < x') { + assume sx_l_sx: suc(x') < suc(x') enable {operator <, operator ≤} have x_l_x: x' < x' by sx_l_sx conclude false by apply IH to x_l_x @@ -1351,7 +1351,7 @@ To summarize this section: * To expression that a formula is false, use `not`. * Deduce treats the formula `not P` just like `if P then false`. -* Therefore, to prove a `not` formula, suppose `P` then prove `false`. +* Therefore, to prove a `not` formula, assume `P` then prove `false`. * To use a formula like `not P`, apply it to a proof of `P` to obtain a proof of `false`. @@ -1369,7 +1369,7 @@ theorem intro_less_not_equal: all x:Nat, y:Nat. if x < y then not (x = y) proof arbitrary x:Nat, y:Nat - suppose x_l_y: x < y + assume x_l_y: x < y ? end ``` @@ -1385,11 +1385,11 @@ Givens: x_l_y: x < y ``` -So following the usual recipe to prove an `if`-`then`, we `suppose` the +So following the usual recipe to prove an `if`-`then`, we `assume` the condition `x = y`. ``` - suppose x_y: x = y + assume x_y: x = y ``` Now we need to prove false, and we have the hint to use the @@ -1427,8 +1427,8 @@ theorem intro_less_not_equal: all x:Nat, y:Nat. if x < y then not (x = y) proof arbitrary x:Nat, y:Nat - suppose x_l_y: x < y - suppose x_y: x = y + assume x_l_y: x < y + assume x_y: x = y have y_l_y: y < y by rewrite x_y in x_l_y conclude false by apply intro_less_irreflexive[y] to y_l_y end @@ -1467,7 +1467,7 @@ numbers is an even number. Here's the beginning of the proof. if Even(x) and Even(y) then Even(x + y) proof arbitrary x:Nat, y:Nat - suppose even_xy: Even(x) and Even(y) + assume even_xy: Even(x) and Even(y) have even_x: some m:Nat. x = 2 * m by definition Even in even_xy have even_y: some m:Nat. y = 2 * m by definition Even in even_xy ? @@ -1533,7 +1533,7 @@ theorem intro_addition_of_evens: if Even(x) and Even(y) then Even(x + y) proof arbitrary x:Nat, y:Nat - suppose even_xy: Even(x) and Even(y) + assume even_xy: Even(x) and Even(y) have even_x: some m:Nat. x = 2 * m by definition Even in even_xy have even_y: some m:Nat. y = 2 * m by definition Even in even_xy obtain a where x_2a: x = 2*a from even_x diff --git a/doc/Reference.md b/doc/Reference.md index 612fd7c..46650f5 100644 --- a/doc/Reference.md +++ b/doc/Reference.md @@ -194,7 +194,7 @@ theorem apply_to_example: all P:bool, Q:bool, R:bool. then R proof arbitrary P:bool, Q:bool, R:bool - suppose prem: (if P then Q) and (if Q then R) and P + assume prem: (if P then Q) and (if Q then R) and P have pq: if P then Q by prem have p: P by prem have q: Q by apply pq to p @@ -1121,7 +1121,7 @@ proof case 0 { conclude 0 + 0 = 0 by definition operator+ } - case suc(n') suppose IH: n' + 0 = n' { + case suc(n') assume IH: n' + 0 = n' { equations suc(n') + 0 = suc(n' + 0) by definition operator+ ... = suc(n') by rewrite IH @@ -1146,7 +1146,7 @@ theorem injective_example: all x:Nat, y:Nat, z:Nat. if suc(x) = suc(y) and suc(y) = suc(z) then x = z proof arbitrary x:Nat, y:Nat, z:Nat - suppose prem: suc(x) = suc(y) and suc(y) = suc(z) + assume prem: suc(x) = suc(y) and suc(y) = suc(z) have: x = y by injective suc prem have: y = z by injective suc prem transitive (recall x = y) (recall y = z) @@ -1312,7 +1312,7 @@ proof to only apply to that subterm. theorem mark_example: all x:Nat. if x = 1 then x + x + x = 3 proof arbitrary x:Nat - suppose: x = 1 + assume: x = 1 equations #x# + x + x = 1 + x + x by rewrite recall x = 1 $ 1 + #x# + x = 1 + 1 + x by rewrite recall x = 1 diff --git a/gh-pages/deduce-code/proof_contra_false.pf b/gh-pages/deduce-code/proof_contra_false.pf index a2b1da0..eb3912a 100644 --- a/gh-pages/deduce-code/proof_contra_false.pf +++ b/gh-pages/deduce-code/proof_contra_false.pf @@ -8,7 +8,7 @@ theorem contra_false: all a:bool, b:bool. if a = b and a = true and b = false then false proof arbitrary a:bool, b:bool - suppose prem: a = b and a = true and b = false + assume prem: a = b and a = true and b = false have a_true: a = true by prem have b_true: b = false by prem conclude false by rewrite a_true | b_true in prem diff --git a/gh-pages/deduce-code/proof_false_any.pf b/gh-pages/deduce-code/proof_false_any.pf index 0f1710b..99791c6 100644 --- a/gh-pages/deduce-code/proof_false_any.pf +++ b/gh-pages/deduce-code/proof_false_any.pf @@ -7,6 +7,6 @@ import Maps theorem false_any: all x:bool, y:bool. if false then x = y proof arbitrary x:bool, y:bool - suppose f: false + assume f: false conclude x = y by f end \ No newline at end of file diff --git a/gh-pages/deduce-code/proof_intro_addition_of_evens.pf b/gh-pages/deduce-code/proof_intro_addition_of_evens.pf index 82dd1e4..b4b70a2 100644 --- a/gh-pages/deduce-code/proof_intro_addition_of_evens.pf +++ b/gh-pages/deduce-code/proof_intro_addition_of_evens.pf @@ -9,7 +9,7 @@ theorem intro_addition_of_evens: if Even(x) and Even(y) then Even(x + y) proof arbitrary x:Nat, y:Nat - suppose even_xy: Even(x) and Even(y) + assume even_xy: Even(x) and Even(y) have even_x: some m:Nat. x = 2 * m by definition Even in even_xy have even_y: some m:Nat. y = 2 * m by definition Even in even_xy obtain a where x_2a: x = 2*a from even_x diff --git a/gh-pages/deduce-code/proof_intro_less_irreflexive.pf b/gh-pages/deduce-code/proof_intro_less_irreflexive.pf index f67a285..05485f7 100644 --- a/gh-pages/deduce-code/proof_intro_less_irreflexive.pf +++ b/gh-pages/deduce-code/proof_intro_less_irreflexive.pf @@ -8,11 +8,11 @@ theorem intro_less_irreflexive: all x:Nat. not (x < x) proof induction Nat case zero { - suppose z_l_z: 0 < 0 + assume z_l_z: 0 < 0 conclude false by definition {operator <, operator ≤} in z_l_z } - case suc(x') suppose IH: not (x' < x') { - suppose sx_l_sx: suc(x') < suc(x') + case suc(x') assume IH: not (x' < x') { + assume sx_l_sx: suc(x') < suc(x') enable {operator <, operator ≤} have x_l_x: x' < x' by sx_l_sx conclude false by apply IH to x_l_x diff --git a/gh-pages/deduce-code/proof_intro_less_not_equal.pf b/gh-pages/deduce-code/proof_intro_less_not_equal.pf index 43eebd7..e860b7e 100644 --- a/gh-pages/deduce-code/proof_intro_less_not_equal.pf +++ b/gh-pages/deduce-code/proof_intro_less_not_equal.pf @@ -8,8 +8,8 @@ theorem intro_less_not_equal: all x:Nat, y:Nat. if x < y then not (x = y) proof arbitrary x:Nat, y:Nat - suppose x_l_y: x < y - suppose x_y: x = y + assume x_l_y: x < y + assume x_y: x = y have y_l_y: y < y by rewrite x_y in x_l_y conclude false by apply intro_less_irreflexive[y] to y_l_y end \ No newline at end of file diff --git a/gh-pages/deduce-code/proof_length_append_zero_empty.pf b/gh-pages/deduce-code/proof_length_append_zero_empty.pf index c485fa1..c02223b 100644 --- a/gh-pages/deduce-code/proof_length_append_zero_empty.pf +++ b/gh-pages/deduce-code/proof_length_append_zero_empty.pf @@ -10,7 +10,7 @@ theorem length_append_zero_empty: all T:type. all xs:List, ys:List. proof arbitrary T:type arbitrary xs:List, ys:List - suppose len_xs_ys: length(xs ++ ys) = 0 + assume len_xs_ys: length(xs ++ ys) = 0 have len_xs_len_ys: length(xs) + length(ys) = 0 by transitive (symmetric length_append[xs][ys]) len_xs_ys have len_xs: length(xs) = 0 by apply add_to_zero to len_xs_len_ys diff --git a/gh-pages/deduce-code/proof_less_alt_max.pf b/gh-pages/deduce-code/proof_less_alt_max.pf index 99ffdd9..7f05a69 100644 --- a/gh-pages/deduce-code/proof_less_alt_max.pf +++ b/gh-pages/deduce-code/proof_less_alt_max.pf @@ -8,11 +8,11 @@ theorem less_max: all x:Nat, y:Nat. x ≤ max'(x,y) proof arbitrary x:Nat, y:Nat switch x ≤ y { - case true suppose x_le_y_true { + case true assume x_le_y_true { suffices x ≤ y by definition max' and rewrite x_le_y_true rewrite x_le_y_true } - case false suppose x_le_y_false { + case false assume x_le_y_false { suffices x ≤ x by definition max' and rewrite x_le_y_false less_equal_refl[x] } diff --git a/gh-pages/deduce-code/proof_list_append_empty.pf b/gh-pages/deduce-code/proof_list_append_empty.pf index 783adba..ae8451a 100644 --- a/gh-pages/deduce-code/proof_list_append_empty.pf +++ b/gh-pages/deduce-code/proof_list_append_empty.pf @@ -12,7 +12,7 @@ proof case empty { conclude @[] ++ [] = [] by definition operator++ } - case node(n, xs') suppose IH: xs' ++ [] = xs' { + case node(n, xs') assume IH: xs' ++ [] = xs' { equations node(n,xs') ++ [] = node(n, xs' ++ []) by definition operator++ diff --git a/gh-pages/deduce-code/proof_list_length_zero_empty.pf b/gh-pages/deduce-code/proof_list_length_zero_empty.pf index b58caf7..c10fb52 100644 --- a/gh-pages/deduce-code/proof_list_length_zero_empty.pf +++ b/gh-pages/deduce-code/proof_list_length_zero_empty.pf @@ -9,10 +9,10 @@ theorem list_length_zero_empty: all T:type. all xs:List. proof arbitrary T:type arbitrary xs:List - suppose len_z: length(xs) = 0 + assume len_z: length(xs) = 0 switch xs { case empty { . } - case node(x, xs') suppose xs_xxs: xs = node(x,xs') { + case node(x, xs') assume xs_xxs: xs = node(x,xs') { have len_z2: length(node(x,xs')) = 0 by rewrite xs_xxs in len_z conclude false by apply not_one_add_zero[length(xs')] to definition length in len_z2 diff --git a/gh-pages/deduce-code/reference_apply_to_example.pf b/gh-pages/deduce-code/reference_apply_to_example.pf index e340691..ac2fd3e 100644 --- a/gh-pages/deduce-code/reference_apply_to_example.pf +++ b/gh-pages/deduce-code/reference_apply_to_example.pf @@ -9,7 +9,7 @@ theorem apply_to_example: all P:bool, Q:bool, R:bool. then R proof arbitrary P:bool, Q:bool, R:bool - suppose prem: (if P then Q) and (if Q then R) and P + assume prem: (if P then Q) and (if Q then R) and P have pq: if P then Q by prem have p: P by prem have q: Q by apply pq to p diff --git a/gh-pages/deduce-code/reference_induction_example.pf b/gh-pages/deduce-code/reference_induction_example.pf index 29efa4c..015111a 100644 --- a/gh-pages/deduce-code/reference_induction_example.pf +++ b/gh-pages/deduce-code/reference_induction_example.pf @@ -11,7 +11,7 @@ proof case 0 { conclude 0 + 0 = 0 by definition operator+ } - case suc(n') suppose IH: n' + 0 = n' { + case suc(n') assume IH: n' + 0 = n' { equations suc(n') + 0 = suc(n' + 0) by definition operator+ ... = suc(n') by rewrite IH diff --git a/gh-pages/deduce-code/reference_injective_example.pf b/gh-pages/deduce-code/reference_injective_example.pf index 58d47db..43639fd 100644 --- a/gh-pages/deduce-code/reference_injective_example.pf +++ b/gh-pages/deduce-code/reference_injective_example.pf @@ -8,7 +8,7 @@ theorem injective_example: all x:Nat, y:Nat, z:Nat. if suc(x) = suc(y) and suc(y) = suc(z) then x = z proof arbitrary x:Nat, y:Nat, z:Nat - suppose prem: suc(x) = suc(y) and suc(y) = suc(z) + assume prem: suc(x) = suc(y) and suc(y) = suc(z) have: x = y by injective suc prem have: y = z by injective suc prem transitive (recall x = y) (recall y = z) diff --git a/gh-pages/deduce-code/reference_mark_example.pf b/gh-pages/deduce-code/reference_mark_example.pf index d3fbace..79bc1f3 100644 --- a/gh-pages/deduce-code/reference_mark_example.pf +++ b/gh-pages/deduce-code/reference_mark_example.pf @@ -7,7 +7,7 @@ import Maps theorem mark_example: all x:Nat. if x = 1 then x + x + x = 3 proof arbitrary x:Nat - suppose: x = 1 + assume: x = 1 equations #x# + x + x = 1 + x + x by rewrite recall x = 1 $ 1 + #x# + x = 1 + 1 + x by rewrite recall x = 1 diff --git a/gh-pages/pages/deduce-proofs.html b/gh-pages/pages/deduce-proofs.html index f4336c2..34f2aca 100644 --- a/gh-pages/pages/deduce-proofs.html +++ b/gh-pages/pages/deduce-proofs.html @@ -447,7 +447,7 @@

Proving all     ?
  }
-  case node(n, xs') suppose IH: xs' ++ [] = xs' {
+  case node(n, xs') assume IH: xs' ++ [] = xs' {
    ?
  }
end
@@ -492,7 +492,7 @@

Proving all++, so we can let Deduce tell us the expansion by putting ? on the right-hand side of the equation.

-
case node(n, xs') suppose IH: xs' ++ [] = xs' {
+
case node(n, xs') assume IH: xs' ++ [] = xs' {
  equations
    node(n,xs') ++ []
        = ?                       by definition operator++
@@ -506,7 +506,7 @@

Proving allIt has transformed the left-hand side of the equation by expanding the definition of ++. We copy and paste the node(n, xs' ++ empty) to replace the ?.

-
case node(n, xs') suppose IH: xs' ++ [] = xs' {
+
case node(n, xs') assume IH: xs' ++ [] = xs' {
  equations
    node(n,xs') ++ []
        = node(n, xs' ++ [])   by definition operator++
@@ -516,7 +516,7 @@

Proving allNext, we see that the subterm xs' ++ [] matches the right-hand side of the induction hypothesis IH. We use the rewrite statement to apply the IH equation to this subterm.

-
case node(n, xs') suppose IH: xs' ++ [] = xs' {
+
case node(n, xs') assume IH: xs' ++ [] = xs' {
  equations
    node(n,xs') ++ []
        = node(n, xs' ++ [])   by definition operator++
@@ -713,9 +713,9 @@

Cond
incomplete proof
Goal:
    (if length(xs) = 0 then xs = [])
-

To prove an if-then formula, we suppose the condition and then +

To prove an if-then formula, we assume the condition and then prove the conclusion.

-
  suppose len_z: length(xs) = 0
+
  assume len_z: length(xs) = 0

Deduce adds len_z to the givens (similar to have).

incomplete proof
Goal:
@@ -727,7 +727,7 @@

Cond obtain a contradiction.

  switch xs {
    case empty { . }
-    case node(x, xs') suppose xs_xxs: xs = node(x,xs') {
+    case node(x, xs') assume xs_xxs: xs = node(x,xs') {
      ?
    }
  }
@@ -754,7 +754,7 @@

Cond proof
  arbitrary T:type
  arbitrary xs:List<T>, ys:List<T>
-  suppose len_xs_ys: length(xs ++ ys) = 0
+  assume len_xs_ys: length(xs ++ ys) = 0
  ?
end

Recall that in a previous exercise, you proved that

@@ -782,7 +782,7 @@

Cond

To summarize this section:

  • A conditional formula is stated in Deduce using the if-then syntax.
    • -
  • To prove an if-then formula, suppose the condition +
  • To prove an if-then formula, assume the condition and prove the conclusion.
  • To use a fact that is an if-then formula, apply it to a proof of the condition.
    • @@ -844,17 +844,17 @@

    Reasoning about not

      ?
    }
    -case suc(x') suppose IH: not (x' < x') {
    +case suc(x') assume IH: not (x' < x') {
      ?
    }

Deduce treats not as syntactic sugar for a conditional formal with a false conclusion. So in the first case, we must prove that 0 < 0 implies false. -So we suppose the premise 0 < 0 and then conclude false by the +So we assume the premise 0 < 0 and then conclude false by the definitions of < and ≤.

case zero {
-  suppose z_l_z: 0 < 0
+  assume z_l_z: 0 < 0
  conclude false by definition {operator <, operator ≤} in z_l_z
}
@@ -862,7 +862,7 @@

Reasoning about not

suc(x') < suc(x') implies false. So we assume the premise suc(x') < suc(x') from which we can prove that x' < x' using the definitions of < and ≤.

-
suppose sx_l_sx: suc(x') < suc(x')
+
assume sx_l_sx: suc(x') < suc(x')
enable {operator <, operator ≤}
have x_l_x: x' < x' by sx_l_sx
@@ -875,7 +875,7 @@

Reasoning about not

  • To expression that a formula is false, use not.
  • Deduce treats the formula not P just like if P then false.
    • -
  • Therefore, to prove a not formula, suppose P then prove false.
    • +
  • Therefore, to prove a not formula, assume P then prove false.
  • To use a formula like not P, apply it to a proof of P to obtain a proof of false.
    • @@ -890,7 +890,7 @@

    Rewriting Facts with Equations

      if x < y then not (x = y)
    proof
      arbitrary x:Nat, y:Nat
    -  suppose x_l_y: x < y
    +  assume x_l_y: x < y
      ?
    end

    Deduce responds with the current goal, in which not (x = y) is @@ -900,9 +900,9 @@

    Rewriting Facts with Equations

        (if x = y then false)
    Givens:
        x_l_y: x < y
    -

    So following the usual recipe to prove an if-then, we suppose the +

    So following the usual recipe to prove an if-then, we assume the condition x = y.

    -
      suppose x_y: x = y
    +
      assume x_y: x = y

    Now we need to prove false, and we have the hint to use the intro_less_irreflexive theorem.

    incomplete proof
    @@ -940,7 +940,7 @@

    Reasoning about proof
      arbitrary x:Nat, y:Nat
    -  suppose even_xy: Even(x) and Even(y)
    +  assume even_xy: Even(x) and Even(y)
      have even_x: some m:Nat. x = 2 * m by definition Even in even_xy
      have even_y: some m:Nat. y = 2 * m by definition Even in even_xy
      ?
    diff --git a/index.md b/index.md index adf167d..a68fe28 100644 --- a/index.md +++ b/index.md @@ -43,7 +43,7 @@ proof suffices not (y ∈ ∅) by definition {search, take, set_of} empty_no_members } - case node(x, xs') suppose + case node(x, xs') assume IH: (all y:Nat. not (y ∈ set_of(take(search(xs', y), xs')))) { arbitrary y:Nat @@ -55,7 +55,7 @@ proof case false assume xy_false: (x = y) = false { suffices not (y ∈ single(x) ∪ set_of(take(search(xs', y), xs'))) by definition {take, set_of} - suppose c: y ∈ single(x) ∪ set_of(take(search(xs', y), xs')) + assume c: y ∈ single(x) ∪ set_of(take(search(xs', y), xs')) cases (apply member_union to c) case y_in_x: y ∈ single(x) { have: x = y by apply single_equal to y_in_x diff --git a/proof_checker.py b/proof_checker.py index f8fa29b..8b07425 100644 --- a/proof_checker.py +++ b/proof_checker.py @@ -860,7 +860,7 @@ def proof_advice(formula, env): if num_recursive > 0: rec_params =[(p,ty) for (p,ty) in zip(params,param_types)\ if is_recursive(name, ty)] - ind_advice += ' suppose ' + ind_advice += ' assume ' ind_advice += ',\n\t\t\t'.join(['IH' + str(i+1) + ': ' \ + str(body.substitute({var_x: Var(loc3, param_ty, param, [])})) \ for i, (param,param_ty) in enumerate(rec_params)]) @@ -1382,7 +1382,7 @@ def check_proof_of(proof, formula, env): if assumptions[0][1] != None: case_assumption = type_synth_term(assumptions[0][1], body_env, None, []) if case_assumption != new_assumption: - error(scase.location, 'in case, expected suppose of\n' + str(new_assumption) \ + error(scase.location, 'in case, expected assume of\n' + str(new_assumption) \ + '\nnot\n' + str(case_assumption)) body_env = body_env.declare_local_proof_var(loc, assumptions[0][0], new_assumption) if len(assumptions) > 1: diff --git a/test/should-error/induction2.pf.err b/test/should-error/induction2.pf.err index 8ada766..ca822ce 100644 --- a/test/should-error/induction2.pf.err +++ b/test/should-error/induction2.pf.err @@ -12,7 +12,7 @@ Advice: case empty(b1) { ? } - case node(T1, N2, T3) suppose IH1: size(T1) = size(T1), + case node(T1, N2, T3) assume IH1: size(T1) = size(T1), IH2: size(T3) = size(T3) { ? } diff --git a/test/should-error/induction_advice_partial.pf.err b/test/should-error/induction_advice_partial.pf.err index 6444290..fc98259 100644 --- a/test/should-error/induction_advice_partial.pf.err +++ b/test/should-error/induction_advice_partial.pf.err @@ -12,7 +12,7 @@ Advice: case zero { ? } - case suc(N1) suppose IH1: suc(length(null)) = length(cons(N1, null)) { + case suc(N1) assume IH1: suc(length(null)) = length(cons(N1, null)) { ? }