Class 10

// Let's step back and try to understand better how Dafny processes proofs, so
// we can better predict what will be accepted.  This section of the code is
// heavily inspired by Amazon's training materials at:
//   https://dafny.org/teaching-material/Lectures/2-4-Logic-ProvingByConvincing.html

// First, a review from the associated reading and the previous class:

// Consider this lemma statement.
lemma Example(x: int) 
  requires x % 2 == 0 
  ensures 2 * (x / 2) == x

// We can explain what we are asking Dafny to prove using a notation for *goals*
// inspired by the literature on automated computer theorem proving.
//   x: int, x % 2 == 0 |- 2 * (x / 2) == x
// The "|-" is a "turnstile," which separates assumptions (lefthand side) from
// conclusions (righthand side).  Assumptions can include variables like `x`
// with their types, as well as logical facts, and we separate the parts with
// commas.  The goal can be read as a "proof challenge": prove the conclusion,
// assuming only the given assumptions.

// How can we predict which proof challenges Dafny can meet?  A fully precise
// answer is very difficult to give, but we will survey some simple rules that
// are safe to assume Dafny will apply automatically.

// The following goes through automatically, despite being a bit of a mouthful.
lemma UseAssumption<T1, T2, T3, T4>(x1: T1, x2: int, x3: int -> T4, P: bool, Q: T1 -> bool)
  requires Q(x1)
  requires P
  ensures P
{
}
// Intuitively, we expect that proof is easy, because we assume what we want to
// prove!  We can use our goal notation to explain what rule we want Dafny to use.
// I'll write 'G' in place of the Greek letter capital Gamma that is more commonly
// used in the literature.
//   G, P |- P
// Assumptions are fundamentally unordered, so the notation above is just for
// picking some known fact `P` out of the assumptions.  If we are trying to
// prove that fact, we are done.

// Every logical connective has its associated rules that explain how to work
// with it.  We need to know how to *prove* a connective, with what are called
// *introduction* rules; and we need to know how to *use* a connective to prove
// something else, and these are called *elimination* rules.  (Don't worry about
// that terminology for purposes of this class; we just mention the words for
// those curious to read more outside our scope.)

// The easiest example is "and".
// How to prove it:
//   G, P, Q |- P && Q
// In other words, if you know `P` and `Q`, you know `P && Q`.
// We kind of just switched out one kind of "and" for another!

// How to use it:
//   G, P && Q |- P
//   G, P && Q |- Q
// In other words, if you know `P && Q`, you also know either operand.

// Each of these rules can be embodied as a fully general Dafny lemma.  We'll go
// through the exercise for "and" but not bother for most later examples.

lemma ProveAnd(P: bool, Q: bool)
  requires P
  requires Q
  ensures P && Q
{
}

lemma UseAnd1(P: bool, Q: bool)
  requires P && Q
  ensures P
{
}

lemma UseAnd2(P: bool, Q: bool)
  requires P && Q
  ensures Q
{
}

// We could invoke these lemmas from other proofs, but it isn't worth the
// effort, because Dafny already applies these rules automatically.

// Let's take a look at "or".
// How to prove it:
//   G, P |- P || Q
//   G, Q |- P || Q
// How to use it:
//   G, P || Q, P ==> R, Q ==> R ⊢ R
// That last rule is interesting for using the implication connective `==>`,
// too.  The rule is basically formalizing the idea of a proof by cases.  At
// least one of `P` or `Q` must be true, and we check that our goal is provable
// under either new assumption.
// Translating the above into lemmas:

lemma ProveOr1(P: bool, Q: bool)
  requires P
  ensures P || Q
{
}

lemma ProveOr2(P: bool, Q: bool)
  requires Q
  ensures P || Q
{
}

lemma UseOr(P: bool, Q: bool, R: bool)
  requires P || Q
  requires P ==> R
  requires Q ==> R
  ensures R
{
}

// But then how do we prove implications?  The rule says that if we are looking
// at proving:
//   G |- P ==> Q
// we can switch to proving instead:
//   G, P |- Q
// The new premise moves into our assumptions.
// And using an implication is as simple as the classic modus ponens rule:
//   G, P ==> Q, P |- Q

// We can think of negation as implication of falsehood, giving rise to two rules.
//   G, P ==> false |- !P
//   G, P, !P |- false

