// Proofs

method binarySearch(a : array<int>, key : int) returns (pos : int)
  requires sorted1(a)
//  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
//  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures pos == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
  ensures pos != -1 ==> 0 <= pos < a.Length && a[pos] == key
{
  var left := 0;
  var right := a.Length - 1;
  while (left <= right)
    invariant 0 <= left <= a.Length
    invariant -1 <= right < a.Length
    invariant forall i :: 0 <= i < left ==> a[i] < key
    invariant forall i :: right < i < a.Length ==> a[i] > key
    decreases right - left
  {
    var mid := (left + right) / 2;
    if (a[mid] == key) {
      return mid;
    } else if (key < a[mid]) {
      right := mid - 1;
    } else {
      left := mid + 1;
    }
  }
  return -1;
}

predicate sorted1(a : array<int>)
  reads a
{
  forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
}

predicate sorted2(a : array<int>)
  reads a
{
  forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
}

method experiment1(a : array<int>)
  requires sorted1(a)
{
  if (a.Length > 10) {
    assert a[0] <= a[8];
  }
}

method experiment2(a : array<int>)
  requires sorted2(a)
{
  if (a.Length > 10) {
    //assert a[0] <= a[8];
    assert a[0] <= a[1];
    assert a[1] <= a[2];
    assert a[0] <= a[2];
  }
}

method experiment3(a : array<int>)
  requires sorted1(a)
  ensures sorted2(a)
{
}

// method experiment4(a : array<int>)
//   requires sorted2(a)
//   ensures sorted1(a)
// {
// }

function identitate(x : int) : int
{
  x
}

predicate sorted2'(a : array<int>)
  reads a
{
  forall i {:trigger identitate(i)} :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
}

method experiment5(a : array<int>)
  requires sorted2'(a)
{
  if (a.Length > 10) {
    assert identitate(0) == 0;
    assert a[0] <= a[1];
  }
}

method experiment6(a : array<int>)
  requires sorted2'(a)
{
  if (a.Length > 10) {
    assert identitate(0) == 0;
    // in context: identitate(0)
    // in context: forall i {:trigger identitate(i)} :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
    // "declanseaza" forall-ul: i = 0: 0 <= 0 < a.Length - 1 ==> a[0] <= a[1]
    assert identitate(1) == 1;
    // in context: identitate(0)
    // "declanseaza" forall-ul: i = 1: 0 <= 1 < a.Length - 1 ==> a[1] <= a[2]
    //assert identitate(2) == 2;
    assert a[0] <= a[2];
  }
}

function declanseaza(i : int, j : int) : bool
{
  true
}

predicate sorted1'(a : array<int>)
  reads a
{
  forall i, j {:trigger declanseaza(i, j)} :: 0 <= i < j < a.Length ==> a[i] <= a[j]
}

lemma experiment7''auto(a : array<int>, i : int)
  requires sorted1(a)
  requires 0 <= i < a.Length - 1
  ensures a[i] <= a[i + 1]
{
}

lemma experiment7''(a : array<int>, i : int)
  requires sorted1'(a)
  requires 0 <= i < a.Length - 1
  ensures a[i] <= a[i + 1]
{
  assert declanseaza(i, i + 1);
}

lemma experiment7'(a : array<int>, i : int)
  requires sorted1'(a)
  ensures 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  // ca sa demonstrez o implicatie P ==> Q:
  // presupun P, demonstrez Q
  // if (P)
  // {
  ///   <demonstratie pentru Q>
  // }
{
  if (0 <= i < a.Length - 1) {
    // stiu: 0 <= i < a.Length - 1
    assert 0 <= i < a.Length - 1;
    // demonstrez: a[i] <= a[i + 1]
    experiment7''(a, i);
  }
}

lemma experiment7(a : array<int>)
  requires sorted1'(a)
  ensures forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures sorted2'(a)
  // ca sa demonstrez un forall: forall x, P(x)
  // fie x arbitrar  <--- cum scriu asta in Dafny (folosind un
  //                                         "forall statement")
  // (adica o instructiune forall)
  // demonstrez P(x)
{
  forall x : int // fie x : int arbitrar
    ensures 0 <= x < a.Length - 1 ==> a[x] <= a[x + 1]
    // demonstrez 0 <= x < a.Length - 1 ==> a[x] <= a[x + 1]
  {
    //assert x == x;
    experiment7'(a, x);
  }
}

