diff options
Diffstat (limited to 'plugins/dp')
| -rw-r--r-- | plugins/dp/Dp.v | 120 | ||||
| -rw-r--r-- | plugins/dp/TODO | 24 | ||||
| -rw-r--r-- | plugins/dp/dp.ml | 1134 | ||||
| -rw-r--r-- | plugins/dp/dp.mli | 20 | ||||
| -rw-r--r-- | plugins/dp/dp_plugin.mllib | 5 | ||||
| -rw-r--r-- | plugins/dp/dp_why.ml | 186 | ||||
| -rw-r--r-- | plugins/dp/dp_why.mli | 17 | ||||
| -rw-r--r-- | plugins/dp/dp_zenon.mli | 7 | ||||
| -rw-r--r-- | plugins/dp/dp_zenon.mll | 189 | ||||
| -rw-r--r-- | plugins/dp/fol.mli | 58 | ||||
| -rw-r--r-- | plugins/dp/g_dp.ml4 | 79 | ||||
| -rw-r--r-- | plugins/dp/test2.v | 80 | ||||
| -rw-r--r-- | plugins/dp/tests.v | 300 | ||||
| -rw-r--r-- | plugins/dp/vo.itarget | 1 | ||||
| -rw-r--r-- | plugins/dp/zenon.v | 94 |
15 files changed, 2314 insertions, 0 deletions
diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v new file mode 100644 index 00000000..bc7d73f6 --- /dev/null +++ b/plugins/dp/Dp.v @@ -0,0 +1,120 @@ +(* Calls to external decision procedures *) + +Require Export ZArith. +Require Export Classical. + +(* Zenon *) + +(* Copyright 2004 INRIA *) +(* $Id$ *) + +Lemma zenon_nottrue : + (~True -> False). +Proof. tauto. Qed. + +Lemma zenon_noteq : forall (T : Type) (t : T), + ((t <> t) -> False). +Proof. tauto. Qed. + +Lemma zenon_and : forall P Q : Prop, + (P -> Q -> False) -> (P /\ Q -> False). +Proof. tauto. Qed. + +Lemma zenon_or : forall P Q : Prop, + (P -> False) -> (Q -> False) -> (P \/ Q -> False). +Proof. tauto. Qed. + +Lemma zenon_imply : forall P Q : Prop, + (~P -> False) -> (Q -> False) -> ((P -> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_equiv : forall P Q : Prop, + (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notand : forall P Q : Prop, + (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notor : forall P Q : Prop, + (~P -> ~Q -> False) -> (~(P \/ Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notimply : forall P Q : Prop, + (P -> ~Q -> False) -> (~(P -> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notequiv : forall P Q : Prop, + (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_ex : forall (T : Type) (P : T -> Prop), + (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T), + ((P t) -> False) -> ((forall x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T), + (~(P t) -> False) -> (~(exists x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_notall : forall (T : Type) (P : T -> Prop), + (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False). +Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed. + +Lemma zenon_equal_base : forall (T : Type) (f : T), f = f. +Proof. auto. Qed. + +Lemma zenon_equal_step : + forall (S T : Type) (fa fb : S -> T) (a b : S), + (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)). +Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed. + +Lemma zenon_pnotp : forall P Q : Prop, + (P = Q) -> (P -> ~Q -> False). +Proof. intros P Q Ha. rewrite Ha. auto. Qed. + +Lemma zenon_notequal : forall (T : Type) (a b : T), + (a = b) -> (a <> b -> False). +Proof. auto. Qed. + +Ltac zenon_intro id := + intro id || let nid := fresh in (intro nid; clear nid) +. + +Definition zenon_and_s := fun P Q a b => zenon_and P Q b a. +Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a. +Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a. +Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a. +Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a. +Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a. +Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a. +Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a. +Definition zenon_ex_s := fun T P a b => zenon_ex T P b a. +Definition zenon_notall_s := fun T P a b => zenon_notall T P b a. + +Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b. +Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x. + +(* Ergo *) + +Set Implicit Arguments. +Section congr. + Variable t:Type. +Lemma ergo_eq_concat_1 : + forall (P:t -> Prop) (x y:t), + P x -> x = y -> P y. +Proof. + intros; subst; auto. +Qed. + +Lemma ergo_eq_concat_2 : + forall (P:t -> t -> Prop) (x1 x2 y1 y2:t), + P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2. +Proof. + intros; subst; auto. +Qed. + +End congr. diff --git a/plugins/dp/TODO b/plugins/dp/TODO new file mode 100644 index 00000000..44349e21 --- /dev/null +++ b/plugins/dp/TODO @@ -0,0 +1,24 @@ + +TODO +---- + +- axiomes pour les prédicats récursifs comme + + Fixpoint even (n:nat) : Prop := + match n with + O => True + | S O => False + | S (S p) => even p + end. + + ou encore In sur les listes du module Coq List. + +- discriminate + +- inversion (Set et Prop) + + +BUGS +---- + + diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml new file mode 100644 index 00000000..34b32c0a --- /dev/null +++ b/plugins/dp/dp.ml @@ -0,0 +1,1134 @@ +(* Authors: Nicolas Ayache and Jean-Christophe Filliâtre *) +(* Tactics to call decision procedures *) + +(* Works in two steps: + + - first the Coq context and the current goal are translated in + Polymorphic First-Order Logic (see fol.mli in this directory) + + - then the resulting query is passed to the Why tool that translates + it to the syntax of the selected prover (Simplify, CVC Lite, haRVey, + Zenon) +*) + +open Util +open Pp +open Libobject +open Summary +open Term +open Tacmach +open Tactics +open Tacticals +open Fol +open Names +open Nameops +open Namegen +open Termops +open Coqlib +open Hipattern +open Libnames +open Declarations +open Dp_why + +let debug = ref false +let set_debug b = debug := b +let trace = ref false +let set_trace b = trace := b +let timeout = ref 10 +let set_timeout n = timeout := n + +let (dp_timeout_obj,_) = + declare_object + {(default_object "Dp_timeout") with + cache_function = (fun (_,x) -> set_timeout x); + load_function = (fun _ (_,x) -> set_timeout x)} + +let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) + +let (dp_debug_obj,_) = + declare_object + {(default_object "Dp_debug") with + cache_function = (fun (_,x) -> set_debug x); + load_function = (fun _ (_,x) -> set_debug x)} + +let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) + +let (dp_trace_obj,_) = + declare_object + {(default_object "Dp_trace") with + cache_function = (fun (_,x) -> set_trace x); + load_function = (fun _ (_,x) -> set_trace x)} + +let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x) + +let logic_dir = ["Coq";"Logic";"Decidable"] +let coq_modules = + init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + @ [["Coq"; "ZArith"; "BinInt"]; + ["Coq"; "Reals"; "Rdefinitions"]; + ["Coq"; "Reals"; "Raxioms";]; + ["Coq"; "Reals"; "Rbasic_fun";]; + ["Coq"; "Reals"; "R_sqrt";]; + ["Coq"; "Reals"; "Rfunctions";]] + @ [["Coq"; "omega"; "OmegaLemmas"]] + +let constant = gen_constant_in_modules "dp" coq_modules + +(* integers constants and operations *) +let coq_Z = lazy (constant "Z") +let coq_Zplus = lazy (constant "Zplus") +let coq_Zmult = lazy (constant "Zmult") +let coq_Zopp = lazy (constant "Zopp") +let coq_Zminus = lazy (constant "Zminus") +let coq_Zdiv = lazy (constant "Zdiv") +let coq_Zs = lazy (constant "Zs") +let coq_Zgt = lazy (constant "Zgt") +let coq_Zle = lazy (constant "Zle") +let coq_Zge = lazy (constant "Zge") +let coq_Zlt = lazy (constant "Zlt") +let coq_Z0 = lazy (constant "Z0") +let coq_Zpos = lazy (constant "Zpos") +let coq_Zneg = lazy (constant "Zneg") +let coq_xH = lazy (constant "xH") +let coq_xI = lazy (constant "xI") +let coq_xO = lazy (constant "xO") +let coq_iff = lazy (constant "iff") + +(* real constants and operations *) +let coq_R = lazy (constant "R") +let coq_R0 = lazy (constant "R0") +let coq_R1 = lazy (constant "R1") +let coq_Rgt = lazy (constant "Rgt") +let coq_Rle = lazy (constant "Rle") +let coq_Rge = lazy (constant "Rge") +let coq_Rlt = lazy (constant "Rlt") +let coq_Rplus = lazy (constant "Rplus") +let coq_Rmult = lazy (constant "Rmult") +let coq_Ropp = lazy (constant "Ropp") +let coq_Rminus = lazy (constant "Rminus") +let coq_Rdiv = lazy (constant "Rdiv") +let coq_powerRZ = lazy (constant "powerRZ") + +(* not Prop typed expressions *) +exception NotProp + +(* not first-order expressions *) +exception NotFO + +(* Renaming of Coq globals *) + +let global_names = Hashtbl.create 97 +let used_names = Hashtbl.create 97 + +let rename_global r = + try + Hashtbl.find global_names r + with Not_found -> + let rec loop id = + if Hashtbl.mem used_names id then + loop (lift_subscript id) + else begin + Hashtbl.add used_names id (); + let s = string_of_id id in + Hashtbl.add global_names r s; + s + end + in + loop (Nametab.basename_of_global r) + +let foralls = + List.fold_right + (fun (x,t) p -> Forall (x, t, p)) + +let fresh_var = function + | Anonymous -> rename_global (VarRef (id_of_string "x")) + | Name x -> rename_global (VarRef x) + +(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of + env names, and returns the new variables together with the new + environment *) +let coq_rename_vars env vars = + let avoid = ref (ids_of_named_context (Environ.named_context env)) in + List.fold_right + (fun (na,t) (newvars, newenv) -> + let id = next_name_away na !avoid in + avoid := id :: !avoid; + id :: newvars, Environ.push_named (id, None, t) newenv) + vars ([],env) + +(* extract the prenex type quantifications i.e. + type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *) +let decomp_type_quantifiers env t = + let rec loop vars t = match kind_of_term t with + | Prod (n, a, t) when is_Set a || is_Type a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +(* same thing with lambda binders (for axiomatize body) *) +let decomp_type_lambdas env t = + let rec loop vars t = match kind_of_term t with + | Lambda (n, a, t) when is_Set a || is_Type a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +let decompose_arrows = + let rec arrows_rec l c = match kind_of_term c with + | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c + | Cast (c,_,_) -> arrows_rec l c + | _ -> List.rev l, c + in + arrows_rec [] + +let rec eta_expanse t vars env i = + assert (i >= 0); + if i = 0 then + t, vars, env + else + match kind_of_term (Typing.type_of env Evd.empty t) with + | Prod (n, a, b) when not (dependent (mkRel 1) b) -> + let avoid = ids_of_named_context (Environ.named_context env) in + let id = next_name_away n avoid in + let env' = Environ.push_named (id, None, a) env in + let t' = mkApp (t, [| mkVar id |]) in + eta_expanse t' (id :: vars) env' (pred i) + | _ -> + assert false + +let rec skip_k_args k cl = match k, cl with + | 0, _ -> cl + | _, _ :: cl -> skip_k_args (k-1) cl + | _, [] -> raise NotFO + +(* Coq global references *) + +type global = Gnot_fo | Gfo of Fol.decl + +let globals = ref Refmap.empty +let globals_stack = ref [] + +(* synchronization *) +let () = + Summary.declare_summary "Dp globals" + { Summary.freeze_function = (fun () -> !globals, !globals_stack); + Summary.unfreeze_function = + (fun (g,s) -> globals := g; globals_stack := s); + Summary.init_function = (fun () -> ()) } + +let add_global r d = globals := Refmap.add r d !globals +let mem_global r = Refmap.mem r !globals +let lookup_global r = match Refmap.find r !globals with + | Gnot_fo -> raise NotFO + | Gfo d -> d + +let locals = Hashtbl.create 97 + +let lookup_local r = match Hashtbl.find locals r with + | Gnot_fo -> raise NotFO + | Gfo d -> d + +let iter_all_constructors i f = + let _, oib = Global.lookup_inductive i in + Array.iteri + (fun j tj -> f j (mkConstruct (i, j+1))) + oib.mind_nf_lc + + +(* injection c [t1,...,tn] adds the injection axiom + forall x1:t1,...,xn:tn,y1:t1,...,yn:tn. + c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *) + +let injection c l = + let i = ref 0 in + let var s = incr i; id_of_string (s ^ string_of_int !i) in + let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in + i := 0; + let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in + let f = + List.fold_right2 + (fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p)) + xl yl True + in + let vars = List.map (fun (x,_) -> App(x,[])) in + let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in + let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in + let f = foralls xl (foralls yl f) in + let ax = Axiom ("injection_" ^ c, f) in + globals_stack := ax :: !globals_stack + +(* rec_names_for c [|n1;...;nk|] builds the list of constant names for + identifiers n1...nk with the same path as c, if they exist; otherwise + raises Not_found *) +let rec_names_for c = + let mp,dp,_ = Names.repr_con c in + array_map_to_list + (function + | Name id -> + let c' = Names.make_con mp dp (label_of_id id) in + ignore (Global.lookup_constant c'); + msgnl (Printer.pr_constr (mkConst c')); + c' + | Anonymous -> + raise Not_found) + +(* abstraction tables *) + +let term_abstractions = Hashtbl.create 97 + +let new_abstraction = + let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r + +(* Arithmetic constants *) + +exception NotArithConstant + +(* translates a closed Coq term p:positive into a FOL term of type int *) + +let big_two = Big_int.succ_big_int Big_int.unit_big_int + +let rec tr_positive p = match kind_of_term p with + | Term.Construct _ when p = Lazy.force coq_xH -> + Big_int.unit_big_int + | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> +(* + Plus (Mult (Cst 2, tr_positive a), Cst 1) +*) + Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a)) + | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> +(* + Mult (Cst 2, tr_positive a) +*) + Big_int.mult_big_int big_two (tr_positive a) + | Term.Cast (p, _, _) -> + tr_positive p + | _ -> + raise NotArithConstant + +(* translates a closed Coq term t:Z or R into a FOL term of type int or real *) +let rec tr_arith_constant t = match kind_of_term t with + | Term.Construct _ when t = Lazy.force coq_Z0 -> + Cst Big_int.zero_big_int + | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> + Cst (tr_positive a) + | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> + Cst (Big_int.minus_big_int (tr_positive a)) + | Term.Const _ when t = Lazy.force coq_R0 -> + RCst Big_int.zero_big_int + | Term.Const _ when t = Lazy.force coq_R1 -> + RCst Big_int.unit_big_int + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> + let ta = tr_arith_constant a in + let tb = tr_arith_constant b in + begin match ta,tb with + | RCst na, RCst nb -> RCst (Big_int.add_big_int na nb) + | _ -> raise NotArithConstant + end + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> + let ta = tr_arith_constant a in + let tb = tr_arith_constant b in + begin match ta,tb with + | RCst na, RCst nb -> RCst (Big_int.mult_big_int na nb) + | _ -> raise NotArithConstant + end + | Term.App (f, [|a;b|]) when f = Lazy.force coq_powerRZ -> + tr_powerRZ a b + | Term.Cast (t, _, _) -> + tr_arith_constant t + | _ -> + raise NotArithConstant + +(* translates a constant of the form (powerRZ 2 int_constant) *) +and tr_powerRZ a b = + (* checking first that a is (R1 + R1) *) + match kind_of_term a with + | Term.App (f, [|c;d|]) when f = Lazy.force coq_Rplus -> + begin + match kind_of_term c,kind_of_term d with + | Term.Const _, Term.Const _ + when c = Lazy.force coq_R1 && d = Lazy.force coq_R1 -> + begin + match tr_arith_constant b with + | Cst n -> Power2 n + | _ -> raise NotArithConstant + end + | _ -> raise NotArithConstant + end + | _ -> raise NotArithConstant + + +(* translate a Coq term t:Set into a FOL type expression; + tv = list of type variables *) +and tr_type tv env t = + let t = Reductionops.nf_betadeltaiota env Evd.empty t in + if t = Lazy.force coq_Z then + Tid ("int", []) + else if t = Lazy.force coq_R then + Tid ("real", []) + else match kind_of_term t with + | Var x when List.mem x tv -> + Tvar (string_of_id x) + | _ -> + let f, cl = decompose_app t in + begin try + let r = global_of_constr f in + match tr_global env r with + | DeclType (id, k) -> + assert (k = List.length cl); (* since t:Set *) + Tid (id, List.map (tr_type tv env) cl) + | _ -> + raise NotFO + with + | Not_found -> + raise NotFO + | NotFO -> + (* we need to abstract some part of (f cl) *) + (*TODO*) + raise NotFO + end + +and make_term_abstraction tv env c = + let ty = Typing.type_of env Evd.empty c in + let id = new_abstraction () in + match tr_decl env id ty with + | DeclFun (id,_,_,_) as _d -> + raise NotFO + (* [CM 07/09/2009] deactivated because it generates + unbound identifiers 'abstraction_<number>' + begin try + Hashtbl.find term_abstractions c + with Not_found -> + Hashtbl.add term_abstractions c id; + globals_stack := d :: !globals_stack; + id + end + *) + | _ -> + raise NotFO + +(* translate a Coq declaration id:ty in a FOL declaration, that is either + - a type declaration : DeclType (id, n) where n:int is the type arity + - a function declaration : DeclFun (id, tl, t) ; that includes constants + - a predicate declaration : DeclPred (id, tl) + - an axiom : Axiom (id, p) + *) +and tr_decl env id ty = + let tv, env, t = decomp_type_quantifiers env ty in + if is_Set t || is_Type t then + DeclType (id, List.length tv) + else if is_Prop t then + DeclPred (id, List.length tv, []) + else + let s = Typing.type_of env Evd.empty t in + if is_Prop s then + Axiom (id, tr_formula tv [] env t) + else + let l, t = decompose_arrows t in + let l = List.map (tr_type tv env) l in + if is_Prop t then + DeclPred(id, List.length tv, l) + else + let s = Typing.type_of env Evd.empty t in + if is_Set s || is_Type s then + DeclFun (id, List.length tv, l, tr_type tv env t) + else + raise NotFO + +(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *) +and tr_global env r = match r with + | VarRef id -> + lookup_local id + | r -> + try + lookup_global r + with Not_found -> + try + let ty = Global.type_of_global r in + let id = rename_global r in + let d = tr_decl env id ty in + (* r can be already declared if it is a constructor *) + if not (mem_global r) then begin + add_global r (Gfo d); + globals_stack := d :: !globals_stack + end; + begin try axiomatize_body env r id d with NotFO -> () end; + d + with NotFO -> + add_global r Gnot_fo; + raise NotFO + +and axiomatize_body env r id d = match r with + | VarRef _ -> + assert false + | ConstRef c -> + begin match (Global.lookup_constant c).const_body with + | Some b -> + let b = force b in + let axioms = + (match d with + | DeclPred (id, _, []) -> + let tv, env, b = decomp_type_lambdas env b in + let value = tr_formula tv [] env b in + [id, Iff (Fatom (Pred (id, [])), value)] + | DeclFun (id, _, [], _) -> + let tv, env, b = decomp_type_lambdas env b in + let value = tr_term tv [] env b in + [id, Fatom (Eq (Fol.App (id, []), value))] + | DeclFun (id, _, l, _) | DeclPred (id, _, l) -> + (*Format.eprintf "axiomatize_body %S@." id;*) + let b = match kind_of_term b with + (* a single recursive function *) + | Fix (_, (_,_,[|b|])) -> + subst1 (mkConst c) b + (* mutually recursive functions *) + | Fix ((_,i), (names,_,bodies)) -> + (* we only deal with named functions *) + begin try + let l = rec_names_for c names in + substl (List.rev_map mkConst l) bodies.(i) + with Not_found -> + b + end + | _ -> + b + in + let tv, env, b = decomp_type_lambdas env b in + let vars, t = decompose_lam b in + let n = List.length l in + let k = List.length vars in + assert (k <= n); + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + let t, vars, env = eta_expanse t vars env (n-k) in + let vars = List.rev vars in + let bv = vars in + let vars = List.map (fun x -> string_of_id x) vars in + let fol_var x = Fol.App (x, []) in + let fol_vars = List.map fol_var vars in + let vars = List.combine vars l in + begin match d with + | DeclFun (_, _, _, ty) -> + begin match kind_of_term t with + | Case (ci, _, e, br) -> + equations_for_case env id vars tv bv ci e br + | _ -> + let t = tr_term tv bv env t in + let ax = + add_proof (Fun_def (id, vars, ty, t)) + in + let p = Fatom (Eq (App (id, fol_vars), t)) in + [ax, foralls vars p] + end + | DeclPred _ -> + let value = tr_formula tv bv env t in + let p = Iff (Fatom (Pred (id, fol_vars)), value) in + [id, foralls vars p] + | _ -> + assert false + end + | DeclType _ -> + raise NotFO + | Axiom _ -> assert false) + in + let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in + globals_stack := axioms @ !globals_stack + | None -> + () (* Coq axiom *) + end + | IndRef i -> + iter_all_constructors i + (fun _ c -> + let rc = global_of_constr c in + try + begin match tr_global env rc with + | DeclFun (_, _, [], _) -> () + | DeclFun (idc, _, al, _) -> injection idc al + | _ -> () + end + with NotFO -> + ()) + | _ -> () + +and equations_for_case env id vars tv bv ci e br = match kind_of_term e with + | Var x when List.exists (fun (y, _) -> string_of_id x = y) vars -> + let eqs = ref [] in + iter_all_constructors ci.ci_ind + (fun j cj -> + try + let cjr = global_of_constr cj in + begin match tr_global env cjr with + | DeclFun (idc, _, l, _) -> + let b = br.(j) in + let rec_vars, b = decompose_lam b in + let rec_vars, env = coq_rename_vars env rec_vars in + let coq_rec_vars = List.map mkVar rec_vars in + let b = substl coq_rec_vars b in + let rec_vars = List.rev rec_vars in + let coq_rec_term = applist (cj, List.rev coq_rec_vars) in + let b = replace_vars [x, coq_rec_term] b in + let bv = bv @ rec_vars in + let rec_vars = List.map string_of_id rec_vars in + let fol_var x = Fol.App (x, []) in + let fol_rec_vars = List.map fol_var rec_vars in + let fol_rec_term = App (idc, fol_rec_vars) in + let rec_vars = List.combine rec_vars l in + let fol_vars = List.map fst vars in + let fol_vars = List.map fol_var fol_vars in + let fol_vars = List.map (fun y -> match y with + | App (id, _) -> + if id = string_of_id x + then fol_rec_term + else y + | _ -> y) + fol_vars in + let vars = vars @ rec_vars in + let rec remove l e = match l with + | [] -> [] + | (y, t)::l' -> if y = string_of_id e then l' + else (y, t)::(remove l' e) in + let vars = remove vars x in + let p = + Fatom (Eq (App (id, fol_vars), + tr_term tv bv env b)) + in + eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs + | _ -> + assert false end + with NotFO -> + ()); + !eqs + | _ -> + raise NotFO + +(* assumption: t:T:Set *) +and tr_term tv bv env t = + try + tr_arith_constant t + with NotArithConstant -> + match kind_of_term t with + (* binary operations on integers *) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> + Plus (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> + Moins (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> + Mult (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> + Div (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a|]) when f = Lazy.force coq_Zopp -> + Opp (tr_term tv bv env a) + (* binary operations on reals *) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> + Plus (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rminus -> + Moins (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> + Mult (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rdiv -> + Div (tr_term tv bv env a, tr_term tv bv env b) + | Term.Var id when List.mem id bv -> + App (string_of_id id, []) + | _ -> + let f, cl = decompose_app t in + begin try + let r = global_of_constr f in + match tr_global env r with + | DeclFun (s, k, _, _) -> + let cl = skip_k_args k cl in + Fol.App (s, List.map (tr_term tv bv env) cl) + | _ -> + raise NotFO + with + | Not_found -> + raise NotFO + | NotFO -> (* we need to abstract some part of (f cl) *) + let rec abstract app = function + | [] -> + Fol.App (make_term_abstraction tv env app, []) + | x :: l as args -> + begin try + let s = make_term_abstraction tv env app in + Fol.App (s, List.map (tr_term tv bv env) args) + with NotFO -> + abstract (applist (app, [x])) l + end + in + let app,l = match cl with + | x :: l -> applist (f, [x]), l | [] -> raise NotFO + in + abstract app l + end + +and quantifiers n a b tv bv env = + let vars, env = coq_rename_vars env [n,a] in + let id = match vars with [x] -> x | _ -> assert false in + let b = subst1 (mkVar id) b in + let t = tr_type tv env a in + let bv = id :: bv in + id, t, bv, env, b + +(* assumption: f is of type Prop *) +and tr_formula tv bv env f = + let c, args = decompose_app f in + match kind_of_term c, args with + | Var id, [] -> + Fatom (Pred (rename_global (VarRef id), [])) + | _, [t;a;b] when c = build_coq_eq () -> + let ty = Typing.type_of env Evd.empty t in + if is_Set ty || is_Type ty then + let _ = tr_type tv env t in + Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b)) + else + raise NotFO + (* comparisons on integers *) + | _, [a;b] when c = Lazy.force coq_Zle -> + Fatom (Le (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zlt -> + Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zge -> + Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zgt -> + Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b)) + (* comparisons on reals *) + | _, [a;b] when c = Lazy.force coq_Rle -> + Fatom (Le (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Rlt -> + Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Rge -> + Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Rgt -> + Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b)) + | _, [] when c = build_coq_False () -> + False + | _, [] when c = build_coq_True () -> + True + | _, [a] when c = build_coq_not () -> + Not (tr_formula tv bv env a) + | _, [a;b] when c = build_coq_and () -> + And (tr_formula tv bv env a, tr_formula tv bv env b) + | _, [a;b] when c = build_coq_or () -> + Or (tr_formula tv bv env a, tr_formula tv bv env b) + | _, [a;b] when c = Lazy.force coq_iff -> + Iff (tr_formula tv bv env a, tr_formula tv bv env b) + | Prod (n, a, b), _ -> + if is_imp_term f then + Imp (tr_formula tv bv env a, tr_formula tv bv env b) + else + let id, t, bv, env, b = quantifiers n a b tv bv env in + Forall (string_of_id id, t, tr_formula tv bv env b) + | _, [_; a] when c = build_coq_ex () -> + begin match kind_of_term a with + | Lambda(n, a, b) -> + let id, t, bv, env, b = quantifiers n a b tv bv env in + Exists (string_of_id id, t, tr_formula tv bv env b) + | _ -> + (* unusual case of the shape (ex p) *) + raise NotFO (* TODO: we could eta-expanse *) + end + | _ -> + begin try + let r = global_of_constr c in + match tr_global env r with + | DeclPred (s, k, _) -> + let args = skip_k_args k args in + Fatom (Pred (s, List.map (tr_term tv bv env) args)) + | _ -> + raise NotFO + with Not_found -> + raise NotFO + end + + +let tr_goal gl = + Hashtbl.clear locals; + let tr_one_hyp (id, ty) = + try + let s = rename_global (VarRef id) in + let d = tr_decl (pf_env gl) s ty in + Hashtbl.add locals id (Gfo d); + d + with NotFO -> + Hashtbl.add locals id Gnot_fo; + raise NotFO + in + let hyps = + List.fold_right + (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc) + (pf_hyps_types gl) [] + in + let c = tr_formula [] [] (pf_env gl) (pf_concl gl) in + let hyps = List.rev_append !globals_stack (List.rev hyps) in + hyps, c + + +type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy | CVC3 | Z3 + +let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ()) + +let sprintf = Format.sprintf + +let file_contents f = + let buf = Buffer.create 1024 in + try + let c = open_in f in + begin try + while true do + let s = input_line c in Buffer.add_string buf s; + Buffer.add_char buf '\n' + done; + assert false + with End_of_file -> + close_in c; + Buffer.contents buf + end + with _ -> + sprintf "(cannot open %s)" f + +let timeout_sys_command cmd = + if !debug then Format.eprintf "command line: %s@." cmd; + let out = Filename.temp_file "out" "" in + let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in + let ret = Sys.command cmd in + if !debug then + Format.eprintf "Output file %s:@.%s@." out (file_contents out); + ret, out + +let timeout_or_failure c cmd out = + if c = 152 then + Timeout + else + Failure + (sprintf "command %s failed with output:\n%s " cmd (file_contents out)) + +let call_prover ?(opt="") file = + if !debug then Format.eprintf "calling prover on %s@." file; + let out = Filename.temp_file "out" "" in + let cmd = + sprintf "why-dp -timeout %d -batch %s > %s 2>&1" !timeout file out in + match Sys.command cmd with + 0 -> Valid None + | 1 -> Failure (sprintf "could not run why-dp\n%s" (file_contents out)) + | 2 -> Invalid + | 3 -> DontKnow + | 4 -> Timeout + | 5 -> Failure (sprintf "prover failed:\n%s" (file_contents out)) + | n -> Failure (sprintf "Unknown exit status of why-dp: %d" n) + +let prelude_files = ref ([] : string list) + +let set_prelude l = prelude_files := l + +let (dp_prelude_obj,_) = + declare_object + {(default_object "Dp_prelude") with + cache_function = (fun (_,x) -> set_prelude x); + load_function = (fun _ (_,x) -> set_prelude x)} + +let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x) + +let why_files f = String.concat " " (!prelude_files @ [f]) + +let call_simplify fwhy = + let cmd = + sprintf "why --simplify %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in +(* + let cmd = + sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out" + !timeout fsx + in + let out = Sys.command cmd in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in +*) + let r = call_prover fsx in + if not !debug then remove_files [fwhy; fsx]; + r + +let call_ergo fwhy = + let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in + (*let ftrace = Filename.temp_file "ergo_trace" "" in*) + (*NB: why-dp can't handle -cctrace + let cmd = + if !trace then + sprintf "alt-ergo -cctrace %s %s" ftrace fwhy + + else + sprintf "alt-ergo %s" fwhy + in*) + let r = call_prover fwhy in + if not !debug then remove_files [fwhy; (*out*)]; + r + + +let call_zenon fwhy = + let cmd = + sprintf "why --no-zenon-prelude --zenon %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in +(* why-dp won't let us having coqterm... + let out = Filename.temp_file "dp_out" "" in + let cmd = + sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out + in + let c = Sys.command cmd in + if not !debug then remove_files [fwhy; fznn]; + if c = 137 then + Timeout + else begin + if c <> 0 then anomaly ("command failed: " ^ cmd); + if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then + error "Zenon failed"; + let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in + if c = 0 then Valid (Some out) else Invalid + end + *) + let r = call_prover fznn in + if not !debug then remove_files [fwhy; fznn]; + r + +let call_smt ~smt fwhy = + let cmd = + sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in + let opt = "-smt-solver " ^ smt in + let r = call_prover ~opt fsmt in + if not !debug then remove_files [fwhy; fsmt]; + r + +(* +let call_yices fwhy = + let cmd = + sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in + let cmd = + sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out" + !timeout fsmt + in + let out = Sys.command cmd in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in + if not !debug then remove_files [fwhy; fsmt]; + r + +let call_cvc3 fwhy = + let cmd = + sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in + let cmd = + sprintf "why-cpulimit %d cvc3 -lang smt %s > out 2>&1 && grep -q -w unsat out" + !timeout fsmt + in + let out = Sys.command cmd in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in + if not !debug then remove_files [fwhy; fsmt]; + r +*) + +let call_cvcl fwhy = + let cmd = + sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in +(* + let cmd = + sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out" + !timeout fcvc + in + let out = Sys.command cmd in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in +*) + let r = call_prover fcvc in + if not !debug then remove_files [fwhy; fcvc]; + r + +let call_harvey fwhy = + let cmd = + sprintf "why --harvey --encoding strat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in +(* + let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in + if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed"); + let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in + let outf = Filename.temp_file "rv" ".out" in + let out = + Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1" + !timeout f outf) + in + let r = + if out <> 0 then + Timeout + else + let cmd = + sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf + in + if Sys.command cmd = 0 then Valid None else Invalid + in + if not !debug then remove_files [fwhy; frv; outf]; +*) + let r = call_prover frv in + if not !debug then remove_files [fwhy; frv]; + r + +let call_gwhy fwhy = + let cmd = sprintf "gwhy %s" (why_files fwhy) in + if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy)); + NoAnswer + +let ergo_proof_from_file f gl = + let s = + let buf = Buffer.create 1024 in + let c = open_in f in + try + while true do Buffer.add_string buf (input_line c) done; assert false + with End_of_file -> + close_in c; + Buffer.contents buf + in + let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in + let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in + exact_check t gl + +let call_prover prover q = + let fwhy = Filename.temp_file "coq_dp" ".why" in + Dp_why.output_file fwhy q; + match prover with + | Simplify -> call_simplify fwhy + | Ergo -> call_ergo fwhy + | CVC3 -> call_smt ~smt:"cvc3" fwhy + | Yices -> call_smt ~smt:"yices" fwhy + | Z3 -> call_smt ~smt:"z3" fwhy + | Zenon -> call_zenon fwhy + | CVCLite -> call_cvcl fwhy + | Harvey -> call_harvey fwhy + | Gwhy -> call_gwhy fwhy + +let dp prover gl = + Coqlib.check_required_library ["Coq";"ZArith";"ZArith"]; + let concl_type = pf_type_of gl (pf_concl gl) in + if not (is_Prop concl_type) then error "Conclusion is not a Prop"; + try + let q = tr_goal gl in + begin match call_prover prover q with + | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl + | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl + | Valid _ -> Tactics.admit_as_an_axiom gl + | Invalid -> error "Invalid" + | DontKnow -> error "Don't know" + | Timeout -> error "Timeout" + | Failure s -> error s + | NoAnswer -> Tacticals.tclIDTAC gl + end + with NotFO -> + error "Not a first order goal" + + +let simplify = tclTHEN intros (dp Simplify) +let ergo = tclTHEN intros (dp Ergo) +let cvc3 = tclTHEN intros (dp CVC3) +let yices = tclTHEN intros (dp Yices) +let z3 = tclTHEN intros (dp Z3) +let cvc_lite = tclTHEN intros (dp CVCLite) +let harvey = dp Harvey +let zenon = tclTHEN intros (dp Zenon) +let gwhy = tclTHEN intros (dp Gwhy) + +let dp_hint l = + let env = Global.env () in + let one_hint (qid,r) = + if not (mem_global r) then begin + let ty = Global.type_of_global r in + let s = Typing.type_of env Evd.empty ty in + if is_Prop s then + try + let id = rename_global r in + let tv, env, ty = decomp_type_quantifiers env ty in + let d = Axiom (id, tr_formula tv [] env ty) in + add_global r (Gfo d); + globals_stack := d :: !globals_stack + with NotFO -> + add_global r Gnot_fo; + msg_warning + (pr_reference qid ++ + str " ignored (not a first order proposition)") + else begin + add_global r Gnot_fo; + msg_warning + (pr_reference qid ++ str " ignored (not a proposition)") + end + end + in + List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l) + +let (dp_hint_obj,_) = + declare_object + {(default_object "Dp_hint") with + cache_function = (fun (_,l) -> dp_hint l); + load_function = (fun _ (_,l) -> dp_hint l)} + +let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l) + +let dp_predefined qid s = + let r = Nametab.global qid in + let ty = Global.type_of_global r in + let env = Global.env () in + let id = rename_global r in + try + let d = match tr_decl env id ty with + | DeclType (_, n) -> DeclType (s, n) + | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty) + | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl) + | Axiom _ as d -> d + in + match d with + | Axiom _ -> msg_warning (str " ignored (axiom)") + | d -> add_global r (Gfo d) + with NotFO -> + msg_warning (str " ignored (not a first order declaration)") + +let (dp_predefined_obj,_) = + declare_object + {(default_object "Dp_predefined") with + cache_function = (fun (_,(id,s)) -> dp_predefined id s); + load_function = (fun _ (_,(id,s)) -> dp_predefined id s)} + +let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s)) + +let _ = declare_summary "Dp options" + { freeze_function = + (fun () -> !debug, !trace, !timeout, !prelude_files); + unfreeze_function = + (fun (d,tr,tm,pr) -> + debug := d; trace := tr; timeout := tm; prelude_files := pr); + init_function = + (fun () -> + debug := false; trace := false; timeout := 10; + prelude_files := []) } diff --git a/plugins/dp/dp.mli b/plugins/dp/dp.mli new file mode 100644 index 00000000..f40f8688 --- /dev/null +++ b/plugins/dp/dp.mli @@ -0,0 +1,20 @@ + +open Libnames +open Proof_type + +val simplify : tactic +val ergo : tactic +val cvc3 : tactic +val yices : tactic +val cvc_lite : tactic +val harvey : tactic +val zenon : tactic +val gwhy : tactic +val z3: tactic + +val dp_hint : reference list -> unit +val dp_timeout : int -> unit +val dp_debug : bool -> unit +val dp_trace : bool -> unit +val dp_prelude : string list -> unit +val dp_predefined : reference -> string -> unit diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib new file mode 100644 index 00000000..63252d6a --- /dev/null +++ b/plugins/dp/dp_plugin.mllib @@ -0,0 +1,5 @@ +Dp_why +Dp_zenon +Dp +G_dp +Dp_plugin_mod diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml new file mode 100644 index 00000000..9a62f39d --- /dev/null +++ b/plugins/dp/dp_why.ml @@ -0,0 +1,186 @@ + +(* Pretty-print PFOL (see fol.mli) in Why syntax *) + +open Format +open Fol + +type proof = + | Immediate of Term.constr + | Fun_def of string * (string * typ) list * typ * term + +let proofs = Hashtbl.create 97 +let proof_name = + let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r + +let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n + +let find_proof = Hashtbl.find proofs + +let rec print_list sep print fmt = function + | [] -> () + | [x] -> print fmt x + | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r + +let space fmt () = fprintf fmt "@ " +let comma fmt () = fprintf fmt ",@ " + +let is_why_keyword = + let h = Hashtbl.create 17 in + List.iter + (fun s -> Hashtbl.add h s ()) + ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin"; + "bool"; "do"; "done"; "else"; "end"; "exception"; "exists"; + "external"; "false"; "for"; "forall"; "fun"; "function"; "goal"; + "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not"; + "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises"; + "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try"; + "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; + Hashtbl.mem h + +let ident fmt s = + if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s + +let rec print_typ fmt = function + | Tvar x -> fprintf fmt "'%a" ident x + | Tid ("int", []) -> fprintf fmt "int" + | Tid ("real", []) -> fprintf fmt "real" + | Tid (x, []) -> fprintf fmt "%a" ident x + | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x + | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x + +let print_arg fmt (id,typ) = fprintf fmt "%a: %a" ident id print_typ typ + +let rec print_term fmt = function + | Cst n -> + fprintf fmt "%s" (Big_int.string_of_big_int n) + | RCst s -> + fprintf fmt "%s.0" (Big_int.string_of_big_int s) + | Power2 n -> + fprintf fmt "0x1p%s" (Big_int.string_of_big_int n) + | Plus (a, b) -> + fprintf fmt "@[(%a +@ %a)@]" print_term a print_term b + | Moins (a, b) -> + fprintf fmt "@[(%a -@ %a)@]" print_term a print_term b + | Mult (a, b) -> + fprintf fmt "@[(%a *@ %a)@]" print_term a print_term b + | Div (a, b) -> + fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b + | Opp (a) -> + fprintf fmt "@[(-@ %a)@]" print_term a + | App (id, []) -> + fprintf fmt "%a" ident id + | App (id, tl) -> + fprintf fmt "@[%a(%a)@]" ident id print_terms tl + +and print_terms fmt tl = + print_list comma print_term fmt tl + +let rec print_predicate fmt p = + let pp = print_predicate in + match p with + | True -> + fprintf fmt "true" + | False -> + fprintf fmt "false" + | Fatom (Eq (a, b)) -> + fprintf fmt "@[(%a =@ %a)@]" print_term a print_term b + | Fatom (Le (a, b)) -> + fprintf fmt "@[(%a <=@ %a)@]" print_term a print_term b + | Fatom (Lt (a, b))-> + fprintf fmt "@[(%a <@ %a)@]" print_term a print_term b + | Fatom (Ge (a, b)) -> + fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b + | Fatom (Gt (a, b)) -> + fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b + | Fatom (Pred (id, [])) -> + fprintf fmt "%a" ident id + | Fatom (Pred (id, tl)) -> + fprintf fmt "@[%a(%a)@]" ident id print_terms tl + | Imp (a, b) -> + fprintf fmt "@[(%a ->@ %a)@]" pp a pp b + | Iff (a, b) -> + fprintf fmt "@[(%a <->@ %a)@]" pp a pp b + | And (a, b) -> + fprintf fmt "@[(%a and@ %a)@]" pp a pp b + | Or (a, b) -> + fprintf fmt "@[(%a or@ %a)@]" pp a pp b + | Not a -> + fprintf fmt "@[(not@ %a)@]" pp a + | Forall (id, t, p) -> + fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p + | Exists (id, t, p) -> + fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p + +let rec remove_iff args = function + Forall (id,t,p) -> remove_iff ((id,t)::args) p + | Iff(_,b) -> List.rev args, b + | _ -> raise Not_found + +let print_query fmt (decls,concl) = + let find_declared_preds l = + function + DeclPred (id,_,args) -> (id,args) :: l + | _ -> l + in + let find_defined_preds declared l = function + Axiom(id,f) -> + (try + let _decl = List.assoc id declared in + (id,remove_iff [] f)::l + with Not_found -> l) + | _ -> l + in + let declared_preds = + List.fold_left find_declared_preds [] decls in + let defined_preds = + List.fold_left (find_defined_preds declared_preds) [] decls + in + let print_dtype = function + | DeclType (id, 0) -> + fprintf fmt "@[type %a@]@\n@\n" ident id + | DeclType (id, 1) -> + fprintf fmt "@[type 'a %a@]@\n@\n" ident id + | DeclType (id, n) -> + fprintf fmt "@[type ("; + for i = 1 to n do + fprintf fmt "'a%d" i; if i < n then fprintf fmt ", " + done; + fprintf fmt ") %a@]@\n@\n" ident id + | DeclFun _ | DeclPred _ | Axiom _ -> + () + in + let print_dvar_dpred = function + | DeclFun (id, _, [], t) -> + fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t + | DeclFun (id, _, l, t) -> + fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" + ident id (print_list comma print_typ) l print_typ t + | DeclPred (id, _, []) when not (List.mem_assoc id defined_preds) -> + fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id + | DeclPred (id, _, l) when not (List.mem_assoc id defined_preds) -> + fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" + ident id (print_list comma print_typ) l + | DeclType _ | Axiom _ | DeclPred _ -> + () + in + let print_assert = function + | Axiom(id,_) when List.mem_assoc id defined_preds -> + let args, def = List.assoc id defined_preds in + fprintf fmt "@[predicate %a(%a) =@\n%a@]@\n" ident id + (print_list comma print_arg) args print_predicate def + | Axiom (id, f) -> + fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f + | DeclType _ | DeclFun _ | DeclPred _ -> + () + in + List.iter print_dtype decls; + List.iter print_dvar_dpred decls; + List.iter print_assert decls; + fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl + +let output_file f q = + let c = open_out f in + let fmt = formatter_of_out_channel c in + fprintf fmt "include \"real.why\"@."; + fprintf fmt "@[%a@]@." print_query q; + close_out c diff --git a/plugins/dp/dp_why.mli b/plugins/dp/dp_why.mli new file mode 100644 index 00000000..0efa24a2 --- /dev/null +++ b/plugins/dp/dp_why.mli @@ -0,0 +1,17 @@ + +open Fol + +(* generation of the Why file *) + +val output_file : string -> query -> unit + +(* table to translate the proofs back to Coq (used in dp_zenon) *) + +type proof = + | Immediate of Term.constr + | Fun_def of string * (string * typ) list * typ * term + +val add_proof : proof -> string +val find_proof : string -> proof + + diff --git a/plugins/dp/dp_zenon.mli b/plugins/dp/dp_zenon.mli new file mode 100644 index 00000000..0a727d1f --- /dev/null +++ b/plugins/dp/dp_zenon.mli @@ -0,0 +1,7 @@ + +open Fol + +val set_debug : bool -> unit + +val proof_from_file : string -> Proof_type.tactic + diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll new file mode 100644 index 00000000..949e91e3 --- /dev/null +++ b/plugins/dp/dp_zenon.mll @@ -0,0 +1,189 @@ + +{ + + open Lexing + open Pp + open Util + open Names + open Tacmach + open Dp_why + open Tactics + open Tacticals + + let debug = ref false + let set_debug b = debug := b + + let buf = Buffer.create 1024 + + let string_of_global env ref = + Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref) + + let axioms = ref [] + + (* we cannot interpret the terms as we read them (since some lemmas + may need other lemmas to be already interpreted) *) + type lemma = { l_id : string; l_type : string; l_proof : string } + type zenon_proof = lemma list * string + +} + +let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+ +let space = [' ' '\t' '\r'] + +rule start = parse +| "(* BEGIN-PROOF *)" "\n" { scan lexbuf } +| _ { start lexbuf } +| eof { anomaly "malformed Zenon proof term" } + +(* here we read the lemmas and the main proof term; + meanwhile we maintain the set of axioms that were used *) + +and scan = parse +| "Let" space (ident as id) space* ":" + { let t = read_coq_term lexbuf in + let p = read_lemma_proof lexbuf in + let l,pr = scan lexbuf in + { l_id = id; l_type = t; l_proof = p } :: l, pr } +| "Definition theorem:" + { let t = read_main_proof lexbuf in [], t } +| _ | eof + { anomaly "malformed Zenon proof term" } + +and read_coq_term = parse +| "." "\n" + { let s = Buffer.contents buf in Buffer.clear buf; s } +| "coq__" (ident as id) (* a Why keyword renamed *) + { Buffer.add_string buf id; read_coq_term lexbuf } +| ("dp_axiom__" ['0'-'9']+) as id + { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf } +| _ as c + { Buffer.add_char buf c; read_coq_term lexbuf } +| eof + { anomaly "malformed Zenon proof term" } + +and read_lemma_proof = parse +| "Proof" space + { read_coq_term lexbuf } +| _ | eof + { anomaly "malformed Zenon proof term" } + +(* skip the main proof statement and then read its term *) +and read_main_proof = parse +| ":=" "\n" + { read_coq_term lexbuf } +| _ + { read_main_proof lexbuf } +| eof + { anomaly "malformed Zenon proof term" } + + +{ + + let read_zenon_proof f = + Buffer.clear buf; + let c = open_in f in + let lb = from_channel c in + let p = start lb in + close_in c; + if not !debug then begin try Sys.remove f with _ -> () end; + p + + let constr_of_string gl s = + let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in + Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s) + + (* we are lazy here: we build strings containing Coq terms using a *) + (* pretty-printer Fol -> Coq *) + module Coq = struct + open Format + open Fol + + let rec print_list sep print fmt = function + | [] -> () + | [x] -> print fmt x + | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r + + let space fmt () = fprintf fmt "@ " + let comma fmt () = fprintf fmt ",@ " + + let rec print_typ fmt = function + | Tvar x -> fprintf fmt "%s" x + | Tid ("int", []) -> fprintf fmt "Z" + | Tid (x, []) -> fprintf fmt "%s" x + | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t + | Tid (x,tl) -> + fprintf fmt "(%s %a)" x (print_list comma print_typ) tl + + let rec print_term fmt = function + | Cst n -> + fprintf fmt "%s" (Big_int.string_of_big_int n) + | RCst s -> + fprintf fmt "%s" (Big_int.string_of_big_int s) + | Power2 n -> + fprintf fmt "@[(powerRZ 2 %s)@]" (Big_int.string_of_big_int n) + + (* TODO: bug, it might be operations on reals *) + | Plus (a, b) -> + fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b + | Moins (a, b) -> + fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b + | Mult (a, b) -> + fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b + | Div (a, b) -> + fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b + | Opp (a) -> + fprintf fmt "@[(Zopp %a)@]" print_term a + | App (id, []) -> + fprintf fmt "%s" id + | App (id, tl) -> + fprintf fmt "@[(%s %a)@]" id print_terms tl + + and print_terms fmt tl = + print_list space print_term fmt tl + + (* builds the text for "forall vars, f vars = t" *) + let fun_def_axiom f vars t = + let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in + fprintf str_formatter + "@[(forall %a, %s %a = %a)@]@." + (print_list space binder) vars f + (print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars + print_term t; + flush_str_formatter () + + end + + let prove_axiom id = match Dp_why.find_proof id with + | Immediate t -> + exact_check t + | Fun_def (f, vars, ty, t) -> + tclTHENS + (fun gl -> + let s = Coq.fun_def_axiom f vars t in + if !debug then Format.eprintf "axiom fun def = %s@." s; + let c = constr_of_string gl s in + assert_tac (Name (id_of_string id)) c gl) + [tclTHEN intros reflexivity; tclIDTAC] + + let exact_string s gl = + let c = constr_of_string gl s in + exact_check c gl + + let interp_zenon_proof (ll,p) = + let interp_lemma l gl = + let ty = constr_of_string gl l.l_type in + tclTHENS + (assert_tac (Name (id_of_string l.l_id)) ty) + [exact_string l.l_proof; tclIDTAC] + gl + in + tclTHEN (tclMAP interp_lemma ll) (exact_string p) + + let proof_from_file f = + axioms := []; + msgnl (str "proof_from_file " ++ str f); + let zp = read_zenon_proof f in + msgnl (str "proof term is " ++ str (snd zp)); + tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp) + +} diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli new file mode 100644 index 00000000..4fb763a6 --- /dev/null +++ b/plugins/dp/fol.mli @@ -0,0 +1,58 @@ + +(* Polymorphic First-Order Logic (that is Why's input logic) *) + +type typ = + | Tvar of string + | Tid of string * typ list + +type term = + | Cst of Big_int.big_int + | RCst of Big_int.big_int + | Power2 of Big_int.big_int + | Plus of term * term + | Moins of term * term + | Mult of term * term + | Div of term * term + | Opp of term + | App of string * term list + +and atom = + | Eq of term * term + | Le of term * term + | Lt of term * term + | Ge of term * term + | Gt of term * term + | Pred of string * term list + +and form = + | Fatom of atom + | Imp of form * form + | Iff of form * form + | And of form * form + | Or of form * form + | Not of form + | Forall of string * typ * form + | Exists of string * typ * form + | True + | False + +(* the integer indicates the number of type variables *) +type decl = + | DeclType of string * int + | DeclFun of string * int * typ list * typ + | DeclPred of string * int * typ list + | Axiom of string * form + +type query = decl list * form + + +(* prover result *) + +type prover_answer = + | Valid of string option + | Invalid + | DontKnow + | Timeout + | NoAnswer + | Failure of string + diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 new file mode 100644 index 00000000..82f86cd8 --- /dev/null +++ b/plugins/dp/g_dp.ml4 @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Dp + +TACTIC EXTEND Simplify + [ "simplify" ] -> [ simplify ] +END + +TACTIC EXTEND Ergo + [ "ergo" ] -> [ ergo ] +END + +TACTIC EXTEND Yices + [ "yices" ] -> [ yices ] +END + +TACTIC EXTEND CVC3 + [ "cvc3" ] -> [ cvc3 ] +END + +TACTIC EXTEND Z3 + [ "z3" ] -> [ z3 ] +END + +TACTIC EXTEND CVCLite + [ "cvcl" ] -> [ cvc_lite ] +END + +TACTIC EXTEND Harvey + [ "harvey" ] -> [ harvey ] +END + +TACTIC EXTEND Zenon + [ "zenon" ] -> [ zenon ] +END + +TACTIC EXTEND Gwhy + [ "gwhy" ] -> [ gwhy ] +END + +(* should be part of basic tactics syntax *) +TACTIC EXTEND admit + [ "admit" ] -> [ Tactics.admit_as_an_axiom ] +END + +VERNAC COMMAND EXTEND Dp_hint + [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ] +END + +VERNAC COMMAND EXTEND Dp_timeout +| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ] +END + +VERNAC COMMAND EXTEND Dp_prelude +| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ] +END + +VERNAC COMMAND EXTEND Dp_predefined +| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ] +END + +VERNAC COMMAND EXTEND Dp_debug +| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ] +END + +VERNAC COMMAND EXTEND Dp_trace +| [ "Dp_trace" ] -> [ dp_trace true ] +END + diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v new file mode 100644 index 00000000..0940b135 --- /dev/null +++ b/plugins/dp/test2.v @@ -0,0 +1,80 @@ +Require Import ZArith. +Require Import Classical. +Require Import List. + +Open Scope list_scope. +Open Scope Z_scope. + +Dp_debug. +Dp_timeout 3. +Require Export zenon. + +Definition neg (z:Z) : Z := match z with + | Z0 => Z0 + | Zpos p => Zneg p + | Zneg p => Zpos p + end. + +Goal forall z, neg (neg z) = z. + Admitted. + +Open Scope nat_scope. +Print plus. + +Goal forall x, x+0=x. + induction x; ergo. + (* simplify resoud le premier, pas le second *) + Admitted. + +Goal 1::2::3::nil = 1::2::(1+2)::nil. + zenon. + Admitted. + +Definition T := nat. +Parameter fct : T -> nat. +Goal fct O = O. + Admitted. + +Fixpoint even (n:nat) : Prop := + match n with + O => True + | S O => False + | S (S p) => even p + end. + +Goal even 4%nat. + try zenon. + Admitted. + +Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil. + +Definition head := +fun (A : Set) (l : list A) => +match l with +| nil => None (A:=A) +| x :: _ => Some x +end. + +Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1. + +Admitted. + +(* +BUG avec head prédéfini : manque eta-expansion sur A:Set + +Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1. + +Print value. +Print Some. + +zenon. +*) + +Inductive IN (A:Set) : A -> list A -> Prop := + | IN1 : forall x l, IN A x (x::l) + | IN2: forall x l, IN A x l -> forall y, IN A x (y::l). +Implicit Arguments IN [A]. + +Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l). + zenon. +Print In. diff --git a/plugins/dp/tests.v b/plugins/dp/tests.v new file mode 100644 index 00000000..dc85d2ee --- /dev/null +++ b/plugins/dp/tests.v @@ -0,0 +1,300 @@ + +Require Import ZArith. +Require Import Classical. +Require Export Reals. + + +(* real numbers *) + +Lemma real_expr: (0 <= 9 * 4)%R. +ergo. +Qed. + +Lemma powerRZ_translation: (powerRZ 2 15 < powerRZ 2 17)%R. +ergo. +Qed. + +Dp_debug. +Dp_timeout 3. + +(* module renamings *) + +Module M. + Parameter t : Set. +End M. + +Lemma test_module_0 : forall x:M.t, x=x. +ergo. +Qed. + +Module N := M. + +Lemma test_module_renaming_0 : forall x:N.t, x=x. +ergo. +Qed. + +Dp_predefined M.t => "int". + +Lemma test_module_renaming_1 : forall x:N.t, x=x. +ergo. +Qed. + +(* Coq lists *) + +Require Export List. + +Lemma test_pol_0 : forall l:list nat, l=l. +ergo. +Qed. + +Parameter nlist: list nat -> Prop. + +Lemma poly_1 : forall l, nlist l -> True. +intros. +simplify. +Qed. + +(* user lists *) + +Inductive list (A:Set) : Set := +| nil : list A +| cons: forall a:A, list A -> list A. + +Fixpoint app (A:Set) (l m:list A) {struct l} : list A := +match l with +| nil => m +| cons a l1 => cons A a (app A l1 m) +end. + +Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True. +intros; ergo. +Qed. + +(* polymorphism *) +Require Import List. + +Inductive mylist (A:Set) : Set := + mynil : mylist A +| mycons : forall a:A, mylist A -> mylist A. + +Parameter my_nlist: mylist nat -> Prop. + + Goal forall l, my_nlist l -> True. + intros. + simplify. +Qed. + +(* First example with the 0 and the equality translated *) + +Goal 0 = 0. +simplify. +Qed. + +(* Examples in the Propositional Calculus + and theory of equality *) + +Parameter A C : Prop. + +Goal A -> A. +simplify. +Qed. + + +Goal A -> (A \/ C). + +simplify. +Qed. + + +Parameter x y z : Z. + +Goal x = y -> y = z -> x = z. +ergo. +Qed. + + +Goal ((((A -> C) -> A) -> A) -> C) -> C. + +ergo. +Qed. + +(* Arithmetic *) +Open Scope Z_scope. + +Goal 1 + 1 = 2. +yices. +Qed. + + +Goal 2*x + 10 = 18 -> x = 4. + +simplify. +Qed. + + +(* Universal quantifier *) + +Goal (forall (x y : Z), x = y) -> 0=1. +try zenon. +ergo. +Qed. + +Goal forall (x: nat), (x + 0 = x)%nat. + +induction x0; ergo. +Qed. + + +(* No decision procedure can solve this problem + Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a. +*) + + +(* Functions definitions *) + +Definition fst (x y : Z) : Z := x. + +Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x. + +simplify. +Qed. + + +(* Eta-expansion example *) + +Definition snd_of_3 (x y z : Z) : Z := y. + +Definition f : Z -> Z -> Z := snd_of_3 0. + +Goal forall (x y z z1 : Z), snd_of_3 x y z = f y z1. + +simplify. +Qed. + + +(* Inductive types definitions - call to dp/injection function *) + +Inductive even : Z -> Prop := +| even_0 : even 0 +| even_plus2 : forall z : Z, even z -> even (z + 2). + + +(* Simplify and Zenon can't prove this goal before the timeout + unlike CVC Lite *) + +Goal even 4. +ergo. +Qed. + + +Definition skip_z (z : Z) (n : nat) := n. + +Definition skip_z1 := skip_z. + +Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n. +yices. +Qed. + + +(* Axioms definitions and dp_hint *) + +Parameter add : nat -> nat -> nat. +Axiom add_0 : forall (n : nat), add 0%nat n = n. +Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2). + +Dp_hint add_0. +Dp_hint add_S. + +(* Simplify can't prove this goal before the timeout + unlike zenon *) + +Goal forall n : nat, add n 0 = n. +induction n ; yices. +Qed. + + +Definition pred (n : nat) : nat := match n with + | 0%nat => 0%nat + | S n' => n' +end. + +Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat. +yices. +(*zenon.*) +Qed. + + +Fixpoint plus (n m : nat) {struct n} : nat := + match n with + | 0%nat => m + | S n' => S (plus n' m) +end. + +Goal forall n : nat, plus n 0%nat = n. + +induction n; ergo. +Qed. + + +(* Mutually recursive functions *) + +Fixpoint even_b (n : nat) : bool := match n with + | O => true + | S m => odd_b m +end +with odd_b (n : nat) : bool := match n with + | O => false + | S m => even_b m +end. + +Goal even_b (S (S O)) = true. +ergo. +(* +simplify. +zenon. +*) +Qed. + + +(* sorts issues *) + +Parameter foo : Set. +Parameter ff : nat -> foo -> foo -> nat. +Parameter g : foo -> foo. +Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O. +yices. +(*zenon.*) +Qed. + + + +(* abstractions *) + +Parameter poly_f : forall A:Set, A->A. + +Goal forall x:nat, poly_f nat x = poly_f nat x. +ergo. +(*zenon.*) +Qed. + + + +(* Anonymous mutually recursive functions : no equations are produced + +Definition mrf := + fix even2 (n : nat) : bool := match n with + | O => true + | S m => odd2 m + end + with odd2 (n : nat) : bool := match n with + | O => false + | S m => even2 m + end for even. + + Thus this goal is unsolvable + +Goal mrf (S (S O)) = true. + +zenon. + +*) diff --git a/plugins/dp/vo.itarget b/plugins/dp/vo.itarget new file mode 100644 index 00000000..4d282709 --- /dev/null +++ b/plugins/dp/vo.itarget @@ -0,0 +1 @@ +Dp.vo diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v new file mode 100644 index 00000000..502465c6 --- /dev/null +++ b/plugins/dp/zenon.v @@ -0,0 +1,94 @@ +(* Copyright 2004 INRIA *) +(* $Id$ *) + +Require Export Classical. + +Lemma zenon_nottrue : + (~True -> False). +Proof. tauto. Qed. + +Lemma zenon_noteq : forall (T : Type) (t : T), + ((t <> t) -> False). +Proof. tauto. Qed. + +Lemma zenon_and : forall P Q : Prop, + (P -> Q -> False) -> (P /\ Q -> False). +Proof. tauto. Qed. + +Lemma zenon_or : forall P Q : Prop, + (P -> False) -> (Q -> False) -> (P \/ Q -> False). +Proof. tauto. Qed. + +Lemma zenon_imply : forall P Q : Prop, + (~P -> False) -> (Q -> False) -> ((P -> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_equiv : forall P Q : Prop, + (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notand : forall P Q : Prop, + (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notor : forall P Q : Prop, + (~P -> ~Q -> False) -> (~(P \/ Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notimply : forall P Q : Prop, + (P -> ~Q -> False) -> (~(P -> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_notequiv : forall P Q : Prop, + (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False). +Proof. tauto. Qed. + +Lemma zenon_ex : forall (T : Type) (P : T -> Prop), + (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T), + ((P t) -> False) -> ((forall x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T), + (~(P t) -> False) -> (~(exists x : T, (P x)) -> False). +Proof. firstorder. Qed. + +Lemma zenon_notall : forall (T : Type) (P : T -> Prop), + (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False). +Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed. + +Lemma zenon_equal_base : forall (T : Type) (f : T), f = f. +Proof. auto. Qed. + +Lemma zenon_equal_step : + forall (S T : Type) (fa fb : S -> T) (a b : S), + (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)). +Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed. + +Lemma zenon_pnotp : forall P Q : Prop, + (P = Q) -> (P -> ~Q -> False). +Proof. intros P Q Ha. rewrite Ha. auto. Qed. + +Lemma zenon_notequal : forall (T : Type) (a b : T), + (a = b) -> (a <> b -> False). +Proof. auto. Qed. + +Ltac zenon_intro id := + intro id || let nid := fresh in (intro nid; clear nid) +. + +Definition zenon_and_s := fun P Q a b => zenon_and P Q b a. +Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a. +Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a. +Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a. +Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a. +Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a. +Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a. +Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a. +Definition zenon_ex_s := fun T P a b => zenon_ex T P b a. +Definition zenon_notall_s := fun T P a b => zenon_notall T P b a. + +Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b. +Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x. |