// Logica propozitionala in Dafny

// Cand reprezint un limbaj (de programare)
// intr-un alt limbaj
// 2 moduri de a face reprezentarea:
// deep embedding
// shallow embedding

// 1. Shallow embedding
// limbajul obiect (cel pe care il reprezint) (LP)
// meta-limbajul (cel pe care il folosesc) (Dafny)

// p /\ q
lemma and_e_1(p : bool, q : bool)
  requires p && q
  ensures p
{
}

// fiecare obiect din limbajul obiect devine
// un obiect in meta-limbaj
// Exemplu: variabila propozitionala = variabila de tip bool in Dafny
// Formula propozitionala = formula in Dafny

// 2. Deep embedding
// obiect din limbajul obiect este reprezentat
// ca o structura de date in meta-limbaj

// Variabile propozitionale, Formule propozitionale = string-uri
method example1()
{
  var formula1 : string := "p /\\ q";
  var formula2 : string := "(p /\\ r) \\/ q";
}

datatype Formula =
  Var(string)
  | Not(f : Formula)
  | And(f1 : Formula, f2 : Formula)
  | Or(f1 : Formula, f2 : Formula)
  | Implies(f1 : Formula, f2 : Formula)
  | Bottom
  | Top

method example2()
{
  var formula1 : Formula := And(Var("p"), Var("q"));
  var formula2 : Formula := Or(And(Var("p"), Var("r")), Var("q"));
}

type TruthAssignment = string -> bool

function ta1(x : string) : bool
{
  if (x == "p" || x == "r") then
    true
  else
    false
}
  
function ta2(x : string) : bool
{
  x == "p1" || x == "p2" || x == "p3"
}
  
function value(f : Formula, tau : TruthAssignment) : bool
{
  match f
  case Var(x) => tau(x) 
  case Not(f) => !value(f, tau)
  case And(f1, f2) => value(f1, tau) && value(f2, tau)
  case Or(f1, f2) => value(f1, tau) || value(f2, tau)
  case Implies(f1, f2) => value(f1, tau) ==> value(f2, tau)
  case Top => true
  case Bottom => false
}

lemma and_e_1'(f1 : Formula, f2 : Formula, tau : TruthAssignment)
  requires value(And(f1, f2), tau)
  ensures value(f1, tau)
{
}

lemma and_e_2'(f1 : Formula, f2 : Formula, tau : TruthAssignment)
  requires value(And(f1, f2), tau)
  ensures value(f2, tau)
{
}

lemma example3(f1 : Formula, f2 : Formula, f3 : Formula, f4 : Formula, tau : TruthAssignment)
  requires value(And(f1, And(f2, And(f3, f4))), tau)
  ensures value(f4, tau)
{
  and_e_2'(f1, And(f2, And(f3, f4)), tau);
  and_e_2'(f2, And(f3, f4), tau);
  and_e_2'(f3, f4, tau);
}

function containsNot(f : Formula) : bool
{
  match f
  case Var(_) => false
  case Not(_) => true
  case Or(f1, f2) => containsNot(f1) || containsNot(f2)
  case And(f1, f2) => containsNot(f1) || containsNot(f2)
  case Implies(f1, f2) => containsNot(f1) || containsNot(f2)
  case Top => false
  case Bottom => false
}

lemma example4()
{
  var formula1 : Formula := And(Var("p"), Var("q"));
  var formula2 : Formula := Or(And(Var("p"), Var("r")), Var("q"));
  var formula3 : Formula := Or(Not(And(Var("p"), Var("r"))), Var("q"));
  var formula4 : Formula := Or(And(Var("p"), Var("r")), Not(Var("q")));
  assert !containsNot(formula1);
  assert !containsNot(formula2);
  assert containsNot(formula3);
  assert containsNot(formula4);
}

// calculez toti conectorii care apar intr-o formula

datatype Connective = COr | CAnd | CNot | CImplies | CTop | CBottom

function connectives(f : Formula) : set<Connective>
{
  match f
  case Var(_) => {}
  case Not(f) => { CNot } + connectives(f)
  case Or(f1, f2) => { COr } + connectives(f1) + connectives(f2)
  case And(f1, f2) => { CAnd } + connectives(f1) + connectives(f2)
  case Implies(f1, f2) => { CImplies } + connectives(f1) + connectives(f2)
  case Top => { CTop }
  case Bottom => { CBottom }
}

lemma example5()
{
  var formula1 : Formula := And(Var("p"), Var("q"));
  assert connectives(formula1) == { CAnd };
  var formula2 : Formula := Or(And(Var("p"), Var("r")), Var("q"));
  assert connectives(formula2) == { CAnd, COr };
  var formula3 : Formula := Or(Not(And(Var("p"), Var("r"))), Var("q"));
  assert connectives(formula3) == { CAnd, COr, CNot };
  var formula4 : Formula := Or(And(Var("p"), Var("r")), Not(Var("q")));
  assert connectives(formula4) == { CAnd, COr, CNot };
}

// Refinement Types = Tipuri de Date + Un Predicate

type Nat = x : int | x >= 0

type StrictlyPositive = x : int | x > 0 witness 7

method example6()
{
  //var x : Nat := -10;
  var x : Nat := 17;
}

method adunare(x : Nat, y : Nat) returns (z : Nat)
{
  z := x + y;
}