// And then we can explain falsehood itself, which notably has no rule to prove it.
//   G, false |- P
// That is, when we know `false`, we can conclude anything, because the situation
// is inherently contradictory.

// We can think of `P <==> Q` as expanding to `(P ==> Q) && (Q ==> P)`, which
// implies the following rules.
//   G, P ==> Q, Q ==> P |- P <==> Q
//   G, P <==> Q |- P ==> Q
//   G, P <==> Q |- Q ==> P

// Quantifiers are more interesting still.  Here's `exists`.
//   G, k: T, P(k) |- exists c: T :: P(c)
// In other words, to prove an existential, we should find a known fact that
// matches the body of the quantifier, with a specific witness plugged in.
// To use an `exists`:
//   G, (exists x: T :: P(x)), (forall x: T :: P(x) ==> Q) ⊢ Q
// The rule lefts us switch to thinking in terms of all potential witnesses for
// the quantifier, via a `forall`, which tends to be easier to work with.

// But how *do* we work with `forall`?  The easiest is using one.
//   G, (forall x: T :: P(x)), c: T |- P(c)
// Any value of the right type yields a true fact, when plugged into the
// quantifier.
// How do we prove a `forall`?  This one we have to express like for
// implication, as a rule for transforming a goal into a simpler one.
// To prove:
//   G |- forall x: T :: P(x)
// We can switch to proving:
//   G, x : T |- P(x)
// Note how the quantified variable became part of the proof goal, like any
// other variable that might e.g. be a lemma parameter.

// With those rules stated, let's see how Dafny produces proof challenges to
// tackle, given the structure of a lemma or other code.

type T
predicate P(x: T)
predicate Q(x: T)
predicate R(x: T)

lemma Example2(x: T) 
  requires P(x) 
  ensures Q(x) 
{
  // We start from this goal, read off from the lemma statement.
  // x: T, P(x) |- Q(x)

  // Then whatever follows is supposed to *transform* the goal into one that is
  // easily enough proved using the rules we gave above, e.g. a simple case
  // where we managed to get `Q(x)` as an assumption.

  // x: T, P(x), Q(x) |- Q(x)

  assume false; // This marker included just to avoid Dafny complaining.
                // We know the proof isn't finished!
}

// Let's see how different programming constructs tweak proof goals.

lemma AssertExample(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  assert R(x) by {
    // x: T, P(x) |- R(x)
    assume false;
  }

  // We get the conclusion of the `assert` added as a new assumption.
  // x: T, P(x), R(x) |- Q(x)

  assume false;
}

lemma AssumeExample(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  assume R(x);
  // T, x: T, P(x), R(x) |- Q(x)
  // We unceremoniously added a new assumption without proving it.
  assume false;
}

lemma Premise(x: T)
  requires P(x)
  ensures R(x)

lemma HelperExample(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  Premise(x); // x: T, P(x) |- P(x) [proving the precondition]
  // T, x: T, P(x), R(x) |- Q(x)
  // We added the postcondition of `Premise` as a new assumption.
  assume false;
}

// Note how the following is subtly different, for using logical implication
// instead of a precondition.
lemma Premise2(x: T)
  ensures P(x) ==> R(x)

lemma HelperExample2(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  Premise2(x);
  // x: T, P(x), P(x) ==> R(x) |- Q(x)
  assume false;
}

// We can go even further and use `forall` instead of a lemma parameter.
lemma Premise3()
  ensures forall x: T :: P(x) ==> R(x)

lemma HelperExample3(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  Premise3();
  // x: T, P(x), forall x: T :: P(x) ==> R(x) |- Q(x)
  assume false;
}

lemma IfExample(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  if R(x) {
    // x: T, P(x), R(x) |- S(x)
    // The `if` expression is added as an assumption.
    assume false;
  }
  // x: T, P(x), R(x) ==> S(x) |- Q(x)
  // Note how the goal of the `if` is wrapped in an implication, to produce what
  // we remember afterward.
  assume false;
}

lemma IfExample2(x: T)
  ensures P(x) ==> Q(x)
{
  // x: T |- P(x) ==> Q(x)
  if P(x) {
    Premise(x); // x: T, P(x) |- P(x) [proving precondition]
    // x: T, P(x), Q(x) |- R(x)
    // ^-- added postcondition, and we arbitrarily chose to prove `R(x)`.
  }
  // x: T, P(x) ==> R(x) |- P(x) ==> Q(x)
  assume false;
}

