mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1428 lines
59 KiB
Plaintext
1428 lines
59 KiB
Plaintext
|
|
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
|