why3doc index index
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
Generated by why3doc 1.7.0