lemma ForallExample(x: T)
  requires P(x)
  ensures Q(x)
{
  // x: T, P(x) |- Q(x)
  forall x: T
    ensures R(x)
  {
    // x: T, P(x) |- R(x)
    // Note how (1) the variable was added to the assumptions, and (2) the
    // `forall` body became our conclusion.
    assume false;
  }
  // T, x: T, P(x), forall x: T :: R(x) |- Q(x)
  // Then we get the expected `forall` as a new assumption.
  assume false;
}

predicate A()
predicate B()
predicate C()

lemma ExistsExample()
  requires exists y: T :: P(y)
  ensures A()
{
  // exists x: T :: P(x) |- A()
  var y: T :| P(y); 
  // y: T, P(y) |- A()
  assume false;
}

lemma AssignmentExample(x: T)
  ensures A()
{
  // x: T |- A()
  var y: T := x; 
  // x: T, y: T, y == x |- A()
  assume false;
}

// Here is one quite mechanical approach to deriving a proof step-by-step:
// assume what you want to prove, and keep replacing `assume` statements with
// more specific steps that may themselves contain further `assume`s (at first).

// Here are some general rules for replacing `assume`s with more specific code.

// Can change:
//   assume A && B;
// into:
//   assert A && B by {
//     assume A;
//     assume B;
//   }

// Can change:
//   assume A || B;
// into:
//   assert A || B by {
//     assume A;
//   }
// or:
//   assert A || B by {
//     assume B;
//   }
// or:
//   assert A || B by {
//     if !A {
//       assume B;
//     }
//   }
// or:
//   assert A || B by {
//     if !B {
//       assume A;
//     }
//   }
// Note that it is important to choose the right one of these rules, based on an
// understanding of what will be provable later.

// Can change:
//   assume A ==> B;
// into:
//   assert A ==> B by {
//     if A {
//       assume B;
//     }
//   }
// or (contrapositive):
//   assert A ==> B by {
//     if !B {
//       assume !A;
//     }
//   }

// Can change:
//   assume !A;
// into:
//   assert !A by {
//     if A {
//       assume false;
//     }
//   }

// Can change:
//   assume forall x: nat :: P(x);
// into:
//   assert forall x: nat :: P(x) by {
//     forall x: nat
//       ensures P(x)
//     {
//       assume P(x);
//     }
//   }

// Can change:
//   assume exists x: nat :: P(x);
// into:
//   assert exists x: nat :: P(x) by {
//     assume P(c);
//   }
// Note that, like with "or," we have to make a choice (of the right `c`), and
// the wrong choice can take us to an unprovable new goal.

// Often we can't prove a fact by the above rules.  Instead, we need to use some
// of our hypotheses (appearing to the left of `|-` in goals) to make progress.
// Here are some schematic examples of using hypotheses.  Again, it is a
// deliberate, strategic choice to pick a hypothesis to exploit.

lemma UseImplication()
  requires A() ==> B()
  ensures B()
{
  // A() ==> B() |- B()
  assume A();
  // A() ==> B(), A() |- B()
}

lemma UseDisjunction() 
  requires A() || B()
  ensures C()
{
  // A() || B() |- C()
  if A() {
    assume C();
  }
  // A() || B(), A() ==> C() |- C()
  if B() {
    assume C();
  }
  // A() || B(), A() ==> C(), B() ==> C() |- C()
}

lemma UseNegation() 
  requires !A()
  ensures false
{
  // !A() |- false 
  assume A(); 
  // !A(), A() |- false
}

lemma UseExistential() 
  requires exists c: T :: P(c)
  ensures C()
{
  // exists c: T :: P(c) |- C()
  assume forall x: T :: P(x) ==> C();
  // exists c: T :: P(c), forall x: T :: P(x) ==> C() |- C()
  var c: T :| P(c);
  // exists c: T :: P(c), c:T, P(c), forall x: T :: P(x) ==> C() |- C()
}

// This proof can be produced starting from `assume`ing the lemma statement and
// gradually refining using the rules above (we often don't bother to write the
// `assert`s from above, which were mostly included for documentation value).
lemma s1()
  ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
{
  // |- GOAL
  forall x: nat
    ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    if x % 2 == 0 {
      // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
      assert exists y: nat :: x == 2 * y by {
        // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
        assert x == 2 * (x / 2);
        // x: nat, x % 2 == 0, x == 2 * (x / 2) |- exists y: nat :: x == 2 * y
      }
      // x: nat, x % 2 == 0, exists y: nat :: x == 2 * y |- exists y: nat :: x == 2 * y
    }
    // x: nat, x % 2 == 0 ==> exists y: nat :: x == 2 * y 
    //                  |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
  }
  // GOAL |- GOAL
}

