CC: added injection theory

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 388 insertions, 232 deletions

diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index 2dc2216a5..d7f056dcc 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -11,76 +11,179 @@
 (* 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}
 
-type valid={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}
 
-let congr_valid i j= {lhs=i;rhs=j;rule=Congruence}
+(* Signature table *)
 
-let ax_valid i j id= {lhs=i;rhs=j;rule=Axiom id}
+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
 
-  type cl=Rep of int*(int list)|Eqto of int*valid
+module PacSet=Set.Make(struct type t=int*int let compare=compare end) 
+
+  type representative=
+      {mutable nfathers:int;
+       mutable fathers:int list;
+       mutable constructors:pa_constructor PacMap.t}
 
-  type vertex=Leaf|Node of (int*int) 
+  type cl = Rep of representative| Eqto of int*equality
 
-  type node={clas:cl;vertex:vertex;term:term}    
+  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}
-	
+          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}
+		  syms=Hashtbl.create init_size;
+		  sigtable=ST.empty ()}
 
-  let add_lst i t uf=
-    let node=Hashtbl.find uf.map i in
-      match node.clas with
-	  Rep(l,lst)->Hashtbl.replace uf.map i 
-	    {node with clas=Rep(l+1,t::lst)}
-	| _ ->failwith "add_lst: not a representative"
-	    
   let rec find uf i=
     match (Hashtbl.find uf.map i).clas with
-	Rep(_,_) -> i
-      | Eqto(j,_) ->find uf j
+	Rep _ -> i
+      | Eqto (j,_) ->find uf j
 	  
-  let list uf i=
-    match (Hashtbl.find uf.map i).clas with
-	Rep(_,lst)-> lst
-      | _ ->failwith "list: not a class"
+  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 fathers uf i=
+    (get_representative uf i).fathers
 	  
   let size uf i=
-    match (Hashtbl.find uf.map i).clas with
-	Rep (l,_) -> l
-      | _ ->failwith "size: not a class"
+    (get_representative uf i).nfathers
 
-  let term uf i=(Hashtbl.find uf.map i).term
+  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
+  
+  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 qq=
+		      {lhs=k;rhs=l;rule=Injection(tk,tl,pac.head_constr,n)}::q 
+		    in
+		      f (n-1) qk ql qq 
+		| _->anomaly 
+		    "add_pacs : weird error in injection subterms merge"
+	      else q in
+ 	      combine:=f pac.nhyps pac.args opac.args !combine
+      with Not_found ->
+	rep.constructors <- PacMap.add sg pac rep.constructors;
+	pending:=(fathers uf (find uf pac.term_head))@rep.fathers@ !pending 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)
-      | _ -> failwith "subterms: not a node"
+      | _ -> anomaly "subterms: not a node"
 
   let signature uf i=
-    match (Hashtbl.find uf.map i).vertex with
-	Node(j,k)->(find uf j,find uf k)
-      | _ ->failwith "signature: not a node"
+    let j,k=subterms uf i in (find uf j,find uf k)
 
   let nodes uf=  (* cherche les noeuds binaires *)
     Hashtbl.fold 
@@ -92,43 +195,51 @@ module UF = struct
   let next uf=
     let n=uf.size in uf.size<-n+1; n
 	
-  let rec add t uf= 
+  let new_representative l={nfathers=0;fathers=[];constructors=l}
+
+  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 (0,[]);
-		   vertex=Leaf;
-		   term=t}
+		  {clas=Rep (new_representative PacMap.empty);
+		   vertex=Leaf;term=t;node_constr=PacMap.empty}
 	      | Appli (t1,t2) -> 