lemma experiment8''A(a : array<int>, i : int, j : int)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  requires 0 <= i < j < a.Length
  ensures a[i] <= a[j]
{
  // inductie dupa j - i
  if (j - i == 1)
  {
    // cazul de baza: j - i == 1 (alternativ" j == i + 1)
  }
  else
  {
    // cazul inductiv: j - i > 1 (alternativ: j > i + 1)
    // ipoteza de inductie: a[i] <= a[j - 1]
    experiment8''A(a, i, j - 1);
    assert a[i] <= a[j - 1];
    assert a[j - 1] <= a[j];
    assert a[i] <= a[j];
  }
}

lemma experiment8''B(a : array<int>, i : int, j : int)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  requires 0 <= i < j < a.Length
  ensures a[i] <= a[j]
{
  var k := i;
  while (k < j)
    invariant i <= k <= j
    invariant a[i] <= a[k]
  {
    assert a[k] <= a[k + 1];
    k := k + 1;
  }
}

lemma experiment8'(a : array<int>, i : int, j : int)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures 0 <= i < j < a.Length ==> a[i] <= a[j]
{
  if (0 <= i < j < a.Length) {
    experiment8''B(a, i, j);
  }
}

lemma experiment8(a : array<int>)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
{
  forall i : int, j : int
    ensures 0 <= i < j < a.Length ==> a[i] <= a[j]
  {
    experiment8'(a, i, j);
  }
}

method binarySearch'(a : array<int>, key : int) returns (pos : int)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures pos == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
  ensures pos != -1 ==> 0 <= pos < a.Length && a[pos] == key
{
  experiment8(a);
  var left := 0;
  var right := a.Length - 1;
  while (left <= right)
    invariant 0 <= left <= a.Length
    invariant -1 <= right < a.Length
    invariant forall i :: 0 <= i < left ==> a[i] < key
    invariant forall i :: right < i < a.Length ==> a[i] > key
    decreases right - left
  {
    var mid := (left + right) / 2;
    if (a[mid] == key) {
      return mid;
    } else if (key < a[mid]) {
      right := mid - 1;
    } else {
      left := mid + 1;
    }
  }
  return -1;
}

method binarySearch''(a : array<int>, key : int) returns (pos : int)
  requires forall i :: 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  ensures pos == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
  ensures pos != -1 ==> 0 <= pos < a.Length && a[pos] == key
{
  // start ghost code
  forall i : int, j : int
    ensures 0 <= i < j < a.Length ==> a[i] <= a[j]
  {
    if (0 <= i < j < a.Length)
    {
      var k := i;
      while (k < j)
        invariant i <= k <= j
        invariant a[i] <= a[k]
      {
        k := k + 1;
      }
    }
  }
  // end ghost code
  var left := 0;
  var right := a.Length - 1;
  while (left <= right)
    invariant 0 <= left <= a.Length
    invariant -1 <= right < a.Length
    invariant forall i :: 0 <= i < left ==> a[i] < key
    invariant forall i :: right < i < a.Length ==> a[i] > key
    decreases right - left
  {
    var mid := (left + right) / 2;
    if (a[mid] == key) {
      return mid;
    } else if (key < a[mid]) {
      right := mid - 1;
    } else {
      left := mid + 1;
    }
  }
  return -1;
}

/*
   Mecanismul de declansare pentru propozitii universale (forall x.P(x))
   (trigger-ing)
   
   mecanismul prin care sistemul poate folosi propozitii de forma
         forall x.P(x)

   Instructiunea "forall" (forall statement, diferita de cuantificarea
   universala din propozitii de forma forall x.P(x))
   /*
    forall i : int, j : int
      ensures 0 <= i < j < a.Length ==> a[i] <= a[j]
    {
      // ...
   }
   demonstrez o propozitie universala (pp un "x" fixat)
 */

   cum pot demonstra o implicatie:
   - cu instructiunea obisnuita "if {} else {}"
 */
lemma experiment7''bis(a : array<int>, i : int)
  requires sorted1'(a)
  requires 0 <= i < a.Length - 1
  ensures a[i] <= a[i + 1]
{
  assert declanseaza(i, i + 1);
}

lemma experiment7'bis(a : array<int>, i : int)
  requires sorted1'(a)
  ensures 0 <= i < a.Length - 1 ==> a[i] <= a[i + 1]
  // ca sa demonstrez o implicatie P ==> Q:
  // presupun P, demonstrez Q
  // if (P)
  // {
  ///   <demonstratie pentru Q>
  // }
{
  if (0 <= i < a.Length - 1) {
    // stiu: 0 <= i < a.Length - 1
    assert 0 <= i < a.Length - 1;
    // demonstrez: a[i] <= a[i + 1]
    experiment7''bis(a, i);
  } else {
    assert !(0 <= i < a.Length - 1);
  }
}

