ground->firstorder, cc-> congruence, CC final commit

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

6 files changed, 119 insertions, 68 deletions

diff --git a/contrib/cc/CC.v b/contrib/cc/CCSolve.v
index ff850ea57..30622aeaa 100644
--- a/contrib/cc/CC.v
+++ b/contrib/cc/CCSolve.v
@@ -8,15 +8,13 @@
 
 (* $Id$ *)
 
-(* Here were some deprecated lemmata *)
-
 Tactic Definition CCsolve :=
  Repeat (Match Context With
  [ H: ?1 |- ?2] -> 
   Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1);[CC|(Rewrite Heq;Exact H)])
+ (Assert Heq:(?2==?1);[Congruence|(Rewrite Heq;Exact H)])
  |[ H: ?1; G: ?2 -> ?3 |- ?] ->                        
   Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1) ;[CC|                              
+ (Assert Heq:(?2==?1) ;[Congruence|                              
      (Rewrite Heq in G;Generalize (G H);Clear G;Intro G)])).  
 
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index d7f056dcc..5f83e3f79 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -86,12 +86,13 @@ end
     
 module UF = struct
 
-module PacSet=Set.Make(struct type t=int*int let compare=compare end) 
+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 constructors:pa_constructor PacMap.t;
+       mutable inductives:(int * int) IndMap.t}
 
   type cl = Rep of representative| Eqto of int*equality
 
@@ -124,6 +125,12 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	  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
 	  
@@ -149,6 +156,8 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
   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 
@@ -161,17 +170,26 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	    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 
+		    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 ->
+      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 in
+	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
 	
@@ -195,7 +213,11 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
   let next uf=
     let n=uf.size in uf.size<-n+1; n
 	
-  let new_representative l={nfathers=0;fathers=[];constructors=l}
+  let new_representative pm im=
+    {nfathers=0;
+     fathers=[];
+     constructors=pm;
+     inductives=im}
 
   let rec add uf t= 
     try Hashtbl.find uf.syms t with 
@@ -204,20 +226,25 @@ module PacSet=Set.Make(struct type t=int*int let compare=compare end)
 	  let new_node=
 	    match t with
 		Symb s -> 
-		  {clas=Rep (new_representative PacMap.empty);
+		  {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);
+		    {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
-		    {clas=Rep (new_representative pacs);
+		  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;
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 941adab17..0343c9621 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -41,11 +41,14 @@ 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 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
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 95752c122..9bcdf56f2 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -48,9 +48,11 @@ 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=
+type ('a,'b) mission=
+    Prove of 'a
+  | Refute of 'b
+
+let build_proof uf=
   
   let rec equal_proof i j=
     if i=j then Refl (UF.term uf i) else 
@@ -66,35 +68,41 @@ let build_proof uf i j=
 	| 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
+	    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 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 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 j q,edge_proof x)
+    | 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
-    equal_proof i j
+    function
+	Prove(i,j)-> equal_proof i j
+      | Refute(i,ci,j,cj)-> discr_proof i ci j cj
 
 let rec nth_arg t n=
   match t with 
@@ -121,21 +129,27 @@ let rec type_proof axioms p=
 	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 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 anomaly "Oops !! Wrong equality proof generated"
-  else
-    None
-
-    
-
+let cc_proof (axioms,m)=
+  try
+    let uf=make_uf axioms in
+      match m with 
+	  Some (v,w) ->
+	    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 (Prove(i1,i2)) in
+		  if (v,w)=type_proof axioms prf then
+		    Prove (prf,axioms)
+		  else anomaly "wrong proof generated"
+	      else
+		errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+	| None ->
+	    cc uf;
+	    errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+    with UF.Discriminable (i,ci,j,cj,uf) ->
+      let prf=build_proof uf (Refute(i,ci,j,cj)) in 
+      let (t1,t2)=type_proof axioms prf in 
+	Refute (t1,t2,prf,axioms) 
 
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 99ed30d99..664ac31f8 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -23,16 +23,17 @@ val ptrans : proof * proof -> proof
 val psym : proof -> proof
 val pcongr : proof * proof -> proof
 
-val pid : string -> proof -> proof
+type ('a,'b) mission=
+    Prove of 'a
+  | Refute of 'b
 
-val build_proof : UF.t -> int -> int -> proof
-
-exception Wrong_proof of proof
+val build_proof : UF.t -> (int * int, int * int * int * int) mission -> proof
 
 val type_proof :
   (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
+  (Names.identifier * (term * term)) list * (term * term) option ->
+  (proof * (Names.identifier * (term * term)) list, 
+   term * term * proof * (Names.identifier * (term * term)) list ) mission
 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 2bc225b66..2089d5997 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -37,8 +37,6 @@ 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 congr_theo = constant ["cc";"CC"] "Congr_nodep"
-let congr_dep_theo = constant ["cc";"CC"] "Congr_dep"
 
 (* decompose member of equality in an applicative format *)
 
@@ -96,7 +94,10 @@ let rec read_hyps env=function
 	
 let make_prb gl=
   let env=pf_env gl in
-  (read_hyps env gl.it.evar_hyps,read_eq env gl.it.evar_concl)
+  let hyps=read_hyps env gl.it.evar_hyps in
+    try (hyps,Some (read_eq env gl.it.evar_concl)) with 
+	Not_an_eq -> (hyps,None)
+
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
@@ -126,13 +127,13 @@ let build_projection (cstr:constructor) nargs argind ttype default atype gls=
 
 (* generate an adhoc tactic following the proof tree  *)
 
-let rec proof_tac uf axioms=function
+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 uf axioms p1);(proof_tac uf axioms p2)])
+	 [(proof_tac axioms p1);(proof_tac axioms p2)])
   | Congr (p1,p2)->
       fun gls->
 	let (f1,f2)=(type_proof axioms p1) 
@@ -148,9 +149,9 @@ let rec proof_tac uf axioms=function
 	and lemma2=
 	  mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in
 	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
-	     [tclTHEN (apply lemma1) (proof_tac uf axioms p1);
+	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
   	      tclFIRST
-		[tclTHEN (apply lemma2) (proof_tac uf axioms p2);
+		[tclTHEN (apply lemma2) (proof_tac axioms p2);
 		 reflexivity;
 		 fun gls ->
 		   errorlabstrm  "CC" 
@@ -169,7 +170,7 @@ let rec proof_tac uf axioms=function
 	 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)
+	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
 
 (* wrap everything *)
 	
@@ -180,13 +181,20 @@ let cc_tactic gls=
 	Not_an_eq ->
 	  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)->proof_tac uf axioms p gls
-	
+        Prove (p,axioms)-> proof_tac axioms p gls
+      | Refute (t1,t2,p,axioms) ->
+	  let tt1=make_term t1 and tt2=make_term t2 in
+	  let typ=pf_type_of gls tt1 in
+	  let id=pf_get_new_id (id_of_string "Heq") gls in     
+	  let neweq=
+	    mkApp(constr_of_reference Coqlib.glob_eq,[|typ;tt1;tt2|]) in
+	    tclTHENS (true_cut (Some id) neweq)
+	      [proof_tac axioms p;Equality.discr id] gls
+
 (* Tactic registration *)
       
 TACTIC EXTEND CC
- [ "CC" ] -> [ cc_tactic ]
+ [ "Congruence" ] -> [ cc_tactic ]
 END