// Verificarea intrinseca si extrinseca a programelor functionale

// function increment(x : int) : int               // specificatia metodei increment'
// {
//   x + 1
// }

// method increment'(x : int) returns (r : int)    // implementarea
//   ensures r == increment(x) // postconditie
// {
//   return x + 1;
// }

// method increment''(x : int) returns (r : int) 
//   ensures r > x 
// {
//   return x + 1;
// }

// function inc(x : int) : int
//   ensures inc(x) == x + 1 // specificatie pentru functie
// {
//   x + 1
// }

// function {:opaque} inc'(x : int) : int
//   ensures inc'(x) > x // specificatie pentru functie (intrinseca)
// {
//   x + 1
// }

// lemma test1()
// {
//   //assert inc'(10) == 11;
//   assert inc'(10) > 10;
// }

// function {:opaque} inc''(x : int) : int
// {
//   x + 1
// }

// lemma inc''_gt(x : int)
//   ensures inc''(x) > x // specificatie extrinseca a functiei inc''
// {
//   calc
//   {
//     inc''(x);
//     ==
//       {
//         reveal inc'';
//       }
//       x + 1;
//       >
//         x;
//   }
// }


// lemma test2()
// {
//   inc''_gt(10);
//   assert inc''(10) > 10;
// }

/*
   Specificatii intrinseci: ca postconditie a functiei
   Specificatii extrinseci: ca o lema separata de functie

   Avantaje specificatie instrinseca:
   - grad mai mare de automatizare
   - cod mai putin
   
   Avantaj specificatie extrinseca:
   - grad mai mare de control
   - unele conditii sunt imposibil de enuntat intrinsec (e.g., asociativitatea concatenarii)

   Dezavantaj specificatie instrinseca:
   - potential, timp de verificare foarte mare
   (fiindca, daca postconditia este complicata, poate "polua" knowledge base-ul verificatorului)
   de ce: la fiecare apel de functie aduce si specificatiile in context
   
   Dezavantaj extrinsec:
   - mai mult cod, mai putina automatizare
 */

datatype List = Empty | Cons(head : int, tail : List)

function len(l : List) : int
  ensures len(l) >= 0
{
  match l
  case Empty => 0
  case Cons(_, tail) => 1 + len(tail)
}

// lemma test3(l : List)
// {
//   assert len(Cons(42, Cons(7, Cons(13, l)))) >= 0;
// }

// function app(l1 : List, l2 : List) : List
//   ensures l1 == Empty ==> app(l1, l2) == l2
//   ensures l2 == Empty ==> app(l1, l2) == l1
//   ensures len(app(l1, l2)) == len(l1) + len(l2)
// {
//   match l1
//   case Empty => l2
//   case Cons(hd, tl) => Cons(hd, app(tl, l2))
// }

// lemma test4(l : List)
// {
//   assert len(app(Empty, l)) == len(l);
//   assert len(app(l, Empty)) == len(l);
// }

function append(l1 : List, l2 : List) : List
{
  match l1
  case Empty => l2
  case Cons(hd, tl) => Cons(hd, append(tl, l2))
}

lemma {:induction false} len_append(l1 : List, l2 : List)
  ensures len(append(l1, l2)) == len(l1) + len(l2)
{
  if l1 == Empty
  {
  }
  else
  {
    len_append(l1.tail, l2); // len(append(l1.tail, l2)) == len(l1.tail) + len(l2)
                             // append(Cons(l1.head, l1.tail), l2) == Cons(l1.head, append(l1.tail, l2))
                             // len(Cons(l1.head, append(l1.tail, l2))) = 1 + len(append(l1.tail, l2))
  }
}

lemma test5(l1 : List, l2 : List)
  requires len(l1) == 10
  requires len(l2) == 10
{
  len_append(l1, l2);
  assert len(append(l1, l2)) == 20;
}


lemma {:induction false} append_assoc(l1 : List, l2 : List, l3 : List)
  ensures append(l1, append(l2, l3)) == append(append(l1, l2), l3)
{
  // if l1 == Empty {
  // } else {
  //   append_assoc(l1.tail, l2, l3);
  // }
  if l1 != Empty {
    append_assoc(l1.tail, l2, l3);
  }
}

