| 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
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 =
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
| 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) ->
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 @
module T = ProceduralTypes
module Cl = ProceduralClassify
+module M = ProceduralMode
(* helpers ******************************************************************)
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
+*)
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
val is_eliminator: Cic.term list -> bool
val bkd: Cic.context -> Cic.term -> bool
+
+val is_appl: bool -> Cic.term -> bool
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
| 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
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 =
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
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
(* 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
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
| 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
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) ->
[] -> 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
.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 *)
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
|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 *)
]
projects / helm.git / commitdiff