From: Ferruccio Guidi Date: Fri, 12 Jan 2007 19:34:58 +0000 (+0000) Subject: procedural: added fwd rewrite in arbitrary proofs (not just premises) X-Git-Tag: make_still_working~6527 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=664ce15981e66bc897f31963b2f9f2f1e3d11470;p=helm.git procedural: added fwd rewrite in arbitrary proofs (not just premises) added whd conversion before intros when needed prova.ma : highlighted a bug with the "in" clause of the "match" constr. --- diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 759898ac6..78cde4140 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -32,6 +32,8 @@ content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi cicClassify.cmo: cicClassify.cmi cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt index 759898ac6..78cde4140 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -32,6 +32,8 @@ content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi cicClassify.cmo: cicClassify.cmi cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi diff --git a/helm/software/components/content_pres/Makefile b/helm/software/components/content_pres/Makefile index a3b153029..9c627cb23 100644 --- a/helm/software/components/content_pres/Makefile +++ b/helm/software/components/content_pres/Makefile @@ -1,24 +1,25 @@ PACKAGE = content_pres PREDICATES = -INTERFACE_FILES = \ - renderingAttrs.mli \ - cicNotationLexer.mli \ - cicNotationParser.mli \ - mpresentation.mli \ - box.mli \ - content2presMatcher.mli \ - termContentPres.mli \ - cicNotationPres.mli \ - boxPp.mli \ - content2pres.mli \ - cicClassify.mli \ - proceduralTypes.mli \ - acic2Procedural.mli \ - objPp.mli \ - sequent2pres.mli \ +INTERFACE_FILES = \ + renderingAttrs.mli \ + cicNotationLexer.mli \ + cicNotationParser.mli \ + mpresentation.mli \ + box.mli \ + content2presMatcher.mli \ + termContentPres.mli \ + cicNotationPres.mli \ + boxPp.mli \ + content2pres.mli \ + cicClassify.mli \ + proceduralConversion.mli \ + proceduralTypes.mli \ + acic2Procedural.mli \ + objPp.mli \ + sequent2pres.mli \ $(NULL) -IMPLEMENTATION_FILES = \ +IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) cicNotationPres.cmi: OCAMLOPTIONS += -rectypes diff --git a/helm/software/components/content_pres/acic2Procedural.ml b/helm/software/components/content_pres/acic2Procedural.ml index 9b8dbf063..c92d108e5 100644 --- a/helm/software/components/content_pres/acic2Procedural.ml +++ b/helm/software/components/content_pres/acic2Procedural.ml @@ -24,26 +24,30 @@ *) module C = Cic -module L = CicClassify -module P = ProceduralTypes module D = Deannotate module DTI = DoubleTypeInference module TC = CicTypeChecker -module U = CicUniv +module Un = CicUniv module UM = UriManager module Obj = LibraryObjects module HObj = HelmLibraryObjects module A = Cic2acic -module T = CicUtil +module Ut = CicUtil +module E = CicEnvironment + +module Cl = CicClassify +module T = ProceduralTypes +module Cn = ProceduralConversion type status = { - sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t; + sorts : (C.id, A.sort_kind) Hashtbl.t; types : (C.id, A.anntypes) Hashtbl.t; prefix: string; max_depth: int option; depth: int; entries: C.context; - intros: string list + intros: string list; + ety: C.annterm option } (* helpers ******************************************************************) @@ -53,8 +57,8 @@ let cic = D.deannotate_term let split2_last l1 l2 = try let n = pred (List.length l1) in - let before1, after1 = P.list_split n l1 in - let before2, after2 = P.list_split n l2 in + let before1, after1 = T.list_split n l1 in + let before2, after2 = T.list_split n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" @@ -76,9 +80,13 @@ let string_of_head = function | C.AMeta _ -> "meta" | C.AImplicit _ -> "implict" -let next st = {st with depth = succ st.depth; intros = []} +let next st = {st with depth = succ st.depth; intros = []; ety = None} + +let set_ety st ety = + if st.ety = None then {st with ety = ety} else st -let add st entry intro = +let add st entry intro ety = + let st = set_ety st ety in {st with entries = entry :: st.entries; intros = intro :: st.intros} let test_depth st = @@ -90,17 +98,54 @@ try if st.depth < d then true, msg else false, "DEPTH EXCEDED" with Invalid_argument _ -> failwith "A2P.test_depth" -let get_itype st v = +let is_rewrite_right = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri + | _ -> false + +let is_rewrite_left = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri + | _ -> false +(* +let get_ind_name uri tno xcno = +try + let ts = match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (ts, _, _,_), _ -> ts + | _ -> assert false + in + let tname, cs = match List.nth ts tno with + | (name, _, _, cs) -> name, cs + in + match xcno with + | None -> tname + | Some cno -> fst (List.nth cs (pred cno)) +with Invalid_argument _ -> failwith "A2P.get_ind_name" +*) +let get_inner_types st v = try - let id = T.id_of_annterm v in - try Some ((Hashtbl.find st.types id).A.annsynthesized) + let id = Ut.id_of_annterm v in + try match Hashtbl.find st.types id with + | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et) + | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st) with Not_found -> None -with Invalid_argument _ -> failwith "A2P.get_itype" +with Invalid_argument _ -> failwith "A2P.get_inner_types" + +let get_inner_sort st v = +try + let id = Ut.id_of_annterm v in + try Hashtbl.find st.sorts id + with Not_found -> `Type (CicUniv.fresh()) +with Invalid_argument _ -> failwith "A2P.get_sort" (* proof construction *******************************************************) let unused_premise = "UNUSED" +let defined_premise = "DEFINED" + +let assumed_premise = "ASSUMED" + let get_intro name t = try match name with @@ -113,114 +158,128 @@ let mk_intros st script = try if st.intros = [] then script else let count = List.length st.intros in - P.Intros (Some count, List.rev st.intros, "") :: script + let p0 = T.Whd (count, "") in + let p1 = T.Intros (Some count, List.rev st.intros, "") in + match st.ety with + | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script + | _ -> p1 :: script with Invalid_argument _ -> failwith "A2P.mk_intros" +(* +let rec mk_premise st dtext = function + | C.ARel (_, _, _, binder) -> [], binder + | where -> + let name = contracted_premise in + mk_fwd_proof st dtext name where, name +*) +let rec mk_fwd_rewrite st dtext name tl direction = + let what, where = List.nth tl 5, List.nth tl 3 in + let rewrite premise = + [T.Rewrite (direction, what, Some (premise, name), dtext)] + in + match where with + | C.ARel (_, _, _, binder) -> rewrite binder + | _ -> + assert (get_inner_sort st where = `Prop); + let pred, old = List.nth tl 2, List.nth tl 1 in + let pred_name = defined_premise in + let pred_text = "extracted" in + let p1 = T.LetIn (pred_name, pred, pred_text) in + let cut_name = assumed_premise in + let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in + let cut_text = "" in + let p2 = T.Cut (cut_name, cut_type, cut_text) in + let qs = [rewrite cut_name; mk_proof (next st) where] in + [T.Branch (qs, ""); p2; p1] -let is_rewrite_right = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri - | _ -> false - -let is_rewrite_left = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri - | _ -> false - -let mk_premise = function - | C.ARel (_, _, _, binder) -> binder - | C.AVar (_, uri, _) - | C.AConst (_, uri, _) -> UM.name_of_uri uri - | C.ASort (_, sort) -> assert false - | C.AMutInd (_, uri, tno, _) -> assert false - | C.AMutConstruct (_, uri, tno, cno, _) -> assert false - | _ -> assert false - -let rec mk_fwd_proof st dtext name = function +and mk_fwd_proof st dtext name = function | C.AAppl (_, hd :: tl) as v -> - if is_rewrite_right hd then - let what, where = List.nth tl 5, List.nth tl 3 in - let premise = mk_premise where in - [P.Rewrite (true, what, Some (premise, name), dtext)] - else if is_rewrite_left hd then - let what, where = List.nth tl 5, List.nth tl 3 in - let premise = mk_premise where in - [P.Rewrite (false, what, Some (premise, name), dtext)] - else begin match get_itype st v with - | Some ty -> - let qs = [[P.Id ""]; mk_proof (next st) v] in - [P.Branch (qs, ""); P.Cut (name, ty, dtext)] - | None -> - let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in - let (classes, rc) as h = L.classify ty in - let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in - [P.LetIn (name, v, dtext ^ text)] + if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else + if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else + begin match get_inner_types st v with + | Some (ity, _) -> + let qs = [[T.Id ""]; mk_proof (next st) v] in + [T.Branch (qs, ""); T.Cut (name, ity, dtext)] + | None -> + let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify ty in + let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in + [T.LetIn (name, v, dtext ^ text)] end | v -> - [P.LetIn (name, v, dtext)] + [T.LetIn (name, v, dtext)] and mk_proof st = function - | C.ALambda (_, name, v, t) -> + | C.ALambda (_, name, v, t) as what -> let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name t in - mk_proof (add st entry intro) t + let ety = match get_inner_types st what with + | Some (_, ety) -> Some ety + | None -> None + in + mk_proof (add st entry intro ety) t | C.ALetIn (_, name, v, t) as what -> let proceed, dtext = test_depth st in let script = if proceed then let entry = Some (name, C.Def (cic v, None)) in let intro = get_intro name t in - let q = mk_proof (next (add st entry intro)) t in + let q = mk_proof (next (add st entry intro None)) t in List.rev_append (mk_fwd_proof st dtext intro v) q else - [P.Apply (what, dtext)] + [T.Apply (what, dtext)] in mk_intros st script | C.ARel _ as what -> let _, dtext = test_depth st in - let script = [P.Apply (what, dtext)] in + let text = "assumption" in + let script = [T.Apply (what, dtext ^ text)] in mk_intros st script + | C.AMutConstruct _ as what -> + let _, dtext = test_depth st in + let script = [T.Apply (what, dtext)] in + mk_intros st script | C.AAppl (_, hd :: tl) as t -> let proceed, dtext = test_depth st in let script = if proceed then - let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in - let (classes, rc) as h = L.classify ty in - let synth = L.S.singleton 0 in - let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in + let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify ty in + let synth = Cl.S.singleton 0 in + let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in match rc with | Some (i, j) when i > 1 -> let classes, tl, _, what = split2_last classes tl in - let synth = L.S.add 1 synth in + let synth = Cl.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then - [P.Rewrite (false, what, None, dtext); P.Branch (qs, "")] + [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] else if is_rewrite_left hd then - [P.Rewrite (true, what, None, dtext); P.Branch (qs, "")] + [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] else let using = Some hd in - [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")] + [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")] | _ -> let qs = mk_bkd_proofs (next st) synth classes tl in - [P.Apply (hd, dtext ^ text); P.Branch (qs, "")] + [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else - [P.Apply (t, dtext)] + [T.Apply (t, dtext)] in mk_intros st script | t -> let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in - let script = [P.Note text] in + let script = [T.Note text] in mk_intros st script and mk_bkd_proofs st synth classes ts = try let _, dtext = test_depth st in let aux inv v = - if L.overlaps synth inv then None else - if L.S.is_empty inv then Some (mk_proof st v) else - Some [P.Apply (v, dtext ^ "dependent")] + if Cl.overlaps synth inv then None else + if Cl.S.is_empty inv then Some (mk_proof st v) else + Some [T.Apply (v, dtext ^ "dependent")] in let l1, l2 = List.length classes, List.length ts in if l1 > l2 then failwith "partial application" else if l1 < l2 then failwith "too many arguments" else - P.list_map2_filter aux classes ts + T.list_map2_filter aux classes ts with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs" (* object costruction *******************************************************) @@ -231,10 +290,10 @@ let is_theorem pars = let mk_obj st = function | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars -> - let ast = mk_proof st v in - let count = P.count_steps 0 ast in + let ast = mk_proof (set_ety st (Some t)) v in + let count = T.count_steps 0 ast in let text = Printf.sprintf "tactics: %u" count in - P.Theorem (s, t, text) :: ast @ [P.Qed ""] + T.Theorem (s, t, text) :: ast @ [T.Qed ""] | _ -> failwith "not a theorem" @@ -248,9 +307,10 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj = max_depth = None; depth = 0; entries = []; - intros = [] + intros = []; + ety = None } in prerr_endline "Level 2 transformation"; let steps = mk_obj st aobj in prerr_endline "grafite rendering"; - List.rev (P.render_steps [] steps) + List.rev (T.render_steps [] steps) diff --git a/helm/software/components/content_pres/proceduralConversion.ml b/helm/software/components/content_pres/proceduralConversion.ml new file mode 100644 index 000000000..e506a8f6e --- /dev/null +++ b/helm/software/components/content_pres/proceduralConversion.ml @@ -0,0 +1,32 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic + +let rec need_whd i = function + | C.ACast (_, t, _) -> need_whd i t + | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t + | _ when i > 0 -> true + | _ -> false diff --git a/helm/software/components/content_pres/proceduralConversion.mli b/helm/software/components/content_pres/proceduralConversion.mli new file mode 100644 index 000000000..448112cdb --- /dev/null +++ b/helm/software/components/content_pres/proceduralConversion.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val need_whd: int -> Cic.annterm -> bool diff --git a/helm/software/components/content_pres/proceduralTypes.ml b/helm/software/components/content_pres/proceduralTypes.ml index 0ef73e248..b7f6d3c6b 100644 --- a/helm/software/components/content_pres/proceduralTypes.ml +++ b/helm/software/components/content_pres/proceduralTypes.ml @@ -75,6 +75,7 @@ type step = Note of note | Rewrite of how * what * where * note | Elim of what * using option * note | Apply of what * note + | Whd of count * note | Branch of step list list * note (* annterm constructors *****************************************************) @@ -85,6 +86,8 @@ let mk_arel i b = Cic.ARel ("", "", i, b) let floc = H.dummy_floc +let hole = C.AImplicit ("", Some `Hole) + let mk_note str = G.Comment (floc, G.Note (floc, str)) let mk_theorem name t = @@ -114,7 +117,6 @@ let mk_letin name what = mk_tactic tactic let mk_rewrite direction what where = - let hole = C.AImplicit ("", Some `Hole) in let direction = if direction then `RightToLeft else `LeftToRight in let pattern, rename = match where with | None -> (None, [], Some hole), [] @@ -131,6 +133,11 @@ let mk_apply t = let tactic = G.Apply (floc, t) in mk_tactic tactic +let mk_whd i = + let pattern = None, [], Some hole in + let tactic = G.Reduce (floc, `Whd, pattern) in + mk_tactic tactic + let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None)) let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None)) @@ -154,6 +161,7 @@ let rec render_step sep a = function | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a) | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) + | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) | Branch ([], s) -> a | Branch ([ps], s) -> render_steps sep a ps | Branch (pss, s) -> diff --git a/helm/software/components/content_pres/proceduralTypes.mli b/helm/software/components/content_pres/proceduralTypes.mli index ebadd9da8..b06acd104 100644 --- a/helm/software/components/content_pres/proceduralTypes.mli +++ b/helm/software/components/content_pres/proceduralTypes.mli @@ -51,10 +51,11 @@ type step = Note of note | Rewrite of how * what * where * note | Elim of what * using option * note | Apply of what * note + | Whd of count * note | Branch of step list list * note val render_steps: - (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> + (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> step list -> (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma index a3357f8e0..a2012b12f 100644 --- a/helm/software/matita/contribs/prova.ma +++ b/helm/software/matita/contribs/prova.ma @@ -16,6 +16,26 @@ set "baseuri" "cic:/matita/test/prova". include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma". +alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)". +alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)". +(* +alias id "B" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1)". +*) +theorem not_abbr_abst: + (Abbr\neq Abst) +.(* tactics: 7 *) +whd in \vdash (%). +intros 1 (H). +letin DEFINED \def (\lambda ee:B + .match ee in B return \lambda _:B.Prop with + [Abbr\rArr True|Abst\rArr False|Void\rArr False]).(* extracted *) +cut (DEFINED Abbr) as ASSUMED; +[rewrite > H in ASSUMED:(%) as (H0) +|apply I +]. +elim H0 using False_ind names 0.(* 2 C I 2 0 *) +qed. + alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)". alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)". alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)".