Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 2648 insertions, 0 deletions

diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v
new file mode 100644
index 0000000000..47d67725f2
--- /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 0000000000..44349e2147
--- /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 0000000000..79ffaf3f90
--- /dev/null
+++ b/plugins/dp/dp.ml
@@ -0,0 +1,991 @@
+(* 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 "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 --no-arrays --simplify --encoding sstrat %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 "timeout %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 --no-arrays --why %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 --no-arrays -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 "timeout %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 --no-arrays --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 --no-arrays --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 --no-arrays  %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/plugins/dp/dp.mli b/plugins/dp/dp.mli
new file mode 100644
index 0000000000..6dbc05e17c
--- /dev/null
+++ b/plugins/dp/dp.mli
@@ -0,0 +1,20 @@
+
+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/plugins/dp/dp_gappa.ml b/plugins/dp/dp_gappa.ml
new file mode 100644
index 0000000000..9c035aa855
--- /dev/null
+++ b/plugins/dp/dp_gappa.ml
@@ -0,0 +1,445 @@
+
+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/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
new file mode 100644
index 0000000000..361d6f8323
--- /dev/null
+++ b/plugins/dp/dp_plugin.mllib
@@ -0,0 +1,5 @@
+Dp_why
+Dp_zenon
+Dp
+Dp_gappa
+G_dp
diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml
new file mode 100644
index 0000000000..e24049ad6a
--- /dev/null
+++ b/plugins/dp/dp_why.ml
@@ -0,0 +1,151 @@
+
+(* 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/plugins/dp/dp_why.mli b/plugins/dp/dp_why.mli
new file mode 100644
index 0000000000..b38a3d3762
--- /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 0000000000..0a727d1f10
--- /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 0000000000..e15e280db0
--- /dev/null
+++ b/plugins/dp/dp_zenon.mll
@@ -0,0 +1,181 @@
+
+{
+
+  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/plugins/dp/fol.mli b/plugins/dp/fol.mli
new file mode 100644
index 0000000000..b94bd3e358
--- /dev/null
+++ b/plugins/dp/fol.mli
@@ -0,0 +1,55 @@
+
+(* 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/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
new file mode 100644
index 0000000000..95135694d4
--- /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 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/plugins/dp/test2.v b/plugins/dp/test2.v
new file mode 100644
index 0000000000..3e4c0f6dd0
--- /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/test_gappa.v b/plugins/dp/test_gappa.v
new file mode 100644
index 0000000000..eb65a59d68
--- /dev/null
+++ b/plugins/dp/test_gappa.v
@@ -0,0 +1,91 @@
+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/plugins/dp/tests.v b/plugins/dp/tests.v
new file mode 100644
index 0000000000..fa6a13ef09
--- /dev/null
+++ b/plugins/dp/tests.v
@@ -0,0 +1,288 @@
+
+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 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/zenon.v b/plugins/dp/zenon.v
new file mode 100644
index 0000000000..502465c6be
--- /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.