method adunare'(x : Nat, y : int) returns (z : Nat)
  requires y > 10
{
  z := x + y;
}

type NonZeroInt = x : int | x != 0 witness 42

method divide(x : int, y : NonZeroInt) returns (r : int)
{
  r := x / y;
}

method divide'(x : int, y : int) returns (r : int)
  requires y != 0
{
  r := x / y;
}

method asdf(x : int)
  // Q: se poate testat ca x satisface predicatul lui "Nat"
  // A: nu sunt sigur
  //requires x is Nat
{
}

type LP_and_or_not = f : Formula | connectives(f) <= { CAnd, COr, CNot } witness Var("p")

function complement(f : LP_and_or_not) : LP_and_or_not
{
  match f
  case Var(x) => Not(Var(x))
  case Not(f) => f
  case Or(f1, f2) => And(complement(f1), complement(f2))
  case And(f1, f2) => Or(complement(f1), complement(f2))
}

lemma example7()
{
  var formula1 : LP_and_or_not := And(Var("p"), Var("q"));
  var formula2 : Formula := Or(And(Var("p"), Var("r")), Var("q"));
  var formula3 : Formula := Or(Not(And(Var("p"), Var("r"))), Var("q"));
  var formula4 : Formula := Or(And(Var("p"), Var("r")), Not(Var("q")));
  assert complement(formula1) == Or(Not(Var("p")), Not(Var("q")));
  assert complement(formula3) == And(And(Var("p"), Var("r")), Not(Var("q")));
}

function size(f : Formula) : nat
{
  match f
  case Var(_) => 1
  case Not(f) => 1 + size(f)
  case Or(f1, f2) => 1 + size(f1) + size(f2)
  case And(f1, f2) => 1 + size(f1) + size(f2)
  case Implies(f1, f2) => 1 + size(f1) + size(f2)
  case Top => 1
  case Bottom => 1
}

function max(a : nat, b : nat) : nat
{
  if a > b then
    a
  else
    b
}

lemma max_smaller_sum(a : nat, b : nat)
  ensures max(a, b) <= a + b
{
}

function height(f : Formula) : nat
{
  match f
  case Var(_) => 1
  case Not(f) => 1 + height(f)
  case Or(f1, f2) => 1 + max(height(f1), height(f2))
  case And(f1, f2) => 1 + max(height(f1), height(f2))
  case Implies(f1, f2) => 1 + max(height(f1), height(f2))
  case Top => 1
  case Bottom => 1
}

lemma {:induction false} height_size(f : Formula)
  ensures height(f) <= size(f)
{
  match f {
    case Var(_) =>
    case Not(f) =>
      height_size(f);
    case Or(f1, f2) =>
      height_size(f1);
      height_size(f2);
    case And(f1, f2) =>
      height_size(f1);
      height_size(f2);
    case Implies(f1, f2) =>
      height_size(f1);
      height_size(f2);
    case Top =>
    case Bottom =>
  }
}

lemma height_size'(f : Formula)
  ensures height(f) <= size(f)
{
}

ghost predicate satisfiable(f : Formula)
{
  exists tau :: value(f, tau)
}

ghost predicate valid(f : Formula)
{
  forall tau :: value(f, tau)
}


lemma example8()
{
  var formula1 : LP_and_or_not := Or(Var("p"), Not(Var("p")));
  assert valid(formula1);
  var formula2 : LP_and_or_not := And(Var("p"), Not(Var("p")));
  assert !satisfiable(formula2);
}

ghost predicate eq(f1 : Formula, f2 : Formula)
{
  forall tau :: value(f1, tau) == value(f2, tau)
}

ghost predicate conseq(gamma : set<Formula>, psi : Formula)
{
  forall tau ::
    (forall phi :: phi in gamma ==> value(phi, tau)) ==>
    value(psi, tau)
}

lemma example9()
{
  var formula1 : LP_and_or_not := Var("p");
  var formula2 : LP_and_or_not := Or(Var("p"), Var("q"));
  assert conseq({ formula1 }, formula2);
}

lemma implication_consequence(f1 : Formula, f2 : Formula)
  ensures conseq({ f1 }, f2) <==> valid(Implies(f1, f2))
{
  assert conseq({ f1 }, f2) ==> valid(Implies(f1, f2)) by
    {
      
    }
  assert conseq({ f1 }, f2) <== valid(Implies(f1, f2)) by
    {
      if (valid(Implies(f1, f2)))
      {
        forall tau | value(f1, tau)
          ensures value(f2, tau)
        {
          assert value(Implies(f1, f2), tau);
        }
        assert forall tau ::
          value(f1, tau) ==>
          value(f2, tau);
        assert conseq({ f1 }, f2);
      }
    }
}

ghost predicate ipoteza(gamma : set<Formula>, phi : Formula)
{
  phi in gamma
}

ghost predicate nd(gamma : set<Formula>, phi : Formula)
{
  ipoteza(gamma, phi)
    // || and_i || and_e1 || ...
}

lemma soundness(gamma : set<Formula>, phi : Formula)
  requires nd(gamma, phi)
  ensures conseq(gamma, phi)
{
}

lemma completeness(gamma : set<Formula>, phi : Formula)
  requires conseq(gamma, phi)
  ensures nd(gamma, phi)
{
  assume false;
}