diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/cc/CC.v | 36 | ||||
| -rw-r--r-- | contrib/cc/README | 18 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.ml | 203 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.mli | 67 | ||||
| -rw-r--r-- | contrib/cc/ccproof.ml | 118 | ||||
| -rw-r--r-- | contrib/cc/ccproof.mli | 48 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml4 | 161 |
7 files changed, 651 insertions, 0 deletions
diff --git a/contrib/cc/CC.v b/contrib/cc/CC.v new file mode 100644 index 0000000000..7bd3497872 --- /dev/null +++ b/contrib/cc/CC.v @@ -0,0 +1,36 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $id$ *) + +Require Export Eqdep_dec. + +(* Congruence lemma *) + +Theorem Congr_nodep: (A,B:Type)(f,g:A->B)(x,y:A)f==g->x==y->(f x)==(g y). +Intros A B f g x y eq1 eq2;Rewrite eq1;Rewrite eq2;Reflexivity. +Defined. + +Theorem Congr_dep: + (A:Type; P:(A->Type); f,g:((a:A)(P a)); x:A)f==g->(f x)==(g x). +Intros A P f g x e;Rewrite e;Reflexivity. +Defined. + +(* Basic application : try to prove that goal is equal to one hypothesis *) + +Lemma convert_goal : (A,B:Prop)B->(A==B)->A. +Intros A B H E;Rewrite E;Assumption. +Save. + +Tactic Definition CCsolve := + Match Context With + [ H: ?1 |- ?2] -> + (Assert (?2==?1);[CC| + Match Reverse Context With + [ H: ?1;Heq: (?2==?1)|- ?2] ->(Rewrite Heq;Exact H)]). + diff --git a/contrib/cc/README b/contrib/cc/README new file mode 100644 index 0000000000..f19820d32b --- /dev/null +++ b/contrib/cc/README @@ -0,0 +1,18 @@ + +cctac: congruence-closure for coq + +author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan + +Files : + +- ccalgo.ml : congruence closure algorithm +- ccproof.ml : proof generation code +- cctac.ml4 : the tactic itself +- CC.v : a few lemmas to handle eq/eqT conversions and congruence + +Known Bugs : CC tactic can fail due to type dependencies. + +Related documents: + Peter J. Downey, Ravi Sethi, and Robert E. Tarjan. + Variations on the common subexpression problem. + JACM, 27(4):758-771, October 1980. diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml new file mode 100644 index 0000000000..93b60531b2 --- /dev/null +++ b/contrib/cc/ccalgo.ml @@ -0,0 +1,203 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(* This file implements the basic congruence-closure algorithm by *) +(* Downey,Sethi and Tarjan. *) + +open Names +open Term + +let init_size=251 + +type term=Symb of constr|Appli of term*term + + +(* Basic Union-Find algo w/o path compression *) + +module UF = struct + type tag=Congr|Ax of identifier + + type cl=Rep of int*(int list)|Eqto of int*(int*int*tag) + + type vertex=Leaf|Node of (int*int) + + type t=(int ref)*((int,(cl*vertex*term)) Hashtbl.t) + + let empty ()=(((ref 0),(Hashtbl.create init_size)):t) + + let add_lst i t ((a,m):t)= + match Hashtbl.find m i with + ((Rep(l,lst)),v,trm)->Hashtbl.replace m i ((Rep((l+1),(t::lst))),v,trm) + | _ ->failwith "add_lst: not a representative" + + let rec find ((a,m):t) i= + let (cl,_,_)=Hashtbl.find m i in + match cl with + Rep(_,_) -> i + | Eqto(j,_) ->find (a,m) j + + let list ((a,m):t) i= + match Hashtbl.find m i with + ((Rep(_,lst)),_,_)-> lst + | _ ->failwith "list: not a class" + + let size ((a,m):t) i= + match Hashtbl.find m i with + ((Rep (l,_)),_,_) -> l + | _ ->failwith "size: not a class" + + let signature ((a,m):t) i= + let (_,v,_)=Hashtbl.find m i in + match v with + Node(j,k)->(find (a,m) j,find (a,m) k) + | _ ->failwith "signature: not a node" + + let nodes ((a,m):t)= (* cherche les noeuds binaires *) + Hashtbl.fold (fun i (_,v,_) l->match v with Node (_,_)->i::l|_->l) m [] + + let rec add t (a,m) syms = + try Hashtbl.find syms t with Not_found -> + match t with + Symb s -> + let b= !a in incr a; + Hashtbl.add m b ((Rep (0,[])),Leaf,t); + Hashtbl.add syms t b; + b + | Appli (t1,t2) -> + let i1=add t1 (a,m) syms and i2=add t2 (a,m) syms in + let b= !a in incr a; + add_lst (find (a,m) i1) b (a,m); + add_lst (find (a,m) i2) b (a,m); + Hashtbl.add m b ((Rep (0,[])),(Node(i1,i2)),t); + Hashtbl.add syms t b; + b + + let union ((a,m):t) i1 i2 t= + let (cl1,v1,t1)=(Hashtbl.find m i1) and + (cl2,v2,t2)=(Hashtbl.find m i2) in + match cl1,cl1 with + ((Rep (l1,lst1)),(Rep (l2,lst2))) -> + Hashtbl.replace m i2 ((Eqto (i1,t)),v2,t2); + Hashtbl.replace m i1 ((Rep((l2+l1),(lst2@lst1))),v1,t1) + | _ ->failwith "union: not classes" + + +end + +(* Signature table *) + +module ST=struct + +(* l: sign -> term r: term -> sign *) + + type t = ((int*int,int) Hashtbl.t) * ((int,int*int) Hashtbl.t) + + let empty ()=((Hashtbl.create init_size),(Hashtbl.create init_size)) + + let enter t sign ((l,r) as st:t)= + if Hashtbl.mem l sign then + failwith "enter: signature already entered" + else + Hashtbl.replace l sign t; + Hashtbl.replace r t sign + + let query sign ((l,r):t)=Hashtbl.find l sign + + let delete t ((l,r) as st:t)= + try let sign=Hashtbl.find r t in + Hashtbl.remove l sign; + Hashtbl.remove r t + with + Not_found -> () + + let rec delete_list l st= + match l with + []->() + | t::q -> delete t st;delete_list q st + +end + +let rec combine_rec uf st=function + []->[] + | v::pending-> + let combine=(combine_rec uf st pending) in + let s=UF.signature uf v in + try (v,(ST.query s st))::combine with + Not_found-> + ST.enter v s st;combine + +let rec process_rec uf st=function + []->[] + | (v,w)::combine-> + let pending=process_rec uf st combine in + let i=UF.find uf v + and j=UF.find uf w in + if (i==j)|| ((Hashtbl.hash i)=(Hashtbl.hash j) && (i=j)) then + pending + else + if (UF.size uf i)<(UF.size uf j) then + let l=UF.list uf i in + UF.union uf j i (v,w,UF.Congr); + ST.delete_list l st; + l@pending + else + let l=UF.list uf j in + UF.union uf i j (w,v,UF.Congr); + ST.delete_list l st; + l@pending + +let rec cc_rec uf st=function + []->() + | pending-> + let combine=combine_rec uf st pending in + let pending0=process_rec uf st combine in + (cc_rec uf st pending0) + +let cc uf=(cc_rec uf (ST.empty ()) (UF.nodes uf)) + +let rec make_uf syms=function + []->(UF.empty ()) + | (ax,(v,w))::q-> + let uf=make_uf syms q in + let i1=UF.add v uf syms in + let i2=UF.add w uf syms in + UF.union uf (UF.find uf i2) (UF.find uf i1) (i1,i2,(UF.Ax ax)); + uf + +let decide_prb (axioms,(v,w))= + let syms=Hashtbl.create init_size in + let uf=make_uf syms axioms in + let i1=UF.add v uf syms in + let i2=UF.add w uf syms in + cc uf; + (UF.find uf i1)=(UF.find uf i2) + + + + + + + + + + + + + + + + + + + + + + + diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli new file mode 100644 index 0000000000..6f55d85418 --- /dev/null +++ b/contrib/cc/ccalgo.mli @@ -0,0 +1,67 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +val init_size : int + +type term = Symb of Term.constr | Appli of term * term + +module UF : + sig + type tag = Congr | Ax of Names.identifier + and cl = + Rep of int * int list + | Eqto of int * (int * int * tag) + and vertex = Leaf | Node of (int * int) + and t = int ref * (int, cl * vertex * term) Hashtbl.t + val empty : unit -> t + val add_lst : int -> int -> t -> unit + val find : t -> int -> int + val list : t -> int -> int list + val size : t -> int -> int + val signature : t -> int -> int * int + val nodes : t -> int list + val add : + term -> + int ref * (int, cl * vertex * term) Hashtbl.t -> + (term, int) Hashtbl.t -> int + val union : + t -> int -> int -> int * int * tag -> unit + end + +module ST : + sig + type t = + (int * int, int) Hashtbl.t * + (int, int * int) Hashtbl.t + val empty : + unit -> ('a, 'b) Hashtbl.t * ('c, 'd) Hashtbl.t + val enter : int -> int * int -> t -> unit + val query : int * int -> t -> int + val delete : int -> t -> unit + val delete_list : int list -> t -> unit + end + +val combine_rec : + UF.t -> ST.t -> int list -> (int * int) list + +val process_rec : + UF.t -> ST.t -> (int * int) list -> int list + +val cc_rec : UF.t -> ST.t -> int list -> unit + +val cc : UF.t -> unit + +val make_uf : + (term, int) Hashtbl.t -> + (Names.identifier * (term * term)) list -> UF.t + +val decide_prb : + (Names.identifier * (term * term)) list * (term * term) -> + bool diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml new file mode 100644 index 0000000000..26e2299179 --- /dev/null +++ b/contrib/cc/ccproof.ml @@ -0,0 +1,118 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(* This file uses the (non-compressed) union-find structure to generate *) +(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) + +open Names +open Ccalgo + +type proof= + Ax of identifier + | Refl of term + | Trans of proof*proof + | Sym of proof + | Congr of proof*proof + +let rec up_path uf i l= + let (cl,_,_)=(Hashtbl.find uf i) in + match cl with + UF.Eqto(j,t)->up_path uf j (((i,j),t)::l) + | UF.Rep(_,_)->l + +let rec min_path=function + ([],l2)->([],l2) + | (l1,[])->(l1,[]) + | (((c1,t1)::q1),((c2,t2)::q2)) as cpl-> + if c1=c2 then + min_path (q1,q2) + else + cpl + +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 + | Sym p->p + | Ax s-> Sym(Ax s) + | Trans (p1,p2)-> ptrans ((psym p2),(psym p1)) + | Congr (p1,p2)-> pcongr ((psym p1),(psym p2)) + +let pcongr=function + ((Refl t1),(Refl t2))->Refl (Appli (t1,t2)) + | (p1,p2) -> Congr (p1,p2) + +let build_proof ((a,m):UF.t) i j= + let rec equal_proof i j= + let (li,lj)=min_path ((up_path m i []),(up_path m j [])) in + ptrans ((path_proof i li),(psym (path_proof j lj))) + and arrow_proof ((i,j),t)= + let (i0,j0,t0)=t in + let pi=(equal_proof i i0) in + let pj=psym (equal_proof j j0) in + let pij= + match t0 with + UF.Ax s->Ax s + | UF.Congr->(congr_proof i0 j0) + in ptrans(ptrans (pi,pij),pj) + and path_proof i=function + []->let (_,_,t)=Hashtbl.find m i in Refl t + | (((_,j),_) as x)::q->ptrans ((path_proof j q),(arrow_proof x)) + and congr_proof i j= + let (_,vi,_)=(Hashtbl.find m i) and (_,vj,_)=(Hashtbl.find m j) in + match (vi,vj) with + ((UF.Node(i1,i2)),(UF.Node(j1,j2)))-> + pcongr ((equal_proof i1 j1),(equal_proof i2 j2)) + | _ -> failwith "congr_proof: couldn't find subterms" + in + (equal_proof i j) + +let rec type_proof uf axioms p= + match p with + Ax s->List.assoc s axioms + | Refl t->(t,t) + | Trans (p1,p2)-> + let (s1,t1)=type_proof uf axioms p1 + and (t2,s2)=type_proof uf axioms p2 in + if t1=t2 then (s1,s2) else failwith "invalid transitivity" + | Sym p->let (t1,t2)=type_proof uf axioms p in (t2,t1) + | Congr (p1,p2)-> + let (i1,j1)=(type_proof uf axioms p1) + and (i2,j2)=(type_proof uf axioms p2) in + ((Appli (i1,i2)),(Appli (j1,j2))) + +let cc_proof (axioms,(v,w))= + let syms=Hashtbl.create init_size in + let uf=make_uf syms axioms in + let i1=(UF.add v uf syms) in + let i2=(UF.add w uf syms) in + cc uf; + if (UF.find uf i1)=(UF.find uf i2) then + let p=(build_proof uf i1 i2) in + (if (v,w)=(type_proof uf axioms p) then Some (p,uf,axioms) + else failwith "Proof check failed !!") + else + None;; + + + + + diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli new file mode 100644 index 0000000000..a699af6941 --- /dev/null +++ b/contrib/cc/ccproof.mli @@ -0,0 +1,48 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Ccalgo + +type proof = + Ax of Names.identifier + | Refl of term + | Trans of proof * proof + | Sym of proof + | Congr of proof * proof + +val up_path : + (int, UF.cl * 'a * 'b) Hashtbl.t -> + int -> + ((int * int) * (int * int * UF.tag)) list -> + ((int * int) * (int * int * UF.tag)) list + +val min_path : + ('a * 'b) list * ('a * 'c) list -> + ('a * 'b) list * ('a * 'c) list + +val pcongr : proof * proof -> proof +val ptrans : proof * proof -> proof +val psym : proof -> proof +val pcongr : proof * proof -> proof + +val build_proof : UF.t -> int -> int -> proof + +val type_proof : + 'a -> + (Names.identifier * (term * term)) list -> + proof -> term * term + +val cc_proof : + (Names.identifier * (term * term)) list * + (term * term) -> + (proof * UF.t * + (Names.identifier * (term * term)) list) + option + diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 new file mode 100644 index 0000000000..f7a9e723fa --- /dev/null +++ b/contrib/cc/cctac.ml4 @@ -0,0 +1,161 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*) + +(* $Id$ *) + +(* This file is the interface between the c-c algorithm and Coq *) + +open Evd +open Proof_type +open Names +open Libnames +open Nameops +open Term +open Tacmach +open Tactics +open Tacticals +open Ccalgo +open Tacinterp +open Ccproof +open Pp +open Util +open Format + +exception Not_an_eq + +let fail()=raise Not_an_eq + +let constr_of_string s () = + Declare.constr_of_reference (Nametab.locate (qualid_of_string s)) + +let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT" +let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq" +let congr_theo = constr_of_string "Coq.cc.CC.Congr_nodep" +let congr_dep_theo = constr_of_string "Coq.cc.CC.Congr_dep" + +let fresh_id1=id_of_string "eq1" and fresh_id2=id_of_string "eq2" + +let t_make_app=(Array.fold_left (fun s t->Appli (s,t))) + +(* decompose member of equality in an applicative format *) + +let rec decompose_term t= + match kind_of_term t with + App (f,args)->let targs=Array.map decompose_term args in + (t_make_app (Symb f) targs) + | _->(Symb t) + +(* decompose equality in members and type *) + +let eq_type_of_term term= + match kind_of_term term with + App (f,args)-> + (try + let ref = Declare.reference_of_constr f in + if (ref=Coqlib.glob_eq || ref=Coqlib.glob_eqT) && + (Array.length args)=3 + then (args.(0),args.(1),args.(2)) + else fail() + with + Not_found -> fail ()) + | _ ->fail () + +(* read an equality *) + +let read_eq term= + let (_,t1,t2)=eq_type_of_term term in + ((decompose_term t1),(decompose_term t2)) + +(* rebuild a term from applicative format *) + +let rec make_term=function + Symb s->s + | Appli (s1,s2)->make_app [(make_term s2)] s1 +and make_app l=function + Symb s->mkApp (s,(Array.of_list l)) + | Appli (s1,s2)->make_app ((make_term s2)::l) s1 + +(* store all equalities from the context *) + +let rec read_hyps=function + []->[] + | (id,_,e)::hyps->let q=(read_hyps hyps) in + try (id,(read_eq e))::q with Not_an_eq -> q + +(* build a problem ( i.e. read the goal as an equality ) *) + +let make_prb gl= + let concl=gl.evar_concl in + let hyps=gl.evar_hyps in + (read_hyps hyps),(read_eq concl) + +(* apply tac, followed (or not) by aplication of theorem theo *) + +let st_wrap theo tac= + tclORELSE tac (tclTHEN (apply theo) tac) + +(* generate an adhoc tactic following the proof tree *) + +let rec proof_tac uf axioms=function + Ax id->(fun gl->(st_wrap (eq2eqT_theo ()) (exact_check (mkVar id)) gl)) + | Refl t->reflexivity + | Trans (p1,p2)->let t=(make_term (snd (type_proof uf axioms p1))) in + (tclTHENS (transitivity t) + [(proof_tac uf axioms p1);(proof_tac uf axioms p2)]) + | Sym p->tclTHEN symmetry (proof_tac uf axioms p) + | Congr (p1,p2)-> + (fun gl-> + let (s1,t1)=(type_proof uf axioms p1) and + (s2,t2)=(type_proof uf axioms p2) in + let ts1=(make_term s1) and tt1=(make_term t1) + and ts2=(make_term s2) and tt2=(make_term t2) in + let typ1=pf_type_of gl ts1 and typ2=pf_type_of gl ts2 in + let (typb,_,_)=(eq_type_of_term gl.it.evar_concl) in + let act=mkApp ((congr_theo ()),[|typ2;typb;ts1;tt1;ts2;tt2|]) in + tclORELSE + (tclTHENS + (apply act) + [(proof_tac uf axioms p1);(proof_tac uf axioms p2)]) + (tclTHEN + (let p=mkLambda(destProd typ1) in + let acdt=mkApp((congr_dep_theo ()),[|typ2;p;ts1;tt1;ts2|]) in + apply acdt) (proof_tac uf axioms p1)) + gl) + +(* wrap everything *) + +let cc_tactic gl_sg= + Library.check_required_library ["Coq";"cc";"CC"]; + let gl=gl_sg.it in + let prb=try make_prb gl with Not_an_eq -> + errorlabstrm "CC" [< str "Couldn't match goal with an equality" >] in + match (cc_proof prb) with + None->errorlabstrm "CC" [< str "CC couldn't solve goal" >] + | Some (p,uf,axioms)->let tac=proof_tac uf axioms p in + (tclORELSE (st_wrap (eqT2eq_theo ()) tac) + (fun _->errorlabstrm "CC" + [< str "CC doesn't know how to handle dependent equality." >]) gl_sg) + +(* Tactic registration *) + +TACTIC EXTEND CC + [ "CC" ] -> [ cc_tactic ] +END + + + + + + + + + + + |