diff options
Diffstat (limited to 'plugins/cc/ccproof.ml')
| -rw-r--r-- | plugins/cc/ccproof.ml | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml new file mode 100644 index 00000000..2a019ebf --- /dev/null +++ b/plugins/cc/ccproof.ml @@ -0,0 +1,153 @@ +(************************************************************************) +(* 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$ *) + +(* 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 Term +open Ccalgo + +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 +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 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 prefl (term uf i) else + let (li,lj)=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,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 + 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 + equal_proof i t + else + let npac=tail_pac ipac in + let (j,arg)=subterms uf t in + let targ=term uf arg in + 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 (prefl targ)) + + and path_proof i=function + [] -> 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) + + 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) + in + function + `Prove (i,j) -> equal_proof i j + | `Discr (i,ci,j,cj)-> ind_proof i ci j cj + + + |