congruence now handles disequalities

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

6 files changed, 146 insertions, 83 deletions

diff --git a/contrib/cc/CCSolve.v b/contrib/cc/CCSolve.v
index c80ba16ec3..9c541ce84d 100644
--- a/contrib/cc/CCSolve.v
+++ b/contrib/cc/CCSolve.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Ltac CCsolve :=
+Ltac ccsolve :=
   repeat
    match goal with
    | H:?X1 |- ?X2 =>
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index 5f83e3f790..eb640d5d72 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -343,3 +343,15 @@ let rec make_uf=function
 		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 i2 = 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
index ee34b5e8f7..f5b05f5182 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -67,5 +67,18 @@ 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
index fadd2d080c..88669f45d2 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -48,10 +48,6 @@ let pcongr=function
     Refl t1, Refl t2 ->Refl (Appli (t1,t2))
   | p1, p2 -> Congr (p1,p2)
 
-type ('a,'b) mission=
-    Prove of 'a
-  | Refute of 'b
-
 let build_proof uf=
   
   let rec equal_proof i j=
@@ -101,8 +97,8 @@ let build_proof uf=
       ptrans(psym p1,ptrans(p,p2))
   in
     function
-	Prove(i,j)-> equal_proof i j
-      | Refute(i,ci,j,cj)-> discr_proof i ci j cj
+	`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 
@@ -129,27 +125,34 @@ let rec type_proof axioms p=
 	let (ti,tj)=type_proof axioms p in
 	  nth_arg ti (n-a),nth_arg tj (n-a)
 
-let cc_proof (axioms,m)=
+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
-      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)
+    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
-		errorlabstrm  "Congruence" (Pp.str "I couldn't solve goal")
-	| None ->
-	    cc uf;
-	    errorlabstrm  "Congruence" (Pp.str "I couldn't solve goal")
+	      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 (Refute(i,ci,j,cj)) in 
-      let (t1,t2)=type_proof axioms prf in 
-	Refute (UF.get_constructor uf ci,t1,t2,prf,axioms) 
+      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
index 7f21f9dc10..8b3ed3f919 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -9,32 +9,37 @@
 (* $Id$ *)
 
 open Ccalgo
+open Names
 
 type proof =
-    Ax of Names.identifier
-  | SymAx of Names.identifier
+    Ax of identifier
+  | SymAx of identifier
   | Refl of term
   | Trans of proof * proof
   | Congr of proof * proof
-  | Inject of proof * Names.constructor * int * int
+  | 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
 
-type ('a,'b) mission=
-    Prove of 'a
-  | Refute of 'b
-
-val build_proof : UF.t -> (int * int, int * int * int * int) mission -> 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 :
-  (Names.identifier * (term * term)) list -> proof -> term * term
+  (identifier * (term * term)) list -> proof -> term * term
 
 val cc_proof :
-  (Names.identifier * (term * term)) list * (term * term) option ->
-  (proof * (Names.identifier * (term * term)) list, 
-   Names.constructor * term * term * proof * 
-   (Names.identifier * (term * term)) list ) mission
+  (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
index 69e2be12c6..5c2c935ff3 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -57,23 +57,35 @@ let rec decompose_term env t=
 	
 (* decompose equality in members and type *)
 	
-let eq_type_of_term term=
+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 (args.(0),args.(1),args.(2)) 
-	     else fail()
-	 with
-	     Not_found -> fail ())
-    | _ ->fail ()
-
+	     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 (_,t1,t2)=eq_type_of_term term in 
-    (decompose_term env t1,decompose_term env t2)
+  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 *)
     
@@ -90,18 +102,24 @@ and make_app l=function
 (* store all equalities from the context *)
 	
 let rec read_hyps env=function
-    []->[]
-  | (id,_,e)::hyps->let q=(read_hyps env hyps) in
-      try (id,(read_eq env e))::q with Not_an_eq -> q
+    []->[],[]
+  | (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 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)
-
+  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) *)
 
@@ -177,42 +195,54 @@ let rec proof_tac axioms=function
 	   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 prb=make_prb gls in
-    match (cc_proof prb) with
-        Prove (p,axioms)-> proof_tac axioms p gls
-      | Refute (cstr,t1,t2,p,axioms) ->
-	  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
+  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" ] -> [ cc_tactic ]
+ [ "Congruence" ] -> [ tclSOLVE [tclTHEN (tclREPEAT introf) cc_tactic] ]
 END