diff options
Diffstat (limited to 'contrib/dp')
| -rw-r--r-- | contrib/dp/Dp.v | 120 | ||||
| -rw-r--r-- | contrib/dp/TODO | 24 | ||||
| -rw-r--r-- | contrib/dp/dp.ml | 991 | ||||
| -rw-r--r-- | contrib/dp/dp.mli | 20 | ||||
| -rw-r--r-- | contrib/dp/dp_gappa.ml | 445 | ||||
| -rw-r--r-- | contrib/dp/dp_why.ml | 151 | ||||
| -rw-r--r-- | contrib/dp/dp_why.mli | 17 | ||||
| -rw-r--r-- | contrib/dp/dp_zenon.mli | 7 | ||||
| -rw-r--r-- | contrib/dp/dp_zenon.mll | 181 | ||||
| -rw-r--r-- | contrib/dp/fol.mli | 55 | ||||
| -rw-r--r-- | contrib/dp/g_dp.ml4 | 79 | ||||
| -rw-r--r-- | contrib/dp/test2.v | 80 | ||||
| -rw-r--r-- | contrib/dp/test_gappa.v | 91 | ||||
| -rw-r--r-- | contrib/dp/tests.v | 288 | ||||
| -rw-r--r-- | contrib/dp/zenon.v | 94 |
15 files changed, 0 insertions, 2643 deletions
diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v deleted file mode 100644 index 857c182c..00000000 --- a/contrib/dp/Dp.v +++ /dev/null @@ -1,120 +0,0 @@ -(* Calls to external decision procedures *) - -Require Export ZArith. -Require Export Classical. - -(* Zenon *) - -(* Copyright 2004 INRIA *) -(* $Id: Dp.v 10739 2008-04-01 14:45:20Z herbelin $ *) - -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/contrib/dp/TODO b/contrib/dp/TODO deleted file mode 100644 index 44349e21..00000000 --- a/contrib/dp/TODO +++ /dev/null @@ -1,24 +0,0 @@ - -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/contrib/dp/dp.ml b/contrib/dp/dp.ml deleted file mode 100644 index d8803847..00000000 --- a/contrib/dp/dp.ml +++ /dev/null @@ -1,991 +0,0 @@ -(* 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 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); - export_function = (fun x -> Some 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); - export_function = (fun x -> Some 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); - export_function = (fun x -> Some 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"; "omega"; "OmegaLemmas"]] - -let constant = gen_constant_in_modules "dp" coq_modules - -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") - -(* 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_ident 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.id_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 () -> ()); - Summary.survive_module = false; - Summary.survive_section = false } - -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 rec tr_positive p = match kind_of_term p with - | Term.Construct _ when p = Lazy.force coq_xH -> - Cst 1 - | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> - Plus (Mult (Cst 2, tr_positive a), Cst 1) - | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> - Mult (Cst 2, tr_positive a) - | Term.Cast (p, _, _) -> - tr_positive p - | _ -> - raise NotArithConstant - -(* translates a closed Coq term t:Z into a FOL term of type int *) -let rec tr_arith_constant t = match kind_of_term t with - | Term.Construct _ when t = Lazy.force coq_Z0 -> - Cst 0 - | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> - tr_positive a - | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - Moins (Cst 0, tr_positive a) - | Term.Cast (t, _, _) -> - tr_arith_constant t - | _ -> - 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 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 -> - 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 = match kind_of_term t with - | 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.Var id when List.mem id bv -> - App (string_of_id id, []) - | _ -> - try - tr_arith_constant t - with NotArithConstant -> - 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 - | _, [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)) - | _, [] 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 - -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 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); - export_function = (fun x -> Some 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 - 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 - let cmd = - if !trace then - sprintf "ergo -cctrace %s %s" ftrace fwhy - else - sprintf "ergo %s" fwhy - in - let ret,out = timeout_sys_command cmd in - let r = - if ret <> 0 then - timeout_or_failure ret cmd out - else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then - Valid (if !trace then Some ftrace else None) - else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then - DontKnow - else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then - Invalid - else - Failure ("command failed: " ^ cmd) - in - if not !debug then remove_files [fwhy; out]; - r - -let call_zenon fwhy = - let cmd = - sprintf "why --no-prelude --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 - 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 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_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 - 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]; - 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 - | Yices -> call_yices 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 yices = tclTHEN intros (dp Yices) -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); - export_function = (fun x -> Some x)} - -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); - export_function = (fun x -> Some x)} - -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 := []); - survive_module = true; - survive_section = true } diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli deleted file mode 100644 index 6dbc05e1..00000000 --- a/contrib/dp/dp.mli +++ /dev/null @@ -1,20 +0,0 @@ - -open Libnames -open Proof_type - -val simplify : tactic -val ergo : tactic -val yices : tactic -val cvc_lite : tactic -val harvey : tactic -val zenon : tactic -val gwhy : 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/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml deleted file mode 100644 index 9c035aa8..00000000 --- a/contrib/dp/dp_gappa.ml +++ /dev/null @@ -1,445 +0,0 @@ - -open Format -open Util -open Pp -open Term -open Tacmach -open Tactics -open Tacticals -open Names -open Nameops -open Termops -open Coqlib -open Hipattern -open Libnames -open Declarations -open Evarutil - -let debug = ref false - -(* 1. gappa syntax trees and output *) - -module Constant = struct - - open Bigint - - type t = { mantissa : bigint; base : int; exp : bigint } - - let create (b, m, e) = - { mantissa = m; base = b; exp = e } - - let of_int x = - { mantissa = x; base = 1; exp = zero } - - let print fmt x = match x.base with - | 1 -> fprintf fmt "%s" (to_string x.mantissa) - | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp) - | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp) - | _ -> assert false - -end - -type binop = Bminus | Bplus | Bmult | Bdiv - -type unop = Usqrt | Uabs | Uopp - -type rounding_mode = string - -type term = - | Tconst of Constant.t - | Tvar of string - | Tbinop of binop * term * term - | Tunop of unop * term - | Tround of rounding_mode * term - -type pred = - | Pin of term * Constant.t * Constant.t - -let rec print_term fmt = function - | Tconst c -> Constant.print fmt c - | Tvar s -> pp_print_string fmt s - | Tbinop (op, t1, t2) -> - let op = match op with - | Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/" - in - fprintf fmt "(%a %s %a)" print_term t1 op print_term t2 - | Tunop (Uabs, t) -> - fprintf fmt "|%a|" print_term t - | Tunop (Uopp | Usqrt as op, t) -> - let s = match op with - | Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false - in - fprintf fmt "(%s(%a))" s print_term t - | Tround (m, t) -> - fprintf fmt "(%s(%a))" m print_term t - -let print_pred fmt = function - | Pin (t, c1, c2) -> - fprintf fmt "%a in [%a, %a]" - print_term t Constant.print c1 Constant.print c2 - -let temp_file f = if !debug then f else Filename.temp_file f ".v" -let remove_file f = if not !debug then try Sys.remove f with _ -> () - -let read_gappa_proof f = - let buf = Buffer.create 1024 in - Buffer.add_char buf '('; - let cin = open_in f in - let rec skip_space () = - let c = input_char cin in if c = ' ' then skip_space () else c - in - while input_char cin <> '=' do () done; - try - while true do - let c = skip_space () in - if c = ':' then raise Exit; - Buffer.add_char buf c; - let s = input_line cin in - Buffer.add_string buf s; - Buffer.add_char buf '\n'; - done; - assert false - with Exit -> - close_in cin; - remove_file f; - Buffer.add_char buf ')'; - Buffer.contents buf - -exception GappaFailed -exception GappaProofFailed - -let patch_gappa_proof fin fout = - let cin = open_in fin in - let cout = open_out fout in - let fmt = formatter_of_out_channel cout in - let last = ref "" in - let defs = ref "" in - try - while true do - let s = input_line cin in - if s = "Qed." then - fprintf fmt "Defined.@\n" - else begin - begin - try Scanf.sscanf s "Lemma %s " - (fun n -> defs := n ^ " " ^ !defs; last := n) - with Scanf.Scan_failure _ -> - try Scanf.sscanf s "Definition %s " - (fun n -> defs := n ^ " " ^ !defs) - with Scanf.Scan_failure _ -> - () - end; - fprintf fmt "%s@\n" s - end - done - with End_of_file -> - close_in cin; - fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last; - close_out cout - -let call_gappa hl p = - let gappa_in = temp_file "gappa_input" in - let c = open_out gappa_in in - let fmt = formatter_of_out_channel c in - fprintf fmt "@[{ "; - List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl; - fprintf fmt "%a }@]@." print_pred p; - close_out c; - let gappa_out = temp_file "gappa_output" in - let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in - let out = Sys.command cmd in - if out <> 0 then raise GappaFailed; - remove_file gappa_in; - let gappa_out2 = temp_file "gappa2" in - patch_gappa_proof gappa_out gappa_out2; - remove_file gappa_out; - let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in - let out = Sys.command cmd in - if out <> 0 then raise GappaProofFailed; - let gappa_out3 = temp_file "gappa3" in - let c = open_out gappa_out3 in - let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in - Printf.fprintf c - "Require \"%s\". Set Printing Depth 999999. Print %s.proof." - (Filename.chop_suffix gappa_out2 ".v") gappa2; - close_out c; - let lambda = temp_file "gappa_lambda" in - let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in - let out = Sys.command cmd in - if out <> 0 then raise GappaProofFailed; - remove_file gappa_out2; remove_file gappa_out3; - remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o"); - read_gappa_proof lambda - -(* 2. coq -> gappa translation *) - -exception NotGappa - -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";]; - ["Gappa"; "Gappa_tactic";]; - ["Gappa"; "Gappa_fixed";]; - ["Gappa"; "Gappa_float";]; - ["Gappa"; "Gappa_round_def";]; - ["Gappa"; "Gappa_pred_bnd";]; - ["Gappa"; "Gappa_definitions";]; - ] - -let constant = gen_constant_in_modules "gappa" coq_modules - -let coq_refl_equal = lazy (constant "refl_equal") -let coq_Rle = lazy (constant "Rle") -let coq_R = lazy (constant "R") -(* -let coq_Rplus = lazy (constant "Rplus") -let coq_Rminus = lazy (constant "Rminus") -let coq_Rmult = lazy (constant "Rmult") -let coq_Rdiv = lazy (constant "Rdiv") -let coq_powerRZ = lazy (constant "powerRZ") -let coq_R1 = lazy (constant "R1") -let coq_Ropp = lazy (constant "Ropp") -let coq_Rabs = lazy (constant "Rabs") -let coq_sqrt = lazy (constant "sqrt") -*) - -let coq_convert = lazy (constant "convert") -let coq_reUnknown = lazy (constant "reUnknown") -let coq_reFloat2 = lazy (constant "reFloat2") -let coq_reFloat10 = lazy (constant "reFloat10") -let coq_reInteger = lazy (constant "reInteger") -let coq_reBinary = lazy (constant "reBinary") -let coq_reUnary = lazy (constant "reUnary") -let coq_reRound = lazy (constant "reRound") -let coq_roundDN = lazy (constant "roundDN") -let coq_roundUP = lazy (constant "roundUP") -let coq_roundNE = lazy (constant "roundNE") -let coq_roundZR = lazy (constant "roundZR") -let coq_rounding_fixed = lazy (constant "rounding_fixed") -let coq_rounding_float = lazy (constant "rounding_float") -let coq_boAdd = lazy (constant "boAdd") -let coq_boSub = lazy (constant "boSub") -let coq_boMul = lazy (constant "boMul") -let coq_boDiv = lazy (constant "boDiv") -let coq_uoAbs = lazy (constant "uoAbs") -let coq_uoNeg = lazy (constant "uoNeg") -let coq_uoSqrt = lazy (constant "uoSqrt") -let coq_subset = lazy (constant "subset") -let coq_makepairF = lazy (constant "makepairF") - -let coq_true = lazy (constant "true") -let coq_false = lazy (constant "false") - -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_IZR = lazy (constant "IZR") - -(* translates a closed Coq term p:positive into a FOL term of type int *) -let rec tr_positive p = match kind_of_term p with - | Term.Construct _ when p = Lazy.force coq_xH -> - 1 - | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> - 2 * (tr_positive a) + 1 - | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> - 2 * (tr_positive a) - | Term.Cast (p, _, _) -> - tr_positive p - | _ -> - raise NotGappa - -(* translates a closed Coq term t:Z into a term of type int *) -let rec tr_arith_constant t = match kind_of_term t with - | Term.Construct _ when t = Lazy.force coq_Z0 -> 0 - | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a - | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a) - | Term.Cast (t, _, _) -> tr_arith_constant t - | _ -> raise NotGappa - -(* translates a closed Coq term p:positive into a FOL term of type bigint *) -let rec tr_bigpositive p = match kind_of_term p with - | Term.Construct _ when p = Lazy.force coq_xH -> - Bigint.one - | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> - Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a)) - | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> - (Bigint.mult_2 (tr_bigpositive a)) - | Term.Cast (p, _, _) -> - tr_bigpositive p - | _ -> - raise NotGappa - -(* translates a closed Coq term t:Z into a term of type bigint *) -let rec tr_arith_bigconstant t = match kind_of_term t with - | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero - | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a - | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - Bigint.neg (tr_bigpositive a) - | Term.Cast (t, _, _) -> tr_arith_bigconstant t - | _ -> raise NotGappa - -let decomp c = - let c, args = decompose_app c in - kind_of_term c, args - -let tr_bool c = match decompose_app c with - | c, [] when c = Lazy.force coq_true -> true - | c, [] when c = Lazy.force coq_false -> false - | _ -> raise NotGappa - -let tr_float b m e = - (b, tr_arith_bigconstant m, tr_arith_bigconstant e) - -let tr_binop c = match decompose_app c with - | c, [] when c = Lazy.force coq_boAdd -> Bplus - | c, [] when c = Lazy.force coq_boSub -> Bminus - | c, [] when c = Lazy.force coq_boMul -> Bmult - | c, [] when c = Lazy.force coq_boDiv -> Bdiv - | _ -> assert false - -let tr_unop c = match decompose_app c with - | c, [] when c = Lazy.force coq_uoNeg -> Uopp - | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt - | c, [] when c = Lazy.force coq_uoAbs -> Uabs - | _ -> raise NotGappa - -let tr_var c = match decomp c with - | Var x, [] -> string_of_id x - | _ -> assert false - -let tr_mode c = match decompose_app c with - | c, [] when c = Lazy.force coq_roundDN -> "dn" - | c, [] when c = Lazy.force coq_roundNE -> "ne" - | c, [] when c = Lazy.force coq_roundUP -> "up" - | c, [] when c = Lazy.force coq_roundZR -> "zr" - | _ -> raise NotGappa - -let tr_rounding_mode c = match decompose_app c with - | c, [a;b] when c = Lazy.force coq_rounding_fixed -> - let a = tr_mode a in - let b = tr_arith_constant b in - sprintf "fixed<%d,%s>" b a - | c, [a;p;e] when c = Lazy.force coq_rounding_float -> - let a = tr_mode a in - let p = tr_positive p in - let e = tr_arith_constant e in - sprintf "float<%d,%d,%s>" p (-e) a - | _ -> - raise NotGappa - -(* REexpr -> term *) -let rec tr_term c0 = - let c, args = decompose_app c0 in - match kind_of_term c, args with - | _, [a] when c = Lazy.force coq_reUnknown -> - Tvar (tr_var a) - | _, [a; b] when c = Lazy.force coq_reFloat2 -> - Tconst (Constant.create (tr_float 2 a b)) - | _, [a; b] when c = Lazy.force coq_reFloat10 -> - Tconst (Constant.create (tr_float 10 a b)) - | _, [a] when c = Lazy.force coq_reInteger -> - Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero)) - | _, [op;a;b] when c = Lazy.force coq_reBinary -> - Tbinop (tr_binop op, tr_term a, tr_term b) - | _, [op;a] when c = Lazy.force coq_reUnary -> - Tunop (tr_unop op, tr_term a) - | _, [op;a] when c = Lazy.force coq_reRound -> - Tround (tr_rounding_mode op, tr_term a) - | _ -> - msgnl (str "tr_term: " ++ Printer.pr_constr c0); - assert false - -let tr_rle c = - let c, args = decompose_app c in - match kind_of_term c, args with - | _, [a;b] when c = Lazy.force coq_Rle -> - begin match decompose_app a, decompose_app b with - | (ac, [at]), (bc, [bt]) - when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert -> - at, bt - | _ -> - raise NotGappa - end - | _ -> - raise NotGappa - -let tr_pred c = - let c, args = decompose_app c in - match kind_of_term c, args with - | _, [a;b] when c = build_coq_and () -> - begin match tr_rle a, tr_rle b with - | (c1, t1), (t2, c2) when t1 = t2 -> - begin match tr_term c1, tr_term c2 with - | Tconst c1, Tconst c2 -> - Pin (tr_term t1, c1, c2) - | _ -> - raise NotGappa - end - | _ -> - raise NotGappa - end - | _ -> - raise NotGappa - -let is_R c = match decompose_app c with - | c, [] when c = Lazy.force coq_R -> true - | _ -> false - -let tr_hyps = - List.fold_left - (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) [] - -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) - -let var_name = function - | Name id -> - let s = string_of_id id in - let s = String.sub s 1 (String.length s - 1) in - mkVar (id_of_string s) - | Anonymous -> - assert false - -let build_proof_term c0 = - let bl,c = decompose_lam c0 in - List.fold_right - (fun (x,t) pf -> - mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |])) - bl c0 - -let gappa_internal gl = - try - let c = tr_pred (pf_concl gl) in - let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in - let pf = constr_of_string gl s in - let pf = build_proof_term pf in - Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl - with - | NotGappa -> error "not a gappa goal" - | GappaFailed -> error "gappa failed" - | GappaProofFailed -> error "incorrect gappa proof term" - -let gappa_prepare = - let id = Ident (dummy_loc, id_of_string "gappa_prepare") in - lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id))) - -let gappa gl = - Coqlib.check_required_library ["Gappa"; "Gappa_tactic"]; - Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl - -(* -Local Variables: -compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt" -End: -*) - diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml deleted file mode 100644 index e24049ad..00000000 --- a/contrib/dp/dp_why.ml +++ /dev/null @@ -1,151 +0,0 @@ - -(* 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 (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 rec print_term fmt = function - | Cst n -> - fprintf fmt "%d" 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 - | 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 print_query fmt (decls,concl) = - 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, _, []) -> - fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id - | DeclPred (id, _, l) -> - fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" - ident id (print_list comma print_typ) l - | DeclType _ | Axiom _ -> - () - in - let print_assert = function - | 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 "@[%a@]@." print_query q; - close_out c - - diff --git a/contrib/dp/dp_why.mli b/contrib/dp/dp_why.mli deleted file mode 100644 index b38a3d37..00000000 --- a/contrib/dp/dp_why.mli +++ /dev/null @@ -1,17 +0,0 @@ - -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/contrib/dp/dp_zenon.mli b/contrib/dp/dp_zenon.mli deleted file mode 100644 index 0a727d1f..00000000 --- a/contrib/dp/dp_zenon.mli +++ /dev/null @@ -1,7 +0,0 @@ - -open Fol - -val set_debug : bool -> unit - -val proof_from_file : string -> Proof_type.tactic - diff --git a/contrib/dp/dp_zenon.mll b/contrib/dp/dp_zenon.mll deleted file mode 100644 index e15e280d..00000000 --- a/contrib/dp/dp_zenon.mll +++ /dev/null @@ -1,181 +0,0 @@ - -{ - - 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 "%d" n - | 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 - | 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/contrib/dp/fol.mli b/contrib/dp/fol.mli deleted file mode 100644 index b94bd3e3..00000000 --- a/contrib/dp/fol.mli +++ /dev/null @@ -1,55 +0,0 @@ - -(* Polymorphic First-Order Logic (that is Why's input logic) *) - -type typ = - | Tvar of string - | Tid of string * typ list - -type term = - | Cst of int - | Plus of term * term - | Moins of term * term - | Mult of term * term - | Div of term * 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/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4 deleted file mode 100644 index 99bcf477..00000000 --- a/contrib/dp/g_dp.ml4 +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* 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: g_dp.ml4 10924 2008-05-13 14:01:11Z filliatr $ *) - -open Dp - -TACTIC EXTEND Simplify - [ "simplify" ] -> [ simplify ] -END - -TACTIC EXTEND Ergo - [ "ergo" ] -> [ ergo ] -END - -TACTIC EXTEND Yices - [ "yices" ] -> [ yices ] -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 - -TACTIC EXTEND Gappa_internal - [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ] -END - -TACTIC EXTEND Gappa - [ "gappa" ] -> [ Dp_gappa.gappa ] -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/contrib/dp/test2.v b/contrib/dp/test2.v deleted file mode 100644 index 3e4c0f6d..00000000 --- a/contrib/dp/test2.v +++ /dev/null @@ -1,80 +0,0 @@ -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/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v deleted file mode 100644 index eb65a59d..00000000 --- a/contrib/dp/test_gappa.v +++ /dev/null @@ -1,91 +0,0 @@ -Require Export Gappa_tactic. -Require Export Reals. - -Open Scope Z_scope. -Open Scope R_scope. - -Lemma test_base10 : - forall x y:R, - 0 <= x <= 4 -> - 0 <= x * (24 * powerRZ 10 (-1)) <= 10. -Proof. - gappa. -Qed. - -(* -@rnd = float< ieee_32, zr >; -a = rnd(a_); b = rnd(b_); -{ a in [3.2,3.3] /\ b in [1.4,1.9] -> - rnd(a - b) - (a - b) in [0,0] } -*) - -Definition rnd := gappa_rounding (rounding_float roundZR 43 (120)). - -Lemma test_float3 : - forall a_ b_ a b : R, - a = rnd a_ -> - b = rnd b_ -> - 52 / 16 <= a <= 53 / 16 -> - 22 / 16 <= b <= 30 / 16 -> - 0 <= rnd (a - b) - (a - b) <= 0. -Proof. - unfold rnd. - gappa. -Qed. - -Lemma test_float2 : - forall x y:R, - 0 <= x <= 1 -> - 0 <= y <= 1 -> - 0 <= gappa_rounding (rounding_float roundNE 53 (1074)) (x+y) <= 2. -Proof. - gappa. -Qed. - -Lemma test_float1 : - forall x y:R, - 0 <= gappa_rounding (rounding_fixed roundDN (0)) x - - gappa_rounding (rounding_fixed roundDN (0)) y <= 0 -> - Rabs (x - y) <= 1. -Proof. - gappa. -Qed. - -Lemma test1 : - forall x y:R, - 0 <= x <= 1 -> - 0 <= -y <= 1 -> - 0 <= x * (-y) <= 1. -Proof. - gappa. -Qed. - -Lemma test2 : - forall x y:R, - 3/4 <= x <= 3 -> - 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). -Proof. - gappa. -Qed. - -Lemma test3 : - forall x y z:R, - 0 <= x - y <= 3 -> - -2 <= y - z <= 4 -> - -2 <= x - z <= 7. -Proof. - gappa. -Qed. - -Lemma test4 : - forall x1 x2 y1 y2 : R, - 1 <= Rabs y1 <= 1000 -> - 1 <= Rabs y2 <= 1000 -> - - powerRZ 2 (-53) <= (x1 - y1) / y1 <= powerRZ 2 (-53) -> - - powerRZ 2 (-53) <= (x2 - y2) / y2 <= powerRZ 2 (-53) -> - - powerRZ 2 (-51) <= (x1 * x2 - y1 * y2) / (y1 * y2) <= powerRZ 2 (-51). -Proof. - gappa. -Qed. - - diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v deleted file mode 100644 index a6d4f2e1..00000000 --- a/contrib/dp/tests.v +++ /dev/null @@ -1,288 +0,0 @@ - -Require Import ZArith. -Require Import Classical. - -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 incontrib/dp/jection 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/contrib/dp/zenon.v b/contrib/dp/zenon.v deleted file mode 100644 index 4ad00a11..00000000 --- a/contrib/dp/zenon.v +++ /dev/null @@ -1,94 +0,0 @@ -(* Copyright 2004 INRIA *) -(* $Id: zenon.v 10739 2008-04-01 14:45:20Z herbelin $ *) - -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. |