rdivyanshu

include "./next_permutations_rank.dfy"

method copy (src: array<nat>, dest: array<nat>)
  modifies dest
  requires src.Length == dest.Length
  ensures forall i :: 0 <= i < src.Length ==> dest[i] == src[i]
{
  var i := 0;
  while i < src.Length
    decreases src.Length - i

rdivyanshu

Five chess fanatics always manage to fit in a round-robin before their train reaches Waterloo. Yesterday there were no ties in the final order (2 points for win, 1 for draw, 0 for loss). Alapin won his game against the only person who took a game off Bird. Catalan was the only person to lose a game against the financier, who was the only person to lose a game to Dunst. Alapin finished below the ghost-writer. The interpreter scored only 1 point total. The journalist fared worse than the hairdresser. As for Evans, you can work that out for yourself. What is each person’s score and occupation?

rdivyanshu

lemma contains_implies_index (k : nat, perm : seq<nat>)
  requires k in perm
  ensures exists m :: 0 <= m < |perm| && perm[m] == k
{
}

method next (perm: array<nat>) returns (res: bool)
  modifies perm
  requires forall k :: 1 <= k <= perm.Length ==> k in perm[..]
  ensures !res ==> forall k :: 0 <= k < perm.Length ==> perm[k] == old(perm[k])

rdivyanshu

lemma pigeonhole(m : int, n: int, f : int -> int)
  requires 0 <= m < n
  requires forall i :: 0 <= i < n ==> 0 <= f(i) < m
  ensures exists j, k :: (0 <= j < k < n) && f(j) == f(k)
{
  if m <= 0 {
    assert 0 <= f(0) < 0;
  }
  else {
    var i : int := 0;

rdivyanshu

#lang rosette
(require rosette/lib/angelic)

(define profession (list 'baker 'carpenter 'driver 'plumber))

(define baker (apply choose* profession))
(define carpenter (apply choose* profession))
(define driver (apply choose* profession))
(define plumber (apply choose* profession))

rdivyanshu

predicate sorted (s: seq<int>)
{
  if |s| <= 1 then true else s[0] <= s[1] && sorted(s[1..])
}

lemma {:induction m, n} sorted_elem_lemma(s: seq<int>, m: int, n: int)
  decreases n - m
  requires sorted(s)
  requires 0 <= m <= n < |s|
  ensures s[m] <= s[n]

rdivyanshu

least predicate perm<T(!new)>(p: seq<T>, q: seq<T>)
{
  || (p == [] && q == [])
  || (exists x: T, m: seq<T>, n: seq<T> :: p == [x] + m && q == [x] + n && perm(m, n))
  || (exists x: T, y: T, m: seq<T> :: p == [x, y] + m && q == [y, x] + m)
  || (exists m: seq<T> :: perm(p, m) && perm(m, q))
}

lemma refl<T(!new)>(p: seq<T>)
  ensures perm(p, p)

rdivyanshu

class Heap {
  var arr: array<int>

  constructor Heap (input: array<int>)
   ensures this.arr == input {
     this.arr := input;
  }

  function parent(idx: int): int
  {

rdivyanshu

abstract module Group {
  type T(==)
  const elems : set<T>
  function identity(): (r: T)
    ensures r in elems
    ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a
  function compose(a: T, b: T): (r: T)
    requires a in elems && b in elems
    ensures r in elems
  function inverse(a: T) : (r: T)

rdivyanshu

predicate decreasing(s: seq<nat>)
{
  forall i :: 0 <= i < |s| - 1 ==> s[i] >= s[i+1]
}

predicate increasing(s: seq<nat>)
{
  forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[i+1]
}