module Sem

  use Choice.Choice
  use Functions.Func
  use Firstorder_symbol_spec.Spec
  use Firstorder_term_spec.Spec
  use Firstorder_formula_spec.Spec
  use Firstorder_formula_list_spec.Spec
  use Firstorder_tableau_spec.Spec
  use bool.Bool
  use list.List
  use option.Option
  use OptionFuncs.Funcs

  type model 'ls 'st = {
    interp_fun : 'ls -> (list 'st -> 'st) ;
    interp_pred : 'ls -> (list 'st -> bool) ;
  }

  function term_semantic (t:fo_term 'ls 'b) (m:model 'ls 'st)
    (rho:'b -> 'st) : 'st = match t with
      | Var_fo_term x -> rho x
      | App (Var_symbol f) l -> let ifun = m.interp_fun in
        ifun f (term_list_semantic l m rho)
    end

  with term_list_semantic (t:fo_term_list 'ls 'b) (m:model 'ls 'st)
    (rho:'b -> 'st) : list 'st = match t with
      | FONil -> Nil
      | FOCons x q -> Cons (term_semantic x m rho) (term_list_semantic q m rho)
    end

  predicate formula_semantic (t:fo_formula 'ls 'b) (m:model 'ls 'st)
    (rho:'b -> 'st) = match t with
      | Forall t -> forall x:'st.
        formula_semantic t m (ocase rho x)
      | Exists t -> exists x:'st.
        formula_semantic t m (ocase rho x)
      | And t1 t2 -> formula_semantic t1 m rho /\ formula_semantic t2 m rho
      | Or t1 t2 -> formula_semantic t1 m rho \/ formula_semantic t2 m rho
      | Not t -> not (formula_semantic t m rho)
      | FTrue -> true
      | FFalse -> false
      | PApp (Var_symbol p) l -> let ipred = m.interp_pred in
        ipred p (term_list_semantic l m rho)
    end

  predicate formula_list_conj_semantic (t:fo_formula_list 'ls 'b)
    (m:model 'ls 'st) (rho:'b -> 'st) = match t with
      | FOFNil -> true
      | FOFCons x q -> formula_semantic x m rho /\
        formula_list_conj_semantic q m rho
    end

  predicate formula_list_disj_semantic (t:fo_formula_list 'ls 'b)
    (m:model 'ls 'st) (rho:'b -> 'st) = match t with
      | FOFNil -> false
      | FOFCons x q -> formula_semantic x m rho \/
        formula_list_disj_semantic q m rho
    end

  predicate tableau_node (b:bool) (phib:fo_formula_list 'ls 'b)
    (phi0:fo_formula 'ls 'b) (m:model 'ls 'st) (rho:'b -> 'st) =
    ( b = True /\ formula_semantic phi0 m rho)
      \/ formula_list_disj_semantic phib m rho

  (* This one work by accumulation, as it is related to a context. *)
  predicate tableau_semantic_with (t:tableau 'ls 'b)
    (b:bool) (m:model 'ls 'st) (rho:'b -> 'st) =
    match t with
      | Root -> b = True
      | Node tnext phi0 phib ->
        let b' = if tableau_node b phib phi0 m rho
          then True
          else False in
        tableau_semantic_with tnext b' m rho
    end

  (* Abstraction-definition axiom :
     function semantic_subst (s:'b -> (fo_term 'ls 'c))
       (m:model 'ls 'st) (rho:'c -> 'st) : 'b -> 'st =
         (\ x:'b. term_semantic (s x) m rho) *)
  function semantic_subst (s:'b -> (fo_term 'ls 'c))
    (m:model 'ls 'st) (rho:'c -> 'st) : 'b -> 'st
  axiom semantic_subst_def : forall s:'b -> (fo_term 'ls 'c),
    m:model 'ls 'st, rho:'c -> 'st, x:'b.
      semantic_subst s m rho x = term_semantic (s x) m rho

  (*(* Abstraction-definition axiom :
     constant symbol_name : (symbol 'b) -> 'b =
       (\ x:symbol 'b. match x with Var_symbol x -> x end) *)
  constant symbol_name : (symbol 'b) -> 'b
  axiom symbol_name_def : forall x:symbol 'b.
    symbol_name x = match x with Var_symbol x -> x end
  let lemma symbol_name_subst_identity_inverse (u:unit) : unit
    ensures { rcompose symbol_name subst_id_symbol =
      (identity:(symbol 'b) -> (symbol 'b)) }
    ensures { rcompose subst_id_symbol symbol_name =
      (identity:'b -> 'b) }
  =
    assert { extensionalEqual (identity:(symbol 'b) -> (symbol 'b))
      (rcompose symbol_name subst_id_symbol) } ;
    assert { extensionalEqual (identity:'b -> 'b)
      (rcompose subst_id_symbol symbol_name) }*)

  function model_rename (r:'b -> 'c) (m:model 'c 'st) :
    model 'b 'st = {
    interp_fun = rcompose r m.interp_fun ;
    interp_pred = rcompose r m.interp_pred ;
  }

  lemma model_rename_id : forall m:model 'b 'st.
    model_rename identity m = m

  (* semantic commutation with substitution.
     Required for example for
     universal quantification elimination deduction rule:
     forall x. phi -> phi[x <- t] come from this lemma
     (*and generally speaking, quantifier handling*) *)

  let rec lemma term_semantic_subst_commutation (t:fo_term 'ls 'b)
    (m:model 'ls2 'st) (rho : 'c -> 'st)
    (thetal:'ls -> 'ls2)
    (theta:'b -> (fo_term 'ls2 'c)) : unit
    ensures { term_semantic (
      subst_fo_term t (rcompose thetal subst_id_symbol) theta) m rho =
      term_semantic t (model_rename thetal m) (semantic_subst theta m rho) }
    variant { size_fo_term t }
  =
    match t with
      | Var_fo_term x -> ()
      | App (Var_symbol f) l ->
        term_list_semantic_subst_commutation l m rho thetal theta ;
        let thetals = rcompose thetal subst_id_symbol in
        assert { subst_fo_term t thetals theta =
          App (Var_symbol (thetal f)) (subst_fo_term_list l thetals theta) } ;
        let m2 = model_rename thetal m in
        let l2 = term_list_semantic l m2 (semantic_subst theta m rho) in
        assert { eval m.interp_fun (thetal f) l2 =
            eval m2.interp_fun f l2 }
    end

  with lemma term_list_semantic_subst_commutation (t:fo_term_list 'ls 'b)
    (m:model 'ls2 'st) (rho : 'c -> 'st)
    (thetal:'ls -> 'ls2)
    (theta:'b -> (fo_term 'ls2 'c)) : unit
    ensures { term_list_semantic (
      subst_fo_term_list t (rcompose thetal subst_id_symbol) theta) m rho =
      term_list_semantic t (model_rename thetal m)
        (semantic_subst theta m rho) }
    variant { size_fo_term_list t }
  =
    match t with
      | FONil -> ()
      | FOCons x q -> term_semantic_subst_commutation x m rho thetal theta ;
        term_list_semantic_subst_commutation q m rho thetal theta
    end

  let lemma term_list_semantic_rename_commutation (t:fo_term_list 'ls 'b)
    (m:model 'ls2 'st) (rho:'c -> 'st)
    (thetal:'ls -> 'ls2) (theta:'b -> 'c) : unit
    ensures { term_list_semantic (
      rename_fo_term_list t thetal theta) m rho =
      term_list_semantic t (model_rename thetal m)
        (rcompose theta rho) }
  =
    let p1 = rcompose theta rho in
    let p2 = semantic_subst (rcompose theta subst_id_fo_term) m rho in
    assert { extensionalEqual p1 p2 && p1 = p2 }

  let lemma term_semantic_rename_commutation (t:fo_term 'ls 'b)
    (m:model 'ls2 'st) (rho:'c -> 'st)
    (thetal:'ls -> 'ls2) (theta:'b -> 'c) : unit
    ensures { term_semantic (rename_fo_term t thetal theta) m rho =
      term_semantic t (model_rename thetal m) (rcompose theta rho) }
  =
    assert { extensionalEqual (rcompose theta rho)
      (semantic_subst (subst_of_rename_fo_term theta) m rho) }


  let lemma semantic_lifting_commutation (theta:'b -> (fo_term 'ls 'c))
    (rho : 'c -> 'st) (m:model 'ls 'st) (x:'st) : unit
    ensures { semantic_subst (olifts_fo_term theta) m (ocase rho x) =
      ocase (semantic_subst theta m rho) x }
  =
    let stheta = olifts_fo_term theta in
    let srho = ocase rho x in
    let p1 = semantic_subst stheta m srho in
    let ctr = semantic_subst theta m rho in
    let p2 = ocase ctr x in
    assert { forall x:option 'b. match x with
      | None -> p1 None = p2 None
      | Some z -> p1 (Some z) = p2 (Some z) end
        && p1 x = p2 x } ;
    assert { extensionalEqual p1 p2 }

  let lemma formula_semantic_subst_commutation (t0:fo_formula 'ls 'b)
    (m0:model 'ls2 'st)
    (thetal0:'ls -> 'ls2)
    (theta0:'b -> (fo_term 'ls2 'c))
    (rho:'c -> 'st) : unit
    ensures { formula_semantic (
      subst_fo_formula t0 (rcompose thetal0 subst_id_symbol) theta0) m0 rho
      <-> formula_semantic t0
        (model_rename thetal0 m0) (semantic_subst theta0 m0 rho) }
  =
    let rec ghost aux (t:fo_formula 'ls3 'b2)
      (m:model 'ls4 'st)
      (thetal:'ls3 -> 'ls4)
      (theta:'b2 -> (fo_term 'ls4 'c2)) : unit
      ensures { forall rho:'c2 -> 'st.
        formula_semantic (
          subst_fo_formula t (rcompose thetal subst_id_symbol) theta) m rho
        <-> formula_semantic t
          (model_rename thetal m) (semantic_subst theta m rho) }
      variant { size_fo_formula t }
    =
      let thetals = rcompose thetal subst_id_symbol in
      match t with
        | Forall t2 -> let os = olifts_fo_term theta in
          let st = subst_fo_formula t thetals theta in
          let st2 = subst_fo_formula t2 thetals os in
          aux t2 m thetal os ;
          assert { st = Forall st2 }
        | Exists t2 -> let os = olifts_fo_term theta in
          let st = subst_fo_formula t thetals theta in
          let st2 = subst_fo_formula t2 thetals os in
          aux t2 m thetal os ;
          assert { st = Exists st2 }
        | And t1 t2 -> aux t1 m thetal theta ;
          aux t2 m thetal theta
        | Or t1 t2 -> aux t1 m thetal theta ;
          aux t2 m thetal theta
        | Not t2 -> aux t2 m thetal theta ;
          let st = subst_fo_formula t thetals theta in
          let st2 = subst_fo_formula t2 thetals theta in
          assert { st = Not st2 }
        | FTrue -> ()
        | FFalse -> ()
        | PApp (Var_symbol p) l ->
          let l2 = subst_fo_term_list l thetals theta in
          let t2 = subst_fo_formula t thetals theta in
          assert { t2 = PApp (Var_symbol (thetal p)) l2 } ;
          let m2 = model_rename thetal m in
          assert { forall rho:'c2 -> 'st.
            let rho2 = semantic_subst theta m rho in
            let l3 = term_list_semantic l m2 rho2 in
            let l4 = term_list_semantic l2 m rho in
            (l3 = l4 /\
             (formula_semantic t m2 rho2 <->
               eval m2.interp_pred p l3) /\
             (formula_semantic t2 m rho <->
               eval m.interp_pred (thetal p) l4)) &&
            (formula_semantic t m2 rho2 <->
             formula_semantic t2 m rho) }
      end in
    aux t0 m0 thetal0 theta0

  let lemma formula_semantic_rename_commutation
    (t:fo_formula 'ls 'b) (m:model 'ls2 'st)
    (thetal:'ls -> 'ls2)
    (theta:'b -> 'c) (rho:'c -> 'st) : unit
    ensures { formula_semantic (rename_fo_formula t thetal theta) m rho
      <-> formula_semantic t (model_rename thetal m) (rcompose theta rho) }
  =
    let thetas = rcompose theta subst_id_fo_term in
    assert { rename_fo_formula t thetal theta =
      subst_fo_formula t (rcompose thetal subst_id_symbol) thetas } ;
    let p1 = rcompose theta rho in let p2 = semantic_subst thetas m rho in
    assert { extensionalEqual p1 p2 && p1 = p2 }

  let lemma formula_semantic_term_subst_commutation
    (t:fo_formula 'ls 'b) (m:model 'ls 'st)
    (theta:'b -> (fo_term 'ls 'c)) (rho:'c -> 'st) : unit
    ensures {
      formula_semantic (subst_fo_formula t subst_id_symbol theta) m rho <->
      formula_semantic t m (semantic_subst theta m rho) }
  =
    let t2 = subst_fo_formula t (rcompose identity subst_id_symbol) theta in
    let rho2 = semantic_subst theta m rho in
    assert { formula_semantic t2 m rho <->
      formula_semantic t (model_rename identity m) rho2 }

  let lemma formula_semantic_term_rename_commutation
    (t:fo_formula 'ls 'b) (m:model 'ls 'st)
    (theta:'b -> 'c) (rho:'c -> 'st) : unit
    ensures { formula_semantic (rename_fo_formula t identity theta) m rho <->
      formula_semantic t m (rcompose theta rho) }
  =
    ()

  let rec lemma formula_list_conj_semantic_subst_commutation
    (t:fo_formula_list 'ls 'b) (m:model 'ls2 'st)
    (thetal:'ls -> 'ls2)
    (theta:'b -> (fo_term 'ls2 'c)) (rho:'c -> 'st) : unit
    ensures { formula_list_conj_semantic (
      subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho
      <-> formula_list_conj_semantic t
        (model_rename thetal m) (semantic_subst theta m rho) }
    variant { size_fo_formula_list t }
  =
    match t with | FOFNil -> () | FOFCons _ q ->
      formula_list_conj_semantic_subst_commutation q m thetal theta rho end

  let rec lemma formula_list_disj_semantic_subst_commutation
    (t:fo_formula_list 'ls 'b) (m:model 'ls2 'st)
    (thetal:'ls -> 'ls2)
    (theta:'b -> (fo_term 'ls2 'c)) (rho:'c -> 'st) : unit
    ensures { formula_list_disj_semantic (
      subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho
      <-> formula_list_disj_semantic t
        (model_rename thetal m) (semantic_subst theta m rho) }
    variant { size_fo_formula_list t }
  =
    match t with | FOFNil -> () | FOFCons _ q ->
      formula_list_disj_semantic_subst_commutation q m thetal theta rho end


  let lemma formula_list_conj_semantic_term_subst_commutation
    (t:fo_formula_list 'ls 'b) (m:model 'ls 'st)
    (theta:'b -> (fo_term 'ls 'c)) (rho:'c -> 'st) : unit
    ensures { formula_list_conj_semantic
        (subst_fo_formula_list t subst_id_symbol theta) m rho <->
      formula_list_conj_semantic t m (semantic_subst theta m rho) }
  =
    formula_list_conj_semantic_subst_commutation t m identity theta rho

  let lemma formula_list_disj_semantic_term_subst_commutation
    (t:fo_formula_list 'ls 'b) (m:model 'ls 'st)
    (theta:'b -> (fo_term 'ls 'c)) (rho:'c -> 'st) : unit
    ensures { formula_list_disj_semantic
        (subst_fo_formula_list t subst_id_symbol theta) m rho <->
      formula_list_disj_semantic t m (semantic_subst theta m rho) }
  =
    formula_list_disj_semantic_subst_commutation t m identity theta rho

  let rec lemma tableau_semantic_subst_commutation
    (t:tableau 'ls 'b) (m:model 'ls2 'st)
    (b:bool)
    (thetal:'ls -> 'ls2)
    (theta:'b -> (fo_term 'ls2 'c)) (rho:'c -> 'st) : unit
    ensures { tableau_semantic_with (
      subst_tableau t (rcompose thetal subst_id_symbol) theta) b m rho
      <-> tableau_semantic_with t b
        (model_rename thetal m) (semantic_subst theta m rho) }
    variant { size_tableau t }
  =
    match t with
      | Root -> ()
      | Node tnext phi0 phib ->
        let s1 = rcompose thetal subst_id_symbol in
        let b' = if tableau_node b
          (subst_fo_formula_list phib s1 theta)
          (subst_fo_formula phi0 s1 theta) m rho
          then True
          else False in
        tableau_semantic_subst_commutation tnext m b' thetal theta rho
    end

  let lemma tableau_semantic_term_subst_commutation
    (t:tableau 'ls 'b) (b:bool) (m:model 'ls 'st)
    (theta:'b -> (fo_term 'ls 'c)) (rho:'c -> 'st) : unit
    ensures { tableau_semantic_with (
      subst_tableau t subst_id_symbol theta) b m rho <->
      tableau_semantic_with t b m (semantic_subst theta m rho) }
  =
    tableau_semantic_subst_commutation t m b identity theta rho

  let rec lemma term_semantic_depend_only_free_var
    (t:fo_term 'ls 'b) (m1 m2:model 'ls 'st)
    (rho1 rho2:'b -> 'st) : unit
    requires { forall f:'ls. is_symbol_free_var_in_fo_term f t ->
      eval m1.interp_fun f = eval m2.interp_fun f /\
      eval m1.interp_pred f = eval m2.interp_pred f }
    requires { forall x:'b. is_fo_term_free_var_in_fo_term x t ->
      rho1 x = rho2 x }
    ensures { term_semantic t m1 rho1 = term_semantic t m2 rho2 }
    variant { size_fo_term t }
  =
    match t with Var_fo_term x -> () | App (Var_symbol f) l ->
      term_list_semantic_depend_only_free_var l m1 m2 rho1 rho2 ;
      assert { is_symbol_free_var_in_fo_term f t } end

  with lemma term_list_semantic_depend_only_free_var
    (t:fo_term_list 'ls 'b) (m1 m2:model 'ls 'st)
    (rho1 rho2:'b -> 'st) : unit
    requires { forall f:'ls. is_symbol_free_var_in_fo_term_list f t ->
      eval m1.interp_fun f = eval m2.interp_fun f /\
      eval m1.interp_pred f = eval m2.interp_pred f }
    requires { forall x:'b. is_fo_term_free_var_in_fo_term_list x t ->
      rho1 x = rho2 x }
    ensures { term_list_semantic t m1 rho1 = term_list_semantic t m2 rho2 }
    variant { size_fo_term_list t }
  =
    match t with FONil -> () | FOCons x q ->
      term_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
      term_list_semantic_depend_only_free_var q m1 m2 rho1 rho2 end

  let lemma formula_semantic_depend_only_free_var
    (t:fo_formula 'ls0 'b0) (m1 m2:model 'ls0 'st0)
    (rho1 rho2:'b0 -> 'st0) : unit
    requires { forall f:'ls0. is_symbol_free_var_in_fo_formula f t ->
      eval m1.interp_fun f = eval m2.interp_fun f /\
      eval m1.interp_pred f = eval m2.interp_pred f }
    requires { forall x:'b0. is_fo_term_free_var_in_fo_formula x t ->
      rho1 x = rho2 x }
    ensures { formula_semantic t m1 rho1 <-> formula_semantic t m2 rho2 }
  =
    let rec aux (t:fo_formula 'ls 'b) (m1 m2:model 'ls 'st) : unit
      requires { forall f:'ls. is_symbol_free_var_in_fo_formula f t ->
        eval m1.interp_fun f = eval m2.interp_fun f /\
        eval m1.interp_pred f = eval m2.interp_pred f }
      ensures { forall rho1 rho2:'b -> 'st.
        (forall x:'b.
          is_fo_term_free_var_in_fo_formula x t -> rho1 x = rho2 x) ->
        formula_semantic t m1 rho1 <-> formula_semantic t m2 rho2 }
      variant { size_fo_formula t }
    =
      match t with
        | Forall t2 -> aux t2 m1 m2 ;
          assert { forall rho1 rho2:'b -> 'st.
            (forall x:'b.
              is_fo_term_free_var_in_fo_formula x t -> rho1 x = rho2 x) ->
            ((forall x:'st. formula_semantic t2 m1 (ocase rho1 x) <->
              formula_semantic t2 m2 (ocase rho2 x)) &&
            ((forall x:'st. formula_semantic t2 m1 (ocase rho1 x)) <->
              formula_semantic t m1 rho1) &&
            ((forall x:'st. formula_semantic t2 m1 (ocase rho2 x)) <->
              formula_semantic t m2 rho2)) }
        | Exists t2 -> aux t2 m1 m2 ;
          assert { forall rho1 rho2:'b -> 'st.
            (forall x:'b.
              is_fo_term_free_var_in_fo_formula x t -> rho1 x = rho2 x) ->
            ((forall x:'st. formula_semantic t2 m1 (ocase rho1 x) <->
              formula_semantic t2 m2 (ocase rho2 x)) &&
            ((exists x:'st. formula_semantic t2 m1 (ocase rho1 x)) <->
              formula_semantic t m1 rho1) &&
            ((exists x:'st. formula_semantic t2 m1 (ocase rho2 x)) <->
              formula_semantic t m2 rho2)) }
        | And t1 t2 -> aux t1 m1 m2 ; aux t2 m1 m2
        | Or t1 t2 -> aux t1 m1 m2 ; aux t2 m1 m2
        | Not t2 -> aux t2 m1 m2
        | FTrue -> ()
        | FFalse -> ()
        | PApp (Var_symbol p) l ->
          assert { is_symbol_free_var_in_fo_formula p t } ;
          assert { forall rho1 rho2:'b -> 'st.
            ((forall x:'b. is_fo_term_free_var_in_fo_formula x t ->
              rho1 x = rho2 x) ->
            term_list_semantic l m1 rho1 = term_list_semantic l m2 rho2) /\
            (formula_semantic t m1 rho1 <->
              eval m1.interp_pred p (term_list_semantic l m1 rho1)) /\
            (formula_semantic t m2 rho2 <->
              eval m2.interp_pred p (term_list_semantic l m2 rho2)) }
      end in
    aux t m1 m2

  let rec lemma formula_list_conj_semantic_depend_only_free_var
    (t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st)
    (rho1 rho2:'b -> 'st) : unit
    requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t ->
      eval m1.interp_fun f = eval m2.interp_fun f /\
      eval m1.interp_pred f = eval m2.interp_pred f }
    requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t ->
      rho1 x = rho2 x }
    ensures { formula_list_conj_semantic t m1 rho1 <->
      formula_list_conj_semantic t m2 rho2 }
    variant { size_fo_formula_list t }
  =
    match t with FOFNil -> () | FOFCons x q ->
      formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
      formula_list_conj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end

  let rec lemma formula_list_disj_semantic_depend_only_free_var
    (t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st)
    (rho1 rho2:'b -> 'st) : unit
    requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t ->
      eval m1.interp_fun f = eval m2.interp_fun f /\
      eval m1.interp_pred f = eval m2.interp_pred f }
    requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t ->
      rho1 x = rho2 x }
    ensures { formula_list_disj_semantic t m1 rho1 <->
      formula_list_disj_semantic t m2 rho2 }
    variant { size_fo_formula_list t }
  =
    match t with FOFNil -> () | FOFCons x q ->
      formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ;
      formula_list_disj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end

  predicate formula_list_mem (phi:fo_formula 'ls 'b)
    (l:fo_formula_list 'ls 'b) = match l with
      | FOFNil -> false | FOFCons x q -> x = phi \/ formula_list_mem phi q end

  let rec lemma formula_list_conj_semantic_other_def
    (l:fo_formula_list 'ls 'b) (m:model 'ls 'st)
    (rho:'b -> 'st) : unit
    ensures { formula_list_conj_semantic l m rho <->
      (forall phi:fo_formula 'ls 'b.
        formula_list_mem phi l -> formula_semantic phi m rho) }
    variant { size_fo_formula_list l }
  = match l with FOFNil -> () | FOFCons _ q ->
    formula_list_conj_semantic_other_def q m rho end

  let rec lemma formula_list_disj_semantic_other_def
    (l:fo_formula_list 'ls 'b) (m:model 'ls 'st)
    (rho:'b -> 'st) : unit
    ensures { formula_list_disj_semantic l m rho <->
      (exists phi:fo_formula 'ls 'b.
        formula_list_mem phi l /\ formula_semantic phi m rho) }
    variant { size_fo_formula_list l }
  = match l with FOFNil -> () | FOFCons x q ->
    formula_list_disj_semantic_other_def q m rho end

  (* Problem : validity/unsatifiability are not even axiomatizable in why3,
     since we would have to introduce it from a type quantification.
     However, we can define a demonstrability predicate and show for it
     the same elimination principle as unsatisfiability. *)

  (* Demonstration object (not directly a predicate,
     so we can actually construct the proof object ourselves). *)

  (* G |- A can be read as : for every model+interpretation,
     if /\G is true then A too.
     Which in particular mean : if G |- false, G have no model,
     so we can use G |- false instead of unsat predicate as long
     as it can represent all our demonstration steps. *)

  (*type demonstration 'ls 'b =
    | Axiom
    | ModusPonens (demonstration 'ls 'b) (demonstration 'ls 'b)
      (fo_formula 'ls 'b)
    | Abstraction (demonstration 'ls 'b) (fo_formula 'ls 'b)
      (fo_formula 'ls 'b)
    | ConjunctionIntro (demonstration 'ls 'b) (fo_formula 'ls 'b)
      (demonstration 'ls 'b) (fo_formula 'ls 'b)
    | ConjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b)
    | ConjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b)
    | DisjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b)
      (fo_formula 'ls 'b)
    | DisjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b)
      (fo_formula 'ls 'b)
    | DisjunctionElim (demonstration 'ls 'b) (demonstration 'ls 'b)
      (demonstration 'ls 'b) (fo_formula 'ls 'b) (fo_formula 'ls 'b)
    | UniversalInstantiation (demonstration 'ls 'b)
      (fo_formula 'ls (option 'b)) (fo_term 'ls 'b)
    | Instantiation (demonstration 'ls 'b)
      (fo_formula_list 'ls 'b)
      (fo_formula 'ls 'b) 'b (fo_term 'ls 'b)
    | ExistentialIntroduction (demonstration 'ls 'b)
      (fo_formula 'ls (option 'b)) (fo_term 'ls 'b)
    | ExistentialElimination (demonstration 'ls 'b)
      (demonstration 'ls 'b)
      (fo_formula 'ls (option 'b)) (fo_formula 'ls (option 'b))
    | PointlessExistential (demonstration 'ls 'b)
    | ExFalso (demonstration 'ls 'b)
    | Trivial
    | Weakening (demonstration 'ls 'b) (fo_formula_list 'ls 'b)
    | Skolemization (demonstration 'ls 'b) (fo_formula 'ls 'b) 'ls*)

  (*predicate is_skolem_axiom (phi:fo_formula 'ls 'b) (f:'ls)
    (env:fo_term_list 'ls 'b) =
    match phi with
      | Forall phi2 -> is_skolem_axiom phi2 f
        (FOCons (Var_fo_term None) (rename_fo_term_list env identity some))
      | Or (Not (Exists phi2)) phi3 ->
        phi3 = subst_fo_formula phi2 subst_id_symbol
          (ocase subst_id_fo_term (App (Var_symbol f) env)) /\
        not(is_symbol_free_var_in_fo_formula f phi2)
      | _ -> false
    end*)

  (*(* Hack to force possibility of instantiation of extend_env
     definition axiom ! *)
  function extend_env_selection (g:(list 'st) -> ('b -> 'st))
    (x:option 'b) (y:'st) (q:list 'st) : 'st = match x with
      | None -> y | Some x -> g q x end
  (* Abstraction-definition axiom :
     function extend_env (g:(list 'st) -> ('b -> 'st) :
       (list 'st) -> ((option 'b) -> 'st) =
       (\ l:list 'st. (\ x:option 'b. match l with
         | Cons y q -> extend_env_selection g x y q
         | Nil -> default ) ) *)
  function extend_env (g:(list 'st) -> ('b -> 'st)) :
    (list 'st) -> ((option 'b) -> 'st)
  axiom extend_env_def : forall g:(list 'st) -> ('b -> 'st),
    l:list 'st,x:option 'b. extend_env g l x =
    match l with
      | Cons y q -> extend_env_selection g x y q
      | Nil -> default
    end

  lemma extend_env_none : forall g:(list 'st) -> ('b -> 'st),
    y:'st,l:list 'st. extend_env g (Cons y l) None = y
  lemma extend_env_some : forall g:(list 'st) -> ('b -> 'st),
    x:'b,y:'st,l:list 'st. extend_env g (Cons y l) (Some x) = g l x*)

  (* Abstraction-definition axiom :
    function skolem_predicate (phi:fo_formula 'ls (option 'b))
      (m:model 'ls 'st) (rho:'b -> 'st) : 'st -> bool =
      (\ x:'st. formula_semantic phi m (ocase rho x) ) *)
  function skolem_predicate (phi:fo_formula 'ls (option 'b))
    (m:model 'ls 'st) (rho:'b -> 'st) : 'st -> bool
  axiom skolem_predicate_def : forall phi:fo_formula 'ls (option 'b),
    m:model 'ls 'st,rho:'b -> 'st,x:'st.
    skolem_predicate phi m rho x <-> formula_semantic phi m (ocase rho x)

  (* Abstraction-definition axiom :
    function skolem_function (phi:fo_formula 'ls (option 'b))
      (m:model 'ls 'st) (g:(list 'st) -> ('b -> 'st)) : (list 'st) -> 'st
      = (\ l:list 'st. choice (skolem_predicate phi m rho (g l)) ) *)
  function skolem_function (phi:fo_formula 'ls (option 'b))
    (m:model 'ls 'st) (g:(list 'st) -> ('b -> 'st)) : (list 'st) -> 'st
  axiom skolem_function_def : forall phi:fo_formula 'ls (option 'b),
    m:model 'ls 'st,g:(list 'st) -> ('b -> 'st),l:list 'st.
    skolem_function phi m g l = choice (skolem_predicate phi m (g l))

  (* Abstraction-definition axiom :
    function skolem_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls)
      (g:(list 'st) -> ('b -> 'st)) : (model 'ls 'st) -> (model 'ls 'st) =
      (\ m:model 'ls 'st.
        {
          interp_fun = m.interp_fun[f <- skolem_function phi m g] ;
          interp_pred = m.interp_pred ;
        }) *)

  function skolem_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls)
    (g:(list 'st) -> ('b -> 'st)) : (model 'ls 'st) -> (model 'ls 'st)
  axiom skolem_transformer_def : forall phi:fo_formula 'ls (option 'b),f:'ls,
    g:(list 'st) -> ('b -> 'st), m:model 'ls 'st.
    skolem_transformer phi f g m = {
      interp_fun = m.interp_fun[f <- skolem_function phi m g] ;
      interp_pred = m.interp_pred ;
    }

  let ghost skolem_model_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls)
    (vars:fo_term_list 'ls 'b)
    (g:(list 'st) -> ('b -> 'st)) : (model 'ls 'st) -> (model 'ls 'st)
    requires { not(is_symbol_free_var_in_fo_formula f phi) }
    requires { forall m:model 'ls 'st, rho:'b -> 'st,x:'b.
      is_fo_term_free_var_in_fo_formula (Some x) phi ->
        g (term_list_semantic vars m rho) x = rho x }
    requires { not(is_symbol_free_var_in_fo_term_list f vars) }
    ensures { forall m:model 'ls 'st.
      m.interp_pred = (result m).interp_pred }
    ensures { forall m:model 'ls 'st,f0:'ls.
      f0 <> f -> eval m.interp_fun f0 = eval (result m).interp_fun f0 }
    ensures { forall m:model 'ls 'st,rho:'b -> 'st.
      formula_semantic (Exists phi) m rho ->
      formula_semantic (subst_fo_formula phi subst_id_symbol
        (ocase subst_id_fo_term (App (Var_symbol f) vars))) (result m) rho }
  =
    let skf = skolem_transformer phi f g in
    let skt = App (Var_symbol f) vars in
    let sks = ocase subst_id_fo_term skt in
    let phi' = subst_fo_formula phi subst_id_symbol sks in
    assert { forall m:model 'ls 'st,rho:'b -> 'st.
      let semf = skolem_function phi m g in
      let skm = skf m in
      let em = term_list_semantic vars m rho in
      let esm = term_list_semantic vars skm rho in
      (skm.interp_fun = m.interp_fun[f <- semf]) &&
      (skm.interp_pred = m.interp_pred) &&
      (em = esm) &&
      (forall x:'st.
        let rhox = ocase rho x in
        let rhox2 = ocase (g em) x in
        (forall y:option 'b.
          is_fo_term_free_var_in_fo_formula y phi ->
            rhox y = rhox2 y) &&
        (formula_semantic phi m rhox <-> formula_semantic phi m rhox2)) &&
      (let s1 = semantic_subst sks skm rho in
       let s2 = ocase rho (semf esm) in
       s1 None = s2 None &&
       (forall y:'b. s1 (Some y) = s2 (Some y)) &&
       extensionalEqual s1 s2 &&
       (forall f':'ls. is_symbol_free_var_in_fo_formula f' phi ->
          eval m.interp_fun f' = eval skm.interp_fun f' /\
          eval m.interp_pred f' = eval skm.interp_pred f') &&
       (forall x:'st.
          let rhox = ocase rho x in
          (formula_semantic phi m (ocase (g em) x) ->
           formula_semantic phi m (ocase (g em) (semf em)) &&
           formula_semantic phi m (ocase rho (semf em)) &&
           formula_semantic phi skm s2 &&
           formula_semantic phi' skm rho) &&
          (formula_semantic phi m rhox ->
           formula_semantic phi' skm rho))) &&
       (formula_semantic (Exists phi) m rho ->
         formula_semantic phi' skm rho)
    } ;
    skf

  (*
  let ghost skolemized_model (phi0:fo_formula 'ls0 'b0) (f0:'ls0)
    (m0:model 'ls0 'st) : model 'ls0 'st
    requires { is_skolem_axiom phi0 f0 FONil }
    requires { forall x:'b0. not(is_fo_term_free_var_in_fo_formula x phi0) }
    ensures { forall rho:'b0 -> 'st.
      formula_semantic phi0 result rho }
    ensures { m0.interp_pred = result.interp_pred }
    ensures { forall f':'ls0. f0 <> f' ->
      eval m0.interp_fun f' = eval result.interp_fun f' }
  =
    let rec aux (phi:fo_formula 'ls 'b) (f:'ls)
      (env:fo_term_list 'ls 'b)
      (g:(list 'st) -> ('b -> 'st))
      (m:model 'ls 'st) : model 'ls 'st
      requires { is_skolem_axiom phi f env }
      requires { forall rho:'b -> 'st,x:'b.
        is_fo_term_free_var_in_fo_formula x phi ->
          g (term_list_semantic env m rho) x = rho x }
      requires { not(is_symbol_free_var_in_fo_term_list f env) }
      ensures { forall rho:'b -> 'st.
        formula_semantic phi result rho }
      ensures { m.interp_pred = result.interp_pred }
      ensures { forall f':'ls. f <> f' ->
        eval m.interp_fun f' = eval result.interp_fun f' }
      variant { size_fo_formula phi }
    =
      match phi with
        | Forall phi2 ->
          let renv = rename_fo_term_list env identity some in
          let nenv = FOCons (Var_fo_term None)
            (rename_fo_term_list env identity some) in
          assert { forall rho:(option 'b) -> 'st,x:option 'b.
            is_fo_term_free_var_in_fo_formula x phi2 ->
              let u = term_list_semantic nenv m rho in
              u = Cons (rho None) (term_list_semantic renv m rho) &&
              match x with
              | None -> rho x = extend_env g u x
              | Some y -> is_fo_term_free_var_in_fo_formula y phi &&
                rcompose some rho y = g (term_list_semantic env m
                  (rcompose some rho)) y = g (term_list_semantic renv m rho) y
                  = extend_env g u x
            end } ;
          aux phi2 f nenv (extend_env g) m
        | Or (Not (Exists phi2)) phi3 ->
          let semf = skolem_function phi2 m g in
          let skm = {
            interp_fun = m.interp_fun[f <- semf] ;
            interp_pred = m.interp_pred ;
          } in
          assert { forall rho:'b -> 'st.
            let em = term_list_semantic env m rho in
            let esm = term_list_semantic env skm rho in
            let skt = App (Var_symbol f) env in
            let sks = ocase subst_id_fo_term skt in
            (em = esm) &&
            (phi3 = subst_fo_formula phi2 subst_id_symbol sks) &&
            (forall x:'st.
             let rhox = ocase rho x in
             let rhox2 = ocase (g em) x in
             (forall y:option 'b.
               is_fo_term_free_var_in_fo_formula y phi2 ->
                 rhox y = rhox2 y) &&
             (formula_semantic phi2 m rhox <->
               formula_semantic phi2 m rhox2)) &&
             (let s1 = semantic_subst sks skm rho in
              let s2 = ocase rho (semf esm) in
              s1 None = s2 None &&
              (forall y:'b. s1 (Some y) = s2 (Some y)) &&
              extensionalEqual s1 s2 &&
            (forall f':'ls. is_symbol_free_var_in_fo_formula f' phi2 ->
              eval m.interp_fun f' = eval skm.interp_fun f' /\
              eval m.interp_pred f' = eval skm.interp_pred f') &&
            (forall x:'st.
             let rhox = ocase rho x in
             (formula_semantic phi2 m (ocase (g em) x) ->
              formula_semantic phi2 m (ocase (g em) (semf em)) &&
              formula_semantic phi2 m (ocase rho (semf em)) &&
              formula_semantic phi2 skm s2 &&
              formula_semantic phi3 skm rho) &&
             (formula_semantic phi2 m rhox <-> formula_semantic phi2 skm rhox)
             && (formula_semantic phi2 skm rhox ->
               formula_semantic phi3 skm rho)))
          } ;
          skm
        | _ -> absurd
      end in
    aux phi0 f0 FONil default m0*)

  (*predicate deducible_from (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) =
    match d with
      | Axiom -> formula_list_mem phi gamma
      | ModusPonens d1 d2 phi2 -> deducible_from gamma phi2 d1 /\
        deducible_from gamma (Or (Not phi2) phi) d2
      | Abstraction d phi1 phi2 ->
        deducible_from (FOFCons phi1 gamma) phi2 d /\
        phi = Or (Not phi1) phi2
      | ConjunctionIntro d1 phi1 d2 phi2 ->
        deducible_from gamma phi1 d1 /\
        deducible_from gamma phi2 d2 /\
        phi = And phi1 phi2
      | ConjunctionLeft d phi2 -> deducible_from gamma (And phi phi2) d
      | ConjunctionRight d phi2 -> deducible_from gamma (And phi2 phi) d
      | DisjunctionLeft d phi1 phi2 ->
        deducible_from gamma phi1 d /\ phi = Or phi1 phi2
      | DisjunctionRight d phi1 phi2 ->
        deducible_from gamma phi2 d /\ phi = Or phi1 phi2
      | DisjunctionElim d1 d2 d3 phi1 phi2 ->
        deducible_from gamma (Or phi1 phi2) d1 /\
        deducible_from gamma (Or (Not phi1) phi) d2 /\
        deducible_from gamma (Or (Not phi2) phi) d3
      | UniversalInstantiation d phi2 t ->
        deducible_from gamma (Forall phi2) d /\
        phi = subst_fo_formula phi2 subst_id_symbol (ocase subst_id_fo_term t)
      | Instantiation d gamma2 phi2 x t ->
        let s = subst_id_fo_term[x<-t] in
        deducible_from gamma2 phi2 d /\
        gamma = subst_fo_formula_list gamma2 subst_id_symbol s /\
        phi = subst_fo_formula phi2 subst_id_symbol s
      | ExistentialIntroduction d phi2 t ->
        phi = Exists phi2 /\
        deducible_from gamma (
          subst_fo_formula phi2 subst_id_symbol (ocase subst_id_fo_term t)) d
      | ExistentialElimination d1 d2 phi1 phi2 ->
        deducible_from gamma (Forall (Or (Not phi1) phi2)) d1 /\
        deducible_from gamma (Exists phi1) d2 /\
        phi = Exists phi2
      | PointlessExistential d ->
        deducible_from gamma (Exists
          (rename_fo_formula phi identity some)) d
      | ExFalso d -> deducible_from gamma FFalse d
      | Trivial -> phi = FTrue
      | Weakening d gamma2 ->
        deducible_from gamma2 phi d /\
        (forall phi0:fo_formula 'ls 'b.
          formula_list_mem phi0 gamma2 ->
          formula_list_mem phi0 gamma)
      | Skolemization d phis f ->
        not(is_symbol_free_var_in_fo_formula_list f gamma) /\
        not(is_symbol_free_var_in_fo_formula f phi) /\
        deducible_from (FOFCons phis gamma) phi d /\
        is_skolem_axiom phis f FONil /\
        (forall x:'b. not(is_fo_term_free_var_in_fo_formula x phis))
    end

  let lemma deducible_correct (gamma0:fo_formula_list 'ls 'b0)
    (phi0:fo_formula 'ls 'b0) (d0:demonstration 'ls 'b0)
    (m0:model 'ls 'st0) (rho0:'b0 -> 'st0) : unit
    requires { deducible_from gamma0 phi0 d0 }
    requires { formula_list_conj_semantic gamma0 m0 rho0 }
    ensures { formula_semantic phi0 m0 rho0 }
  =
    let rec ghost aux (gamma:fo_formula_list 'ls 'b)
      (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b)
      (m:model 'ls 'st) : unit
      requires { deducible_from gamma phi d }
      ensures { forall rho:'b -> 'st.
        formula_list_conj_semantic gamma m rho ->
        formula_semantic phi m rho }
      variant { d }
    =
      match d with
        | Axiom -> ()
        | ModusPonens d1 d2 phi2 ->
          aux gamma phi2 d1 m ; aux gamma (Or (Not phi2) phi) d2 m
        | Abstraction d1 phi1 phi2 ->
          aux (FOFCons phi1 gamma) phi2 d1 m
        | ConjunctionIntro d1 phi1 d2 phi2 ->
          aux gamma phi1 d1 m ; aux gamma phi2 d2 m
        | ConjunctionLeft d1 phi2 -> aux gamma (And phi phi2) d1 m
        | ConjunctionRight d1 phi2 -> aux gamma (And phi2 phi) d1 m
        | DisjunctionLeft d1 phi1 phi2 -> aux gamma phi1 d1 m
        | DisjunctionRight d1 phi1 phi2 -> aux gamma phi2 d1 m
        | DisjunctionElim d1 d2 d3 phi1 phi2 -> aux gamma (Or phi1 phi2) d1 m ;
          aux gamma (Or (Not phi1) phi) d2 m ;
          aux gamma (Or (Not phi2) phi) d3 m
        | UniversalInstantiation d1 phi2 t -> aux gamma (Forall phi2) d1 m ;
          assert { forall rho:'b -> 'st.
            let f1 = semantic_subst (ocase subst_id_fo_term t) m rho in
            let f2 = ocase rho (term_semantic t m rho) in
            (forall x:option 'b. match x with
              | None -> f1 None = f2 None
              | Some z -> f1 (Some z) = f2 (Some z) end && f1 x = f2 x)
            && extensionalEqual f1 f2 && f1 = f2 }
        | Instantiation d gamma2 phi2 x t -> aux gamma2 phi2 d m
        | ExistentialIntroduction d phi2 t ->
          let s = ocase subst_id_fo_term t in
          let phi3 = subst_fo_formula phi2 subst_id_symbol s in
          aux gamma phi3 d m ;
          assert { forall rho:'b -> 'st.
            let f1 = semantic_subst (ocase subst_id_fo_term t) m rho in
            let f2 = ocase rho (term_semantic t m rho) in
            (forall x:option 'b. match x with
              | None -> f1 None = f2 None
              | Some z -> f1 (Some z) = f2 (Some z) end && f1 x = f2 x)
            && extensionalEqual f1 f2 && f1 = f2 }
        | ExistentialElimination d1 d2 phi1 phi2 ->
          aux gamma (Forall (Or (Not phi1) phi2)) d1 m ;
          aux gamma (Exists phi1) d2 m
        | PointlessExistential d ->
          let phi2 = rename_fo_formula phi identity some in
          assert { phi2 = subst_fo_formula phi
            (rcompose identity subst_id_symbol)
            (rcompose some subst_id_fo_term) } ;
          assert { forall rho:'b -> 'st,x:'st.
            formula_semantic phi2 m (ocase rho x) <->
            formula_semantic phi m rho } ;
          aux gamma (Exists (rename_fo_formula phi identity some)) d m
        | ExFalso d -> aux gamma FFalse d m
        | Trivial -> ()
        | Weakening d2 gamma2 -> aux gamma2 phi d2 m
        | Skolemization d phis f ->
          let skm = skolemized_model phis f m in
          assert { forall rho:'b -> 'st.
            (formula_list_conj_semantic gamma m rho
              <-> formula_list_conj_semantic gamma skm rho) /\
            (formula_semantic phi m rho <->
              formula_semantic phi skm rho) } ;
          aux (FOFCons phis gamma) phi d skm
        | _ -> absurd
      end in
    aux gamma0 phi0 d0 m0

  predicate entail (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) =
    exists d:demonstration 'ls 'b.
      deducible_from gamma phi d

  predicate unsat (gamma:fo_formula_list 'ls 'b) =
    entail gamma FFalse

  predicate valid (phi:fo_formula 'ls 'b) =
    entail FOFNil phi

  lemma entail_correct : forall gamma:fo_formula_list 'ls 'b,
    phi:fo_formula 'ls 'b,m:model 'ls 'st,rho:'b -> 'st.
    entail gamma phi ->
      formula_list_conj_semantic gamma m rho -> formula_semantic phi m rho

  lemma unsat_correct : forall gamma:fo_formula_list 'ls 'b,
    m:model 'ls 'st,rho:'b -> 'st.
    unsat gamma -> not(formula_list_conj_semantic gamma m rho)

  lemma valid_correct : forall phi:fo_formula 'ls 'b,
    m:model 'ls 'st,rho:'b -> 'st.
    valid phi -> formula_semantic phi m rho

  function imply (phi1 phi2:fo_formula 'ls 'b) : fo_formula 'ls 'b =
    Or (Not phi1) phi2

  function equiv (phi1 phi2:fo_formula 'ls 'b) : fo_formula 'ls 'b =
    And (imply phi1 phi2) (imply phi2 phi1)

  type sequent 'ls 'b = {
    demo : demonstration 'ls 'b ;
    context : fo_formula_list 'ls 'b ;
    conclusion : fo_formula 'ls 'b ;
  }

  predicate sequent_correct (s:sequent 'ls 'b) =
    deducible_from s.context s.conclusion s.demo

  let ghost make_axiom (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) : sequent 'ls 'b
    requires { formula_list_mem phi gamma }
    ensures { sequent_correct result }
    ensures { result.context = gamma }
    ensures { result.conclusion = phi }
  = { demo = Axiom ; context = gamma ; conclusion = phi }

  let ghost make_abstraction (s:sequent 'ls 'b) :
    sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.context with FOFNil -> false | _ -> true end }
    ensures { sequent_correct result }
    ensures { match s.context with FOFNil -> false | FOFCons x q ->
      result.context = q /\ result.conclusion = imply x s.conclusion end }
  = match s.context with FOFNil -> absurd
      | FOFCons x q -> { demo = Abstraction s.demo x s.conclusion ;
        context = q ; conclusion = imply x s.conclusion }
    end

  let ghost modus_ponens (s1 s2:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s1 /\ sequent_correct s2 }
    requires { match s1.conclusion with
      | Or (Not phi1) phi2 -> s2.conclusion = phi1
      | _ -> false end }
    requires { s1.context = s2.context }
    ensures { sequent_correct result }
    ensures { result.context = s1.context }
    ensures { match s1.conclusion with
      | Or _ phi2 -> result.conclusion = phi2
      | _ -> false end }
  = match s1.conclusion with
    | Or (Not phi1) phi2 -> { demo = ModusPonens s2.demo s1.demo phi1 ;
        context = s1.context ;
        conclusion = phi2 }
    | _ -> absurd end

  let ghost make_classical (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) : sequent 'ls 'b
    ensures { sequent_correct result }
    ensures { result.context = gamma }
    ensures { result.conclusion = Or (Not phi) phi }
  = make_abstraction (make_axiom (FOFCons phi gamma) phi)

  let ghost disjunction_elimination (s1 s2 s3:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s1 /\ sequent_correct s2 /\ sequent_correct s3 }
    requires { match s1.conclusion , s2.conclusion , s3.conclusion with
      | Or phi1 phi2 , Or (Not phi1') phi3 , Or (Not phi2') phi3' ->
        phi1 = phi1' /\ phi2 = phi2' /\ phi3 = phi3'
      | _ -> false end }
    requires { s1.context = s2.context = s3.context }
    ensures { sequent_correct result }
    ensures { result.context = s1.context }
    ensures { match s3.conclusion with
      | Or _ phi3 -> result.conclusion = phi3
      | _ -> false end }
  =
    match s1.conclusion , s3.conclusion with
      | Or phi1 phi2 , Or _ phi3 ->
        { demo = DisjunctionElim s1.demo s2.demo s3.demo phi1 phi2 ;
          context = s1.context ;
          conclusion = phi3 ; }
      | _ -> absurd
    end

  let ghost disjunction_left (s:sequent 'ls 'b) (phi2:fo_formula 'ls 'b) :
    sequent 'ls 'b
    requires { sequent_correct s }
    ensures { sequent_correct result }
    ensures { result.conclusion = Or s.conclusion phi2 }
    ensures { s.context = result.context }
  =
    { demo = DisjunctionLeft s.demo s.conclusion phi2 ;
      context = s.context ;
      conclusion = Or s.conclusion phi2 }

  let ghost disjunction_right (phi1:fo_formula 'ls 'b) (s:sequent 'ls 'b) :
    sequent 'ls 'b
    requires { sequent_correct s }
    ensures { sequent_correct result }
    ensures { result.conclusion = Or phi1 s.conclusion }
    ensures { s.context = result.context }
  =
    { demo = DisjunctionRight s.demo phi1 s.conclusion ;
      context = s.context ;
      conclusion = Or phi1 s.conclusion }

  let ghost conjunction (s1 s2:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s1 /\ sequent_correct s2 }
    requires { s1.context = s2.context }
    ensures { sequent_correct result }
    ensures { result.context = s1.context }
    ensures { result.conclusion = And s1.conclusion s2.conclusion }
  =
    { demo = ConjunctionIntro s1.demo s1.conclusion s2.demo s2.conclusion ;
      context = s1.context ;
      conclusion = And s1.conclusion s2.conclusion }

  let ghost conjunction_left (s:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.conclusion with And _ _ -> true | _ -> false end }
    ensures { sequent_correct result }
    ensures { result.context = s.context }
    ensures { match s.conclusion with And phi _ -> result.conclusion = phi
      | _ -> false end }
  = match s.conclusion with
      | And phi1 phi2 -> { demo = ConjunctionLeft s.demo phi2 ;
        context = s.context ;
        conclusion = phi1 }
      | _ -> absurd
    end

  let ghost conjunction_right (s:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.conclusion with And _ _ -> true | _ -> false end }
    ensures { sequent_correct result }
    ensures { result.context = s.context }
    ensures { match s.conclusion with And _ phi -> result.conclusion = phi
      | _ -> false end }
  = match s.conclusion with
      | And phi2 phi1 -> { demo = ConjunctionRight s.demo phi2 ;
        context = s.context ;
        conclusion = phi1 }
      | _ -> absurd
    end

  let ghost exfalso (s:sequent 'ls 'b) (phi:fo_formula 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.conclusion with FFalse -> true | _ -> false end }
    ensures { sequent_correct result }
    ensures { result.context = s.context }
    ensures { result.conclusion = phi }
  = { demo = ExFalso s.demo ; context = s.context ; conclusion = phi }

  let ghost make_trivial (gamma:fo_formula_list 'ls 'b) : sequent 'ls 'b
    ensures { sequent_correct result }
    ensures { result.context = gamma }
    ensures { result.conclusion = FTrue }
  = { demo = Trivial ; context = gamma ; conclusion = FTrue }

  let ghost weaken (gamma:fo_formula_list 'ls 'b)
    (s:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { forall phi:fo_formula 'ls 'b.
      formula_list_mem phi s.context -> formula_list_mem phi gamma }
    ensures { sequent_correct result }
    ensures { result.context = gamma }
    ensures { result.conclusion = s.conclusion }
  = { demo = Weakening s.demo s.context ;
      context = gamma ;
      conclusion = s.conclusion }

  let ghost skolem_elim (f:'ls) (s:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.context with FOFCons phis gamma ->
      is_skolem_axiom phis f FONil /\
      (forall x:'b. not(is_fo_term_free_var_in_fo_formula x phis)) /\
      not(is_symbol_free_var_in_fo_formula_list f gamma)
      | _ -> false end }
    requires { not(is_symbol_free_var_in_fo_formula f s.conclusion) }
    ensures { sequent_correct result }
    ensures { match s.context with FOFCons _ gamma -> result.context = gamma
      | _ -> false end }
    ensures { result.conclusion = s.conclusion }
  = match s.context with FOFCons phis gamma ->
      { demo = Skolemization s.demo phis f ;
        context = gamma ;
        conclusion = s.conclusion }
      | _ -> absurd end

  let ghost conjunction_commutative (s:sequent 'ls 'b) : sequent 'ls 'b
    requires { sequent_correct s }
    requires { match s.conclusion with And _ _ -> true | _ -> false end }
    ensures { sequent_correct result }
    ensures { result.context = s.context }
    ensures { match s.conclusion with And phi1 phi2 ->
      result.conclusion = And phi2 phi1 | _ -> false end }
  = conjunction (conjunction_right s) (conjunction_left s)

  let ghost equiv_reflexive (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) : sequent 'ls 'b
    ensures { sequent_correct result }
    ensures { result.context = gamma }
    ensures { result.conclusion = equiv phi phi }
  =
    let u = make_classical gamma phi in
    conjunction u u

  (*

  let ghost imply_or_morphism (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2 phi3 phi4:fo_formula 'ls 'b)
    (d1 d2:demonstration 'ls 'b) : demonstration 'ls 'b
    requires { deducible_from gamma (imply phi1 phi3) d1 }
    requires { deducible_from gamma (imply phi2 phi4) d2 }
    ensures { deducible_from gamma
     (imply (Or phi1 phi2) (Or phi3 phi4)) result }
  =
    let o34 = Or phi3 phi4 in
    let o12 = Or phi1 phi2 in
    let gamma12 = FOFCons o12 gamma in
    let gamma121 = FOFCons phi1 gamma12 in
    let gamma122 = FOFCons phi2 gamma12 in
    let d1 = modus_ponens gamma121 phi1 phi3
      (weaken gamma gamma121 (imply phi1 phi3) d1)
      (make_axiom gamma121 phi1) in
    let d2 = modus_ponens gamma122 phi2 phi4
      (weaken gamma gamma122 (imply phi2 phi4) d2)
      (make_axiom gamma122 phi2) in
    disjunction_elimination gamma12 phi1 phi2 o34
      (make_axiom gamma12 o12)
      (make_abstraction gamma12 phi1 o34
        (disjunction_left gamma121 phi3 phi4 d1))
      (make_abstraction gamma12 phi2 o34
        (disjunction_right gamma122 phi3 phi4 d2))

  let ghost equiv_or_morphism (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2 phi3 phi4:fo_formula 'ls 'b)
    (d1 d2:demonstration 'ls 'b) : demonstration 'ls 'b
    requires { deducible_from gamma (equiv phi1 phi3) d1 }
    requires { deducible_from gamma (equiv phi2 phi4) d2 }
    ensures { deducible_from gamma
      (equiv (Or phi1 phi2) (Or phi3 phi4)) result }
  =
    let (o12,o34) = (Or phi1 phi2,Or phi3 phi4) in
    let way1 = imply_or_morphism gamma phi1 phi2 phi3 phi4
      (conjunction_left gamma (imply phi1 phi3) (imply phi3 phi1) d1)
      (conjunction_left gamma (imply phi2 phi4) (imply phi4 phi2) d2) in
    let way2 = imply_or_morphism gamma phi3 phi4 phi1 phi2
      (conjunction_right gamma (imply phi1 phi3) (imply phi3 phi1) d1)
      (conjunction_right gamma (imply phi2 phi4) (imply phi4 phi2) d2) in
    conjunction (imply o12 o34) (imply o34 o12) way1 way2
  *)


  (*
  let ghost disjunction_commutation (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Or phi1 phi2) d }
    ensures { deducible_from gamma (Or phi2 phi1) result }
  =
    let o = Or phi2 phi1 in
    let (gamma1,gamma2) = (FOFCons phi1 gamma,FOFCons phi2 gamma) in
    let d1 = disjunction_right gamma1 phi2 phi1 (make_axiom gamma1 phi1) in
    let d2 = disjunction_left gamma2 phi2 phi1 (make_axiom gamma2 phi2) in
    let d1 = make_abstraction gamma phi1 o d1 in
    let d2 = make_abstraction gamma phi2 o d2 in
    disjunction_elimination gamma phi1 phi2 o d d1 d2

  let ghost disjunction_associative_r (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2 phi3:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Or (Or phi1 phi2) phi3) d }
    ensures { deducible_from gamma (Or phi1 (Or phi2 phi3)) result }
  =
    let o12 = Or phi1 phi2 in
    let o23 = Or phi2 phi3 in
    let ob = Or o12 phi3 in
    let oa = Or phi1 o23 in
    let gamma12 = FOFCons o12 gamma in
    let gamma1 = FOFCons phi1 gamma12 in
    let gamma2 = FOFCons phi2 gamma12 in
    let gamma3 = FOFCons phi3 gamma in
    let d1 = disjunction_left gamma1 phi1 o23
      (make_axiom gamma1 phi1) in
    let d2 = disjunction_right gamma2 phi1 o23
      (disjunction_left gamma2 phi2 phi3 (make_axiom gamma2 phi2)) in
    let d1 = make_abstraction gamma12 phi1 oa d1 in
    let d2 = make_abstraction gamma12 phi2 oa d2 in
    let d12 = disjunction_elimination gamma12 phi1 phi2 oa
      (make_axiom gamma12 o12) d1 d2 in
    let d3 = disjunction_right gamma3 phi1 o23
      (disjunction_right gamma3 phi2 phi3 (make_axiom gamma3 phi3)) in
    let d12 = make_abstraction gamma o12 oa d12 in
    let d3 = make_abstraction gamma phi3 oa d3 in
    disjunction_elimination gamma o12 phi3 oa d d12 d3

  let ghost disjunction_associative_l (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2 phi3:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Or phi1 (Or phi2 phi3)) d }
    ensures { deducible_from gamma (Or (Or phi1 phi2) phi3) result }
  =
    let o23 = Or phi2 phi3 in
    let o12 = Or phi1 phi2 in
    let ob = Or phi1 o23 in
    let oa = Or o12 phi3 in
    let gamma23 = FOFCons o23 gamma in
    let gamma3 = FOFCons phi3 gamma23 in
    let gamma2 = FOFCons phi2 gamma23 in
    let gamma1 = FOFCons phi1 gamma in
    let d3 = disjunction_right gamma3 o12 phi3
      (make_axiom gamma3 phi3) in
    let d2 = disjunction_left gamma2 o12 phi3
      (disjunction_right gamma2 phi1 phi2 (make_axiom gamma2 phi2)) in
    let d3 = make_abstraction gamma23 phi3 oa d3 in
    let d2 = make_abstraction gamma23 phi2 oa d2 in
    let d23 = disjunction_elimination gamma23 phi2 phi3 oa
      (make_axiom gamma23 o23) d2 d3 in
    let d1 = disjunction_left gamma1 o12 phi3
      (disjunction_left gamma1 phi1 phi2 (make_axiom gamma1 phi1)) in
    let d23 = make_abstraction gamma o23 oa d23 in
    let d1 = make_abstraction gamma phi1 oa d1 in
    disjunction_elimination gamma phi1 o23 oa d d1 d23
  *)

  (*
  let ghost double_negation_elimination (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Not (Not phi)) d }
    ensures { deducible_from gamma phi result }
  =
    let nphi = Not phi in
    let nnphi = Not nphi in
    let d0 = make_classical gamma phi in
    let d2 = disjunction_left gamma nnphi phi d in
    disjunction_elimination gamma nphi phi phi d0 d2 d0
  *)

  (*let ghost false_neutral_left_disjunction (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Or FFalse phi) d }
    ensures { deducible_from gamma phi result }
  =
    let d1 = Abstraction (ExFalso Axiom) FFalse phi in
    let d2 = Abstraction Axiom phi phi in
    DisjunctionElim d d1 d2 FFalse phi

  let ghost false_neutral_right_disjunction (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) :
    demonstration 'ls 'b
    requires { deducible_from gamma (Or phi FFalse) d }
    ensures { deducible_from gamma phi result }
  =
    false_neutral_left_disjunction gamma phi
      (disjunction_commutation gamma phi FFalse d)*)

  (*(* Now we do not need the demonstration object anymore. *)

  let lemma entail_axiom (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) : unit
    requires { formula_list_mem phi gamma }
    ensures { entail gamma phi }
  =
    ()

  let lemma entail_modus_ponens (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b) : unit
    requires { entail gamma phi1 /\ entail gamma (Or (Not phi1) phi2) }
    ensures { entail gamma phi2 }
  =
    assert { forall d1 d2:demonstration 'ls 'b.
      deducible_from gamma phi1 d1 /\
      deducible_from gamma (Or (Not phi1) phi2) d2 ->
      deducible_from gamma phi2 (ModusPonens d1 d2 phi1) }

  let lemma entail_abstraction (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b) : unit
    requires { entail (FOFCons phi1 gamma) phi2 }
    ensures { entail gamma (Or (Not phi1) phi2) }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from (FOFCons phi1 gamma) phi2 d ->
      deducible_from gamma (Or (Not phi1) phi2) (Abstraction d phi1 phi2) }

  let lemma entail_conjunction (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b) : unit
    ensures { entail gamma (And phi1 phi2)
      <-> entail gamma phi1 /\ entail gamma phi2 }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma (And phi1 phi2) d ->
      deducible_from gamma phi1 (ConjunctionLeft d phi2) /\
      deducible_from gamma phi2 (ConjunctionRight d phi1) } ;
    assert { forall d1 d2:demonstration 'ls 'b.
      deducible_from gamma phi1 d1 /\
      deducible_from gamma phi2 d2 ->
      deducible_from gamma (And phi1 phi2) (ConjunctionIntro d1 phi1 d2 phi2) }

  let lemma entail_disjunction_left (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b)
    requires { entail gamma phi1 }
    ensures { entail gamma (Or phi1 phi2) }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma phi1 d ->
      deducible_from gamma (Or phi1 phi2) (DisjunctionLeft d phi1 phi2) }

  let lemma entail_disjunction_right (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b)
    requires { entail gamma phi2 }
    ensures { entail gamma (Or phi1 phi2) }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma phi2 d ->
      deducible_from gamma (Or phi1 phi2) (DisjunctionRight d phi1 phi2) }

  let lemma entail_disjunction_elim (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2 phi3:fo_formula 'ls 'b)
    requires { entail gamma (Or phi1 phi2) }
    requires { entail gamma (Or (Not phi1) phi3) }
    requires { entail gamma (Or (Not phi2) phi3) }
    ensures { entail gamma phi3 }
  =
    assert { forall d1 d2 d3:demonstration 'ls 'b.
      deducible_from gamma (Or phi1 phi2) d1 /\
      deducible_from gamma (Or (Not phi1) phi3) d2 /\
      deducible_from gamma (Or (Not phi2) phi3) d3 ->
      deducible_from gamma phi3 (DisjunctionElim d1 d2 d3 phi1 phi2) }

  let lemma entail_universal_instantiation (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls (option 'b)) (t:fo_term 'ls 'b)
    requires { entail gamma (Forall phi) }
    ensures { entail gamma (subst_fo_formula phi
      (ocase subst_id_fo_term t)) }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma (Forall phi) d ->
      deducible_from gamma (subst_fo_formula phi
        (ocase subst_id_fo_term t)) (UniversalInstantiation d phi t) }

  let lemma entail_instantiation (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls 'b) (x:'b) (t:fo_term 'ls 'b)
    requires { entail gamma phi }
    ensures { let s = subst_id_fo_term[x<-t] in
      entail (subst_fo_formula_list gamma s) (subst_fo_formula phi s) }
  =
    let s = subst_id_fo_term[x<-t] in
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma phi d ->
      deducible_from (subst_fo_formula_list gamma s)
        (subst_fo_formula phi s) (Instantiation d gamma phi x t) }

  let lemma entail_existential_introduction (gamma:fo_formula_list 'ls 'b)
    (phi:fo_formula 'ls (option 'b)) (t:fo_term 'ls 'b)
    requires { entail gamma (subst_fo_formula phi
      (ocase subst_id_fo_term t)) }
    ensures { entail gamma (Exists phi) }
  =
    assert { forall d:demonstration 'ls 'b.
      deducible_from gamma (subst_fo_formula phi
        (ocase subst_id_fo_term t)) d ->
      deducible_from gamma (Exists phi) (ExistentialIntroduction d phi t) }

  let lemma entail_existential_elimination (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls (option 'b))
    requires { entail gamma (Forall (Or (Not phi1) phi2)) }
    requires { entail gamma (Exists phi1) }
    ensures { entail gamma (Exists phi2) }
  =
    assert { forall d1 d2:demonstration 'ls 'b.
      deducible_from gamma (Forall (Or (Not phi1) phi2)) d1 /\
      deducible_from gamma (Exists phi1) d2 ->
      deducible_from gamma (Exists phi2)
        (ExistentialElimination d1 d2 phi1 phi2) }

  let lemma disjunction_commutative (gamma:fo_formula_list 'ls 'b)
    (phi1 phi2:fo_formula 'ls 'b)
    requires { entail gamma (Or phi1 phi2) }
    ensures { entail gamma (Or phi2 phi1) }
  =
    entail_axiom (FOFCons phi1 gamma) phi1 ;
    entail_axiom (FOFCons phi2 gamma) phi2 ;
    entail_disjunction_right (FOFCons phi1 gamma) phi2 phi1 ;
    entail_disjunction_left (FOFCons phi2 gamma) phi2 phi1 ;
    entail_disjunction_elim gamma phi1 phi2 (Or phi2 phi1)*)
  *)
end