From 600477f27265ee3226f1bd3e2a1fcd42445c8d5f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 1 Mar 2007 19:00:14 +0000 Subject: [PATCH] Procedural: some improvements rewrite tactic: bug fix in hyps searching TermContentPres: one space added in let-in rendering prova.ma: new procedural proof of ty3_gen_cast --- components/acic_procedural/acic2Procedural.ml | 36 +++++++++---- .../acic_procedural/proceduralConversion.ml | 46 ++++++++++++++++ .../acic_procedural/proceduralConversion.mli | 2 + components/acic_procedural/proceduralMode.mli | 2 + components/acic_procedural/proceduralTypes.ml | 49 +++++++++-------- .../acic_procedural/proceduralTypes.mli | 5 +- components/content_pres/termContentPres.ml | 2 +- components/tactics/equalityTactics.ml | 2 +- matita/contribs/prova.ma | 54 ++++++++++--------- 9 files changed, 136 insertions(+), 62 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 8dd8e02aa..6512938df 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -167,9 +167,10 @@ let convert st ?name v = | Some (st, et) -> let cst, cet = cic st, cic et in if PER.alpha_equivalence cst cet then [] else + let e = Cn.mk_pattern [] (T.mk_arel 1 "") in match name with - | None -> [T.Change (st, et, None, "")] - | Some id -> [T.Change (st, et, Some (id, id), ""); T.ClearBody (id, "")] + | None -> [T.Change (st, et, None, e, "")] + | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")] let eta_expand n t = let id = Ut.id_of_annterm t in @@ -188,7 +189,7 @@ let eta_expand n t = let appl_expand n = function | C.AAppl (id, ts) -> let before, after = T.list_split (List.length ts + n) ts in - C.AAppl ("", C.AAppl (id, before) :: after) + C.AAppl (id, C.AAppl ("", before) :: after) | _ -> assert false let get_intro name t = @@ -218,13 +219,21 @@ let rec mk_atomic st dtext what = and mk_fwd_rewrite st dtext name tl direction = let what, where = List.nth tl 5, List.nth tl 3 in + let rps, predicate = [List.nth tl 4], List.nth tl 2 in + let e = Cn.mk_pattern rps predicate in match where with | C.ARel (_, _, _, premise) -> let script, what = mk_atomic st dtext what in - T.Rewrite (direction, what, Some (premise, name), dtext) :: script + T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script | _ -> assert false and mk_fwd_proof st dtext name = function + | C.ALetIn (_, n, v, t) -> + let entry = Some (n, C.Def (cic v, None)) in + let intro = get_intro n t in + let qt = mk_fwd_proof (add st entry intro) dtext name t in + let qv = mk_fwd_proof st "" intro v in + List.append qt qv | C.AAppl (_, hd :: tl) as v -> if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else @@ -244,7 +253,12 @@ and mk_fwd_proof st dtext name = function | Some v -> mk_fwd_proof st dtext name v end | v -> - [T.LetIn (name, v, dtext)] + 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)] + | _ -> + [T.LetIn (name, v, dtext)] and mk_proof st = function | C.ALambda (_, name, v, t) -> @@ -289,11 +303,15 @@ and mk_proof st = function let synth = I.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then - List.rev script @ convert st t @ - [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] + let rps, predicate = [List.nth tl 4], List.nth tl 2 in + let e = Cn.mk_pattern rps predicate in + List.rev script @ convert st t @ + [T.Rewrite (false, what, None, e, dtext); T.Branch (qs, "")] else if is_rewrite_left hd then - List.rev script @ convert st t @ - [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] + let rps, predicate = [List.nth tl 4], List.nth tl 2 in + let e = Cn.mk_pattern rps predicate in + List.rev script @ convert st t @ + [T.Rewrite (true, what, None, e, dtext); T.Branch (qs, "")] else let using = Some hd in List.rev script @ convert st t @ diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index b3ce56070..77b5a1817 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -32,6 +32,7 @@ module UM = UriManager module T = ProceduralTypes module Cl = ProceduralClassify +module M = ProceduralMode (* helpers ******************************************************************) @@ -174,3 +175,48 @@ try let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in Some (C.AAppl (id, args)) with Invalid_argument _ -> failwith "PCn.mk_ind" + +let apply_substs substs = + let length = List.length substs in + let rec apply_xns k (uri, t) = uri, apply_term k t + and apply_ms k = function + | None -> None + | Some t -> Some (apply_term k t) + and apply_fix len k (id, name, i, ty, bo) = + id, name, i, apply_term k ty, apply_term (k + len) bo + and apply_cofix len k (id, name, ty, bo) = + id, name, apply_term k ty, apply_term (k + len) bo + and apply_term k = function + | C.ASort _ as t -> t + | C.AImplicit _ as t -> t + | C.ARel (id, rid, m, b) as t -> + if m < k || m >= length + k then t + else lift 1 k (List.nth substs (m - k)) + | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (apply_xns k) xnss) + | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (apply_xns k) xnss) + | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (apply_xns k) xnss) + | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (apply_xns k) xnss) + | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (apply_ms k) mss) + | C.AAppl (id, ts) -> C.AAppl (id, List.map (apply_term k) ts) + | C.ACast (id, te, ty) -> C.ACast (id, apply_term k te, apply_term k ty) + | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, apply_term k outty, apply_term k t, List.map (apply_term k) pl) + | C.AProd (id, n, s, t) -> C.AProd (id, n, apply_term k s, apply_term (succ k) t) + | C.ALambda (id, n, s, t) -> C.ALambda (id, n, apply_term k s, apply_term (succ k) t) + | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, apply_term k s, apply_term (succ k) t) + | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (apply_fix (List.length fl) k) fl) + | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (apply_cofix (List.length fl) k) fl) + in + apply_term 1 + +let hole = C.AImplicit ("", Some `Hole) + +let mk_pattern rps predicate = hole +(* let rec clear_absts n = function + | C.ALambda (_, _, _, t) when n > 0 -> clear_absts (pred n) t +(* | t when n > 0 -> assert false *) + | t -> t + in + let substs = hole :: List.rev rps in + let body = clear_absts (succ (List.length rps)) predicate in + if M.is_appl true (cic body) then apply_substs substs body else hole +*) diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli index f27d73aab..3b6520014 100644 --- a/components/acic_procedural/proceduralConversion.mli +++ b/components/acic_procedural/proceduralConversion.mli @@ -29,3 +29,5 @@ val mk_ind: Cic.context -> Cic.id -> UriManager.uri -> int -> Cic.annterm -> Cic.annterm -> Cic.annterm list -> Cic.annterm option + +val mk_pattern: Cic.annterm list -> Cic.annterm -> Cic.annterm diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli index 2f0e7e9f4..96a0b3b13 100644 --- a/components/acic_procedural/proceduralMode.mli +++ b/components/acic_procedural/proceduralMode.mli @@ -26,3 +26,5 @@ val is_eliminator: Cic.term list -> bool val bkd: Cic.context -> Cic.term -> bool + +val is_appl: bool -> Cic.term -> bool diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index 6aa769b03..91f2408b9 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -76,6 +76,7 @@ type count = int type note = string type where = (name * name) option type inferred = Cic.annterm +type pattern = Cic.annterm type step = Note of note | Theorem of name * what * note @@ -84,10 +85,10 @@ type step = Note of note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note - | Rewrite of how * what * where * note + | Rewrite of how * what * where * pattern * note | Elim of what * using option * note | Apply of what * note - | Change of inferred * what * where * note + | Change of inferred * what * where * pattern * note | ClearBody of name * note | Branch of step list list * note @@ -99,8 +100,6 @@ 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 = @@ -129,11 +128,11 @@ let mk_letin name what = let tactic = G.LetIn (floc, what, name) in mk_tactic tactic -let mk_rewrite direction what where = +let mk_rewrite direction what where pattern = let direction = if direction then `RightToLeft else `LeftToRight in let pattern, rename = match where with - | None -> (None, [], Some hole), [] - | Some (premise, name) -> (None, [premise, hole], None), [name] + | None -> (None, [], Some pattern), [] + | Some (premise, name) -> (None, [premise, pattern], None), [name] in let tactic = G.Rewrite (floc, direction, what, pattern, rename) in mk_tactic tactic @@ -146,10 +145,10 @@ let mk_apply t = let tactic = G.Apply (floc, t) in mk_tactic tactic -let mk_change t where = +let mk_change t where pattern = let pattern = match where with - | None -> None, [], Some hole - | Some (premise, _) -> None, [premise, hole], None + | None -> None, [], Some pattern + | Some (premise, _) -> None, [premise, pattern], None in let tactic = G.Change (floc, pattern, t) in mk_tactic tactic @@ -171,21 +170,21 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None)) (* rendering ****************************************************************) let rec render_step sep a = function - | Note s -> mk_note s :: a - | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a - | Qed s -> (* mk_note s :: *) mk_qed :: a - | Id s -> mk_note s :: cont sep (mk_id :: a) - | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) - | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) - | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) - | 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) - | Change (t, _, w, s) -> mk_note s :: cont sep (mk_change t w :: a) - | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a) - | Branch ([], s) -> a - | Branch ([ps], s) -> render_steps sep a ps - | Branch (pss, s) -> + | Note s -> mk_note s :: a + | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a + | Qed s -> (* mk_note s :: *) mk_qed :: a + | Id s -> mk_note s :: cont sep (mk_id :: a) + | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) + | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) + | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) + | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: 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) + | Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a) + | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a) + | Branch ([], s) -> a + | Branch ([ps], s) -> render_steps sep a ps + | Branch (pss, s) -> let a = mk_ob :: a in let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in mk_note s :: cont sep body diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index 980bc1bc1..33a7e9c05 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -43,6 +43,7 @@ type count = int type note = string type where = (name * name) option type inferred = Cic.annterm +type pattern = Cic.annterm type step = Note of note | Theorem of name * what * note @@ -51,10 +52,10 @@ type step = Note of note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note - | Rewrite of how * what * where * note + | Rewrite of how * what * where * pattern * note | Elim of what * using option * note | Apply of what * note - | Change of inferred * what * where * note + | Change of inferred * what * where * pattern * note | ClearBody of name * note | Branch of step list list * note diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 9f720e33b..6b3dcc297 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -202,7 +202,7 @@ let pp_ast0 t k = keyword "let"; space; hvbox false true [ aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ]; - break; keyword "in" ]; + break; space; keyword "in" ]; break; k t ]) | Ast.LetRec (rec_kind, funs, where) -> diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index f2760c30f..b445dfb86 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -75,7 +75,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = [] -> assert false | Some (Cic.Name s,Cic.Decl ty)::_ when name = s -> Cic.Rel n, S.lift n ty - | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet! But does this make any sense?*) + | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*) | _::tl -> find_hyp (n+1) tl in let arg,gty = find_hyp 1 context in diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma index b975eaffb..fc8f9d854 100644 --- a/matita/contribs/prova.ma +++ b/matita/contribs/prova.ma @@ -32,7 +32,7 @@ theorem ty3_gen_cast: .ty3 g c (THead (Flat Cast) t2 t1) x \rarr pc3 c t2 x\land ty3 g c t1 t2) . -(* tactics: 68 *) +(* tactics: 80 *) intros 6 (g c t1 t2 x H). apply insert_eq;(* 6 P P P C I I 3 0 *) [apply T(* dependent *) @@ -43,7 +43,6 @@ alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.co elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *) [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6). letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *) -clearbody H7. rewrite > H7 in H4:(%) as (H8). cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10; [id @@ -161,28 +160,35 @@ letin H6 \def (f_equal T T |TLRef (_:nat)\rArr t3 |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *) -alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con". -letin DEFINED \def (let H7 \def - f_equal T T - (\lambda e:T - .match e in T return \lambda _:T.T with - [TSort (_:nat)\rArr t0 - |TLRef (_:nat)\rArr t0 - |THead (_:K) (_:T) (t:T)\rArr t]) - (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5 - in - \lambda H8:t3=t2 - .(let H11 \def - eq_ind T t3 - (\lambda t:T - .t0=THead (Flat Cast) t2 t1 - \rarr pc3 c0 t2 t\land ty3 g c0 t1 t2) H2 t2 H8 - in - let H12 \def eq_ind T t3 (\lambda t:T.ty3 g c0 t0 t) H1 t2 H8 in - eq_ind_r T t2 (\lambda t:T.pc3 c0 t2 t\land ty3 g c0 t1 t2) - (let H14 \def eq_ind T t0 (\lambda t:T.ty3 g c0 t t2) H12 t1 H7 in - conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) H14) t3 - H8)). +letin H7 \def (f_equal T T + (\lambda e:T + .match e in T return \lambda _:T.T with + [TSort (_:nat)\rArr t0 + |TLRef (_:nat)\rArr t0 + |THead (_:K) (_:T) (t:T)\rArr t]) (THead (Flat Cast) t3 t0) + (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *) +cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED; +[id +|intros 1 (H8). +rewrite > H8 in H2:(%) as (UNUSED). +rewrite > H8 in H1:(%) as (H12). +rewrite > H8 in \vdash (%). +clearbody H7. +change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with + [TSort (_:nat)\rArr t0 + |TLRef (_:nat)\rArr t0 + |THead (_:K) (_:T) (t:T)\rArr t] + =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with + [TSort (_:nat)\rArr t0 + |TLRef (_:nat)\rArr t0 + |THead (_:K) (_:T) (t:T)\rArr t]). +rewrite > H7 in H12:(%) as (H14). +apply conj;(* 4 C C I I *) +[alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con". +apply pc3_refl(* 2 C C *) +|apply H14(* assumption *) +] +]. apply DEFINED.(* 1 I *) apply H6(* assumption *) ] -- 2.39.2