function append'(l1 : List, l2 : List) : List
  // fails to work: ensures forall l3 : List :: append'(append'(l1, l2), l3) == append'(l1, append'(l2, l3))
{
  match l1
  case Empty => l2
  case Cons(hd, tl) => Cons(hd, append'(tl, l2))
}

/*
   Cand folosesc o specificatie intrinseca:
   - pentru conditii simple, care sunt foarte probabil utile in orice context

   De exemplu:
function len(l : List) : int
  ensures len(l) >= 0
{
  match l
  case Empty => 0
  case Cons(_, tail) => 1 + len(tail)
   }

   Cand folosesc o specificatie extrinseca:
   - conditia este mai complicata
   - am nevoie de ea doar in cateva locuri
 */


function {:opaque} inc(x : int) : int
{
  x + 1
}

// P1:
// inc(x) > x                           intrinsec/extrinsec (?)
// ca principiu: fiind simpla si fiind probabil sa am nevoie de ea in mai multe locuri ==> intrinsec

// P2:
// x % 2 == 0 ==> inc(x) % 2 == 1       intrinsec/extrinsec (?)
// ca principiu: fiind mai complicata (foloseste %, e utila doar pentru "jumatate" dintre input-uri) ==> extrinsec
// P3:
// x % 2 == 1 ==> inc(x) % 2 == 0       intrinsec/extrinsec (?)
// ca principiu: fiind mai complicata (foloseste %, e utila doar pentru "jumatate" dintre input-uri) ==> extrinsec

lemma inc_P2_x'(x : int)
  requires x % 2 == 0
  ensures inc(x) % 2 == 1
{
  reveal inc;
}

lemma inc_P2_x(x : int)
  ensures x % 2 == 0 ==> inc(x) % 2 == 1
{
  if x % 2 == 0 {
    inc_P2_x'(x);
  }
}

lemma inc_P2()
  ensures forall x :: x % 2 == 0 ==> inc(x) % 2 == 1
{
  forall x : int
    ensures x % 2 == 0 ==> inc(x) % 2 == 1
  {
    inc_P2_x(x);
  }
}

/*
   nu este "tail-recursive"
function len(l : List) : int
  ensures len(l) >= 0
{
  match l
  case Empty => 0
  case Cons(_, tail) => 1 + len(tail)
   }
   */

// varianta "tail-recursive" a functiei len
// orice compilator modern transforma functiile tail-recursive in instructiuni repetitive
function len_aux(l : List, a : int) : int
  ensures l != Empty ==> len_aux(l, a) == 1 + len_aux(l.tail, a) // helper pentru demonstratia len_len_aux_0 (negeneralizata)
{
  match l
  case Empty => a
  case Cons(_, tail) => len_aux(tail, a + 1)
}
//     assert len_aux(l, 0) == 1 + len_aux(l.tail, 0); // intrinseca (?)


function len'(l : List) : int
{
  len_aux(l, 0)
}

/*
   a := 0;
   while l != Empty
   {
     a := a + 1;
     l := l.tail
   }
 */
/*  len(l) = match l
  case Empty => 0
  case Cons(_, tail) => 1 + len(tail) */
lemma len_len_aux_0(l : List)
  ensures len(l) == len_aux(l, 0)
{
  if l == Empty {
  } else {
    len_len_aux_0(l.tail);
    assert len(l.tail) == len_aux(l.tail, 0);
    // assert len(l) == 1 + len(l.tail);
    assert len_aux(l, 0) == 1 + len_aux(l.tail, 0); // intrinseca (?)
    // assert len(l) == len_aux(l, 0);
    //assume false;
  }
}

lemma {:induction false} len_len_aux_0_general(l : List, a : int)
  ensures a + len(l) == len_aux(l, a)
{
  if l == Empty {
  } else {
    // len_len_aux_0_general(l.tail, a);
    
    // assert a + len(l.tail) == len_aux(l.tail, a);
    // // assert len(l) == 1 + len(l.tail);
    // // assert len_aux(l, 0) == 1 + len_aux(l.tail, 0);
    // assert a + len(l) == len_aux(l, a);
    calc
    {
      a + len(l);
      ==
        a + 1 + len(l.tail);
        ==
          {
            len_len_aux_0_general(l.tail, a + 1);
          }
          len_aux(l.tail, a + 1);
    }
    //assume false;
  }
}

function {:opaque} Len(l : List) : int
  ensures len(l) >= 0
{
  match l
  case Empty => 0
  case Cons(_, tail) => 1 + len(tail)
}

function {:opaque} Append(l1 : List, l2 : List) : List
{
  match l1
  case Empty => l2
  case Cons(hd, tl) => Cons(hd, append(tl, l2))
}

lemma Len_Append(l1 : List, l2 : List)
  ensures Len(Append(l1, l2)) == Len(l1) + Len(l2)
  // cat mai putine "reveal"
{
  if l1 == Empty {
    reveal Append(Empty, l2);
    reveal Len(Empty);
  } else {
    calc {
      Len(Append(l1, l2));
      ==
        Len(Append(Cons(l1.head, l1.tail), l2));
        ==
          {
            reveal Append(Cons(l1.head, l1.tail));
          }
          Len(Cons(l1.head, Append(l1.tail, l2)));
          ==
            {
              reveal Len(Cons(l1.head, Append(l1.tail, l2)));
            }
            1 + Len(Append(l1.tail, l2));
            ==
              {
                Len_Append(l1.tail, l2);
              }
              1 + Len(l1.tail) + Len(l2);
              ==
                {
                  reveal Len(l1);
                }
                Len(l1) + Len(l2);
    }
  }
}

/*
   Specificatiile intrinseci:
   - impreuna cu functia
   - utile pentru proprietati simple, utile in f. multe cazuri
   
   Extrinsec:
   - enunta ca leme externe functiei
   - utile pentru proprietati mai complicate, utile in cazuri limitate
   
 */