summaryrefslogtreecommitdiff
path: root/contrib/cc
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cc')
-rw-r--r--contrib/cc/ccproof.ml146
-rw-r--r--contrib/cc/ccproof.mli14
-rw-r--r--contrib/cc/cctac.ml153
3 files changed, 181 insertions, 132 deletions
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 1ffa347a..d336f599 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
@@ -16,58 +16,107 @@ open Names
open Term
open Ccalgo
-type proof=
+type rule=
Ax of constr
| SymAx of constr
| 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)
+and proof =
+ {p_lhs:term;p_rhs:term;p_rule:rule}
+
+let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
+
+let pcongr p1 p2 =
+ match p1.p_rule,p2.p_rule with
+ Refl t1, Refl t2 -> prefl (Appli (t1,t2))
+ | _, _ ->
+ {p_lhs=Appli (p1.p_lhs,p2.p_lhs);
+ p_rhs=Appli (p1.p_rhs,p2.p_rhs);
+ p_rule=Congr (p1,p2)}
+
+let rec ptrans p1 p3=
+ match p1.p_rule,p3.p_rule with
+ Refl _, _ ->p3
+ | _, Refl _ ->p1
+ | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
+ | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
+ | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
+ ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
+ | _, _ ->
+ if p1.p_rhs = p3.p_lhs then
+ {p_lhs=p1.p_lhs;
+ p_rhs=p3.p_rhs;
+ p_rule=Trans (p1,p3)}
+ else anomaly "invalid cc transitivity"
-let pcongr=function
- Refl t1, Refl t2 ->Refl (Appli (t1,t2))
- | p1, p2 -> Congr (p1,p2)
+let rec psym p =
+ match p.p_rule with
+ Refl _ -> p
+ | SymAx s ->
+ {p_lhs=p.p_rhs;
+ p_rhs=p.p_lhs;
+ p_rule=Ax s}
+ | Ax s->
+ {p_lhs=p.p_rhs;
+ p_rhs=p.p_lhs;
+ p_rule=SymAx s}
+ | Inject (p0,c,n,a)->
+ {p_lhs=p.p_rhs;
+ p_rhs=p.p_lhs;
+ p_rule=Inject (psym p0,c,n,a)}
+ | Trans (p1,p2)-> ptrans (psym p2) (psym p1)
+ | Congr (p1,p2)-> pcongr (psym p1) (psym p2)
+
+let pax axioms s =
+ let l,r = Hashtbl.find axioms s in
+ {p_lhs=l;
+ p_rhs=r;
+ p_rule=Ax s}
+
+let psymax axioms s =
+ let l,r = Hashtbl.find axioms s in
+ {p_lhs=r;
+ p_rhs=l;
+ p_rule=SymAx s}
+
+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 pinject p c n a =
+ {p_lhs=nth_arg p.p_lhs (n-a);
+ p_rhs=nth_arg p.p_rhs (n-a);
+ p_rule=Inject(p,c,n,a)}
let build_proof uf=
-
+
+ let axioms = axioms uf in
+
let rec equal_proof i j=
- if i=j then Refl (term uf i) else
+ if i=j then prefl (term uf i) else
let (li,lj)=join_path uf i j in
- ptrans (path_proof i li,psym (path_proof j lj))
+ 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,reversed)->if reversed then SymAx s else Ax s
+ Axiom (s,reversed)->
+ if reversed then psymax axioms s
+ else pax axioms s
| Congruence ->congr_proof eq.lhs eq.rhs
| Injection (ti,ipac,tj,jpac,k) ->
let p=ind_proof ti ipac tj jpac in
let cinfo= get_constructor_info uf ipac.cnode in
- Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k)
- in ptrans(ptrans (pi,pij),pj)
+ pinject p cinfo.ci_constr cinfo.ci_nhyps k
+ in ptrans (ptrans pi pij) pj
and constr_proof i t ipac=
if ipac.args=[] then
@@ -79,49 +128,26 @@ let build_proof uf=
let rj=find uf j in
let u=find_pac uf rj npac in
let p=constr_proof j u npac in
- ptrans (equal_proof i t, pcongr (p,Refl targ))
+ ptrans (equal_proof i t) (pcongr p (prefl targ))
and path_proof i=function
- [] -> Refl (term uf i)
- | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x)
+ [] -> prefl (term uf i)
+ | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
and congr_proof i j=
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
- pcongr (equal_proof i1 j1, equal_proof i2 j2)
+ pcongr (equal_proof i1 j1) (equal_proof i2 j2)
and ind_proof i ipac j jpac=
let p=equal_proof i j
and p1=constr_proof i i ipac
and p2=constr_proof j j jpac in
- ptrans(psym p1,ptrans(p,p2))
+ ptrans (psym p1) (ptrans p p2)
in
function
`Prove (i,j) -> equal_proof i j
| `Discr (i,ci,j,cj)-> ind_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->Hashtbl.find axioms s
- | SymAx s-> let (t1,t2)=Hashtbl.find axioms s 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)
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index abdd6fea..572b2c53 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -6,26 +6,26 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *)
open Ccalgo
open Names
open Term
-type proof =
+type rule=
Ax of constr
| SymAx of constr
| Refl of term
- | Trans of proof * proof
- | Congr of proof * proof
- | Inject of proof * constructor * int * int
+ | Trans of proof*proof
+ | Congr of proof*proof
+ | Inject of proof*constructor*int*int
+and proof =
+ private {p_lhs:term;p_rhs:term;p_rule:rule}
val build_proof :
forest ->
[ `Discr of int * pa_constructor * int * pa_constructor
| `Prove of int * int ] -> proof
-val type_proof :
- (constr, (term * term)) Hashtbl.t -> proof -> term * term
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index ea8aceeb..86251254 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -37,6 +37,12 @@ let _f_equal = constant ["Init";"Logic"] "f_equal"
let _eq_rect = constant ["Init";"Logic"] "eq_rect"
+let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+
+let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+
+let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+
let _eq = constant ["Init";"Logic"] "eq"
let _False = constant ["Init";"Logic"] "False"
@@ -210,54 +216,73 @@ let build_projection intype outtype (cstr:constructor) special default gls=
(* generate an adhoc tactic following the proof tree *)
-let rec proof_tac axioms=function
- Ax c -> exact_check c
- | SymAx c -> tclTHEN symmetry (exact_check c)
- | Refl t -> reflexivity
- | Trans (p1,p2)->let t=(constr_of_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=constr_of_term f1 and tx1=constr_of_term x1
- and tf2=constr_of_term f2 and tx2=constr_of_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,[|typf;typfx;appx1;tf1;tf2|])
- and lemma2=
- mkApp(Lazy.force _f_equal,[|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=constr_of_term ti in
- let ctj=constr_of_term tj in
- let cai=constr_of_term ai in
- let intype=pf_type_of gls cti in
- let outtype=pf_type_of gls cai in
+let _M =mkMeta
+
+let rec proof_tac p gls =
+ match p.p_rule with
+ Ax c -> exact_check c gls
+ | SymAx c ->
+ let l=constr_of_term p.p_lhs and
+ r=constr_of_term p.p_rhs in
+ let typ = pf_type_of gls l in
+ exact_check
+ (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+ | Refl t ->
+ let lr = constr_of_term t in
+ let typ = pf_type_of gls lr in
+ exact_check
+ (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+ | Trans (p1,p2)->
+ let t1 = constr_of_term p1.p_lhs and
+ t2 = constr_of_term p1.p_rhs and
+ t3 = constr_of_term p2.p_rhs in
+ let typ = pf_type_of gls t2 in
+ let prf =
+ mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
+ tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
+ | Congr (p1,p2)->
+ let tf1=constr_of_term p1.p_lhs
+ and tx1=constr_of_term p2.p_lhs
+ and tf2=constr_of_term p1.p_rhs
+ and tx2=constr_of_term p2.p_rhs in
+ let typf = pf_type_of gls tf1 in
+ let typx = pf_type_of gls tx1 in
+ let typfx = prod_applist typf [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,
+ [|typf;typfx;appx1;tf1;tf2;_M 1|]) in
+ let lemma2=
+ mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+ let prf =
+ mkApp(Lazy.force _trans_eq,
+ [|typfx;
+ mkApp(tf1,[|tx1|]);
+ mkApp(tf2,[|tx1|]);
+ mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
+ tclTHENS (refine prf)
+ [tclTHEN (refine lemma1) (proof_tac p1);
+ tclFIRST
+ [tclTHEN (refine lemma2) (proof_tac p2);
+ reflexivity;
+ fun gls ->
+ errorlabstrm "Congruence"
+ (Pp.str
+ "I don't know how to handle dependent equality")]] gls
+ | Inject (prf,cstr,nargs,argind) ->
+ let ti=constr_of_term prf.p_lhs in
+ let tj=constr_of_term prf.p_rhs in
+ let default=constr_of_term p.p_lhs in
+ let intype=pf_type_of gls ti in
+ let outtype=pf_type_of gls default in
let special=mkRel (1+nargs-argind) in
- let default=constr_of_term ai in
let proj=build_projection intype outtype cstr special default gls in
let injt=
- mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in
- tclTHEN (apply injt) (proof_tac axioms prf) gls)
+ mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
+ tclTHEN (refine injt) (proof_tac prf) gls
-let refute_tac axioms c t1 t2 p gls =
+let refute_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let intype=pf_type_of gls tt1 in
let neweq=
@@ -266,9 +291,9 @@ let refute_tac axioms c t1 t2 p gls =
let hid=pf_get_new_id (id_of_string "Heq") gls in
let false_t=mkApp (c,[|mkVar hid|]) in
tclTHENS (true_cut (Name hid) neweq)
- [proof_tac axioms p; simplest_elim false_t] gls
+ [proof_tac p; simplest_elim false_t] gls
-let convert_to_goal_tac axioms c t1 t2 p gls =
+let convert_to_goal_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let sort=pf_type_of gls tt2 in
let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
@@ -278,20 +303,19 @@ let convert_to_goal_tac axioms c t1 t2 p gls =
let endt=mkApp (Lazy.force _eq_rect,
[|sort;tt1;identity;c;tt2;mkVar e|]) in
tclTHENS (true_cut (Name e) neweq)
- [proof_tac axioms p;exact_check endt] gls
+ [proof_tac p;exact_check endt] gls
-let convert_to_hyp_tac axioms c1 t1 c2 t2 p gls =
+let convert_to_hyp_tac c1 t1 c2 t2 p gls =
let tt2=constr_of_term t2 in
let h=pf_get_new_id (id_of_string "H") gls in
let false_t=mkApp (c2,[|mkVar h|]) in
tclTHENS (true_cut (Name h) tt2)
- [convert_to_goal_tac axioms c1 t1 t2 p;
+ [convert_to_goal_tac c1 t1 t2 p;
simplest_elim false_t] gls
-let discriminate_tac axioms cstr p gls =
- let t1,t2=type_proof axioms p in
- let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let intype=pf_type_of gls tt1 in
+let discriminate_tac cstr p gls =
+ let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+ let intype=pf_type_of gls t1 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
@@ -303,12 +327,12 @@ let discriminate_tac axioms cstr p gls =
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,
- [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in
+ [|intype;outtype;proj;t1;t2;mkVar hid|]) in
let endt=mkApp (Lazy.force _eq_rect,
[|outtype;trivial;pred;identity;concl;injt|]) in
- let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in
+ let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
tclTHENS (true_cut (Name hid) neweq)
- [proof_tac axioms p;exact_check endt] gls
+ [proof_tac p;exact_check endt] gls
(* wrap everything *)
@@ -333,12 +357,12 @@ let cc_tactic depth additionnal_terms gls=
debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
match reason with
Discrimination (i,ipac,j,jpac) ->
- let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+ let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
- discriminate_tac (axioms uf) cstr p gls
+ discriminate_tac cstr p gls
| Incomplete ->
let metacnt = ref 0 in
- let newmeta _ = incr metacnt; mkMeta !metacnt in
+ let newmeta _ = incr metacnt; _M !metacnt in
let terms_to_complete =
List.map
(build_term_to_complete uf newmeta)
@@ -363,14 +387,13 @@ let cc_tactic depth additionnal_terms gls=
| Contradiction dis ->
let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
let ta=term uf dis.lhs and tb=term uf dis.rhs in
- let axioms = axioms uf in
match dis.rule with
- Goal -> proof_tac axioms p gls
- | Hyp id -> refute_tac axioms id ta tb p gls
+ Goal -> proof_tac p gls
+ | Hyp id -> refute_tac id ta tb p gls
| HeqG id ->
- convert_to_goal_tac axioms id ta tb p gls
+ convert_to_goal_tac id ta tb p gls
| HeqnH (ida,idb) ->
- convert_to_hyp_tac axioms ida ta idb tb p gls
+ convert_to_hyp_tac ida ta idb tb p gls
let cc_fail gls =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 06:36:04 +0000