diff options
| -rw-r--r-- | contrib/omega/Zlogarithm.v | 4 | ||||
| -rw-r--r-- | contrib/ring/Ring.v | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 7 | ||||
| -rw-r--r-- | scripts/coqc.ml | 11 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 15 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 1950 | ||||
| -rwxr-xr-x | theories/Bool/Bool.v | 2 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 8 | ||||
| -rw-r--r-- | theories/Lists/PolyList.v | 2 | ||||
| -rwxr-xr-x | theories/Sets/Partial_Order.v | 3 | ||||
| -rwxr-xr-x | theories/Sets/Relations_1_facts.v | 2 | ||||
| -rw-r--r-- | theories/Zarith/auxiliary.v | 2 |
12 files changed, 1975 insertions, 33 deletions
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index 803981e33..5d343880e 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -140,10 +140,10 @@ Induction p; Simpl; Intros; [Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ]. Intros; Apply Zle_le_S. Generalize H0; Elim p1; Intros; Simpl; - [ Tauto | Tauto | Apply ZERO_le_POS ]. + [ Assumption | Assumption | Apply ZERO_le_POS ]. Intros; Apply Zle_le_S. Generalize H0; Elim p1; Intros; Simpl; - [ Tauto | Tauto | Apply ZERO_le_POS ]. + [ Assumption | Assumption | Apply ZERO_le_POS ]. Save. Theorem log_near_correct2: (p:positive) diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index 81b2077a4..b6f75a584 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -58,7 +58,7 @@ Destruct n; Reflexivity. Destruct n; Reflexivity. Destruct n; Reflexivity. Destruct n; Destruct m; Destruct p; Reflexivity. -Destruct x; Destruct y; Reflexivity Orelse Tauto. +Destruct x; Destruct y; Reflexivity Orelse Simpl; Tauto. Defined. Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 0c5dc14e0..9b78d19a9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -88,7 +88,12 @@ let check_fix_reversibility labs args ((lv,i),(tys,_,bds)) = raise Elimconst) args in if list_distinct (List.map fst li) then - EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n)) + let k = lv.(i) in + if k < nargs then + let p = destRel (List.nth args k) in + EliminationFix (n-p+1,(nbfix,li,n)) + else + EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n)) else raise Elimconst diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 4dc09bc18..e93008b5f 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -19,6 +19,7 @@ let environment = Unix.environment () let bindir = ref Coq_config.bindir let binary = ref ("coqtop." ^ Coq_config.best) +let image = ref "" (* the $COQBIN environment variable has priority over the Coq_config value *) let _ = @@ -122,8 +123,12 @@ let parse_args () = binary := "coqtop.byte"; parse (cfiles,args) rem | "-opt" :: rem -> binary := "coqtop.opt"; parse (cfiles,args) rem + | "-image" :: f :: rem -> + image := f; parse (cfiles,args) rem + | "-image" :: [] -> + usage () | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-image"|"-libdir"|"-I"|"-include"|"-outputstate" + | ("-libdir"|"-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" |"-init-file" as o) :: rem -> @@ -164,7 +169,9 @@ let main () = prerr_endline "coqc: too few arguments" ; usage () end; - let coqtopname = Filename.concat !bindir !binary in + let coqtopname = + if !image <> "" then !image else Filename.concat !bindir !binary + in List.iter (compile coqtopname args) cfiles let _ = Printexc.print main (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 0723aec67..9cafd5f7f 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -58,20 +58,12 @@ let top = ref false let searchisos = ref false let echo = ref false +let src_dirs = [ []; [ "config" ]; [ "toplevel" ] ] + let includes () = List.fold_right (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l) - [ [ "config" ] ; - [ "scripts" ] ; - [ "lib" ] ; - [ "kernel" ] ; - [ "library" ] ; - [ "pretyping" ] ; - [ "parsing" ] ; - [ "proofs" ] ; - [ "tactics" ] ; - [ "toplevel" ] - ] + src_dirs ["-I"; Coq_config.camlp4lib] (* Transform bytecode object file names in native object file names *) @@ -113,7 +105,6 @@ let all_subdirs dir = let l = ref [] in let add f = l := f :: !l in let rec traverse dir = - Printf.printf "%s\n" dir; let dirh = try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index f181957f3..0415bae4d 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -100,6 +100,7 @@ let intuition_main () = and t_simplif = tacticIn simplif in <:tactic<$t_simplif;$t_axioms Orelse Auto with *>> +(*i let compute = function | None -> interp <:tactic<Compute>> | Some id -> @@ -107,24 +108,1961 @@ let compute = function interp <:tactic<Compute in $ast_id>> let reduction = Tacticals.onAllClauses (fun ido -> compute ido) +i*) + +let unfold_not_iff = function + | None -> interp <:tactic<Unfold not iff>> + | Some id -> + let ast_id = nvar (string_of_id id) in + interp <:tactic<Unfold not iff in $ast_id>> + +let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido) (* As a simple heuristic, first we try to avoid reduction both in *) (* tauto and intuition *) let tauto = (tclTHEN (init_intros ()) - (tclORELSE - (interp (tauto_main ())) - (tclTHEN reduction (interp (tauto_main ())))) - ) + (tclORELSE + (interp (tauto_main ())) + (tclTHEN reduction_not_iff (interp (tauto_main ())))) + ) let intuition = tclTHEN (init_intros ()) (tclORELSE (interp (intuition_main ())) - (tclTHEN reduction (interp (intuition_main ()))) + (tclTHEN reduction_not_iff (interp (intuition_main ()))) ) - +(*FIXME let _ = hide_atomic_tactic "Tauto" tauto let _ = hide_atomic_tactic "Intuition" intuition +*) + + +(****************************************************************************) +(* VIEUX TAUTO RÉTABLI EN ATTENDANT QUE LE NOUVEAU TAUTO SOIT STABLE *) +(* COUPER TOUT CE QUI SUIT QUAND CE SERA LE CAS *) +(****************************************************************************) + +(* Autor: Cesar A. Munnoz H *) + +open Pp +open Util +open Names +(* open Generic *) +open Term +open Sign +open Environ +open Declare +open Tacmach +open Reduction +open Tacticals +open Tactics +open Pattern +open Hipattern +open Auto +(* Chet's code *) +open Proof_trees +open Clenv +open Pattern + +(* Faut-il comparer le corps des définitions de l'environnement ? *) +let hlset_subset hls1 hls2 = + List.for_all + (fun (_,_,e) -> List.exists + (fun (_,_,e') -> eq_constr (body_of_type e) (body_of_type e')) + hls2) + hls1 + +let hlset_eq hls1 hls2 = + hlset_subset hls1 hls2 & hlset_subset hls2 hls1 + +let eq_gls g1 g2 = + eq_constr (pf_concl g1) (pf_concl g2) & hlset_eq (pf_hyps g1) (pf_hyps g2) + +let gls_memb bTS g = List.exists (eq_gls g) bTS + +let gls_add g bTS = + if gls_memb bTS g then error "backtrack in tauto"; + g::bTS + +let classically cltac = function + | (Some _ as cls) -> (tclTHEN (cltac cls) (clear_clause cls)) + | None -> cltac None + +let module_mark = ["Logic"] +(* patterns *) +let mmk = make_module_marker ["Prelude"] +let false_pattern_mark = put_pat mmk "False" +let true_pattern_mark = put_pat mmk "True" +let and_pattern_mark = put_pat mmk "(and ?1 ?2)" +let or_pattern_mark = put_pat mmk "(or ?1 ?2)" +let eq_pattern_mark = put_pat mmk "(eq ?1 ?2 ?3)" +let pi_pattern = put_pat mmk "(x : ?)((?1)@[x])" +let imply_pattern = put_pat mmk "?1 -> ?2" +let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2" +let iff_pattern_mark = put_pat mmk "(iff ?1 ?2)" +let not_pattern_mark = put_pat mmk "(not ?1)" +(* squeletons *) +(* +let imply_squeleton = put_squel mmk "?1 -> ?2" +let mkIMP a b = soinstance imply_squeleton [a;b] +*) +let mkIMP a b = mkProd (Anonymous, a, b) + +let false_pattern () = get_pat false_pattern_mark +let true_pattern () = get_pat true_pattern_mark +let and_pattern () = get_pat and_pattern_mark +let or_pattern () = get_pat or_pattern_mark +let eq_pattern () = get_pat eq_pattern_mark +let iff_pattern () = get_pat iff_pattern_mark +let not_pattern () = get_pat not_pattern_mark + +let is_atomic m = + (not (is_conjunction m) || + (is_disjunction m) || + (is_matching (get_pat pi_pattern) m) || + (is_matching (not_pattern ()) m)) + +(* Steps of the procedure *) + +(* 1. A,Gamma |- A *) +let dyck_hypothesis id = exact_check (mkVar id) + +(* 2. False,Gamma |- G *) +let dyck_absurdity_elim = contradiction_on_hyp + +(*3. A,B,Gamma |- G + --------------- + A/\B,Gamma |- G + *) +let dyck_and_elim = compose (classically dAnd) in_some + +(*4. Gamma |- A Gamma |- B + ----------------------- + Gamma |- A /\ B + *) +let dyck_and_intro = (dAnd None) + + +(*5. A,Gamma |- G B,Gamma|- G + --------------------------- + A\/B,Gamma |- G + *) + +let dyck_or_elim = compose (classically (dorE false)) in_some + +(*6. Gamma |- A + ---------- + Gamma |- A\/B + *) +let dyck_or_introleft = (dorE false) + + +(*7. Gamma |-B + --------- + Gamma |- A\/B + *) +let dyck_or_introright = (dorE true) + + +(*8. A,Gamma |- B + -------------- + Gamma |- A -> B + *) +let dyck_imply_intro = (dImp None) + + +(*9. + B,A,Gamma |- G + -------------- + A->B,A,Gamma |- G (A Atomique) + *) + +let atomic_imply_step cls gls = + begin try + let mvb = matches (get_pat atomic_imply_bot_pattern) (clause_type cls gls) in + if not (is_atomic (List.assoc 1 mvb)) then + error "atomic_imply_step" + with PatternMatchingFailure -> error "atomic_imply_step" end; + (tclTHENS (dImp cls) ([clear_clause cls;assumption])) gls + +let dyck_atomic_imply_elim = compose (atomic_imply_step) in_some + +(*10. + C ->(D-> B),Gamma |- G + ----------------------- + (C/\D)->B,Gamma |- G + *) + +let and_imply_step cls gls = + try + match matches (get_pat imply_pattern) (clause_type cls gls) with + | [(1,a);(2,b)] -> + let l = match match_with_conjunction a with + | Some (_,l) -> l + | None -> error "and_imply_step" + in + (tclTHENS (cut_intro (List.fold_right mkIMP l b)) + [clear_clause cls ; + (tclTHENS (tclTHEN (tclDO (List.length l) intro) (dImp cls)) + [assumption; + (tclTHEN (dAnd None) assumption)])]) gls + | _ -> anomaly "Inconsistent pattern-matching" + with PatternMatchingFailure -> error "and_imply_step" + +let dyck_and_imply_elim = compose (and_imply_step) in_some + +(*11. + C->B,D->B,Gamma |-G + -------------------- + (C\/D)->B,Gamma |- G +*) + +let or_imply_step cls gls = + try + match matches (get_pat imply_pattern) (clause_type cls gls) with + | [(1,a);(2,b)] -> + let l = match match_with_disjunction a with + | Some (_,l) -> l + | None -> error "or_imply_step" + in + (tclTHENS (cut_in_parallel (List.map (fun x -> (mkIMP x b)) l)) + (clear_clause cls:: + (List.map + (fun i -> (tclTHENS (tclTHEN intro (dImp cls)) + [assumption ; + (tclTHEN (one_constructor i []) assumption)])) + (interval 1 (List.length l))))) gls + | _ -> anomaly "Inconsistent pattern-matching" + with PatternMatchingFailure -> error "or_imply_step" + +let dyck_or_imply_elim = compose (or_imply_step) in_some + +(*12. +B,Gamma|- G D->B,Gamma |- C->D +---------------------------------- +(C->D)->B,Gamma |- G +*) + +let back_thru_2 id = + applist(mkVar id,[mkMeta (new_meta());mkMeta (new_meta())]) + +let back_thru_1 id = + applist(mkVar id,[mkMeta(new_meta())]) + +let exact_last_hyp = onLastHyp (fun h -> exact_no_check (mkVar (out_some h))) + +let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3" + +let imply_imply_step cls gls = + let h0 = out_some cls in (* (C->D)->B *) + try + match matches (get_pat imply_imply_bot_pattern) (clause_type cls gls) with + | [(1,c);(2,d);(3,b)] -> + tclTHENS (cut_intro b) + [clear_clause cls; (* B |- G *) + tclTHENS (cut_intro (mkIMP (mkIMP d b) (mkIMP c d))) + [onLastHyp + (fun h1opt (*(D->B)->(C->D)*) -> + let h1 = out_some h1opt in + (tclTHENS (refine (back_thru_1 h0)) + [tclTHENS + (tclTHEN intro (* C *) (refine (back_thru_2 h1))) + [tclTHENS + (tclTHEN intro (* D *) (refine (back_thru_1 h0))) + [tclTHEN intro (* C *) assumption]; + exact_last_hyp]])); + (tclTHEN (clear_clause cls) (intro)) + ] + ] gls + | _ -> anomaly "Inconsistent pattern-matching" + with PatternMatchingFailure -> error "imply_imply_bot_step" + +let dyck_imply_imply_elim = compose (imply_imply_step) in_some + +(*14. + B,Gamma |-G + -------------------- + True->B,Gamma |- G +*) + +let true_imply_step cls gls = + try + match matches (get_pat imply_pattern) (clause_type cls gls) with + | [(1,a);(2,b)] -> + let l = match match_with_unit_type a with + (* match_with_unit_type retournait un constr list option avec un seul + element dans la liste; maintenant il renvoie un constr option *) + (* Some (_::l) -> l *) + | Some _ -> [] + | None -> error "true_imply_step" + in + let h0 = out_some cls in + (tclTHENS (cut_intro b) + [(clear_clause cls); + (tclTHEN (apply(mkVar h0)) (one_constructor 1 []))]) gls + | _ -> anomaly "Inconsistent pattern-matching" + with PatternMatchingFailure -> error "true_imply_step" + +let dyck_true_imply_elim = compose (true_imply_step) in_some + +(* Chet's original algorithm +let rec prove g = + tclCOMPLETE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tryAllHyps (clauseTacThen ((comp(dyck_hypothesis) (out_some))) prove))) + ((tryAllHyps (clauseTacThen ((comp(dyck_absurdity_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_and_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_or_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_atomic_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_and_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_or_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_imply_imply_elim) (out_some))) prove))))) + (((tclTHEN (dyck_and_intro) (prove)))))) + (((tclTHEN (dyck_or_introleft) (prove)))))) + (((tclTHEN (dyck_or_introright) (prove)))))) + (((tclTHEN (dyck_imply_intro) (prove)))))) g + +*) + +(* Cesar's code *) + +let trans x = ([],Nametab.sp_of_id CCI (id_of_string x)) + +let flat_map f = + let rec flat_map_f = function + | [] -> [] + | x::l -> f x @ flat_map_f l + in + flat_map_f + +type formula = + | FVar of string + | FAnd of formula*formula + | FOr of formula*formula + | FImp of formula*formula + | FEqu of formula*formula + | FNot of formula + | FEq of formula*formula*formula + | FPred of constr (* Predicado proposicional *) + | FFalse + | FTrue + (* La siguiente no puede aparecer en una formula de entrada *) + (* Representa una formula atomica cuando aparece en un principal de una + regla *) + | FLis of formula list (* Lista de formulas *) + | FAto of string (* Formula atomica *) + | FLisfor of string (* Variable para una lista de formulas *) + (* En el antecedente se llama GAMA, + en el sucedente DELTA *) + +(* Terminos en calculo lambda *) +type termino = + | TVar of string + | TApl of formula*formula*termino*termino + | TFun of string*formula*termino + | TPar of formula*formula*termino*termino + | TInl of formula*formula*termino + | TInr of formula*formula*termino + | TFst of formula*formula*termino + | TSnd of formula*formula*termino + | TCase of formula list * termino list + | TZ of formula * termino + | TExi of string + | TRefl of formula * formula (*Reflexividad de la igualdad *) + | TSim of formula * formula * formula * termino + (*Simetria de la igualdad *) + | TTrue + (* Los siguientes terminos se usan solamente en las sustituciones *) + | TSum of termino*termino (* Suma de terminos *) + | TLis of termino list (* Lista de terminos *) + | TLister of string (* Variable para una lista de terminos *) + (* En el antecendete se llama Gama, + en el sucedente Delta *) + | TZero of formula (* Milagro *) + +(* Es una formula asociada con un termino del calculo lambda, o los + multiconjuntos Gama y Delta *) +type formulaT = termino*formula + +(* La primera componente es el antecedente, la segunda es sucedente *) +type sequente = formulaT list * formulaT list + +(* Substitucion de variable por una formula *) +type subsF = (string*formula) list + +(* Substitucion de variable por un lambda termino *) +type subsT = (string*termino) list + +type regla = { + tip: string; (* Tipo de la formula principal *) + heu: bool; (* Si es una regla heuristica o no *) + ant: bool; (* Si principal es antecedente o sucedente *) + pri: formulaT;(* Formula principal de la regla *) + pre: sequente list; (* Premisas de la regla *) + res: sequente;(* Restricciones para la aplicacion de una regla*) + def: subsT; (* Definicion de los terminos del lado derecho *) + sub: subsT; (* Substitucion que se aplica al lado derecho de la + conclusion para obetener el lambda termino *) + ren: string list; (* Variables que se deben renombrar *) + vardelta:bool; (* Si se usa la variable proposicional DELTA *) + ssi:bool; (* Si la regla es reversible o no *) + rendelta: string list } (* Renombramientos de delta *) + (* Note que si Res = A |- B, entonces la conclusion de la regla es + A,Gama,Pri' |- B, Pri'',Delta + Si ant = true Pri'= Pri + Si ant =false Pri''=Pri*) + +(* Substitucion Formula Termino para aplicar una regla *) +type sFT = { + sReg : regla ref; (*Apuntador a la regla *) + sFor : subsF; (*Substitucion de Formulas *) + sGam : formulaT list; (* Lista de formulas de Gamma *) + sDel : formulaT list; (* Lista de formulas de Delta *) + sRen : (string*subsT) list; (* Renombramientos de variables *) + sTer : subsT; (* Susbstitucion de terminos *) + sDef : subsT } (* Definicion de terminos *) + +type subsFT = SNil | SCons of sFT + +type reglaSub = RNil | RCons of (sFT*regla list*formulaT list*sequente) + +(* De un arbol de demostracion *) +type nodo = { + seq: sequente ref; (* Sequente que se resuelve *) + reg: regla ref; (* Regla usada para resolver *) + sd: subsT; (* Substitucion que define los lambda terminos *) + st: subsT } (* Substitucion que calcula el lambda termino *) + +(* Arbol de demostracion *) +type arbol = Nil | Cons of arbol * nodo * arbol + +(* Demostracion *) +(* Si el secuente es valido Arb es un arbol de demostracion y Lisbut + es vacio, sino Lisbut es un contexto en el cual Arb es valido *) +type demostracion = { arb : arbol; lisbut : formulaT list } + +(* Definicion de excepcion para rescribir terminos *) +exception NoAplica +exception TacticFailure + +(* ------------------ Sistema de Gentzen Intuisionista -------------------*) +(* Gama,Delta son metavariables de conjuntos de reglas + A,B son variables de formulas *) + +let gama = (TLister "Gama",FLisfor "GAMA") +let delta = (TLister "Delta",FLisfor "DELTA") +let delta' = (TLister "Delta'",FLisfor "DELTA") +let delta'' = (TLister "Delta''",FLisfor "DELTA") + +let curry(a,b,c,a_0,b_0,p) = TFun(a_0,a,TFun(b_0,b,TApl(FAnd(a,b),c,p, + TPar(a,b,TVar a_0,TVar b_0)))) +let left(a,b,c,a_0,p) = TFun(a_0,a,TApl(FOr(a,b),c,p,TInl(a,b,TVar a_0))) +let right(a,b,c,b_0,p) = TFun(b_0,b,TApl(FOr(a,b),c,p,TInr(a,b,TVar b_0))) +let imp2(a,b,c,a_0,b_0,p) = TFun(a_0,a,TApl(FImp(b,a),c,p,TFun(b_0,b,TVar a_0))) + +(* Regla inicial *) +(* / A,Gama |- A,Delta *) +let inic = { + tip="inic"; + heu=false; + ant=true; + pri= TVar "#x",FAto "#A"; + pre=[]; + res=([],[TVar "#x",FVar "#A"]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x"]; + vardelta = true; + ssi = true; + rendelta=[] } + +(* Regla l_false *) +(* / Gama,False |- Delta *) +let l_false = { + tip="false"; + heu=false; + ant=true; + pri= TVar "#x",FFalse; + pre=[]; + res=([],[]); + def=["Delta",TZ(FLisfor "DELTA",TVar "#x")]; + sub=[]; + ren=["#x"]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla r_true *) +(* / Gama |- True,Delta *) +let r_true = { + tip="true"; + heu=false; + ant=false; + pri= TTrue,FTrue; + pre=[]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=[]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla l_and *) +(* A,B,Gama |- Delta / FAnd(A,B),Gama |- Delta *) +let l_and = { + tip="l_and"; + heu=false; + ant=true; + pri= TVar "#xy",FAnd(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";TVar "#y",FVar "#B";gama],[delta]]; + res=([],[]); + def=[]; + sub=["#x",TFst(FVar "#A",FVar "#B",TVar "#xy"); + "#y",TSnd(FVar "#A",FVar "#B",TVar "#xy")]; + ren=["#x";"#y"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_and *) +(* Gama |- A,Delta' Gama |- B,Delta'' / Gama |- A/\B,Delta *) +let r_and = { + tip="r_and"; + heu=false; + ant=false; + pri= TPar(FVar "#A",FVar "#B",TVar "#x",TVar "#y"), + FAnd(FVar "#A",FVar "#B"); + pre=[[gama],[TVar "#x",FVar "#A";delta'];[gama], + [TVar "#y",FVar "#B";delta'']]; + res=([],[]); + def=["Delta",TSum(TLister "Delta'",TLister "Delta''")]; + sub=[]; + ren=["#x";"#y"]; + vardelta = true; + ssi = true; + rendelta=["Delta'";"Delta''"]} + +(* Regla l_or *) +(* A,Gama |- Delta' B,Gama |- Delta'' / A\/B,Gama |- Delta *) +let l_or = { + tip="l_or"; + heu=false; + ant=true; + pri= TVar "#xy",FOr(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";gama],[delta']; + [TVar "#y",FVar "#B";gama],[delta'']]; + res=([],[]); + sub=[]; + def=["Delta", TCase([FVar "#A";FVar "#B";FLisfor "DELTA"], + [TFun("#x",FVar "#A",TLister "Delta'"); + TFun("#y",FVar "#B",TLister "Delta''"); + TVar "#xy"])]; + ren=["#x";"#y";"#xy"]; + vardelta = true; + ssi = true; + rendelta=["Delta'";"Delta''"]} + +(* Regla r_or *) +(* Gama |- A,B,Delta / Gama |- A\/B,Delta *) +let r_or = { + tip="r_or"; + heu=false; + ant=false; + pri= TSum(TInl(FVar "#A",FVar "#B",TVar "#x"), + TInr(FVar "#A",FVar "#B",TVar "#y")), + FOr(FVar "#A",FVar "#B"); + pre=[[gama], + [TVar "#x",FVar "#A";TVar "#y",FVar "#B";delta]]; + res=([],[]); + sub=[]; + def=[]; + ren=["#x";"#y"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp1 *) +(* A,B,Gama |- Delta / A->B,A,Gama |- Delta (A es un atomo) *) +let l_imp1 = { + tip="l_imp1"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FAto "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama], + [delta]]; + res=([TVar "#a",FVar "#A"],[]); + def=[]; + sub=["#x",TApl(FVar "#A",FVar "#B",TVar "#p",TVar "#a")]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp2 *) +(* C->(D->B),Gama |- Delta / C/\D->B,Gama |- Delta *) +let l_imp2 = { + tip="l_imp2"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FAnd(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FImp(FVar "#C",FImp(FVar "#D",FVar "#B"));gama], + [delta]]; + res=([],[]); + def=[]; + sub=["#x",curry(FVar "#C",FVar "#D",FVar "#B","#c","#d",TVar "#p")]; + ren=["#x";"#c";"#d"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp3 *) +(* C->B,D->B,Gama |- Delta / C\/D->B,Gama |- Delta *) +let l_imp3 = { + tip="l_imp3"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FOr(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FImp(FVar "#C",FVar "#B");TVar "#y", + FImp(FVar "#D",FVar "#B");gama], + [delta]]; + res=([],[]); + def=[]; + sub=["#x",left(FVar "#C",FVar "#D",FVar "#B","#c",TVar "#p"); + "#y",right(FVar "#C",FVar "#D",FVar "#B","#d",TVar "#p")]; + ren=["#x";"#y";"#c";"#d"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp4 *) +(* D->B,Gama |- C->D,Delta B,Gama |- Delta / (C->D)->B,Gama |- Delta *) +let l_imp4 = { + tip="l_imp4"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FImp(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama],[delta]; + [TVar "#z",FImp(FVar "#D",FVar "#B");gama],[TVar "#y", + FImp(FVar "#C",FVar "#D")]]; + res=([],[]); + def=[]; + sub=["#x", + TApl(FImp(FVar "#C",FVar "#D"),FVar "#B",TVar "#p", + TApl(FVar "#D",FVar "#B", + TFun("#z",FImp(FVar "#D",FVar "#B"),TVar "#y"), + imp2(FVar "#D",FVar "#C",FVar "#B","#d","#c",TVar "#p")))]; + ren=["#x";"#y";"#z";"#d";"#c"]; + vardelta = false; + ssi = false; + rendelta=[]} + +(* Regla l_imp5 *) +(* (A->False)->B,Gama |- Delta / Not(A)->B,Gama |- Delta *) +let l_imp5 = { + tip="l_imp5"; + heu=false; + ant=true; + pri= TVar "#x",FImp(FNot(FVar "#A"),FVar "#B"); + pre=[[TVar "#x",FImp(FImp(FVar "#A",FFalse),FVar "#B");gama], + [delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp6 *) +(* (C->D/\D->C)->B,Gama |- Delta / (C<->D)->B,Gama |- Delta *) +let l_imp6 = { + tip="l_imp6"; + heu=false; + ant=true; + pri= TVar "#x",FImp(FEqu(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x", + FImp(FAnd(FImp(FVar "#C",FVar "#D"), + FImp(FVar "#D",FVar "#C")),FVar "#B");gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp7 *) +(* B,Gama |- Delta / True->B,Gama |- Delta *) +let l_imp7 = { + tip="l_imp7"; + heu=false; + ant=true; + pri= TVar "#t",FImp(FTrue,FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama],[delta]]; + res=([],[]); + def=[]; + sub=["#x",TApl(FTrue,FVar "#B",TVar "#t",TTrue)]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_imp *) +(* A,Gama |- B / Gama |- A->B,Delta *) +let r_imp = { + tip="r_imp"; + heu=false; + ant=false; + pri= TFun("#x",FVar "#A",TVar "#y"),FImp(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";gama],[TVar "#y",FVar "#B"]]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x";"#y"]; + vardelta = true; + ssi = false; + rendelta=[]} + +(* Regla l_not *) +(* A->False,Gama |- Delta / Not(A),Gama |- Delta *) +let l_not = { + tip="l_not"; + heu=false; + ant=true; + pri= TVar "#x",FNot(FVar "#A"); + pre=[[TVar "#x",FImp(FVar "#A",FFalse);gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_not *) +(* Gama |- A->False,Delta / Gama |- Not(A),Delta *) +let r_not = { + tip="r_not"; + heu=false; + ant=false; + pri= TVar "#x",FNot(FVar "#A"); + pre=[[gama],[TVar "#x",FImp(FVar "#A",FFalse);delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_equ *) +(* A->B/\B->A,Gama |- Delta / A<->B,Gama |- Delta *) +let l_equ = { + tip="l_equ"; + heu=false; + ant=true; + pri= TVar "#x",FEqu(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FAnd(FImp(FVar "#A",FVar "#B"), + FImp(FVar "#B",FVar "#A"));gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_equ *) +(* Gama |- A->B/\B->A,Delta / Gama |- A<->B,Delta *) +let r_equ = { + tip="r_equ"; + heu=false; + ant=false; + pri= TVar "#x",FEqu(FVar "#A",FVar "#B"); + pre=[[gama], + [TVar "#x",FAnd(FImp(FVar "#A",FVar "#B"), + FImp(FVar "#B",FVar "#A"));delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Definicion de la regla VACIA *) +let vACIA = { + tip="vacia"; + heu=false; + ant=false; + pri=gama; + pre=[]; + res=([],[]); + def=[]; + sub=[]; + ren=[]; + vardelta = false; + ssi = false; + rendelta=[]} + +(*---------------------- Reglas heuristicas ------------------------------*) + +(* Regla simetria de igualdad *) +(* / a=b,Gama |- b=a,Delta *) +let sim = { + tip="sim"; + heu=true; + ant=true; + pri= TVar "#x",FEq(FVar "#A",FVar "#a",FVar "#b"); + pre=[]; + res=([],[TSim(FVar "#A",FVar "#a",FVar"#b",TVar"#x"), + FEq(FVar "#A",FVar "#b",FVar "#a")]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x";"#a";"#b"]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla r_refl *) +(* / Gama |- <t>a=a,Delta *) +let r_refl = { + tip="refl"; + heu=true; + ant=false; + pri= TRefl(FVar "#A",FVar "#a"),FEq(FVar "#A",FVar "#a",FVar "#a"); + pre=[]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#a"]; + vardelta = true; + ssi = true; + rendelta=[]} + +let sistema = [inic;l_false;r_true;l_and;r_and;l_imp1;l_imp2;l_imp3; + l_imp5;l_imp6;l_imp7;l_not;r_not;l_equ;r_equ;r_imp; + l_or;r_or;l_imp4] + +(*----------- Proyecciones del tipos de datos Sequente ----------------------*) + +(* Antecedente de un sequente *) +let ante (a,_) = a + +(* Sucedente de un sequente *) +let suce (_,s) = s + +(*----------- Constructores de los tipos de datos ----------------------*) + +(* Simplifica una substitucion es decir elemina las substituciones + inutiles *) +let rec simple = function + | [] -> [] + | ((x,_) as a)::z -> + if String.get x 0 = '#' then simple z else a::simple z + +(* Construye un node de demostracion *) +let consd a l = {arb=a;lisbut=l} + +(* Construye un nodo de un arbol *) +let consa s r sd st = {seq = ref s;reg = ref r;sd = simple sd; + st= simple st} + +(* Construye un nodo de sustitucion *) +let conss r sf sg sd ren sdef ster = + SCons({sReg=ref r;sFor=sf;sGam=sg;sDel=sd; + sRen=ren;sDef=sdef;sTer=ster}) + +(*----------------------- Aplicacion de Reglas ------------------------------*) + +(* Buscar un nombre de variable en una sustitucion, retorna la lista + que contiene la formula que la variable sustituye *) +let rec busque n = function + | [] -> [] + | (x,f)::y -> if x=n then [f] else busque n y + +(* Aplicar una substitucion a una formula, retorna otra formula *) +let rec apl_f s = function + | (FVar y) as x -> (match busque y s with + | [] -> x + | a::_ -> a ) + | (FLisfor y) as x -> (match busque y s with + | [] -> x + | a::_ -> a) + | FAnd (a,b) -> FAnd(apl_f s a, apl_f s b) + | FOr (a,b) -> FOr(apl_f s a, apl_f s b) + | FImp (a,b) -> FImp(apl_f s a, apl_f s b) + | FEqu (a,b) -> FEqu(apl_f s a, apl_f s b) + | FEq (a,b,c) -> FEq(apl_f s a, apl_f s b,apl_f s c) + | FNot a -> FNot(apl_f s a) + | x -> x + +(* Aplicar una sustitucion a una lista de formulas *) +let apl_lf s l = List.map (apl_f s) l + +(* Encuentra un unificador de primer orden de dos formulas proposicionales, + retorna la pareja (e,u), donde e indica exito o fracaso + y u es el unificador principal (si no existe es [] vacia ) *) +let rec unif_f = function + | FAnd(a,b),FAnd(x,y) -> unif_lf([a;b],[x;y]) + | FOr(a,b),FOr(x,y) -> unif_lf([a;b],[x;y]) + | FImp(a,b),FImp(x,y) -> unif_lf([a;b],[x;y]) + | FEqu(a,b),FEqu(x,y) -> unif_lf([a;b],[x;y]) + | FEq(a,b,c),FEq(x,y,z) -> unif_lf([a;b;c],[x;y;z]) + | FVar(a),x -> (true,[a,x]) + | FAto(a),(FPred(_) as x) -> (true,[a,x]) + | FAto(a),(FEq(_) as x) -> (true,[a,x]) + | FPred(a),FPred(x) -> (eq_constr a x,[]) + | FNot(a),FNot(x) -> unif_f(a,x) + | FFalse,FFalse -> (true,[]) + | FTrue,FTrue -> (true,[]) + | _ -> (false,[]) + +and unif_lf = function + | ([],[]) -> (true,[]) + | (x::y,a::b) -> + let (e,u) = unif_f (x,a) in + if e then + let (e1,u1) = unif_lf (apl_lf u y,b) in + if e1 then (true,u@u1) else (false,[]) + else + (false,[]) + | _ -> (false,[]) + +(* Aplicar una substitucion a un lamda termino, retorna otro lambda termino *) +let rec apl_t st sf = function + | (TVar y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | (TLister y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | TApl(f1,f2,t1,t2) -> TApl (apl_f sf f1,apl_f sf f2, + apl_t st sf t1,apl_t st sf t2) + | TFun(x,f,y) -> (match busque x st with + | [] -> TFun(x,apl_f sf f,apl_t st sf y) + | [TVar n] -> TFun(n,apl_f sf f,apl_t st sf y) + | _ -> raise TacticFailure) + | TCase(lf,lt) -> TCase(List.map (apl_f sf) lf,List.map (apl_t st sf) lt) + | TPar(f1,f2,t1,t2) -> TPar(apl_f sf f1,apl_f sf f2, + apl_t st sf t1,apl_t st sf t2) + | TInl(f1,f2,t) -> TInl(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TInr(f1,f2,t) -> TInr(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TFst(f1,f2,t) -> TFst(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TSnd(f1,f2,t) -> TSnd(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TRefl(f1,f2) -> TRefl(apl_f sf f1,apl_f sf f2) + | TSim(f1,f2,f3,t) -> TSim(apl_f sf f1,apl_f sf f2, + apl_f sf f3,apl_t st sf t) + | TLis lt -> TLis (List.map (apl_t st sf) lt) + | TSum(t1,t2) -> TSum (apl_t st sf t1,apl_t st sf t2) + | TZ(f,t) -> TZ(apl_f sf f,apl_t st sf t) + | (TExi y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | TZero f -> TZero(apl_f sf f) + | t -> t + +(* Aplicar substitucion gama delta y una substitucion de terminos lambda + a una lista de formulasT, retorna una lista de formulasT *) +let rec apl_lft (s,gama_0,delta_0) st rendelta = + (* Aplicar una substitucion gama delta y una substitucion de terminos a una + formulaT, retorna una lista de formulasT *) + let apl_fm = function + | (_,FLisfor "GAMA") -> gama_0 + | (TLister x,FLisfor "DELTA") -> + (match busque x rendelta with + | [] -> delta_0 + | a::_ -> apl_lft ([],[],[]) a [] delta_0) + | (_,FLisfor "DELTA") -> delta_0 + | (t,f) -> [apl_t st [] t,apl_f s f] + in + flat_map apl_fm + +(* Aplicar substitucion gama delta y una substitucion de terminos lambda a un + sequente, retorna un nuevo sequente*) +let apl sf st rendelta = function + (l1,l2) -> (apl_lft sf st rendelta l1,apl_lft sf st rendelta l2) + +(* Aplicar la regla r, dada una substitucion. + Retorna una lista de sequentes *) +let aplr_s subs = List.map (apl (subs.sFor,subs.sGam,subs.sDel) + subs.sDef subs.sRen) !(subs.sReg).pre + +(* Componer dos substituciones de lambda terminos. Aplica la primera + sobre la segunda *) +let rec comp_st st = function + | [] -> st + | (x,y)::z -> (x,apl_t st [] y)::comp_st st z + +(* Renombrar las variables izquierdas de una sustitucion *) +let rec ren_izq ren = function + | [] -> [] + | ((x,y) as a)::z -> match busque x ren with + | [TVar a] -> (a,y)::ren_izq ren z + | _ -> a::ren_izq ren z + +(* Indica si dos formulas son iguales *) +let iguales_f f1 f2 = + let (e,u) = unif_f(f1,f2) in + e & u = [] + +(*------------------- Unificador para lambda terminos --------------------*) + +(* Encuentra un unificador de primer orden de dos lambda terminos, + retorna la pareja (e,u), donde e indica exito o fracaso + y u es el unificador principal (si no existe es [] vacia ). + TPara los terminos que contienen formulas recibe el unificador de + ellas *) +let rec unif_t sf = function + | (TVar x,((TVar y) as y_0)) -> + if (x = y) then (true,[]) else (true,[x,apl_t [] sf y_0]) + | (TVar x, y) -> (true,[x,apl_t [] sf y]) + | TApl(f,ff,t,tt),TApl(f1,ff1,t1,tt1) -> + unif_lft sf [f;ff][f1;ff1][t;tt][t1;tt1] + | TZ(f,t), TZ(f1,t1) -> unif_lft sf [f][f1][t][t1] + | (TExi x,((TExi y) as y_0)) -> + if (x = y) then (true,[]) else (true,[x,apl_t [] sf y_0]) + | TZero f, TZero f1 -> unif_lft sf [f][f1][][] + | TTrue,TTrue -> (true,[]) + | TFun(x,f,t),TFun(a,f1,t1) -> unif_lft sf [f][f1][t][t1] + | TPar(f,ff,t,tt),TPar(f1,ff1,t1,tt1) -> + unif_lft sf [f;ff][f1;ff1] [t;tt][t1;tt1] + | TInl(f,ff,t),TInl(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TInr(f,ff,t),TInr(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TFst(f,ff,t),TFst(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TSnd(f,ff,t),TSnd(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TRefl(f,ff),TRefl(f1,ff1) -> unif_lft sf [f;ff][f1;ff1][][] + | TSim(f1,f2,f3,t),TSim(f1',f2',f3',t') -> + unif_lft sf [f1;f2;f3] [f1';f2';f3'][t][t'] + | _ -> (false,[]) + +and iguales_lf sf = function + | ([],[]) -> true + | (x::y,a::b) -> + if iguales_f (apl_f sf x) (apl_f sf a) then + iguales_lf sf (y,b) + else + false + | _ -> false + +and unif_lt sf = function + | ([],[]) -> (true,[]) + | (x::y,a::b) -> + let (e,u) = unif_t sf (x,a) in + if e then + let (e1,u1) = unif_lt sf (y,b) in + if e1 then (true,u@u1) + else (false,[]) + else + (false,[]) + | _ -> (false,[]) + +and unif_lft sf lf lf1 lt lt1 = + if iguales_lf sf (lf,lf1) then + unif_lt sf (lt,lt1) + else + (false,[]) + +(* Indica si dos terminos son iguales *) +let iguales_t t1 t2 = + let (e,u) = unif_t [] (t1,t2) in + e & u = [] + +(* Indica si dos formulas son iguales. Retorna una pareja con el exito + y un unificador de los dos lambda terminos *) +let iguales_unif uf tr ts fr fs = + if iguales_f fr fs then + let (e,ut) = unif_t uf (ts,tr) in + if e then + (true,ut) + else + raise TacticFailure + else + (false,[]) + +(* Crear una nueva variable *) +let hipvar = ref ((id_of_string "#")::[]) + +let genvar () = + let id = next_ident_away + (id_of_string "H") + !hipvar in + (hipvar := id::(!hipvar); string_of_id id) + +(* Lista de terminos de una substitucion *) +let listerm = List.map snd + +(* Lista de variables de una lista de formulasS *) +let rec lisvar = function + | [] -> [] + | (TVar x,_)::y -> x::lisvar y + | (TExi x,_)::y -> x::lisvar y + | _::y -> lisvar y + +(* Lista de formulas de una lista de formulasS *) +let rec lisfor = function + | [] -> [] + | (TVar _,x)::y -> x::lisfor y + | (TExi _,x)::y -> x::lisfor y + | _::y -> lisfor y + +(* Recibe una lista de variables, retorna un renombramiento de ellas *) +let renombra = List.map (function x -> (x,TVar(genvar()))) + +(* Obtiene un renombramiento de todas las metavariables delta *) +let renombradelta s rend= + let l = lisvar (suce s) in + List.map (function x -> (x,renombra l)) rend + +(* Obtiene una substitucion de las metavariables delta, por lista de + terminos *) +let rec subsdelta = function + | [] -> [] + | (x,y)::y_0 -> match listerm y with + | [] -> [] + | [a] -> (x,a)::subsdelta y_0 + | a -> (x,TLis a)::subsdelta y_0 + +(* Indica si una formula pertenece a una lista de formulasT. + Retorna una pareja con el exito y una unificacion de los lambda terminos *) +let rec pertenece uf ant tr fr = function + | [] -> (false,[]) + | (TLister _,_)::y -> pertenece uf ant tr fr y + | (ts,fs)::y -> + let (e,ut) = + if ant then + iguales_unif uf ts tr fr fs + else + iguales_unif uf tr ts fr fs + in + if e then + (true,ut) + else + pertenece uf ant tr fr y + +(* Indica si la primera lista de formulasT contiene la segunda. + Retorna una pareja con el exito y una unificacion de los lambda terminos *) +let rec contiene uf ant l = function + | [] -> (true,[]) + | (TLister _,_)::y -> contiene uf ant l y + | (tr,fr)::y -> + let (e1,s1) = pertenece uf ant tr fr l in + if e1 then + let (e2,s2) = contiene uf ant l y in + if e2 then + (true,s1@s2) + else + (false,[]) + else + (false,[]) + +(* Decide si un secuente cumple con las restricciones de aplicacion de una + regla. Recibe el unificador de la regla con la restriccion. Retorna una + pareja con el exito y las unificaciones de lambda terminos del antecedente + y el sucedente del secuente *) +let cumple uf res = function (seql,seqr) -> + let (resl,resr) = apl (uf,[],[]) [] [] res in + let (e1,s1) = contiene uf true seql resl in + if e1 then + let (e2,s2) = contiene uf false seqr resr in + if e2 then + (true,s1,s2) + else + (false,[],[]) + else + (false,[],[]) + +(* Compone una substitucion de formulas con una substitucion de terminos *) +let rec comp_sfst uf = function + | [] -> [] + | (x,y)::z -> (x,apl_t [] uf y)::comp_sfst uf z + +(* Crea una substitucion para las variables de un lambda termino, basado + en la regla que aplica *) +let cree_sub s uf ter t ul ur r = + let lv = + if r.vardelta then ["DELTA",FLis(lisfor (suce s))] else [] + in + let rendelta = renombradelta s r.rendelta in + let ren = (renombra r.ren) @ (subsdelta rendelta) in + let sd0 = + if r.ant then + ur (* Calcular definicion basica *) + else + match unif_t uf (t,ter) with + | (false,_) -> raise(TacticFailure) + | (_,u) -> ur@u + in + let sd1 = comp_st r.def sd0 in + let sd2 = comp_sfst (uf@lv) sd1 in (*Susbstituir var. proposicionales *) + let sd = comp_st ren sd2 in (* Componer con un renombramiento *) + let st0 = + if r.ant then (* Calcular sustitucion basica *) + match unif_t uf (ter,t) with + | (false,_) -> raise(TacticFailure) + | (_,u) -> ul@u + else + ul + in + let st1 = comp_st st0 r.sub in + let st2 = comp_sfst (uf@lv) st1 in (*Susbstituir var. proposicionales *) + let st3 = ren_izq ren st2 in (* Componer con un renombramiento *) + let st = comp_st ren st3 in + (sd,st,rendelta) + +(* Decide se una regla dada es aplicable sobre un termino (tf) + de un secuente y un lado de reduccion o. Retorna la sustitucion + apropiada para la regla o SNil si no existe *) + +let rec aplicable s lf tf o = function + ({ant=ant;pri=ter,pri;res=res}) as r -> + if o<>ant then + SNil + else + (match tf with + | (TLister _,_) -> SNil + | (t,f) -> + let (ef,uf) = unif_f(pri,f) in + if ef then + let (et,ul,ur) = cumple uf res s in + if et then + let (gam,del) = if ant then (lf,suce s) + else (ante s,lf) in + let (sd,st,rn) = cree_sub s uf ter t ul ur r in + conss r uf gam del rn sd st + else SNil + else SNil) + +(* Dado una regla, retorna una posicion donde la regla sea aplicable. RNil + si no existe *) +let rec escoja_termino r s o rseq lacum = function + | [] -> + if o=0 then + escoja_termino r s 2 [] lacum rseq + else if o=1 then + escoja_termino r s 2 [] [] rseq + else + RNil + | t::y -> + let oo = if o=0 then 1 else o in + (match aplicable s (lacum@y) t (oo=1) r with + | SNil -> escoja_termino r s oo rseq (lacum@[t]) y + | SCons(s) -> + if oo=1 then RCons(s,[],lacum,(y,rseq)) + else RCons(s,[],lacum,([],y))) + +(* Dado un secuente y un sistema de reglas + retorna una sustitucion apropiada para la regla, o RNil si no existe *) +let rec escoja_regla s (lrseq,lac) = function + | [] -> RNil + | (r::y) as lreg -> + (match escoja_termino r s 0 (suce lrseq) lac (ante lrseq) with + | RNil -> escoja_regla s (s,[]) y + | RCons(subs,_,lanew,lrnew) -> RCons(subs,lreg,lanew,lrnew)) + +(* Si una formula proposicional existe en una lista de formulas *) +let rec existeprop f = function + | [] -> false + | x::y -> if iguales_f f x then true else existeprop f y + +(* Buscar una formula proposicional en una lista de formulasT, + retorna el termino o TZero si no la encuentra *) +let rec busqueprop f = function + | [] -> TZero(FFalse) + | (tt,ff)::y -> if iguales_f f ff then tt else busqueprop f y + +(* Crear un termino como aplicaciones sucesivas del subobjetivo sobre las + hipotesis *) +let rec ter_subobjetivo lisprop subobj = function + | [] -> (fst subobj) + | (x,f)::y -> + if existeprop f lisprop then + ter_subobjetivo lisprop subobj y + else + (match snd(subobj) with + | FImp(a,b) -> ter_subobjetivo (f::lisprop) + (TApl(a,b,fst(subobj),x),b) y + | _ -> TZero(FFalse)) + +(* Convierte la lista del succedente en una disyuncion *) +let rec disyuncion = function + | [] -> FFalse + | [a] -> a + | x::y -> FOr(x,disyuncion y) + +(* Convierte la lista del antecedente en una implicacion *) +let rec implicacion dis vp = function + | [] -> dis + | x::y -> + if (existeprop x vp) then + implicacion dis vp y + else + FImp(x,implicacion dis vp y) + +(* Lista de proposiciones de un secuente sin repetidos *) +let rec it_propos lisacum = function + | [] -> lisacum + | (_,f)::y -> + if (existeprop f lisacum) then + it_propos lisacum y + else + it_propos (lisacum@[f]) y + +let proposiciones = it_propos [] + +(* Generar una subobjetivo de la demostracion de tal manera que + la validez del sequente original sea equivalente a la validez del + subobjetivo *) +let subobjetivo s vp = + let dis = disyuncion (proposiciones (suce s)) in + let ter = TExi(genvar()) in + (ter,implicacion dis vp (proposiciones (ante s))),dis + +(* Crea una substitucion que supone un subobjetivo demostrado *) +let rec termino_caso fapp f = function + | FOr(a,b) -> + let id1 = genvar() in + let t1 = TVar(id1) in + let id2 = genvar() in + let t2 = TVar(id2) in + if iguales_f a f then + TCase([a;b;f],[TFun(id1,a,t1);TFun(id2,b,TZero(f));fapp]) + else + TCase([a;b;f],[TFun(id1,a,TZero(f));TFun(id2,b,termino_caso t2 f b); + fapp]) + | _ -> fapp + +let rec it_subs_subobj subs sec fapp tip = function + | [] -> subs + | ((TVar x,f) as a)::y -> + let t = busqueprop f sec in + if t <> TZero(FFalse) then + it_subs_subobj ((x,apl_t subs [] t)::subs) sec fapp tip y + else + it_subs_subobj ((x,termino_caso fapp f tip)::subs) (a::sec) + fapp tip y + | _ -> assert false + +let subs_subobj fapp tip s = it_subs_subobj [] [] fapp tip s + +let rec esta_en_case l = function + | TApl(_,_,t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TFun(_,_,t) -> + esta_en_case l t + | TPar(_,_,t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TInl(_,_,t) -> + esta_en_case l t + | TInr(_,_,t) -> + esta_en_case l t + | TFst(_,_,t) -> + esta_en_case l t + | TSnd(_,_,t) -> + esta_en_case l t + | TZ(_,t) -> + esta_en_case l t + | TSum(t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TCase([f1;f2;f3],[t1;t2;t3]) -> + (match l with + | [ff1;ff2;ff3] -> + if (iguales_f f1 ff1) & (iguales_f f2 ff2) & + (iguales_f f3 ff3) then + true + else + (esta_en_case l t1) or (esta_en_case l t2) + | _ -> assert false) + | _ -> false + +let rec busque_termino t = function + | [] -> (false,"",false) + | (x,v,o)::y -> if iguales_t t x then (true,v,o) else busque_termino t y + +(* Sistema de reglas para simplificar terminos *) +let rec sistreg lcase = function + | TApl(_,_,TFun (x,_,t),t1) -> apl_t [x,t1] [] t + | TFst(_,_,TPar(_,_,t,_)) -> t + | TSnd(_,_,TPar(_,_,_,t)) -> t + (* Simplificacion con TZero *) + | TApl(_,f,TZero _,t) -> TZero f + | TApl(_,f,t,TZero _) -> TZero f + | TFun(x,f1,TZero f2) -> TZero (FImp(f1,f2)) + | TPar(f1,f2,TZero _,t2) -> TZero (FAnd(f1,f2)) + | TPar(f1,f2,t1,TZero _) -> TZero (FAnd(f1,f2)) + | TInl(f1,f2,TZero _) -> TZero (FOr(f1,f2)) + | TInr(f1,f2,TZero _) -> TZero (FOr(f1,f2)) + | TFst(f1,f2,TZero _) -> TZero f1 + | TSnd(f1,f2,TZero _) -> TZero f2 + | TZ(f,TZero _) -> TZero f + | TSum(TZero _,t) -> t + | TSum(t,TZero _) -> t + | TCase([_;_;f],[_;_;TZero _]) -> TZero f + | TSum(TFun(v1,ff1,t1),TFun(v2,ff2,t2)) -> + TFun(v1,ff1,TSum(t1,apl_t [v2,(TVar v1)][] t2)) + (* Simplificacion del case *) + | TApl(f1,f2,TCase([a;b;FImp(c,d)],[TFun(v1,ff1,t1); + TFun(v2,ff2,t2);t3]),t) -> + TCase([a;b;f2],[TFun(v1,ff1,TApl(c,d,t1,t)); + TFun(v2,ff2,TApl(c,d,t2,t));t3]) + | TApl(f1,f2,t,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f2],[TFun(v1,ff1,TApl(f1,f2,t,t1)); + TFun(v2,ff2,TApl(f1,f2,t,t2));t3]) + | TPar(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]),t) -> + TCase([a;b;FAnd(f1,f2)],[TFun(v1,ff1,TPar(f1,f2,t1,t)); + TFun(v2,ff2,TPar(f1,f2,t2,t));t3]) + | TPar(f1,f2,t,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FAnd(f1,f2)],[TFun(v1,ff1,TPar(f1,f2,t,t1)); + TFun(v2,ff2,TPar(f1,f2,t,t2));t3]) + | TInl(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FOr(f1,f2)],[TFun(v1,ff1,TInl(f1,f2,t1)); + TFun(v2,ff2,TInl(f1,f2,t2));t3]) + | TInr(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FOr(f1,f2)],[TFun(v1,ff1,TInr(f1,f2,t1)); + TFun(v2,ff2,TInr(f1,f2,t2));t3]) + | TFst(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f1],[TFun(v1,ff1,TFst(f1,f2,t1)); + TFun(v2,ff2,TFst(f1,f2,t2));t3]) + | TSnd(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f2],[TFun(v1,ff1,TSnd(f1,f2,t1)); + TFun(v2,ff2,TSnd(f1,f2,t2));t3]) + | TZ(f,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f],[TFun(v1,ff1,TZ(f,t1)); + TFun(v2,ff2,TZ(f,t2));t3]) + | TSum((TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]) as tC1), + (TCase([a';b';c'], + [TFun(v1',ff1',t1');TFun(v2',ff2',t2');t3']) as tC2)) -> + if (iguales_f a a') & (iguales_f b b') then + TCase([a;b;c],[TFun(v1,ff1,TSum(t1,apl_t [v1',(TVar v1)] [] t1')); + TFun(v2,ff2,TSum(t2,apl_t [v2',(TVar v2)] [] t2')); + TSum(t3,t3')]) + else if (esta_en_case [a;b;c] t1') or (esta_en_case [a;b;c] t2') then + TCase([a';b';c'],[TFun(v1',ff1',TSum(t1',tC1)); + TFun(v2',ff2',TSum(t2',tC1));t3']) + else + TCase([a;b;c],[TFun(v1,ff1,TSum(t1,tC2));TFun(v2,ff2,TSum(t2,tC2));t3]) + | TCase([_;_;f],[TFun(_,_,TZero _);TFun(_,_,TZero _);_]) -> TZero(f) + | TCase([a;b;f],[TFun(v1,f1,t1) as tt1;TFun(v2,f2,t2) as tt2;t]) -> + if iguales_t t1 t2 then t2 + else + let (exi,var,ori) = busque_termino t lcase in + if exi then + if ori then apl_t [v1,TVar var][] t1 + else apl_t [v1, TVar var] [] t2 + else raise(NoAplica) + | TSum(t1,t2)-> + if (iguales_t t1 t2) then t1 + else raise (NoAplica) + | TPar(_,_,TFst(_,_,t1),TSnd(_,_,t2)) -> + if iguales_t t1 t2 then + t1 + else raise(NoAplica) + | _ -> raise(NoAplica) + +(* Aplicacion de una regla sobre un termino, si no pudo aplicar retorna + NoAplica. Estrategia mas izquierdo, menos profundo *) + +let pr l = List.hd l + +let sn l = List.hd(List.tl l) + +let rec it_apl_listsistr lcase lacum siapl = function + | [] -> (lacum,siapl) + | x::y -> + let (xp,exi) = + try (apl_sistr lcase x,true) with NoAplica -> (x,false) + in + it_apl_listsistr lcase (lacum@[xp]) (exi or siapl) y + +and apl_listsistr lcase l = it_apl_listsistr lcase [] false l + +and apl_sistr_try lcase x = + try (apl_sistr lcase x,true) with NoAplica -> (x,false) + +and apl_sistr lcase a = + try + sistreg lcase a + with NoAplica -> + (match a with + | TApl(f1,f2,t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TApl(f1,f2,pr lt,sn lt) + else raise(NoAplica) + | TFun(x,f,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TFun(x,f,pr lt) + else raise(NoAplica) + | TPar(f1,f2,t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TPar(f1,f2,pr lt,sn lt) + else raise(NoAplica) + | TInl(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TInl(f1,f2,pr lt) + else raise(NoAplica) + | TInr(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TInr(f1,f2,pr lt) + else raise(NoAplica) + | TFst(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TFst(f1,f2,pr lt) + else raise(NoAplica) + | TSnd(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TSnd(f1,f2,pr lt) + else raise(NoAplica) + | TZ(f,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TZ(f,pr lt) + else raise(NoAplica) + | TSum(t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TSum(pr lt,sn lt) + else raise(NoAplica) + | TCase([f1;f2;f3],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]) -> + let (t1',exi1) = apl_sistr_try ((t3,v1,true)::lcase) t1 in + let (t2',exi2) = apl_sistr_try ((t3,v2,false)::lcase) t2 in + let (t3',exi3) = apl_sistr_try lcase t3 in + if (exi1 or exi2 or exi3) then + TCase([f1;f2;f3],[TFun(v1,ff1,t1'); + TFun(v2,ff2,t2');t3']) + else raise(NoAplica) + | _ -> raise(NoAplica)) + +(* Indica si hay un zero en el termino *) +let rec tiene_zero = function + | TApl(_,_,t,t1) -> tiene_zero(t) or tiene_zero(t1) + | TFun(_,_,t) -> tiene_zero(t) + | TPar(_,_,t,t1) -> tiene_zero(t) or tiene_zero(t1) + | TInl(_,_,t) -> tiene_zero(t) + | TInr(_,_,t) -> tiene_zero(t) + | TFst(_,_,t) -> tiene_zero(t) + | TSnd(_,_,t) -> tiene_zero(t) + | TCase(_,[t;t1;t2]) -> tiene_zero (t) or tiene_zero (t1) or + tiene_zero(t2) + | TZ(_,t) -> tiene_zero(t) + | TZero(f) -> true + | a -> false + +(* Elemento de la posicion p de una lista *) +let rec lis_pos p = function + | [] -> raise(TacticFailure) + | x::y -> if (p=0) then x else lis_pos (p-1) y + +(* Genera una copia de una formula con reemplazo de los terminos de tipo + FLis por las formulas que aparecen en la posicion p'esima de las + listas respectivas *) +let rec copia_f p = function + | FAnd(a,b) -> FAnd(copia_f p a,copia_f p b) + | FEqu(a,b) -> FEqu(copia_f p a,copia_f p b) + | FOr(a,b) -> FOr(copia_f p a,copia_f p b) + | FImp(a,b) -> FImp(copia_f p a,copia_f p b) + | FNot(a) -> FNot(copia_f p a) + | FLis lf -> lis_pos p lf + | a -> a + +(* Genera una copia de un termino con reemplazo de los terminos de tipo + Lista por los terminos que aparecen en la posicion p'esima de las listas + respectivas *) +let rec copia_t sinplus p = function + | TApl(f,f1,t,t1) -> TApl(copia_f p f,copia_f p f1, + copia_t sinplus p t,copia_t sinplus p t1) + | TFun(x,f,t) -> TFun(x,copia_f p f,copia_t sinplus p t) + | TPar(f,f1,t,t1) -> TPar(copia_f p f,copia_f p f1, + copia_t sinplus p t,copia_t sinplus p t1) + | TInl(f,f1,t) -> TInl(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TInr(f,f1,t) -> TInr(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TFst(f,f1,t) -> TFst(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TSnd(f,f1,t) -> TSnd(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TLis lt -> lis_pos p lt + | TSum(t,t1) -> let s = copia_t sinplus p t in + let s1 = copia_t sinplus p t1 in + if sinplus then + if tiene_zero s then s1 + else s + else TSum(s,s1) + | TCase(lf,lt) -> + TCase(List.map (copia_f p) lf,List.map (copia_t sinplus p) lt) + | TZ(f,t) -> TZ(copia_f p f,copia_t sinplus p t) + | TZero(f) -> TZero(copia_f p f) + | a -> a + +(* Reescribe un lambda termino con constructores TZero y TSum a un lambda + termino *) +let rec normal t = + try normal(apl_sistr [] t) with NoAplica -> copia_t true 0 t + +(*-------------------- Procedimiento de decision --------------------------*) + +(* Indica que no debe buscar mas en el arbol *) +let no_back rev = function + {arb=a;lisbut=l} -> (a <> Nil) & (l=[] or rev) + +(* Funcion que dice si un sequente es demostrable o no. Retorna + un arbol de demostracion del sequente, o vacio. *) +let rec naive intu vp = function + (l,r) as s -> naive_s s intu (s,[]) vp sistema + +(* Dado un secuente s y un subsecuente (en el cual busca una formula + para aplicarle una regla), encuentra un elemento de demostracion. + Si intu es true genera subojetivos equivalentes al original en caso + de no encontrar la demostracion. Si es false, retorna el arbol Vacio*) + +and naive_s s intu seq_acum vp listareg = + (match escoja_regla s seq_acum listareg with + | RNil -> + if intu then + let obj = subobjetivo s vp in + let fapp = ter_subobjetivo vp (fst obj) (ante s) in + let subs_sub = subs_subobj fapp (snd obj) (suce s) in + consd (Cons(Nil,consa s vACIA subs_sub [],Nil)) + [fst obj] + else consd Nil [] + | RCons(subs,lreg,lanew,lrnew) -> + let reversible = !(subs.sReg).ssi or subs.sDel = [] in + ( match aplr_s subs with + | [] -> + consd(Cons(Nil, + consa s !(subs.sReg) subs.sDef subs.sTer, + Nil)) [] + | [a] -> + let {arb=a1;lisbut=l1} as al = (naive intu vp a) in + if no_back reversible al then + consd (Cons(a1, + consa s !(subs.sReg) subs.sDef subs.sTer, + Nil)) l1 + else if (not (reversible)) then + naive_s s intu (lrnew,lanew) vp lreg + else + consd Nil [] + | a::(b::_) -> + let {arb=a1;lisbut=l1} as al1 = naive intu vp a in + let {arb=a2;lisbut=l2} as al2 = naive intu vp b in + if (no_back reversible al1) & (no_back reversible al2) then + consd (Cons(a1, + consa s !(subs.sReg) subs.sDef subs.sTer, + a2)) (l1@l2) + else if (not (reversible)) then + naive_s s intu (lrnew,lanew) vp lreg + else + consd Nil [])) + +(* Crea nuevas substituciones para cada variable del sucedente *) +let rec nuevas_subs t p = function + | [] -> [] + | x::y -> (x,copia_t false p t) :: nuevas_subs t (p+1) y + +(* Busca todos lo Delta que aparecen en el lado izquierdo de la + sustitucion y lo reemplaza por las variables del sucedente del secuente *) +let rec remplacedelta lisv = function + | [] -> [] + | ("Delta",t)::y -> nuevas_subs t 0 lisv @ remplacedelta lisv y + | x::y -> x :: remplacedelta lisv y + +(* Calcula una lista de susbtituciones sobre las variables que aparecen al + en el sucedente del secuente de un arbol de demostracion. De tal forma + que al componerlas y aplicarlas se obtienen los lambda terminos que expresan + la demostracion*) +let rec subs_t = function + | Nil -> [] + | Cons(a,{seq=seq;sd=sd0;st=st0;reg=r},b) -> + let sd = if (!r.rendelta <> []) or (!r.vardelta) then + remplacedelta (lisvar (suce !seq)) sd0 + else sd0 in + let st = if (!r.rendelta <> []) or (!r.vardelta) then + remplacedelta (lisvar (suce !seq)) st0 + else st0 in + [sd] @ (subs_t a) @ [st] @ (subs_t b) + +(* Funcion que compone recursivamente una substitucion con una lista + de substituciones *) +let rec componga_r s = function + | [] -> s + | x::y -> componga_r (comp_st x s) y + +(* Dado un arbol de demostracion de un secuente, calcula los lambda terminos + que expresan la demostracion *) +let lterm = function + | Nil -> [] + | (Cons(_,{seq=seq},_)) as a -> + List.map (function (x,y) -> (x,normal y)) (componga_r [] (subs_t a)) + +(*--------------------- Interface con Coq ---------------------------------*) +(*-- Convierte una formula cci a una formula notacion Tauto --*) + +let tAUTOFAIL (g:goal sigma) = + (errorlabstrm "TAUTOFAIL" [< 'sTR "Tauto failed.">] : + goal list sigma * validation) + +let is_imp_term t = + match kind_of_term t with + | IsProd (_,_,b) -> (not((dependent (mkRel 1) b))) + | _ -> false + +(* Chet's code depends on the names of the logical constants. *) + +let tauto_of_cci_fmla gls cciterm = + let rec tradrec cciterm = + if pf_is_matching gls (and_pattern ()) cciterm then + match pf_matches gls (and_pattern ()) cciterm with + | [(1,a);(2,b)] -> FAnd(tradrec a,tradrec b) + | _ -> assert false + else if pf_is_matching gls (or_pattern ()) cciterm then + match pf_matches gls (or_pattern ()) cciterm with + | [(1,a);(2,b)] -> FOr(tradrec a,tradrec b) + | _ -> assert false + else if pf_is_matching gls (iff_pattern ()) cciterm then + match pf_matches gls (iff_pattern ()) cciterm with + | [(1,a);(2,b)] -> FEqu(tradrec a,tradrec b) + | _ -> assert false + else if pf_is_matching gls (eq_pattern ()) cciterm then + match pf_matches gls (eq_pattern ()) cciterm with + | [(1,a);(2,b);(3,c)] -> FEq(FPred a,FPred b, FPred c) + | _ -> assert false + else if pf_is_matching gls (not_pattern ()) cciterm then + match pf_matches gls (not_pattern ()) cciterm with + | [(1,a)] -> FNot(tradrec a) + | _ -> assert false + else if pf_is_matching gls (false_pattern ()) cciterm then + FFalse + else if pf_is_matching gls (true_pattern ()) cciterm then + FTrue + else if is_imp_term cciterm then + match kind_of_term cciterm with + | IsProd (_,a,b) -> FImp(tradrec a,tradrec (pop b)) + | _ -> assert false + else FPred cciterm + in + tradrec (whd_betaiota cciterm) + +(*-- Retorna una lista de todas las variables proposicionales que + aparescan en una lista de formulasS --*) +let rec lisvarprop = function + | [] -> [] + | (_,((FPred x) as fx))::y -> fx::lisvarprop y + | _::y -> lisvarprop y + +(*-- Dado el ambiente COQ construye el lado izquierdo de un secuente + (hipotesis) --*) +let rec constr_lseq gls = function + | [] -> [] + | (idx,c,hx)::rest -> + match Retyping.get_sort_of (pf_env gls) (project gls) hx with + | Prop Null -> + (TVar(string_of_id idx),tauto_of_cci_fmla gls hx) + :: constr_lseq gls rest + |_-> constr_lseq gls rest + +(*-- Dado un estado COQ construye el lado derecho de un secuente + (conclusion) --*) +let constr_rseq gls but = [TVar(genvar()), + tauto_of_cci_fmla gls but] + +(*-- Calula la posicion de la lista de un elemento --*) +let rec pos_lis x = function + | [] -> raise TacticFailure + | a::r -> if (x=a) then 1 else 1 + (pos_lis x r) + +(*-- Construye un termino constr dado una formula tauto --*) +let rec cci_of_tauto_fml () = + let cAnd = global_reference CCI (id_of_string "and") + and cOr = global_reference CCI (id_of_string "or") + and cFalse = global_reference CCI (id_of_string "False") + and cTrue = global_reference CCI (id_of_string "True") + and cEq = global_reference CCI (id_of_string "eq") in + function + | FAnd(a,b) -> applistc cAnd + [cci_of_tauto_fml () a;cci_of_tauto_fml () b] + | FOr(a,b) -> applistc cOr + [cci_of_tauto_fml () a; cci_of_tauto_fml () b] + | FEq(a,b,c)-> applistc cEq + [cci_of_tauto_fml () a; cci_of_tauto_fml () b; + cci_of_tauto_fml () c] + | FImp(a,b) -> mkArrow (cci_of_tauto_fml () a) (cci_of_tauto_fml () b) + | FPred a -> a + | FFalse -> cFalse + | FTrue -> cTrue + | FLis lf -> raise TacticFailure + | FVar a -> raise TacticFailure + | FAto a -> raise TacticFailure + | FLisfor a -> raise TacticFailure + | _ -> anomaly "Tauto:cci_of_tauto_fml" + +let search env id = + try + mkRel (fst (lookup_rel_id id (Environ.rel_context env))) + with Not_found -> + if mem_named_context id (Environ.named_context env) then + mkVar id + else + global_reference CCI id + +(*-- Construye un termino constr de un termino tauto --*) +let cci_of_tauto_term env t = + let cFalse_ind = global_reference CCI (id_of_string "False_ind") + and cconj = global_reference CCI (id_of_string "conj") + and cor_ind = global_reference CCI (id_of_string "or_ind") + and cor_introl = global_reference CCI (id_of_string "or_introl") + and cor_intror = global_reference CCI (id_of_string "or_intror") + and cproj1 = global_reference CCI (id_of_string "proj1") + and cproj2 = global_reference CCI (id_of_string "proj2") + and crefl = global_reference CCI (id_of_string "refl_equal") + and csim = global_reference CCI (id_of_string "sym_eq") + and ci = global_reference CCI (id_of_string "I") + in + let rec ter_constr l = function + | TVar x -> (try (try mkRel(pos_lis x l) + with TacticFailure -> + search env (id_of_string x)) + with _ -> raise TacticFailure) + | TZ(f,x) -> applistc cFalse_ind + [cci_of_tauto_fml () f;ter_constr l x] + | TSum(t1,t2) -> ter_constr l t1 + | TExi (x) -> (try search env (id_of_string x) with + _ -> raise TacticFailure) + | TApl(_,_,t1,t2) -> applistc (ter_constr l t1) [ter_constr l t2] + | TPar(f1,f2,t1,t2) -> applistc cconj + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + ter_constr l t1;ter_constr l t2] + | TInl(f1,f2,t) -> applistc cor_introl + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + ter_constr l t] + | TInr(f1,f2,t) -> applistc cor_intror + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + ter_constr l t] + | TFst(f1,f2,t) -> applistc cproj1 + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + ter_constr l t] + | TSnd(f1,f2,t) -> applistc cproj2 + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + ter_constr l t] + | TRefl(f1,f2) -> applistc crefl + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2] + | TSim(f1,f2,f3,t) -> applistc csim + [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2; + cci_of_tauto_fml () f3;ter_constr l t] + | TCase(lf,lt) -> applistc cor_ind + ((List.map (cci_of_tauto_fml ()) lf)@ + (List.map (ter_constr l) lt)) + | TFun(n,f,t) -> + Environ.lambda_name env + (Name(id_of_string n ), cci_of_tauto_fml () f,ter_constr (n::l) t) + | TTrue -> ci + | TLis _ -> raise TacticFailure + | TLister _ -> raise TacticFailure + | TZero _ -> raise TacticFailure + in + ter_constr [] t + +let cutUsing id t = (tclTHENS (Tactics.cut t) ([intro_using id;tclIDTAC])) + +let cut_in_parallelUsing idlist l = + let rec prec l_0 = function + | [] -> tclIDTAC + | h::t -> + (tclTHENS (cutUsing (id_of_string (List.hd l_0)) h) + ([prec (List.tl l_0) t;tclIDTAC])) + in + prec (List.rev idlist) (List.rev l) + +let exacto tt gls = + let tac = + try + let t = cci_of_tauto_term (pf_env gls) tt in + exact_no_check t + with _ -> tAUTOFAIL (* Efectivamente, es cualquier cosa!! *) + in tac gls (* Esto confirma el comentario anterior *) + +let subbuts l hyp = cut_in_parallelUsing + (lisvar l) + (List.map (cci_of_tauto_fml ()) (lisfor l)) + +let t_exacto = ref (TVar "#") + +let tautoOR ti gls = + let thyp = pf_hyps gls in + hipvar := ids_of_named_context thyp; + let but = pf_concl gls in + let seq = (constr_lseq gls thyp, constr_rseq gls but) in + let vp = lisvarprop (ante seq) in + match naive ti vp seq with + | {arb=Nil} -> + tAUTOFAIL gls + | {arb=arb;lisbut=l} -> + let se = apl ([],[],[]) (lterm arb) [] seq in + let tt = fst(List.hd(suce se)) in + (t_exacto := tt; + subbuts l thyp gls) + +let tautoOR_0 gl = + tclORELSE + (tclTHENSI (tautoOR false) [fun gl -> exacto (!t_exacto) gl]) + tAUTOFAIL gl + +let intuitionOR = + tclTRY (tclTHEN + (tclTHENSI (tautoOR true) [fun gl -> exacto (!t_exacto) gl]) + default_full_auto) + +(*--- Mixed code Chet-Cesar ---*) + +let rec prove tauto_intu g = + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_hypothesis out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_absurdity_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_and_elim out_some) (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_atomic_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_and_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_or_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tclTHEN dyck_and_intro (prove tauto_intu)) + (tclORELSE (tclTHEN dyck_imply_intro (prove tauto_intu)) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_or_elim out_some) (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen (* 28/5/99, ajout par HH *) + (compose dyck_imply_imply_elim out_some) + (prove tauto_intu))) + tauto_intu)))))))))) g + +let tauto gls = + let strToOccs x = ([],Nametab.constant_sp_of_id (id_of_string x)) in + (tclTHEN (onAllClausesLR + (unfold_option [strToOccs "not";strToOccs "iff"])) + (prove tautoOR_0)) gls + +let intuition gls = + let strToOccs x = ([],Nametab.constant_sp_of_id (id_of_string x)) in + (tclTHEN + ((tclTHEN (onAllClausesLR + (unfold_option [strToOccs "not";strToOccs "iff"])) + (prove intuitionOR))) intros) gls + +let tauto_tac = hide_atomic_tactic "Tauto" tauto + +let intuition_tac = hide_atomic_tactic "Intuition" intuition + diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index f546a1aa1..7826e3882 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -326,7 +326,7 @@ Hints Resolve andb_true_intro : bool v62. Lemma andb_true_intro2 : (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)). Proof. - Destruct b1; Destruct b2; Tauto. + Destruct b1; Destruct b2; Simpl; Tauto. Save. Hints Resolve andb_true_intro2 : bool v62. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index a1c86e78f..3c083aa97 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -189,7 +189,7 @@ Section first_definitions. Simpl; Intros [H1|H2]; Auto with datatypes. Simpl; Do 3 Intro. Elim (Aeq_dec b a0). - Tauto. + Simpl; Tauto. Simpl; Intros; Elim H0. Trivial with datatypes. Tauto. @@ -271,7 +271,7 @@ Section first_definitions. (set_In a (set_inter x y)) -> (set_In a y). Proof. Induction x. - Tauto. + Simpl; Tauto. Simpl; Intros a0 l Hrec y. Generalize (!set_mem_correct1 a0 y). Elim (set_mem a0 y); Simpl; Intros. @@ -291,7 +291,7 @@ Section first_definitions. (set_In a x) -> ~(set_In a y) -> (set_In a (set_diff x y)). Proof. Induction x. - Tauto. + Simpl; Tauto. Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hay. Rewrite Ha0a; Generalize (set_mem_complete2 Hay). Elim (set_mem a y); [ Intro Habs; Discriminate Habs | Auto with datatypes ]. @@ -302,7 +302,7 @@ Section first_definitions. (set_In a (set_diff x y)) -> (set_In a x). Proof. Induction x. - Tauto. + Simpl; Tauto. Simpl; Intros a0 l Hrec y; Elim (set_mem a0 y). EAuto with datatypes. Intro; Generalize (set_add_elim H). diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 6477d9f0c..1a0211d54 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -561,7 +561,7 @@ Save. Lemma in_prod : (A:Set)(B:Set)(l:(list A))(l':(list B)) (x:A)(y:B)(In x l)->(In y l')->(In (x,y) (list_prod l l')). Induction l; -[ Tauto +[ Simpl; Intros; Tauto | Simpl; Intros; Apply in_or_app; Elim H0; Clear H0; [ Left; Rewrite H0; Apply in_prod_aux; Assumption | Right; Auto] diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 7b0f432ba..a1c1639f0 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -87,6 +87,7 @@ Qed. Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)). Red. Intros x y z H' H'0. -Apply Strict_Rel_Transitive_with_Rel with y := y; Intuition. +Apply Strict_Rel_Transitive_with_Rel with y := y; + [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ]. Qed. End Partial_order_facts. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index ad6b55c0c..3c9609182 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -72,7 +72,7 @@ Theorem cong_reflexive_same_relation: (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Reflexive U R) -> (Reflexive U R'). Proof. -Intuition. +Unfold same_relation; Intuition. Qed. Theorem cong_symmetric_same_relation: diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index e7bcdcfab..0b69cd236 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -210,7 +210,7 @@ Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B. Tauto. Save. Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B. -Tauto. Save. +Unfold decidable; Tauto. Save. Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B. Unfold decidable;Tauto. |