// Let's practice these constructions in the context of a very handy feature
// that Dafny has in common with Python: set comprehensions.

function Interval(n: nat, m: nat): set<nat> {
  set k | n <= k < m
}

lemma SizeOfInterval(m: nat, n: nat)
  requires n <= m
  ensures |Interval(n, m)| == m - n
{
  if m == n {
  } else {
    assert m-1 in Interval(n, m);
    assert |Interval(n, m)| == 1 + |Interval(n, m) - {m-1}|;
    assert Interval(n, m) - {m-1} == Interval(n, m-1);
    assert |Interval(n, m)| == 1 + |Interval(n, m-1)|;
    SizeOfInterval(m-1, n);
  }
}

lemma JoinIntervals(m: nat, n: nat, o: nat)
  requires m <= n <= o
  ensures Interval(m, o) == Interval(m, n) + Interval(n, o)
{
}

// The following variant of set comprehensions allows us to form the final set
// elements by applying a function to the variables we quantify over.
function SetMap<A, B>(f: A -> B, s: set<A>): set<B> {
  set x | x in s :: f(x)
}

lemma SizeSetMap<A, B>(f: A -> B, s: set<A>)
  ensures |SetMap(f, s)| <= |s|
{
  if |s| == 0 {
  } else {
    var x :| x in s;
    assert SetMap(f, s) == SetMap(f, s - {x}) + {f(x)};
    SizeSetMap(f, s - {x});
  }
}

// We apologize for the mysterious `(!new)` below, which basically says "this
// type is sufficiently simple and pure," not using object-oriented features.
// More explanation to come when we get to classes in the final month or so.
ghost predicate Injective<A(!new), B>(f: A -> B) {
  forall x, y :: f(x) == f(y) ==> x == y
}

lemma SizeSetMapInjective<A(!new), B>(f: A -> B, s: set<A>)
  requires Injective(f)
  ensures |SetMap(f, s)| == |s|
{
  if |s| == 0 {
  } else {
    var x :| x in s;
    assert SetMap(f, s) == SetMap(f, s - {x}) + {f(x)};
    SizeSetMapInjective(f, s - {x});
  }
}
// OK, that's pretty cool that the proof using injectivity goes through with so
// little modification.

// This next example worked well for us with gradually expanding the proof
// structure and seeing where Dafny was stuck at each stage.
lemma ShiftInterval(a: nat, b: nat, k: nat)
  ensures SetMap((n) => n + k, Interval(a, b)) == Interval(a + k, b + k)
{
  forall x
    ensures x in SetMap((n) => n + k, Interval(a, b)) <==> x in Interval(a + k, b + k) {
      if x in SetMap((n) => n + k, Interval(a, b)) {
        assert x in Interval(a + k, b + k);
      }
      if x in Interval(a + k, b + k) {
        assert a + k <= x < b + k;
        assert a <= x - k < b;

        assert x - k in Interval(a, b);
        // In fact, this line by itself within this 'if' suffices to convince Dafny,
        // but the other lines help explain how it fits into the proof structure.
        
        assert x - k + k in SetMap((n) => n + k, Interval(a, b));
        assert x - k + k == x;
        assert x in SetMap((n) => n + k, Interval(a, b));
      }
  }
}

function SetFilter<A>(f: A -> bool, s: set<A>): set<A> {
  set x | x in s && f(x)
}

lemma FilterInterval(a: nat, b: nat, k: nat)
  requires a <= k <= b
  ensures SetFilter((n) => n >= k, Interval(a, b)) == Interval(k, b)
{
}

// OK, let's get into a fancier example.  It adds two maps together, combining
// the values of shared keys using addition.
function AddMaps(a: map<int, int>, b: map<int, int>): map<int, int> {
  (map x | x in a && x in b :: a[x] + b[x])
    + (map x | x in a && x !in b :: a[x])
    + (map x | x in b && x !in a :: b[x])
}