// Cuantificaatorul existential
// cum pot demonstra o propozitie existentiala:
//   dau un martor pentru valoarea care indeplineste conditia
lemma experiment9(x : nat)
  requires x % 2 == 0
  ensures exists y :: x == 2 * y
{
  var half := x / 2;
  assert x == 2 * half;
}

lemma experiment9'(x : nat)
  requires x % 2 == 0
  // fails: ensures exists y :: x == 2 * y
{
  var half := x / 2;
  assert x == half * 2; // nu provoaca "declansarea"
                        // _ * 2
                        // ce ar provoca declansarea: 2 * _
}

predicate martor(numar : nat)
{
  true
}

lemma experiment10(x : nat)
  requires x % 2 == 0
  ensures exists y {:trigger martor(y)} :: x == 2 * y
{
  assert martor(x / 2);
}

// preferabil in dauna experiment10
// nu doar sa spun ca exista un y cu proprietatea x == 2 * y
// ci sa si spun care este acel y
lemma experiment10'(x : nat) returns (y : nat)
  requires x % 2 == 0
  ensures x == 2 * y
{
  y := x / 2;
}

lemma experiment10''(x : nat)
  requires x % 2 == 0
  ensures exists y {:trigger martor(y)} :: x == 2 * y
{
  var y := experiment10'(x);
  assert martor(y);
}

lemma experiment11(x : nat)
  requires exists y :: x == y * 2
  ensures exists y' :: (x + 2 == y' * 2)
{
  // cum pot sa ma folosesc de o propozitie existentiala
  // ii dam un nume valorii despre care stim ca exista si are o anumita
  // proprietate
  var n : nat :| x == n * 2; // instructiunea assign-such-that
                             // cod ghost
  assert x + 2 == (n + 1) * 2;
}

/*
   Cum folosesc un "exists":
   - folosesc instructiunea assign-such-that

   Cum demonstrez un "exists:
   - dau un martor
 */

predicate A(n : nat)
// {
//   true
// }

predicate B(n : nat)
// {
//   true
// }

predicate C(n : nat)
// {
//   true
// }

predicate D(n : nat)
// {
//   true
// }

lemma {:axiom} A_true(n : nat)
  ensures A(n)

lemma {:axiom} B_true(n : nat)
  ensures B(n)

lemma experiment12(n : nat)
  ensures A(n) && B(n)
{
  // cum demonstrez un "si":
  // demonstrez fiecare dintre cele doua parti ale conjunctiei individual
  A_true(n);
  B_true(n);
}

lemma {:axiom} AB_true(n : nat)
  ensures A(n) && B(n)

lemma experiement13(n : nat)
  ensures A(n)
  ensures B(n)
{
  // cum folosesc o conjunctie
  AB_true(n);
}

// Disjunctie
lemma {:axiom} A_implica_C(n : nat)
  ensures A(n) ==> C(n)

lemma {:axiom} B_implica_C(n : nat)
  ensures B(n) ==> C(n)

lemma AsauB_implica_C(n : nat)
  requires A(n) || B(n)
  ensures C(n)
{
  // cum ma folosesc de o disjunctie: analiza de cazuri
  if (A(n)) {
    A_implica_C(n);
  } else if (B(n)) {
    B_implica_C(n);
  }//  else {
  //   assert false;
  // }
}

// cum demonstrez o disjunctie (daca stiu una dintre cele parti)
lemma AsauB_implica_CsauD(n : nat)
  requires A(n) || B(n)
  ensures C(n) || D(n)
{
  AsauB_implica_C(n);
}

lemma experiment_sau(x : nat, y : nat)
  ensures C(x) || D(x)
{
  if (C(x)) {
    // nu mai am nimic de facut
  } else {
    //assert !C(x);
    assume D(x);
  }
}

lemma experiment_sau'(x : nat, y : nat)
  ensures C(x) || D(x)
{
  if (!C(x)) {
    assume D(x);
  }
}

lemma experiment_sau''(x : nat, y : nat)
  ensures C(x) || D(x)
{
  if (!D(x)) {
    assume C(x);
  }
}

lemma {:axiom} notD_implica_C(x : nat)
  ensures !D(x) ==> C(x)

lemma C_sau_D(x : nat)
  ensures C(x) || D(x)
{
  if (!D(x)) {
    notD_implica_C(x);
  }
}