diff options
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/CCSolve.v | 22 | ||||
| -rw-r--r-- | contrib/cc/README | 20 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.ml | 357 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.mli | 84 | ||||
| -rw-r--r-- | contrib/cc/ccproof.ml | 157 | ||||
| -rw-r--r-- | contrib/cc/ccproof.mli | 45 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml4 | 247 |
7 files changed, 932 insertions, 0 deletions
diff --git a/contrib/cc/CCSolve.v b/contrib/cc/CCSolve.v new file mode 100644 index 00000000..fab6f775 --- /dev/null +++ b/contrib/cc/CCSolve.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: CCSolve.v,v 1.4.2.1 2004/07/16 19:29:58 herbelin Exp $ *) + +Ltac CCsolve := + repeat + match goal with + | H:?X1 |- ?X2 => + let Heq := fresh "Heq" in + (assert (Heq : X2 = X1); [ congruence | rewrite Heq; exact H ]) + | H:?X1,G:(?X2 -> ?X3) |- _ => + let Heq := fresh "Heq" in + (assert (Heq : X2 = X1); + [ congruence + | rewrite Heq in G; generalize (G H); clear G; intro G ]) + end. diff --git a/contrib/cc/README b/contrib/cc/README new file mode 100644 index 00000000..073b140e --- /dev/null +++ b/contrib/cc/README @@ -0,0 +1,20 @@ + +cctac: congruence-closure for coq + +author: Pierre Corbineau, + Stage de DEA au LSV, ENS Cachan + Thèse au LRI, Université Paris Sud XI + +Files : + +- ccalgo.ml : congruence closure algorithm +- ccproof.ml : proof generation code +- cctac.ml4 : the tactic itself +- CCSolve.v : a small Ltac tactic based on congruence + +Known Bugs : the congruence 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 00000000..e73a6221 --- /dev/null +++ b/contrib/cc/ccalgo.ml @@ -0,0 +1,357 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: ccalgo.ml,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *) + +(* This file implements the basic congruence-closure algorithm by *) +(* Downey,Sethi and Tarjan. *) + +open Util +open Names +open Term + +let init_size=251 + +type pa_constructor= + {head_constr: int; + arity:int; + nhyps:int; + args:int list; + term_head:int} + + +module PacMap=Map.Make(struct type t=int*int let compare=compare end) + +type term= + Symb of constr + | Appli of term*term + | Constructor of constructor*int*int (* constructor arity+ nhyps *) + +type rule= + Congruence + | Axiom of identifier + | Injection of int*int*int*int (* terms+head+arg position *) + +type equality = {lhs:int;rhs:int;rule:rule} + +let swap eq= + let swap_rule=match eq.rule with + Congruence -> Congruence + | Injection (i,j,c,a) -> Injection (j,i,c,a) + | Axiom id -> anomaly "no symmetry for axioms" + in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule} + +(* Signature table *) + +module ST=struct + + (* l: sign -> term r: term -> sign *) + + type t = {toterm:(int*int,int) Hashtbl.t; + tosign:(int,int*int) Hashtbl.t} + + let empty ()= + {toterm=Hashtbl.create init_size; + tosign=Hashtbl.create init_size} + + let enter t sign st= + if Hashtbl.mem st.toterm sign then + anomaly "enter: signature already entered" + else + Hashtbl.replace st.toterm sign t; + Hashtbl.replace st.tosign t sign + + let query sign st=Hashtbl.find st.toterm sign + + let delete t st= + try let sign=Hashtbl.find st.tosign t in + Hashtbl.remove st.toterm sign; + Hashtbl.remove st.tosign t + with + Not_found -> () + + let rec delete_list l st= + match l with + []->() + | t::q -> delete t st;delete_list q st + +end + +(* Basic Union-Find algo w/o path compression *) + +module UF = struct + +module IndMap=Map.Make(struct type t=inductive let compare=compare end) + + type representative= + {mutable nfathers:int; + mutable fathers:int list; + mutable constructors:pa_constructor PacMap.t; + mutable inductives:(int * int) IndMap.t} + + type cl = Rep of representative| Eqto of int*equality + + type vertex = Leaf| Node of (int*int) + + type node = + {clas:cl; + vertex:vertex; + term:term; + mutable node_constr: int PacMap.t} + + type t={mutable size:int; + map:(int,node) Hashtbl.t; + syms:(term,int) Hashtbl.t; + sigtable:ST.t} + + let empty ():t={size=0; + map=Hashtbl.create init_size; + syms=Hashtbl.create init_size; + sigtable=ST.empty ()} + + let rec find uf i= + match (Hashtbl.find uf.map i).clas with + Rep _ -> i + | Eqto (j,_) ->find uf j + + let get_representative uf i= + let node=Hashtbl.find uf.map i in + match node.clas with + Rep r ->r + | _ -> anomaly "get_representative: not a representative" + + let get_constructor uf i= + match (Hashtbl.find uf.map i).term with + Constructor (cstr,_,_)->cstr + | _ -> anomaly "get_constructor: not a constructor" + + + let fathers uf i= + (get_representative uf i).fathers + + let size uf i= + (get_representative uf i).nfathers + + let add_father uf i t= + let r=get_representative uf i in + r.nfathers<-r.nfathers+1; + r.fathers<-t::r.fathers + + let pac_map uf i= + (get_representative uf i).constructors + + let pac_arity uf i sg= + (PacMap.find sg (get_representative uf i).constructors).arity + + let add_node_pac uf i sg j= + let node=Hashtbl.find uf.map i in + if not (PacMap.mem sg node.node_constr) then + node.node_constr<-PacMap.add sg j node.node_constr + + let mem_node_pac uf i sg= + PacMap.find sg (Hashtbl.find uf.map i).node_constr + + exception Discriminable of int * int * int * int * t + + let add_pacs uf i pacs = + let rep=get_representative uf i in + let pending=ref [] and combine=ref [] in + let add_pac sg pac= + try + let opac=PacMap.find sg rep.constructors in + if (snd sg)>0 then () else + let tk=pac.term_head + and tl=opac.term_head in + let rec f n lk ll q= + if n > 0 then match (lk,ll) with + k::qk,l::ql-> + let eq= + {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)} + in f (n-1) qk ql (eq::q) + | _-> anomaly + "add_pacs : weird error in injection subterms merge" + else q in + combine:=f pac.nhyps pac.args opac.args !combine + with Not_found -> (* Still Unknown Constructor *) + rep.constructors <- PacMap.add sg pac rep.constructors; + pending:= + (fathers uf (find uf pac.term_head)) @rep.fathers@ !pending; + let (c,a)=sg in + if a=0 then + let (ind,_)=get_constructor uf c in + try + let th2,hc2=IndMap.find ind rep.inductives in + raise (Discriminable (pac.term_head,c,th2,hc2,uf)) + with Not_found -> + rep.inductives<- + IndMap.add ind (pac.term_head,c) rep.inductives in + PacMap.iter add_pac pacs; + !pending,!combine + + let term uf i=(Hashtbl.find uf.map i).term + + let subterms uf i= + match (Hashtbl.find uf.map i).vertex with + Node(j,k) -> (j,k) + | _ -> anomaly "subterms: not a node" + + let signature uf i= + let j,k=subterms uf i in (find uf j,find uf k) + + let nodes uf= (* cherche les noeuds binaires *) + Hashtbl.fold + (fun i node l-> + match node.vertex with + Node (_,_)->i::l + | _ ->l) uf.map [] + + let next uf= + let n=uf.size in uf.size<-n+1; n + + let new_representative pm im= + {nfathers=0; + fathers=[]; + constructors=pm; + inductives=im} + + let rec add uf t= + try Hashtbl.find uf.syms t with + Not_found -> + let b=next uf in + let new_node= + match t with + Symb s -> + {clas=Rep (new_representative PacMap.empty IndMap.empty); + vertex=Leaf;term=t;node_constr=PacMap.empty} + | Appli (t1,t2) -> + let i1=add uf t1 and i2=add uf t2 in + add_father uf (find uf i1) b; + add_father uf (find uf i2) b; + {clas=Rep (new_representative PacMap.empty IndMap.empty); + vertex=Node(i1,i2);term=t;node_constr=PacMap.empty} + | Constructor (c,a,n) -> + let pacs= + PacMap.add (b,a) + {head_constr=b;arity=a;nhyps=n;args=[];term_head=b} + PacMap.empty in + let inds= + if a=0 then + let (ind,_)=c in + IndMap.add ind (b,b) IndMap.empty + else IndMap.empty in + {clas=Rep (new_representative pacs inds); + vertex=Leaf;term=t;node_constr=PacMap.empty} + in + Hashtbl.add uf.map b new_node; + Hashtbl.add uf.syms t b; + b + + let link uf i j eq= (* links i -> j *) + let node=Hashtbl.find uf.map i in + Hashtbl.replace uf.map i {node with clas=Eqto (j,eq)} + + let union uf i1 i2 eq= + let r1= get_representative uf i1 + and r2= get_representative uf i2 in + link uf i1 i2 eq; + r2.nfathers<-r1.nfathers+r2.nfathers; + r2.fathers<-r1.fathers@r2.fathers; + add_pacs uf i2 r1.constructors + + let rec down_path uf i l= + match (Hashtbl.find uf.map i).clas with + Eqto(j,t)->down_path uf j (((i,j),t)::l) + | Rep _ ->l + + let rec min_path=function + ([],l2)->([],l2) + | (l1,[])->(l1,[]) + | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2) + | cpl -> cpl + + let join_path uf i j= + assert (find uf i=find uf j); + min_path (down_path uf i [],down_path uf j []) + +end + +let rec combine_rec uf=function + []->[] + | t::pending-> + let combine=combine_rec uf pending in + let s=UF.signature uf t in + let u=snd (UF.subterms uf t) in + let f (c,a) pac pacs= + if a=0 then pacs else + let sg=(c,a-1) in + UF.add_node_pac uf t sg pac.term_head; + PacMap.add sg {pac with args=u::pac.args;term_head=t} pacs + in + let pacs=PacMap.fold f (UF.pac_map uf (fst s)) PacMap.empty in + let i=UF.find uf t in + let (p,c)=UF.add_pacs uf i pacs in + let combine2=(combine_rec uf p)@c@combine in + try {lhs=t;rhs=ST.query s uf.UF.sigtable;rule=Congruence}::combine2 with + Not_found-> + ST.enter t s uf.UF.sigtable;combine2 + +let rec process_rec uf=function + []->[] + | eq::combine-> + let pending=process_rec uf combine in + let i=UF.find uf eq.lhs + and j=UF.find uf eq.rhs in + if i=j then + pending + else + if (UF.size uf i)<(UF.size uf j) then + let l=UF.fathers uf i in + let (p,c)=UF.union uf i j eq in + let _ =ST.delete_list l uf.UF.sigtable in + let inj_pending=process_rec uf c in + inj_pending@p@l@pending + else + let l=UF.fathers uf j in + let (p,c)=UF.union uf j i (swap eq) in + let _ =ST.delete_list l uf.UF.sigtable in + let inj_pending=process_rec uf c in + inj_pending@p@l@pending + +let rec cc_rec uf=function + []->() + | pending-> + let combine=combine_rec uf pending in + let pending0=process_rec uf combine in + cc_rec uf pending0 + +let cc uf=cc_rec uf (UF.nodes uf) + +let rec make_uf=function + []->UF.empty () + | (ax,(t1,t2))::q-> + let uf=make_uf q in + let i1=UF.add uf t1 in + let i2=UF.add uf t2 in + let j1=UF.find uf i1 and j2=UF.find uf i2 in + if j1=j2 then uf else + let (_,inj_combine)= + UF.union uf j1 j2 {lhs=i1;rhs=i2;rule=Axiom ax} in + let _ = process_rec uf inj_combine in uf + +let add_one_diseq uf (t1,t2)=(UF.add uf t1,UF.add uf t2) + +let add_disaxioms uf disaxioms= + let f (id,cpl)=(id,add_one_diseq uf cpl) in + List.map f disaxioms + +let check_equal uf (i1,i2) = UF.find uf i1 = UF.find uf i2 + +let find_contradiction uf diseq = + List.find (fun (id,cpl) -> check_equal uf cpl) diseq + + diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli new file mode 100644 index 00000000..47cdb3ea --- /dev/null +++ b/contrib/cc/ccalgo.mli @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: ccalgo.mli,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *) + +type pa_constructor + (*{head: int; arity: int; args: (int * int) list}*) + +module PacMap:Map.S with type key=int * int + +type term = + Symb of Term.constr + | Appli of term * term + | Constructor of Names.constructor*int*int + +type rule = + Congruence + | Axiom of Names.identifier + | Injection of int*int*int*int + +type equality = + {lhs : int; + rhs : int; + rule : rule} + +module ST : +sig + type t + val empty : unit -> 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 + +module UF : +sig + type t + exception Discriminable of int * int * int * int * t + val empty : unit -> t + val find : t -> int -> int + val size : t -> int -> int + val get_constructor : t -> int -> Names.constructor + val pac_arity : t -> int -> int * int -> int + val mem_node_pac : t -> int -> int * int -> int + val add_pacs : t -> int -> pa_constructor PacMap.t -> + int list * equality list + val term : t -> int -> term + val subterms : t -> int -> int * int + val add : t -> term -> int + val union : t -> int -> int -> equality -> int list * equality list + val join_path : t -> int -> int -> + ((int*int)*equality) list* + ((int*int)*equality) list +end + + +val combine_rec : UF.t -> int list -> equality list +val process_rec : UF.t -> equality list -> int list + +val cc : UF.t -> unit + +val make_uf : + (Names.identifier * (term * term)) list -> UF.t + +val add_one_diseq : UF.t -> (term * term) -> int * int + +val add_disaxioms : + UF.t -> (Names.identifier * (term * term)) list -> + (Names.identifier * (int * int)) list + +val check_equal : UF.t -> int * int -> bool + +val find_contradiction : UF.t -> + (Names.identifier * (int * int)) list -> + (Names.identifier * (int * int)) + + + diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml new file mode 100644 index 00000000..fa525e65 --- /dev/null +++ b/contrib/cc/ccproof.ml @@ -0,0 +1,157 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: ccproof.ml,v 1.8.2.1 2004/07/16 19:29:58 herbelin Exp $ *) + +(* This file uses the (non-compressed) union-find structure to generate *) +(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) + +open Util +open Names +open Ccalgo + +type proof= + Ax of identifier + | SymAx of identifier + | 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) + +let pcongr=function + Refl t1, Refl t2 ->Refl (Appli (t1,t2)) + | p1, p2 -> Congr (p1,p2) + +let build_proof uf= + + let rec equal_proof i j= + if i=j then Refl (UF.term uf i) else + let (li,lj)=UF.join_path uf i j in + 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->Ax s + | Congruence ->congr_proof eq.lhs eq.rhs + | Injection (ti,tj,c,a) -> + let p=equal_proof ti tj in + let p1=constr_proof ti ti c 0 + and p2=constr_proof tj tj c 0 in + match UF.term uf c with + Constructor (cstr,nargs,nhyps) -> + Inject(ptrans(psym p1,ptrans(p,p2)),cstr,nhyps,a) + | _ -> anomaly "injection on non-constructor terms" + in ptrans(ptrans (pi,pij),pj) + + and constr_proof i j c n= + try + let nj=UF.mem_node_pac uf j (c,n) in + let (ni,arg)=UF.subterms uf j in + let p=constr_proof ni nj c (n+1) in + let targ=UF.term uf arg in + ptrans (equal_proof i j, pcongr (p,Refl targ)) + with Not_found->equal_proof i j + + and path_proof i=function + [] -> Refl (UF.term uf i) + | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x) + + and congr_proof i j= + let (i1,i2) = UF.subterms uf i + and (j1,j2) = UF.subterms uf j in + pcongr (equal_proof i1 j1, equal_proof i2 j2) + + and discr_proof i ci j cj= + let p=equal_proof i j + and p1=constr_proof i i ci 0 + and p2=constr_proof j j cj 0 in + ptrans(psym p1,ptrans(p,p2)) + in + function + `Prove_goal (i,j) | `Refute_hyp (i,j) -> equal_proof i j + | `Discriminate (i,ci,j,cj)-> discr_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->List.assoc s axioms + | SymAx s-> let (t1,t2)=List.assoc s axioms 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) + +let by_contradiction uf diseq axioms disaxioms= + try + let id,cpl=find_contradiction uf diseq in + let prf=build_proof uf (`Refute_hyp cpl) in + if List.assoc id disaxioms=type_proof axioms prf then + `Refute_hyp (id,prf) + else + anomaly "wrong proof generated" + with Not_found -> + errorlabstrm "Congruence" (Pp.str "I couldn't solve goal") + +let cc_proof axioms disaxioms glo= + try + let uf=make_uf axioms in + let diseq=add_disaxioms uf disaxioms in + match glo with + Some cpl -> + let goal=add_one_diseq uf cpl in cc uf; + if check_equal uf goal then + let prf=build_proof uf (`Prove_goal goal) in + if cpl=type_proof axioms prf then + `Prove_goal prf + else anomaly "wrong proof generated" + else by_contradiction uf diseq axioms disaxioms + | None -> cc uf; by_contradiction uf diseq axioms disaxioms + with UF.Discriminable (i,ci,j,cj,uf) -> + let prf=build_proof uf (`Discriminate (i,ci,j,cj)) in + `Discriminate (UF.get_constructor uf ci,prf) + + diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli new file mode 100644 index 00000000..887ed070 --- /dev/null +++ b/contrib/cc/ccproof.mli @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: ccproof.mli,v 1.6.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +open Ccalgo +open Names + +type proof = + Ax of identifier + | SymAx of identifier + | Refl of term + | Trans of proof * proof + | Congr of proof * proof + | Inject of proof * constructor * int * int + +val pcongr : proof * proof -> proof +val ptrans : proof * proof -> proof +val psym : proof -> proof +val pcongr : proof * proof -> proof + +val build_proof : + UF.t -> + [ `Discriminate of int * int * int * int + | `Prove_goal of int * int + | `Refute_hyp of int * int ] + -> proof + +val type_proof : + (identifier * (term * term)) list -> proof -> term * term + +val cc_proof : + (identifier * (term * term)) list -> + (identifier * (term * term)) list -> + (term * term) option -> + [ `Discriminate of constructor * proof + | `Prove_goal of proof + | `Refute_hyp of identifier * proof ] + + diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 new file mode 100644 index 00000000..49fe46fe --- /dev/null +++ b/contrib/cc/cctac.ml4 @@ -0,0 +1,247 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id: cctac.ml4,v 1.13.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +(* This file is the interface between the c-c algorithm and Coq *) + +open Evd +open Proof_type +open Names +open Libnames +open Nameops +open Inductiveops +open Declarations +open Term +open Termops +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 constant dir s = lazy (Coqlib.gen_constant "CC" dir s) + +let f_equal_theo = constant ["Init";"Logic"] "f_equal" + +let eq_rect_theo = constant ["Init";"Logic"] "eq_rect" + +(* decompose member of equality in an applicative format *) + +let rec decompose_term env t= + match kind_of_term t with + App (f,args)-> + let tf=decompose_term env f in + let targs=Array.map (decompose_term env) args in + Array.fold_left (fun s t->Appli (s,t)) tf targs + | Construct c-> + let (_,oib)=Global.lookup_inductive (fst c) in + let nargs=mis_constructor_nargs_env env c in + Constructor (c,nargs,nargs-oib.mind_nparams) + | _ ->(Symb t) + +(* decompose equality in members and type *) + +let rec eq_type_of_term term= + match kind_of_term term with + App (f,args)-> + (try + let ref = reference_of_constr f in + if ref=Coqlib.glob_eq && (Array.length args)=3 + then (true,args.(0),args.(1),args.(2)) + else + if ref=(Lazy.force Coqlib.coq_not_ref) && + (Array.length args)=1 then + let (pol,t,a,b)=eq_type_of_term args.(0) in + if pol then (false,t,a,b) else fail () + else fail () + with Not_found -> fail ()) + | Prod (_,eq,ff) -> + (try + let ref = reference_of_constr ff in + if ref=(Lazy.force Coqlib.coq_False_ref) then + let (pol,t,a,b)=eq_type_of_term eq in + if pol then (false,t,a,b) else fail () + else fail () + with Not_found -> fail ()) + | _ -> fail () + +(* read an equality *) + +let read_eq env term= + let (pol,_,t1,t2)=eq_type_of_term term in + (pol,(decompose_term env t1,decompose_term env t2)) + +(* rebuild a term from applicative format *) + +let rec make_term=function + Symb s->s + | Constructor(c,_,_)->mkConstruct c + | Appli (s1,s2)-> + make_app [(make_term s2)] s1 +and make_app l=function + Symb s->applistc s l + | Constructor(c,_,_)->applistc (mkConstruct c) l + | Appli (s1,s2)->make_app ((make_term s2)::l) s1 + +(* store all equalities from the context *) + +let rec read_hyps env=function + []->[],[] + | (id,_,e)::hyps->let eq,diseq=read_hyps env hyps in + try let pol,cpl=read_eq env e in + if pol then + ((id,cpl)::eq),diseq + else + eq,((id,cpl)::diseq) + with Not_an_eq -> eq,diseq + +(* build a problem ( i.e. read the goal as an equality ) *) + +let make_prb gl= + let env=pf_env gl in + let eq,diseq=read_hyps env gl.it.evar_hyps in + try + let pol,cpl=read_eq env gl.it.evar_concl in + if pol then (eq,diseq,Some cpl) else assert false with + Not_an_eq -> (eq,diseq,None) + +(* 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 destApplication intype with + Invalid_argument _ -> (intype,[||]) in + let ind=destInd h in + let types=Inductive.arities_of_constructors env ind in + let lp=Array.length types in + let ci=(snd cstr)-1 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_default_case_info (pf_env gls) RegularStyle ind 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 rec proof_tac axioms=function + Ax id->exact_check (mkVar id) + | SymAx id->tclTHEN symmetry (exact_check (mkVar id)) + | Refl t->reflexivity + | Trans (p1,p2)->let t=(make_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=make_term f1 and tx1=make_term x1 + and tf2=make_term f2 and tx2=make_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_theo,[|typf;typfx;appx1;tf1;tf2|]) + and lemma2= + mkApp(Lazy.force f_equal_theo,[|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=make_term ti in + let ctj=make_term tj in + let cai=make_term ai in + let intype=pf_type_of gls cti in + let outtype=pf_type_of gls cai in + let special=mkRel (1+nargs-argind) in + let default=make_term ai in + let proj=build_projection intype outtype cstr special default gls in + let injt= + mkApp (Lazy.force f_equal_theo,[|intype;outtype;proj;cti;ctj|]) in + tclTHEN (apply injt) (proof_tac axioms prf) gls) + +let refute_tac axioms disaxioms id p gls = + let t1,t2=List.assoc id disaxioms in + let tt1=make_term t1 and tt2=make_term t2 in + let intype=pf_type_of gls tt1 in + let neweq= + mkApp(constr_of_reference Coqlib.glob_eq, + [|intype;tt1;tt2|]) in + let hid=pf_get_new_id (id_of_string "Heq") gls in + let false_t=mkApp (mkVar id,[|mkVar hid|]) in + tclTHENS (true_cut (Name hid) neweq) + [proof_tac axioms p; simplest_elim false_t] gls + +let discriminate_tac axioms cstr p gls = + let t1,t2=type_proof axioms p in + let tt1=make_term t1 and tt2=make_term t2 in + let intype=pf_type_of gls tt1 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_theo, + [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in + let endt=mkApp (Lazy.force eq_rect_theo, + [|outtype;trivial;pred;identity;concl;injt|]) in + let neweq=mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in + tclTHENS (true_cut (Name hid) neweq) + [proof_tac axioms p;exact_check endt] gls + +(* wrap everything *) + +let cc_tactic gls= + Library.check_required_library ["Coq";"Init";"Logic"]; + let (axioms,disaxioms,glo)=make_prb gls in + match (cc_proof axioms disaxioms glo) with + `Prove_goal p -> proof_tac axioms p gls + | `Refute_hyp (id,p) -> refute_tac axioms disaxioms id p gls + | `Discriminate (cstr,p) -> discriminate_tac axioms cstr p gls + +(* Tactic registration *) + +TACTIC EXTEND CC + [ "Congruence" ] -> [ tclSOLVE [tclTHEN (tclREPEAT introf) cc_tactic] ] +END + |