// This lemma copied from the previous class.
lemma SetHasMinimum(s: set<int>)
  requires |s| != 0
  ensures exists n :: n in s && forall m :: m in s ==> n <= m
{
  var n :| n in s;
  if |s - {n}| == 0 {
  } else {
    SetHasMinimum(s - {n});
    assert forall m :: m in s ==> m == n || m in s - {n};
  }
}

// We can also sum up all entries of a map.
function MapSum(a: map<int, int>): int {
  if |a| == 0 then
    0
  else
    SetHasMinimum(a.Keys);
    var n :| n in a.Keys && forall m :: m in a.Keys ==> n <= m;
    a[n] + MapSum(a - {n})
}

// So how do those last two functions interact?
lemma AddMapsSum(a: map<int, int>, b: map<int, int>)
  ensures MapSum(AddMaps(a, b)) == MapSum(a) + MapSum(b)
{
  if |a| == 0 && |b| == 0 {
  } else {
    AddMapsKeys(a, b);
    var n := MapSumNext(AddMaps(a, b));

    calc {
      MapSum(AddMaps(a, b));
      == AddMaps(a, b)[n] + MapSum(AddMaps(a, b) - {n});
      == { AddMapsRemove(a, b, n); } AddMaps(a, b)[n] + MapSum(AddMaps(a - {n}, b - {n}));
      == { AddMapsSum(a - {n}, b - {n}); } AddMaps(a, b)[n] + MapSum(a - {n}) + MapSum(b - {n});
    }
    MapSumIsolate(a, n);
    MapSumIsolate(b, n);
  }
}

// This pattern is handy for letting us quickly grab ahold of the first key that
// MapSum will process.  Note again use of a lemma *with a return value*.
lemma MapSumNext(a: map<int, int>) returns (n: int)
  requires |a| != 0
  ensures n in a
  ensures forall m :: m in a.Keys ==> n <= m
  ensures MapSum(a) == a[n] + MapSum(a - {n})
{
  SetHasMinimum(a.Keys);
  var n' :| n' in a.Keys && forall m :: m in a.Keys ==> n' <= m;
  n := n';
}

// This simple fact is easy for Dafny to prove, even though Dafny doesn't think
// to use it within larger proofs unless we suggest it explicitly.
lemma AddMapsKeys(a: map<int, int>, b: map<int, int>)
  ensures AddMaps(a, b).Keys == a.Keys + b.Keys
{
}

// This workhorse lemma explains how to pull any single term out of a MapSum.
lemma MapSumRemove(a: map<int, int>, n: int)
  requires n in a
  ensures MapSum(a) == a[n] + MapSum(a - {n})
{
  if |a| > 0 {
    var k := MapSumNext(a);
    if k != n {
      calc {
        MapSum(a);
        a[k] + MapSum(a - {k});
        { MapSumRemove(a - {k}, n); } a[k] + a[n] + MapSum(a - {k} - {n});
        { assert a - {n} - {k} == a - {k} - {n}; } a[k] + a[n] + MapSum(a - {n} - {k});
        a[n] + MapSum(a - {n});
      }
    }   
  }
}

// Dually, there is no impact from pulling out a map key that was not there to
// begin with.
lemma MapSumNoRemove(a: map<int, int>, n: int)
  requires n !in a
  ensures MapSum(a) == MapSum(a - {n})
{
  if |a| > 0 {
    var k := MapSumNext(a);
    calc {
      MapSum(a);
      a[k] + MapSum(a - {k});
      { MapSumNoRemove(a - {k}, n); } a[k] + MapSum(a - {k} - {n});
      { assert a - {n} - {k} == a - {k} - {n}; } a[k] + MapSum(a - {n} - {k});
      MapSum(a - {n});
    }
  }
}

// We can combine the above two lemmas into a general relationship between the
// MapSum before and after removing an arbitrary key.
lemma MapSumIsolate(a: map<int, int>, n: int)
  ensures MapSum(a) == (if n in a then a[n] else 0) + MapSum(a - {n})
{
  if n in a {
    MapSumRemove(a, n);
  } else {
    MapSumNoRemove(a, n);
  }
}

// Here's the last lemma we used in the main proof above.
lemma AddMapsRemove(a: map<int, int>, b: map<int, int>, n: int)
  ensures AddMaps(a, b) - {n} == AddMaps(a - {n}, b - {n})
{
}

// OK, that was quite a workout for practicing proof structuring!
// Now let's add some quantifiers into the mix.