-		  let i1=add t1 uf 
-		  and i2=add t2 uf in
-		    add_lst (find uf i1) b uf;
-		    add_lst (find uf i2) b uf;
-		    {clas=Rep (0,[]);
-		     vertex=Node(i1,i2);
-		     term=t}
-      in
+		  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);
+		     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
+		    {clas=Rep (new_representative pacs);
+		     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 t=
-    let node1=(Hashtbl.find uf.map i1) 
-    and node2=(Hashtbl.find uf.map i2) in
-      match node1.clas,node2.clas with
-	  Rep (l1,lst1),Rep (l2,lst2) -> 
-	    Hashtbl.replace uf.map i2 {node2 with clas=Eqto (i1,t)};
-	    Hashtbl.replace uf.map i1 
-	      {node1 with clas=Rep(l2+l1,lst2@lst1)}
-	| _ ->failwith "union: not classes"	  	  
-	    
-  let rec up_path uf i l=
+  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)->up_path uf j (((i,j),t)::l)
-      | Rep(_,_)->l
+	Eqto(j,t)->down_path uf j (((i,j),t)::l)
+      | Rep _ ->l
 
   let rec min_path=function
       ([],l2)->([],l2)
@@ -138,113 +249,70 @@ module UF = struct
 	
   let join_path uf i j=
     assert (find uf i=find uf j);
-    min_path (up_path uf i [],up_path uf j [])
+    min_path (down_path uf i [],down_path uf j [])
       
 end    
     
-(* 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 
-	failwith "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
-    
-let rec combine_rec uf st=function 
+let rec combine_rec uf=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
+  | 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 v s st;combine
+	  ST.enter t s uf.UF.sigtable;combine2
 	    
-let rec process_rec uf st=function
+let rec process_rec uf=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 then 
-	pending 
+  | 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.list uf i in
-	  UF.union uf j i (congr_valid v w);
-	  ST.delete_list l st;
-	  l@pending
+	  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.list uf j in
-	  UF.union uf i j (congr_valid w v);
-	  ST.delete_list l st;
-	  l@pending
+	  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 st=function
+let rec cc_rec uf=function
     []->()
   | pending->
-      let combine=combine_rec uf st pending in
-      let pending0=process_rec uf st combine in
-      (cc_rec uf st pending0)
+      let combine=combine_rec uf pending in
+      let pending0=process_rec uf combine in
+	cc_rec uf pending0
 	
-let cc uf=(cc_rec uf (ST.empty ()) (UF.nodes uf))
+let cc uf=cc_rec uf (UF.nodes uf)
 
 let rec make_uf=function
-    []->(UF.empty ())
-  | (ax,(v,w))::q->
+    []->UF.empty ()
+  | (ax,(t1,t2))::q->
       let uf=make_uf q in
-      let i1=UF.add v uf in
-      let i2=UF.add w uf in
-      UF.union uf (UF.find uf i2) (UF.find uf i1) (ax_valid i1 i2 ax);
-      uf
-	
-
-
-
-
-
-    
-    
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+      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
+      
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 582df715f..941adab17 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -8,54 +8,60 @@
 
 (* $Id$ *)
 
-val init_size : int
+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      
+  | Axiom of Names.identifier
+  | Injection of int*int*int*int
 
-type valid =
+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 
   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 pac_arity : t -> int -> int * int -> int
+  val mem_node_pac : t -> int -> int * int -> int 
   val term : t -> int -> term    
   val subterms : t -> int -> int * int
-  val signature : t -> int -> int * int
-  val nodes : t -> int list
-  val add : term -> t -> int
-  val union : t -> int -> int -> valid -> unit
+  val add : t -> term -> int
+  val union : t -> int -> int -> equality -> int list * equality list
   val join_path : t -> int -> int -> 
-    ((int*int)*valid) list*
-    ((int*int)*valid) list
+    ((int*int)*equality) list*
+    ((int*int)*equality) list
 end
-
   
-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
 
+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
-
+  
+  
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index f3c86d9c5..95752c122 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -11,18 +11,20 @@
 (* 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
-  | Sym of proof
   | Congr of proof*proof
+  | Inject of proof*constructor*int*int 
 		  
 let pcongr=function
-    Refl t1, Refl t2 ->Refl (Appli (t1,t2))
+    Refl t1, Refl t2 -> Refl (Appli (t1,t2))
   | p1, p2 -> Congr (p1,p2)
 
 let rec ptrans=function
@@ -36,32 +38,54 @@ let rec ptrans=function
 	
 let rec psym=function
     Refl p->Refl p
-  | Sym p->p
-  | Ax s-> Sym(Ax s)
+  | 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 pid (s:string) (p:proof)=p
 	
 let build_proof uf i j=
   
   let rec equal_proof i j=
-    let (li,lj)=UF.join_path uf i j in
-      ptrans (path_proof i li,psym (path_proof j lj))
+    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),t)=
-    let pi=equal_proof i t.lhs in
-    let pj=psym (equal_proof j t.rhs) in
+  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 t.rule with 
+      match eq.rule with 
 	  Axiom s->Ax s
