]> matita.cs.unibo.it Git - helm.git/commitdiff
Procedural: some improvements
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 1 Mar 2007 19:00:14 +0000 (19:00 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 1 Mar 2007 19:00:14 +0000 (19:00 +0000)
rewrite tactic: bug fix in hyps searching
TermContentPres: one space added in let-in rendering
prova.ma: new procedural proof of ty3_gen_cast

helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralConversion.ml
helm/software/components/acic_procedural/proceduralConversion.mli
helm/software/components/acic_procedural/proceduralMode.mli
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/content_pres/termContentPres.ml
helm/software/components/tactics/equalityTactics.ml
helm/software/matita/contribs/prova.ma

index 8dd8e02aa44051b121511de0806b200b7af6cc65..6512938df3435ca46ad2273ae89d538f12cc6693 100644 (file)
@@ -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 @
index b3ce560707348f38f7bd9de27306bd0cc3dc6bdc..77b5a181783ae597c3e0a785c9c105918a20f07b 100644 (file)
@@ -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
+*)
index f27d73aabf0ee8802b5be1806f96b097cb129337..3b65200144a1e9f40eee72bf0a094fdb9d76d39d 100644 (file)
@@ -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
index 2f0e7e9f49d292390458f3e3afdb947f640100c1..96a0b3b132709e620356918894cf83d3c95d6ff3 100644 (file)
@@ -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
index 6aa769b03aa11ec4c209b3b5f60e0e0a1b3ddb68..91f2408b94ba6ea9c15d5e6fee582381a6536a5d 100644 (file)
@@ -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
index 980bc1bc1c71796fe462829b96caa0414968775d..33a7e9c05c51e16a8f23b97407678daeb4a2e5fe 100644 (file)
@@ -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
 
index 9f720e33b9a29740d414f6b5a0cd0d793ae0f2ef..6b3dcc297689783fbe1a99459cc287764c5d0511 100644 (file)
@@ -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) ->
index f2760c30f33f394daded905bc246cc63446e7321..b445dfb868d8d354aeaafb6ad303c43830de5865 100644 (file)
@@ -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
index b975eaffbb360e8cf325df22bf4f9671d281beb1..fc8f9d854bbe7e0dd2095641165b5b40057a88a0 100644 (file)
@@ -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 *)
 ]