From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- contrib/cc/cctac.ml | 465 ---------------------------------------------------- 1 file changed, 465 deletions(-) delete mode 100644 contrib/cc/cctac.ml (limited to 'contrib/cc/cctac.ml') diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml deleted file mode 100644 index 00cbbeee..00000000 --- a/contrib/cc/cctac.ml +++ /dev/null @@ -1,465 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Closure.whd_val infos (Closure.inject t)) - -let whd_delta env= - let infos=Closure.create_clos_infos Closure.betadeltaiota env in - (fun t -> Closure.whd_val infos (Closure.inject t)) - -(* decompose member of equality in an applicative format *) - -let sf_of env sigma c = family_of_sort (destSort (whd_delta env (type_of env sigma c))) - -let rec decompose_term env sigma t= - match kind_of_term (whd env t) with - App (f,args)-> - let tf=decompose_term env sigma f in - let targs=Array.map (decompose_term env sigma) args in - Array.fold_left (fun s t->Appli (s,t)) tf targs - | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> - let b = pop _b in - let sort_b = sf_of env sigma b in - let sort_a = sf_of env sigma a in - Appli(Appli(Product (sort_a,sort_b) , - decompose_term env sigma a), - decompose_term env sigma b) - | Construct c-> - let (oib,_)=Global.lookup_inductive (fst c) in - let nargs=mis_constructor_nargs_env env c in - Constructor {ci_constr=c; - ci_arity=nargs; - ci_nhyps=nargs-oib.mind_nparams} - | _ ->if closed0 t then (Symb t) else raise Not_found - -(* decompose equality in members and type *) - -let atom_of_constr env sigma term = - let wh = (whd_delta env term) in - let kot = kind_of_term wh in - match kot with - App (f,args)-> - if eq_constr f (Lazy.force _eq) && (Array.length args)=3 - then `Eq (args.(0), - decompose_term env sigma args.(1), - decompose_term env sigma args.(2)) - else `Other (decompose_term env sigma term) - | _ -> `Other (decompose_term env sigma term) - -let rec pattern_of_constr env sigma c = - match kind_of_term (whd env c) with - App (f,args)-> - let pf = decompose_term env sigma f in - let pargs,lrels = List.split - (array_map_to_list (pattern_of_constr env sigma) args) in - PApp (pf,List.rev pargs), - List.fold_left Intset.union Intset.empty lrels - | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> - let b =pop _b in - let pa,sa = pattern_of_constr env sigma a in - let pb,sb = pattern_of_constr env sigma (pop b) in - let sort_b = sf_of env sigma b in - let sort_a = sf_of env sigma a in - PApp(Product (sort_a,sort_b), - [pa;pb]),(Intset.union sa sb) - | Rel i -> PVar i,Intset.singleton i - | _ -> - let pf = decompose_term env sigma c in - PApp (pf,[]),Intset.empty - -let non_trivial = function - PVar _ -> false - | _ -> true - -let patterns_of_constr env sigma nrels term= - let f,args= - try destApp (whd_delta env term) with _ -> raise Not_found in - if eq_constr f (Lazy.force _eq) && (Array.length args)=3 - then - let patt1,rels1 = pattern_of_constr env sigma args.(1) - and patt2,rels2 = pattern_of_constr env sigma args.(2) in - let valid1 = - if Intset.cardinal rels1 <> nrels then Creates_variables - else if non_trivial patt1 then Normal - else Trivial args.(0) - and valid2 = - if Intset.cardinal rels2 <> nrels then Creates_variables - else if non_trivial patt2 then Normal - else Trivial args.(0) in - if valid1 <> Creates_variables - || valid2 <> Creates_variables then - nrels,valid1,patt1,valid2,patt2 - else raise Not_found - else raise Not_found - -let rec quantified_atom_of_constr env sigma nrels term = - match kind_of_term (whd_delta env term) with - Prod (_,atom,ff) -> - if eq_constr ff (Lazy.force _False) then - let patts=patterns_of_constr env sigma nrels atom in - `Nrule patts - else - quantified_atom_of_constr env sigma (succ nrels) ff - | _ -> - let patts=patterns_of_constr env sigma nrels term in - `Rule patts - -let litteral_of_constr env sigma term= - match kind_of_term (whd_delta env term) with - | Prod (_,atom,ff) -> - if eq_constr ff (Lazy.force _False) then - match (atom_of_constr env sigma atom) with - `Eq(t,a,b) -> `Neq(t,a,b) - | `Other(p) -> `Nother(p) - else - begin - try - quantified_atom_of_constr env sigma 1 ff - with Not_found -> - `Other (decompose_term env sigma term) - end - | _ -> - atom_of_constr env sigma term - - -(* store all equalities from the context *) - -let rec make_prb gls depth additionnal_terms = - let env=pf_env gls in - let sigma=sig_sig gls in - let state = empty depth gls in - let pos_hyps = ref [] in - let neg_hyps =ref [] in - List.iter - (fun c -> - let t = decompose_term env sigma c in - ignore (add_term state t)) additionnal_terms; - List.iter - (fun (id,_,e) -> - begin - let cid=mkVar id in - match litteral_of_constr env sigma e with - `Eq (t,a,b) -> add_equality state cid a b - | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b - | `Other ph -> - List.iter - (fun (cidn,nh) -> - add_disequality state (HeqnH (cid,cidn)) ph nh) - !neg_hyps; - pos_hyps:=(cid,ph):: !pos_hyps - | `Nother nh -> - List.iter - (fun (cidp,ph) -> - add_disequality state (HeqnH (cidp,cid)) ph nh) - !pos_hyps; - neg_hyps:=(cid,nh):: !neg_hyps - | `Rule patts -> add_quant state id true patts - | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val gls.it.evar_hyps); - begin - match atom_of_constr env sigma gls.it.evar_concl with - `Eq (t,a,b) -> add_disequality state Goal a b - | `Other g -> - List.iter - (fun (idp,ph) -> - add_disequality state (HeqG idp) ph g) !pos_hyps - end; - state - -(* indhyps builds the array of arrays of constructor hyps for (ind largs) *) - -let build_projection intype outtype (cstr:constructor) special default gls= - let env=pf_env gls in - let (h,argv) = - try destApp intype with - Invalid_argument _ -> (intype,[||]) in - let ind=destInd h in - let types=Inductiveops.arities_of_constructors env ind in - let lp=Array.length types in - let ci=pred (snd cstr) in - let branch i= - let ti=Term.prod_appvect types.(i) argv in - let rc=fst (Sign.decompose_prod_assum ti) in - let head= - if i=ci then special else default in - Sign.it_mkLambda_or_LetIn head rc in - let branches=Array.init lp branch in - let casee=mkRel 1 in - let pred=mkLambda(Anonymous,intype,outtype) in - let case_info=make_case_info (pf_env gls) ind RegularStyle in - let body= mkCase(case_info, pred, casee, branches) in - let id=pf_get_new_id (id_of_string "t") gls in - mkLambda(Name id,intype,body) - -(* generate an adhoc tactic following the proof tree *) - -let _M =mkMeta - -let rec proof_tac p gls = - match p.p_rule with - Ax c -> exact_check c gls - | SymAx c -> - let l=constr_of_term p.p_lhs and - r=constr_of_term p.p_rhs in - let typ = refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls - | Refl t -> - let lr = constr_of_term t in - let typ = refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls - | Trans (p1,p2)-> - let t1 = constr_of_term p1.p_lhs and - t2 = constr_of_term p1.p_rhs and - t3 = constr_of_term p2.p_rhs in - let typ = refresh_universes (pf_type_of gls t2) in - let prf = - mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in - tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls - | Congr (p1,p2)-> - let tf1=constr_of_term p1.p_lhs - and tx1=constr_of_term p2.p_lhs - and tf2=constr_of_term p1.p_rhs - and tx2=constr_of_term p2.p_rhs in - let typf = refresh_universes (pf_type_of gls tf1) in - let typx = refresh_universes (pf_type_of gls tx1) in - let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in - let id = pf_get_new_id (id_of_string "f") gls in - let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = - mkApp(Lazy.force _f_equal, - [|typf;typfx;appx1;tf1;tf2;_M 1|]) in - let lemma2= - mkApp(Lazy.force _f_equal, - [|typx;typfx;tf2;tx1;tx2;_M 1|]) in - let prf = - mkApp(Lazy.force _trans_eq, - [|typfx; - mkApp(tf1,[|tx1|]); - mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - tclTHENS (refine prf) - [tclTHEN (refine lemma1) (proof_tac p1); - tclFIRST - [tclTHEN (refine lemma2) (proof_tac p2); - reflexivity; - fun gls -> - errorlabstrm "Congruence" - (Pp.str - "I don't know how to handle dependent equality")]] gls - | Inject (prf,cstr,nargs,argind) -> - let ti=constr_of_term prf.p_lhs in - let tj=constr_of_term prf.p_rhs in - let default=constr_of_term p.p_lhs in - let intype=refresh_universes (pf_type_of gls ti) in - let outtype=refresh_universes (pf_type_of gls default) in - let special=mkRel (1+nargs-argind) in - let proj=build_projection intype outtype cstr special default gls in - let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - tclTHEN (refine injt) (proof_tac prf) gls - -let refute_tac c t1 t2 p gls = - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype=refresh_universes (pf_type_of gls tt1) in - let neweq= - mkApp(Lazy.force _eq, - [|intype;tt1;tt2|]) in - let hid=pf_get_new_id (id_of_string "Heq") gls in - let false_t=mkApp (c,[|mkVar hid|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; simplest_elim false_t] gls - -let convert_to_goal_tac c t1 t2 p gls = - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort=refresh_universes (pf_type_of gls tt2) in - let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in - let e=pf_get_new_id (id_of_string "e") gls in - let x=pf_get_new_id (id_of_string "X") gls in - let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=mkApp (Lazy.force _eq_rect, - [|sort;tt1;identity;c;tt2;mkVar e|]) in - tclTHENS (assert_tac (Name e) neweq) - [proof_tac p;exact_check endt] gls - -let convert_to_hyp_tac c1 t1 c2 t2 p gls = - let tt2=constr_of_term t2 in - let h=pf_get_new_id (id_of_string "H") gls in - let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (assert_tac (Name h) tt2) - [convert_to_goal_tac c1 t1 t2 p; - simplest_elim false_t] gls - -let discriminate_tac cstr p gls = - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype=refresh_universes (pf_type_of gls t1) in - let concl=pf_concl gls in - let outsort=mkType (new_univ ()) in - let xid=pf_get_new_id (id_of_string "X") gls in - let tid=pf_get_new_id (id_of_string "t") gls in - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - let trivial=pf_type_of gls identity in - let outtype=mkType (new_univ ()) in - let pred=mkLambda(Name xid,outtype,mkRel 1) in - let hid=pf_get_new_id (id_of_string "Heq") gls in - let proj=build_projection intype outtype cstr trivial concl gls in - let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p;exact_check endt] gls - -(* wrap everything *) - -let build_term_to_complete uf meta pac = - let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (list_tabulate meta pac.arity) in - let all_args = List.rev_append real_args dummy_args in - applistc (mkConstruct cinfo.ci_constr) all_args - -let cc_tactic depth additionnal_terms gls= - Coqlib.check_required_library ["Coq";"Init";"Logic"]; - let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in - let state = make_prb gls depth additionnal_terms in - let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in - let sol = execute true state in - let _ = debug Pp.msgnl (Pp.str "Computation completed.") in - let uf=forest state in - match sol with - None -> tclFAIL 0 (str "congruence failed") gls - | Some reason -> - debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); - match reason with - Discrimination (i,ipac,j,jpac) -> - let p=build_proof uf (`Discr (i,ipac,j,jpac)) in - let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac cstr p gls - | Incomplete -> - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in - Pp.msgnl - (Pp.str "Goal is solvable by congruence but \ - some arguments are missing."); - Pp.msgnl - (Pp.str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ - prlist_with_sep - (fun () -> str ")" ++ pr_spc () ++ str "(") - (print_constr_env (pf_env gls)) - terms_to_complete ++ - str ")\"," - end); - Pp.msgnl - (Pp.str " replacing metavariables by arbitrary terms."); - tclFAIL 0 (str "Incomplete") gls - | Contradiction dis -> - let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in - let ta=term uf dis.lhs and tb=term uf dis.rhs in - match dis.rule with - Goal -> proof_tac p gls - | Hyp id -> refute_tac id ta tb p gls - | HeqG id -> - convert_to_goal_tac id ta tb p gls - | HeqnH (ida,idb) -> - convert_to_hyp_tac ida ta idb tb p gls - - -let cc_fail gls = - errorlabstrm "Congruence" (Pp.str "congruence failed.") - -let congruence_tac depth l = - tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) - cc_fail - -(* Beware: reflexivity = constructor 1 = apply refl_equal - might be slow now, let's rather do something equivalent - to a "simple apply refl_equal" *) - -let simple_reflexivity () = apply (Lazy.force _refl_equal) - -(* The [f_equal] tactic. - - It mimics the use of lemmas [f_equal], [f_equal2], etc. - This isn't particularly related with congruence, apart from - the fact that congruence is called internally. -*) - -let f_equal gl = - let cut_eq c1 c2 = - let ty = refresh_universes (pf_type_of gl c1) in - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_reflexivity ()) - in - try match kind_of_term (pf_concl gl) with - | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> - begin match kind_of_term t, kind_of_term t' with - | App (f,v), App (f',v') when Array.length v = Array.length v' -> - let rec cuts i = - if i < 0 then tclTRY (congruence_tac 1000 []) - else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) - in cuts (Array.length v - 1) gl - | _ -> tclIDTAC gl - end - | _ -> tclIDTAC gl - with Type_errors.TypeError _ -> tclIDTAC gl -- cgit v1.2.3