-	| Congruence->congr_proof t.lhs t.rhs
+	| Congruence ->congr_proof eq.lhs eq.rhs
+	| Injection (ti,tj,c,a) ->
+	    let p=equal_proof ti tj in
+	    let arity=UF.pac_arity uf (UF.find uf ti) (c,0) in
+	    let p1=constr_proof ti ti c 0 arity
+	    and p2=constr_proof tj tj c 0 arity  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 a=
+       if n<a then 
+	 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) a in
+	 let targ=UF.term uf arg in 
+	   ptrans (equal_proof i j, pcongr (p,Refl targ))
+       else equal_proof i j
+
   and path_proof i=function
-      [] -> let t=UF.term uf i in Refl t
+      [] -> Refl (UF.term uf i)
     | x::q->ptrans (path_proof j q,edge_proof x)
   
   and congr_proof i j=
@@ -72,31 +96,44 @@ let build_proof uf i j=
   in
     equal_proof i j
 
+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
-  | 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 failwith "invalid transitivity"
-  | Sym p->let (t1,t2)=type_proof axioms p in (t2,t1)
-  | Congr (p1,p2)->
-      let (i1,j1)=type_proof axioms p1
-      and (i2,j2)=type_proof axioms p2 in
-      Appli (i1,i2),Appli (j1,j2)
-	
+      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)
+
+exception Wrong_proof of proof
+
 let cc_proof (axioms,(v,w))=
   let uf=make_uf axioms in
-  let i1=UF.add v uf in
-  let i2=UF.add w uf in
+  let i1=UF.add uf v in
+  let i2=UF.add uf w in
   cc uf;
   if UF.find uf i1=UF.find uf i2 then 
     let prf=build_proof uf i1 i2 in
       if (v,w)=type_proof axioms prf then Some (prf,uf,axioms) 
-      else failwith "Proof check failed !!"
+      else anomaly "Oops !! Wrong equality proof generated"
   else
-    None;;
+    None
 
     
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 2dcb01e14..99ed30d99 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -12,18 +12,23 @@ open Ccalgo
 
 type proof =
     Ax of Names.identifier
+  | SymAx of Names.identifier
   | Refl of term
   | Trans of proof * proof
-  | Sym of proof
   | Congr of proof * proof
+  | Inject of proof * Names.constructor * int * int
 
 val pcongr : proof * proof -> proof
 val ptrans : proof * proof -> proof
 val psym : proof -> proof
 val pcongr : proof * proof -> proof
 
+val pid : string -> proof -> proof
+
 val build_proof : UF.t -> int -> int -> proof
 
+exception Wrong_proof of proof
+
 val type_proof :
   (Names.identifier * (term * term)) list -> proof -> term * term
 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 247bac99a..85e8c9ae8 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -17,6 +17,8 @@ open Proof_type
 open Names
 open Libnames
 open Nameops
+open Inductiveops
+open Declarations
 open Term
 open Tacmach
 open Tactics
