Implication (==>)

The implication operator expresses conditional relationships in specifications: "if A then B". It is a proof/specification operator, not a general runtime boolean operator.

Syntax

condition ==> consequence

The expression a ==> b is true when:

• a is false (the condition doesn't hold, so the implication is vacuously true)
• Both a and b are true

It is logically equivalent to not a or b.

==> is accepted in ghost contexts such as contracts, static assert, loop:invariant, pure functions, and lemmas. Runtime expressions should use ordinary if, and, or, and not.

Using Implication in Contracts

Implication is most useful in ensures clauses to express conditional postconditions. Rather than stating what always holds, you state what holds under specific circumstances.

public func sign(x : Int) : async Int
  ensures x >= 0 ==> result >= 0;
  ensures x < 0 ==> result < 0;
{
  if (x >= 0) { x } else { x }
};

This contract says:

• If the input is non-negative, the result is non-negative
• If the input is negative, the result is negative

Using Implication in Assertions

You can use implication inside assert statements to verify logical properties:

public func checkBounds(x : Nat) : async Bool {
  assert x > 10 ==> x > 5;  // If x > 10, then certainly x > 5
  x > 10
};

This means static verification assertions. runtime:assert is executable code and cannot use ==>.

Common Patterns

Guarding Division

Use implication to specify behavior that depends on a condition:

public func safeDivide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
  ensures b > 0 ==> (a >= 0 ==> result >= 0);
{
  a / b
};

Conditional State Changes

Express that a change only happens under certain conditions:

public func maybeIncrement(doIt : Bool) : async ()
  modifies counter
  ensures doIt ==> counter == old(counter) + 1;
  ensures not doIt ==> counter == old(counter);
{
  if (doIt) { counter += 1 };
};

Chained Implications

Multiple implications can express complex conditional logic:

public func classify(n : Nat) : async Nat
  ensures n < 10 ==> (n < 5 ==> result == 0);
  ensures n < 10 ==> (n >= 5 ==> result == 1);
  ensures n >= 10 ==> result == 2;
{
  if (n < 5) { 0 }
  else if (n < 10) { 1 }
  else { 2 }
};

Precedence

The ==> operator has lower precedence than and and or. This means:

a and b ==> c    // Parsed as: (a and b) ==> c
a ==> b or c     // Parsed as: a ==> (b or c)

Use parentheses when the default precedence isn't what you want:

a ==> (b and c)  // Implication to a conjunction
(a ==> b) and c  // Conjunction of an implication and c

The operator is non-associative, so chaining requires explicit parentheses:

// This is rejected:
// a ==> b ==> c

// Use explicit grouping:
a ==> (b ==> c)   // If a, then (if b then c)
(a ==> b) ==> c   // If (a implies b), then c

Truth Table

a	b	a ==> b
false	false	true
false	true	true
true	false	false
true	true	true

Summary

• a ==> b means "if a then b", equivalent to not a or b
• Use in ensures clauses for conditional postconditions
• Only available in ghost/specification contexts
• Lower precedence than and/or, non-associative
• Vacuously true when the antecedent is false

Related Topics

• Biconditional for logical equivalence
• Combining conditions for precedence and larger formulas
• Postconditions for conditional guarantees with result
• Static assertions for checking intermediate logical facts