new version of auto that is able to prove the irrationality of sqrt(2)

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index cfef9452f0a3094c4283c1392f6dfc98495849c1..b229cc05fc2102c396ab87af6de2e51a747022bb 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -46,6 +46,7 @@ and proof =
             (* subst, (rule,eq1, eq2,predicate) *)  
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
+(* the hashtbl eq_id -> proof, max_eq_id *)
 type equality_bag = (int,equality) Hashtbl.t * int ref
 
 type goal = goal_proof * Cic.metasenv * Cic.term
@@ -95,8 +96,8 @@ let string_of_equality ?env eq =
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
-        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
-(*         "..." *)
+(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
+         "..." 
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
       let w, _, (ty, left, right, o), m , id = open_equality eq in
@@ -224,7 +225,8 @@ let mk_trans uri ty t1 t2 t3 p12 p23 =
 ;;
 
 let mk_eq_ind uri ty what pred p1 other p2 =
- Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+  let ens, args = build_ens uri [ty; what; pred; p1; other; p2] in
+  Cic.Appl (Cic.Const (uri, ens) :: args)
 ;;
 
 let p_of_sym ens tl =
@@ -266,34 +268,6 @@ let is_not_fixed t =
    CicSubstitution.subst (Cic.Rel 1) t
 ;;
 
-let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
-let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
-let count_args t = List.length (tail_of_apply t);;
-let rec build_nat = 
-  let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
-  function
-    | 0 -> Cic.MutConstruct(u,0,1,[])
-    | n -> 
-        Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
-;;
-let tyof context menv t =
-  try
-    fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
-  with
-  | CicTypeChecker.TypeCheckerFailure _
-  | CicTypeChecker.AssertFailure _ -> assert false
-;;
-let rec lambdaof left context = function
-  | Cic.Prod (n,s,t) ->
-      Cic.Lambda (n,s,lambdaof left context t)
-  | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r] 
-      when LibraryObjects.is_eq_URI uri -> if left then l else r
-  | t -> 
-      let names = Utils.names_of_context context in
-      prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
-      assert false
-;;
-
 let canonical t context menv = 
   let rec remove_refl t =
     match t with
@@ -334,54 +308,6 @@ let canonical t context menv =
                    Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
                  Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))  
-
-(*
-                 let sym_eq = Cic.Const(uri_sym,ens) in
-                 let eq_f = Cic.Const(uri_feq,[]) in
-                 let b = Cic.MutConstruct (UriManager.uri_of_string
-                   "cic:/matita/datatypes/bool/bool.ind",0,1,[])
-                 in
-                 let u = ty1 in
-                 let ctx = f in
-                 let n = build_nat (count_args p) in
-                 let h = head_of_apply p in
-                 let predl = lambdaof true context (tyof context menv h) in 
-                 let predr = lambdaof false context (tyof context menv h) in
-                 let args = tail_of_apply p in
-                 let appl = 
-                   Cic.Appl
-                    ([Cic.Const(UriManager.uri_of_string
-                      "cic:/matita/paramodulation/rewrite.con",[]);
-                      eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
-                      args)
-                 in
-                 appl
-*)
-(*
-             | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
-                 when LibraryObjects.is_eq_ind_URI uri_ind || 
-                      LibraryObjects.is_eq_ind_r_URI uri_ind ->
-                 let ty, what, pred, p1, other, p2 =
-                   match tl with
-                   | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
-                   | _ -> assert false
-                 in
-                 let pred,l,r = 
-                   match pred with
-                   | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
-                       when LibraryObjects.is_eq_URI uri ->
-                         Cic.Lambda 
-                           (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
-                   | _ -> 
-                       prerr_endline (CicPp.ppterm pred);
-                       assert false
-                 in
-                 let l = CicSubstitution.subst what l in
-                 let r = CicSubstitution.subst what r in
-                 Cic.Appl 
-                   [he;ty;what;pred;
-                    canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
-*)
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
              | _ -> Cic.Appl (List.map (canonical context) args))
@@ -391,11 +317,6 @@ let canonical t context menv =
   remove_refl (canonical context t)
 ;;
   
-let ty_of_lambda = function
-  | Cic.Lambda (_,ty,_) -> ty
-  | _ -> assert false 
-;;
-
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
     ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
@@ -407,11 +328,13 @@ let put_in_ctx ctx t =
 ;;
 
 let mk_eq uri ty l r =
-  Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+  let ens, args = build_ens uri [ty; l; r] in
+  Cic.Appl (Cic.MutInd(uri,0,ens) :: args)
 ;;
 
 let mk_refl uri ty t = 
-  Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+  let ens, args = build_ens uri [ty; t] in
+  Cic.Appl (Cic.MutConstruct(uri,0,1,ens) :: args)
 ;;
 
 let open_eq = function 
@@ -421,7 +344,8 @@ let open_eq = function
 ;;
 
 let mk_feq uri_feq ty ty1 left pred right t = 
-  Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+  let ens, args = build_ens uri_feq [ty;ty1;pred;left;right;t] in
+  Cic.Appl (Cic.Const(uri_feq,ens) :: args)
 ;;
 
 let rec look_ahead aux = function