@@ -34,24 +36,24 @@ let fail()=raise Not_an_eq
     
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
-let eq2eqT_theo = constant ["Logic";"Eqdep_dec"] "eq2eqT"
-let eqT2eq_theo = constant ["Logic";"Eqdep_dec"] "eqT2eq"
+let f_equal_theo = constant ["Init";"Logic"] "f_equal"
 let congr_theo = constant ["cc";"CC"] "Congr_nodep"
 let congr_dep_theo = constant ["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=
+let rec decompose_term env 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)
-
+      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 eq_type_of_term term=
@@ -68,50 +70,77 @@ let eq_type_of_term term=
 
 (* read an equality *)
 	  
-let read_eq term=
+let read_eq env term=
   let (_,t1,t2)=eq_type_of_term term in 
-    ((decompose_term t1),(decompose_term t2))
+    (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=function
+let rec read_hyps env=function
     []->[]
-  | (id,_,e)::hyps->let q=(read_hyps hyps) in
-      try (id,(read_eq e))::q with Not_an_eq -> q
+  | (id,_,e)::hyps->let q=(read_hyps env hyps) in
+      try (id,(read_eq env 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)
+  let env=pf_env gl in
+  (read_hyps env gl.it.evar_hyps,read_eq env gl.it.evar_concl)
+
+(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
+
+let build_projection (cstr:constructor) nargs argind ttype default atype gls=
+  let (h,argv) = destApplication ttype in
+  let ind=destInd h in 
+  let (mib,mip) = Global.lookup_inductive ind in
+  let n = mip.mind_nparams in
+    (* assert (n=(Array.length argv));*)
+  let lp=Array.length mip.mind_consnames in
+  let types=mip.mind_nf_lc 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 mkRel (1+nargs-argind) 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,ttype,atype) in
+  let env=pf_env gls 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 "C") gls in     
+    mkLambda(Name id,ttype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
 let rec proof_tac uf 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 uf axioms p1);(proof_tac uf axioms p2)])
-  | Sym p->tclTHEN symmetry (proof_tac uf axioms p)
   | Congr (p1,p2)->
-      (fun gl->
+      (fun gls->
 	 let (s1,t1)=(type_proof axioms p1) and
 	   (s2,t2)=(type_proof 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 typ1=pf_type_of gls ts1 and typ2=pf_type_of gls ts2 in
+      let (typb,_,_)=(eq_type_of_term gls.it.evar_concl) in
       let act=mkApp ((Lazy.force congr_theo),[|typ2;typb;ts1;tt1;ts2;tt2|]) in
       tclORELSE 
 	(tclTHENS 
@@ -121,18 +150,29 @@ let rec proof_tac uf axioms=function
 	      (let p=mkLambda(destProd typ1) in
 	      let acdt=mkApp((Lazy.force congr_dep_theo),
 			     [|typ2;p;ts1;tt1;ts2|]) in 
-	      apply acdt) (proof_tac uf axioms p1))
-	gl)
+	      apply acdt) (proof_tac uf axioms p1)) 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 ttype=pf_type_of gls cti in
+	 let atype=pf_type_of gls cai in
+	 let proj=build_projection cstr nargs argind ttype cai atype gls in
+	 let injt=
+	   mkApp (Lazy.force f_equal_theo,[|ttype;atype;proj;cti;ctj|]) in   
+	   tclTHEN (apply injt) (proof_tac uf axioms prf) gls)
 
 (* wrap everything *)
 	
 let cc_tactic gls=
   Library.check_required_library ["Coq";"cc";"CC"];
   let prb=
-    try make_prb gls.it with 
+    try make_prb gls with 
 	Not_an_eq ->
-	  errorlabstrm  "CC" 
-	  [< str "Goal is not an equality" >] in
+	  errorlabstrm  "CC" [< str "Goal is not an equality" >] in
     match (cc_proof prb) with
 	None->errorlabstrm  "CC" [< str "CC couldn't solve goal" >] 
       | Some (p,uf,axioms)->