diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/cc | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/cc')
-rw-r--r-- | contrib/cc/ccproof.ml | 146 | ||||
-rw-r--r-- | contrib/cc/ccproof.mli | 14 | ||||
-rw-r--r-- | contrib/cc/cctac.ml | 153 |
3 files changed, 181 insertions, 132 deletions
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index 1ffa347a..d336f599 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) @@ -16,58 +16,107 @@ open Names open Term open Ccalgo -type proof= +type rule= Ax of constr | SymAx of constr | Refl of term | Trans of proof*proof | Congr of proof*proof | Inject of proof*constructor*int*int - -let pcongr=function - Refl t1, Refl t2 -> Refl (Appli (t1,t2)) - | p1, p2 -> Congr (p1,p2) - -let rec ptrans=function - Refl _, p ->p - | p, Refl _ ->p - | Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3)) - | Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4)) - | Congr(p1,p2), Trans(Congr(p3,p4),p5) -> - ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5) - | p1, p2 ->Trans (p1,p2) - -let rec psym=function - Refl p->Refl p - | SymAx s->Ax s - | Ax s-> SymAx s - | Inject (p,c,n,a)-> Inject (psym p,c,n,a) - | Trans (p1,p2)-> ptrans (psym p2,psym p1) - | Congr (p1,p2)-> pcongr (psym p1,psym p2) +and proof = + {p_lhs:term;p_rhs:term;p_rule:rule} + +let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t} + +let pcongr p1 p2 = + match p1.p_rule,p2.p_rule with + Refl t1, Refl t2 -> prefl (Appli (t1,t2)) + | _, _ -> + {p_lhs=Appli (p1.p_lhs,p2.p_lhs); + p_rhs=Appli (p1.p_rhs,p2.p_rhs); + p_rule=Congr (p1,p2)} + +let rec ptrans p1 p3= + match p1.p_rule,p3.p_rule with + Refl _, _ ->p3 + | _, Refl _ ->p1 + | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3) + | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4) + | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) -> + ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5 + | _, _ -> + if p1.p_rhs = p3.p_lhs then + {p_lhs=p1.p_lhs; + p_rhs=p3.p_rhs; + p_rule=Trans (p1,p3)} + else anomaly "invalid cc transitivity" -let pcongr=function - Refl t1, Refl t2 ->Refl (Appli (t1,t2)) - | p1, p2 -> Congr (p1,p2) +let rec psym p = + match p.p_rule with + Refl _ -> p + | SymAx s -> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=Ax s} + | Ax s-> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=SymAx s} + | Inject (p0,c,n,a)-> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=Inject (psym p0,c,n,a)} + | Trans (p1,p2)-> ptrans (psym p2) (psym p1) + | Congr (p1,p2)-> pcongr (psym p1) (psym p2) + +let pax axioms s = + let l,r = Hashtbl.find axioms s in + {p_lhs=l; + p_rhs=r; + p_rule=Ax s} + +let psymax axioms s = + let l,r = Hashtbl.find axioms s in + {p_lhs=r; + p_rhs=l; + p_rule=SymAx s} + +let rec nth_arg t n= + match t with + Appli (t1,t2)-> + if n>0 then + nth_arg t1 (n-1) + else t2 + | _ -> anomaly "nth_arg: not enough args" + +let pinject p c n a = + {p_lhs=nth_arg p.p_lhs (n-a); + p_rhs=nth_arg p.p_rhs (n-a); + p_rule=Inject(p,c,n,a)} let build_proof uf= - + + let axioms = axioms uf in + let rec equal_proof i j= - if i=j then Refl (term uf i) else + if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in - ptrans (path_proof i li,psym (path_proof j lj)) + ptrans (path_proof i li) (psym (path_proof j lj)) and edge_proof ((i,j),eq)= let pi=equal_proof i eq.lhs in let pj=psym (equal_proof j eq.rhs) in let pij= match eq.rule with - Axiom (s,reversed)->if reversed then SymAx s else Ax s + Axiom (s,reversed)-> + if reversed then psymax axioms s + else pax axioms s | Congruence ->congr_proof eq.lhs eq.rhs | Injection (ti,ipac,tj,jpac,k) -> let p=ind_proof ti ipac tj jpac in let cinfo= get_constructor_info uf ipac.cnode in - Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k) - in ptrans(ptrans (pi,pij),pj) + pinject p cinfo.ci_constr cinfo.ci_nhyps k + in ptrans (ptrans pi pij) pj and constr_proof i t ipac= if ipac.args=[] then @@ -79,49 +128,26 @@ let build_proof uf= let rj=find uf j in let u=find_pac uf rj npac in let p=constr_proof j u npac in - ptrans (equal_proof i t, pcongr (p,Refl targ)) + ptrans (equal_proof i t) (pcongr p (prefl targ)) and path_proof i=function - [] -> Refl (term uf i) - | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x) + [] -> prefl (term uf i) + | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x) and congr_proof i j= let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in - pcongr (equal_proof i1 j1, equal_proof i2 j2) + pcongr (equal_proof i1 j1) (equal_proof i2 j2) and ind_proof i ipac j jpac= let p=equal_proof i j and p1=constr_proof i i ipac and p2=constr_proof j j jpac in - ptrans(psym p1,ptrans(p,p2)) + ptrans (psym p1) (ptrans p p2) in function `Prove (i,j) -> equal_proof i j | `Discr (i,ci,j,cj)-> ind_proof i ci j cj -let rec nth_arg t n= - match t with - Appli (t1,t2)-> - if n>0 then - nth_arg t1 (n-1) - else t2 - | _ -> anomaly "nth_arg: not enough args" -let rec type_proof axioms p= - match p with - Ax s->Hashtbl.find axioms s - | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1) - | Refl t-> t,t - | Trans (p1,p2)-> - let (s1,t1)=type_proof axioms p1 - and (t2,s2)=type_proof axioms p2 in - if t1=t2 then (s1,s2) else anomaly "invalid cc transitivity" - | Congr (p1,p2)-> - let (i1,j1)=type_proof axioms p1 - and (i2,j2)=type_proof axioms p2 in - Appli (i1,i2),Appli (j1,j2) - | Inject (p,c,n,a)-> - let (ti,tj)=type_proof axioms p in - nth_arg ti (n-a),nth_arg tj (n-a) diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli index abdd6fea..572b2c53 100644 --- a/contrib/cc/ccproof.mli +++ b/contrib/cc/ccproof.mli @@ -6,26 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *) open Ccalgo open Names open Term -type proof = +type rule= Ax of constr | SymAx of constr | Refl of term - | Trans of proof * proof - | Congr of proof * proof - | Inject of proof * constructor * int * int + | Trans of proof*proof + | Congr of proof*proof + | Inject of proof*constructor*int*int +and proof = + private {p_lhs:term;p_rhs:term;p_rule:rule} val build_proof : forest -> [ `Discr of int * pa_constructor * int * pa_constructor | `Prove of int * int ] -> proof -val type_proof : - (constr, (term * term)) Hashtbl.t -> proof -> term * term diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index ea8aceeb..86251254 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -37,6 +37,12 @@ let _f_equal = constant ["Init";"Logic"] "f_equal" let _eq_rect = constant ["Init";"Logic"] "eq_rect" +let _refl_equal = constant ["Init";"Logic"] "refl_equal" + +let _sym_eq = constant ["Init";"Logic"] "sym_eq" + +let _trans_eq = constant ["Init";"Logic"] "trans_eq" + let _eq = constant ["Init";"Logic"] "eq" let _False = constant ["Init";"Logic"] "False" @@ -210,54 +216,73 @@ let build_projection intype outtype (cstr:constructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let rec proof_tac axioms=function - Ax c -> exact_check c - | SymAx c -> tclTHEN symmetry (exact_check c) - | Refl t -> reflexivity - | Trans (p1,p2)->let t=(constr_of_term (snd (type_proof axioms p1))) in - (tclTHENS (transitivity t) - [(proof_tac axioms p1);(proof_tac axioms p2)]) - | Congr (p1,p2)-> - fun gls-> - let (f1,f2)=(type_proof axioms p1) - and (x1,x2)=(type_proof axioms p2) in - let tf1=constr_of_term f1 and tx1=constr_of_term x1 - and tf2=constr_of_term f2 and tx2=constr_of_term x2 in - let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1 - and typfx=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|]) - and lemma2= - mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in - (tclTHENS (transitivity (mkApp(tf2,[|tx1|]))) - [tclTHEN (apply lemma1) (proof_tac axioms p1); - tclFIRST - [tclTHEN (apply lemma2) (proof_tac axioms p2); - reflexivity; - fun gls -> - errorlabstrm "Congruence" - (Pp.str - "I don't know how to handle dependent equality")]] - gls) - | Inject (prf,cstr,nargs,argind) as gprf-> - (fun gls -> - let ti,tj=type_proof axioms prf in - let ai,aj=type_proof axioms gprf in - let cti=constr_of_term ti in - let ctj=constr_of_term tj in - let cai=constr_of_term ai in - let intype=pf_type_of gls cti in - let outtype=pf_type_of gls cai in +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 = 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 = 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 = 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 = pf_type_of gls tf1 in + let typx = pf_type_of gls tx1 in + let typfx = prod_applist typf [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=pf_type_of gls ti in + let outtype=pf_type_of gls default in let special=mkRel (1+nargs-argind) in - let default=constr_of_term ai in let proj=build_projection intype outtype cstr special default gls in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in - tclTHEN (apply injt) (proof_tac axioms prf) gls) + mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in + tclTHEN (refine injt) (proof_tac prf) gls -let refute_tac axioms c t1 t2 p gls = +let refute_tac c t1 t2 p gls = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype=pf_type_of gls tt1 in let neweq= @@ -266,9 +291,9 @@ let refute_tac axioms c t1 t2 p gls = let hid=pf_get_new_id (id_of_string "Heq") gls in let false_t=mkApp (c,[|mkVar hid|]) in tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p; simplest_elim false_t] gls + [proof_tac p; simplest_elim false_t] gls -let convert_to_goal_tac axioms c t1 t2 p 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=pf_type_of gls tt2 in let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in @@ -278,20 +303,19 @@ let convert_to_goal_tac axioms c t1 t2 p gls = let endt=mkApp (Lazy.force _eq_rect, [|sort;tt1;identity;c;tt2;mkVar e|]) in tclTHENS (true_cut (Name e) neweq) - [proof_tac axioms p;exact_check endt] gls + [proof_tac p;exact_check endt] gls -let convert_to_hyp_tac axioms c1 t1 c2 t2 p 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 (true_cut (Name h) tt2) - [convert_to_goal_tac axioms c1 t1 t2 p; + [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] gls -let discriminate_tac axioms cstr p gls = - let t1,t2=type_proof axioms p in - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype=pf_type_of gls tt1 in +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=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 @@ -303,12 +327,12 @@ let discriminate_tac axioms cstr p gls = 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;tt1;tt2;mkVar hid|]) in + [|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;tt1;tt2|]) in + let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p;exact_check endt] gls + [proof_tac p;exact_check endt] gls (* wrap everything *) @@ -333,12 +357,12 @@ let cc_tactic depth additionnal_terms gls= 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 p=build_proof uf (`Discr (i,ipac,j,jpac)) in let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac (axioms uf) cstr p gls + discriminate_tac cstr p gls | Incomplete -> let metacnt = ref 0 in - let newmeta _ = incr metacnt; mkMeta !metacnt in + let newmeta _ = incr metacnt; _M !metacnt in let terms_to_complete = List.map (build_term_to_complete uf newmeta) @@ -363,14 +387,13 @@ let cc_tactic depth additionnal_terms 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 - let axioms = axioms uf in match dis.rule with - Goal -> proof_tac axioms p gls - | Hyp id -> refute_tac axioms id ta tb p gls + Goal -> proof_tac p gls + | Hyp id -> refute_tac id ta tb p gls | HeqG id -> - convert_to_goal_tac axioms id ta tb p gls + convert_to_goal_tac id ta tb p gls | HeqnH (ida,idb) -> - convert_to_hyp_tac axioms ida ta idb tb p gls + convert_to_hyp_tac ida ta idb tb p gls let cc_fail gls = |