// The following is basically classic function composition, specialized to maps.
function MapCompose<A,B,C>(f: map<A, B>, g: map<B, C>): map<A, C>
  requires forall x :: x in f ==> f[x] in g
{
  map x | x in f :: g[f[x]]
}

// Here are two standard function properties from discrete-math class.

ghost predicate MapInjective<A(!new),B>(f: map<A, B>) {
  forall x, y :: x in f && y in f && f[x] == f[y] ==> x == y
}

ghost predicate MapSurjective<A(!new),B>(f: map<A, B>, s: set<B>) {
  forall y :: y in s ==> exists x :: x in f && f[x] == y
}

// If we assume them, we can prove that the sum of a map remains the same when
// we compose it with any other map that satisfies the above properties.
lemma MapComposeSum(f: map<int, int>, g: map<int, int>)
  requires forall x :: x in f ==> f[x] in g
  requires MapInjective(f)
  requires MapSurjective(f, g.Keys)
  ensures MapSum(MapCompose(f, g)) == MapSum(g)
{
  if |g| != 0 {
    var n := MapSumNext(g);
    var n' :| n' in f && f[n'] == n;

    // Let's check all the requirements for a recursive call (to "invoke the IH").
    assert forall x :: x in f - {n'} ==> (f - {n'})[x] in g - {n};
    assert MapInjective(f - {n'});
    assert MapSurjective(f - {n'}, (g - {n}).Keys) by {
      MapSurjectiveRemove(f, g, n, n');
    }
    // OK, only the last one wasn't proven automatically by Dafny, instead
    // relying on a lemma that appears below.
    
    calc {
      MapSum(MapCompose(f, g));
      == { MapSumRemove(MapCompose(f, g), n'); } MapCompose(f, g)[n'] + MapSum(MapCompose(f, g) - {n'});
      == { MapComposeRemove(f, g, n, n'); } g[n] + MapSum(MapCompose(f - {n'}, g - {n}));
      == { MapComposeSum(f - {n'}, g - {n}); } g[n] + MapSum(g - {n});
      == MapSum(g);
    }
  }
}

lemma MapComposeRemove(f: map<int, int>, g: map<int, int>, n: int, n': int)
  requires n in g
  requires n' in f && f[n'] == n
  requires MapInjective(f)
  requires forall x :: x in f ==> f[x] in g
  ensures MapCompose(f - {n'}, g - {n}) == MapCompose(f, g) - {n'}
{
}

lemma MapSurjectiveRemove(f: map<int, int>, g: map<int, int>, n: int, n': int)
  requires n in g
  requires n' in f && f[n'] == n
  requires MapInjective(f)
  requires MapSurjective(f, g.Keys)
  ensures MapSurjective(f - {n'}, (g - {n}).Keys)
{
  forall y ensures y in (g - {n}).Keys ==> exists x :: x in f - {n'} && (f - {n'})[x] == y {
    if y in (g - {n}).Keys {
      var x :| x in f && f[x] == y;
      assert x in f - {n'};
    }
  }
}

// We just looked at these three rules to encode the meaning of "and".

lemma ProveAnd(P: bool, Q: bool)
  requires P
  requires Q
  ensures P && Q
{
}

lemma UseAnd1(P: bool, Q: bool)
  requires P && Q
  ensures P
{
}

lemma UseAnd2(P: bool, Q: bool)
  requires P && Q
  ensures Q
{
}

// YOUR CHALLENGE: look for three lemmas that similarly capture the full meaning of "or".
// That is, anything we can prove about uses of "or" should follow from just your lemmas,
// if we then go and forget the inherent meaning of "or".
// Hint: there is a nice symmetry between "and" and "or", but it's not quite trivial.
// You will probably want two "Prove" rules and one "Use" rule (flipping the situation for "and").
// You will probably also want to use some other logical connective beside just "or".

// Complete this proof following the mechanical strategy of repeatedly expanding
// "assume"s.
lemma s1()
  ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
{
  assume forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y;
}
// Note that Dafny accepts this "proof," but it's bogus because an "assume"
// remains.  Refine it until there is no "assume" left.

// The following variant of set comprehensions allows us to form the final set
// elements by applying a function to the variables we quantify over.
function SetMap<A, B>(f: A -> B, s: set<A>): set<B> {
  set x | x in s :: f(x)
}

// Prove this size bound.
lemma SizeSetMap<A, B>(f: A -> B, s: set<A>)
  ensures |SetMap(f, s)| <= |s|