(* helpers ******************************************************************)
-let identity x = x
-
-let comp f g x = f (g x)
-
let cic = D.deannotate_term
let split2_last l1 l2 =
let defined_premise = "DEFINED"
-let expanded_premise = "EXPANDED"
-
let convert st ?name v =
match get_inner_types st v with
| None -> []
| 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
+ let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
match name with
| 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 ty = C.AImplicit ("", None) in
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
- let arg i n = T.mk_arel ((* n - *) succ i) (name (n - i - 1)) in
- let rec aux i f a =
- if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
- in
- let absts, args = aux 0 identity [] in
- match Cn.lift 1 n t with
- | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
- | t -> absts (C.AAppl ("", t :: args))
-
-let appl_expand n = function
- | C.AAppl (id, ts) ->
- let before, after = T.list_split (List.length ts + n) ts in
- C.AAppl (id, C.AAppl ("", before) :: after)
- | _ -> assert false
-
let get_intro name t =
try
match name with
and mk_fwd_rewrite st dtext name tl direction =
assert (List.length tl = 6);
- 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
+ let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
+ let e = Cn.mk_pattern 1 predicate in
match where with
| C.ARel (_, _, _, premise) ->
let script, what = mk_atomic st dtext what in
and mk_rewrite st dtext script t what qs tl direction =
assert (List.length tl = 5);
- let rps, predicate = [List.nth tl 4], List.nth tl 2 in
- let e = Cn.mk_pattern rps predicate in
+ let predicate = List.nth tl 2 in
+ let e = Cn.mk_pattern 1 predicate in
List.rev script @ convert st t @
[T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
and mk_fwd_proof st dtext name = function
- | C.ALetIn (_, n, v, t) ->
+ | 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 ->
+ | 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
let ty = get_type "TC1" st hd in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
[T.LetIn (name, v, dtext ^ text)]
end
-(* | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
- begin match Cn.mk_ind st.context id uri tyno outty arg cases with
- | None -> [T.LetIn (name, v, dtext)]
- | Some v -> mk_fwd_proof st dtext name v
- end
-*) | C.ACast (_, v, _) ->
- mk_fwd_proof st dtext name v
- | v ->
+ | C.AMutCase _ -> assert false
+ | C.ACast _ -> assert false
+ | v ->
match get_inner_types st v with
| Some (ity, _) ->
let qs = [[T.Id ""]; mk_proof (next st) v] in
[T.LetIn (name, v, dtext)]
and mk_proof st = function
- | C.ALambda (_, name, v, t) ->
+ | C.ALambda (_, name, v, t) ->
let entry = Some (name, C.Decl (cic v)) in
let intro = get_intro name t in
mk_proof (add st entry intro) t
- | C.ALetIn (_, name, v, t) as what ->
+ | 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
[T.Apply (what, dtext)]
in
mk_intros st script
- | C.ARel _ as what ->
+ | C.ARel _ as what ->
let _, dtext = test_depth st in
let text = "assumption" in
let script = [T.Apply (what, dtext ^ text)] in
mk_intros st script
- | C.AMutConstruct _ as what ->
+ | 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 ->
+ | C.AAppl (_, hd :: tl) as t ->
let proceed, dtext = test_depth st in
let script = if proceed then
let ty = get_type "TC2" st hd in
let (classes, rc) as h = Cl.classify st.context ty in
let premises, _ = P.split st.context ty in
- let decurry = List.length classes - List.length tl in
- if decurry <> 0 then
- Printf.eprintf "DECURRY: %u %s\n" decurry (CicPp.ppterm (cic t));
- assert (decurry = 0);
- if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
- if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
+ assert (List.length classes - List.length tl = 0);
let synth = I.S.singleton 0 in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
match rc with
else if is_rewrite_left hd then
mk_rewrite st dtext script t what qs tl true
else
- let using = Some hd in
+ let l = succ (List.length tl) in
+ let predicate = List.nth tl (l - i) in
+ let e = Cn.mk_pattern j predicate in
+ let using = Some hd in
List.rev script @ convert st t @
- [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
+ [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
| _ ->
let qs = mk_bkd_proofs (next st) synth classes tl in
let script, hd = mk_atomic st dtext hd in
[T.Apply (t, dtext)]
in
mk_intros st script
- | C.AMutCase (id, uri, tyno, outty, arg, cases) as t ->
- begin match Cn.mk_ind st.context id uri tyno outty arg cases with
- | _ (* None *) ->
- let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
- let script = [T.Note text] in
- mk_intros st script
-(* | Some t -> mk_proof st t *)
- end
- | C.ACast (_, t, _) ->
- mk_proof st t
- | t ->
+ | C.AMutCase _ -> assert false
+ | C.ACast _ -> assert false
+ | t ->
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
let script = [T.Note text] in
mk_intros st script
let cic = D.deannotate_term
-let get_ind_type uri tyno =
- match E.get_obj Un.empty_ugraph uri with
- | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
- | _ -> assert false
-
-let get_default_eliminator context uri tyno ty =
- let _, (name, _, _, _) = get_ind_type uri tyno in
- let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
- let ext = match sort with
- | C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.CProp -> "_rec"
- | C.Sort (C.Type _) -> "_rect"
- | C.Meta (_,_) -> assert false
- | _ -> assert false
- in
- let buri = UM.buri_of_uri uri in
- let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
- C.Const (uri, [])
-
let rec list_sub start length = function
| _ :: tl when start > 0 -> list_sub (pred start) length tl
| hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl
in
lift_term k
-let fake_annotate c =
- let get_binder c m =
- try match List.nth c (pred m) with
- | Some (C.Name s, _) -> s
- | _ -> assert false
- with
- | Invalid_argument _ -> assert false
- in
- let mk_decl n v = Some (n, C.Decl v) in
- let mk_def n v = Some (n, C.Def (v, None)) in
- let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
- let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
- let rec ann_xns c (uri, t) = uri, ann_term c t
- and ann_ms c = function
- | None -> None
- | Some t -> Some (ann_term c t)
- and ann_fix newc c (name, i, ty, bo) =
- "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
- and ann_cofix newc c (name, ty, bo) =
- "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
- and ann_term c = function
- | C.Sort sort -> C.ASort ("", sort)
- | C.Implicit ann -> C.AImplicit ("", ann)
- | C.Rel m -> C.ARel ("", "", m, get_binder c m)
- | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
- | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
- | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
- | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
- | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
- | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
- | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
- | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
- | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
- | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
- | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
- | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
- | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
- in
- ann_term c
-
let clear_absts m =
let rec aux k n = function
| C.AImplicit (_, None) as t -> t
in
aux m
-let mk_ind context id uri tyno outty arg cases =
-try
- let sort_disp = 0 in
- let is_recursive = function
- | C.MutInd (u, no, _) -> UM.eq u uri && no = tyno
- | _ -> false
- in
- let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
- let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
- let ps = match Rd.whd ~delta:true context inty with
- | C.MutInd _ -> []
- | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
- | _ -> assert false
- in
- let lps, rps = T.list_split lpsno ps in
- let rpsno = List.length rps in
- let eliminator = get_default_eliminator context uri tyno inty in
- let eliminator = fake_annotate context eliminator in
- let predicate = clear_absts rpsno (1 - sort_disp) outty in
- let map2 case (_, cty) =
- let map (h, case, k) premise =
- if h > 0 then pred h, lift k 1 case, k else
- if is_recursive premise then 0, lift (succ k) 1 case, succ k else
- 0, case, succ k
- in
- let premises, _ = P.split context cty in
- let _, lifted_case, _ =
- List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
- in
- lifted_case
- in
- let lifted_cases = List.map2 map2 cases constructors in
- let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
- Some (C.AAppl (id, args))
-with Invalid_argument _ -> failwith "PCn.mk_ind"
-
let hole id = C.AImplicit (id, Some `Hole)
let meta id = C.AImplicit (id, None)
in
gen_term 0
-let mk_pattern rps predicate =
- let sort_disp = 0 in
- let rpsno = List.length rps in
- let body = generalize (rpsno + sort_disp) predicate in
- clear_absts 0 (rpsno + sort_disp) body
+let mk_pattern rpsno predicate =
+ let body = generalize rpsno predicate in
+ clear_absts 0 rpsno body
val lift: int -> int -> Cic.annterm -> Cic.annterm
-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
+val mk_pattern: int -> Cic.annterm -> Cic.annterm
| Cut of name * what * note
| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
- | Elim of what * using option * note
+ | Elim of what * using option * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| ClearBody of name * note
let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
mk_tactic tactic
-let mk_elim what using =
- let tactic = G.Elim (floc, what, using, Some 0, []) in
+let mk_elim what using pattern =
+ let pattern = Some what, [], Some pattern in
+ let tactic = G.Elim (floc, pattern, using, Some 0, []) in
mk_tactic tactic
let mk_apply t =
| 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)
+ | Elim (t, xu, e, s) -> mk_note s :: cont sep (mk_elim t xu e :: 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)
| Cut of name * what * note
| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
- | Elim of what * using option * note
+ | Elim of what * using option * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| ClearBody of name * note
| Decompose of loc * 'ident list
| Demodulate of loc
| Destruct of loc * 'term
- | Elim of loc * 'term * 'term option * int option * 'ident list
+ | Elim of loc * ('term, 'lazy_term, 'ident) pattern * 'term option *
+ int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list
| Exact of loc * 'term
| Exists of loc
sprintf "decompose%s" (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
| Destruct (_, term) -> "destruct " ^ term_pp term
- | Elim (_, term, using, num, idents) ->
- sprintf "elim " ^ term_pp term ^
+ | Elim (_, pattern, using, num, idents) ->
+ sprintf "elim %s%s%s"
+ (pp_tactic_pattern pattern)
(match using with None -> "" | Some term -> " using " ^ term_pp term)
- ^ pp_intros_specs (num, idents)
+ (pp_intros_specs (num, idents))
| ElimType (_, term, using, num, idents) ->
sprintf "elim type " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,term) -> Tactics.destruct term
- | GrafiteAst.Elim (_, what, using, depth, names) ->
+ | GrafiteAst.Elim (_, pattern, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- what
+ pattern
| GrafiteAst.ElimType (_, what, using, depth, names) ->
Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
what
| GrafiteAst.Exact (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let metasenv,what = disambiguate_term context metasenv what in
+ | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
+ let pattern = disambiguate_pattern pattern in
let metasenv,using = disambiguate_term context metasenv using in
- metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
- | GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let metasenv,what = disambiguate_term context metasenv what in
- metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
+ metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents)
+ | GrafiteAst.Elim (loc, pattern, None, depth, idents) ->
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents)
| GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
let metasenv,what = disambiguate_term context metasenv what in
let metasenv,using = disambiguate_term context metasenv using in
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
| IDENT "elim"; what = tactic_term; using = using;
+ (num, idents) = intros_spec ->
+ let pattern = Some what, [], Some Ast.UserInput in
+ GrafiteAst.Elim (loc, pattern, using, num, idents)
+ | IDENT "elim"; pattern = pattern_spec; using = using;
(num, idents) = intros_spec ->
- GrafiteAst.Elim (loc, what, using, num, idents)
+ GrafiteAst.Elim (loc, pattern, using, num, idents)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, num, idents)
let metano,context,_ = CicUtil.lookup_meta goal metasenv in
let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
let proof' = (n,metasenv,bo,ty,attrs) in
+ let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
ProofEngineTypes.apply_tactic (
Tacticals.thens
~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
~continuations:
- [ Tactics.elim_intros (Cic.Rel 1)
+ [ Tactics.elim_intros pattern
~mk_fresh_name_callback:
(let i = ref 0 in
fun _ _ _ ~typ ->
;;
let andelim t id1 t1 id2 t2 =
- Tactics.elim_intros t
+ Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
~mk_fresh_name_callback:
(let i = ref 0 in
fun _ _ _ ~typ ->
;;
let we_proceed_by_induction_on t pat =
- (*BUG here: pat unused *)
- Tactics.elim_intros ~depth:0 t
+ let pattern = Some (fun c m u -> t, m, u), [], Some pat in
+ Tactics.elim_intros ~depth:0 pattern
;;
let case id ~params =
let _, metasenv, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = H.lookup_type metasenv context what in
+ let pattern = PET.conclusion_pattern (Some (C.Rel index)) in
let tac =
if check_type sorts metasenv context (S.lift index ty) then
- T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+ T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern)
~continuation:(PESR.clear [what])
else
let msg = "unexported elim_clear: not an decomposable type" in
let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
?using what
=
- let elim what =
- P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+ let elim =
+ P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
in
let elim_type_tac status =
+ let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in
let tac =
- T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+ T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac]
in
PET.apply_tactic tac status
in
mk_tactic (exact_tac ~term)
(* not really "primitive" tactics .... *)
-let elim_tac ?using ~term =
+let elim_tac ?using pattern =
let elim_tac (proof, goal) =
let module T = CicTypeChecker in
let module U = UriManager in
let module C = Cic in
let (curi,metasenv,proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let term, metasenv, _ = match pattern with
+ | Some f, [], Some _ -> f context metasenv CicUniv.empty_ugraph
+ | _ -> assert false
+ in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
| _ -> 0
in
let args_no = find_args_no ety in
- let term_to_refine =
+(* we find the predicate for the eliminator as in the rewrite tactic ********)
+(*
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst:[] metasenv' context C.Anonymous ~typ:termty in
+ let lifted_gty = S.lift 1 ty in
+ let lifted_conjecture =
+ metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in
+ let lifted_t1 = S.lift 1 t1x in
+ let lifted_pattern =
+ let lifted_concl_pat =
+ match concl_pat with
+ | None -> None
+ | Some term -> Some (S.lift 1 term) in
+ Some (fun c m u ->
+ let distance = pred (List.length c - List.length context) in
+ S.lift distance lifted_t1, m, u),[],lifted_concl_pat
+ in
+*)
+(****************************************************************************)
+ let term_to_refine =
let rec make_tl base_case =
function
0 -> [base_case]
let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+ ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
;;
(* The simplification is performed only on the conclusion *)
let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+ ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
~continuation:
(Tacticals.thens
~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
val elim_intros_simpl_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?depth:int -> ?using:Cic.term ->
+ ProofEngineTypes.lazy_pattern ->
+ ProofEngineTypes.tactic
val elim_intros_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?depth:int -> ?using:Cic.term ->
+ ProofEngineTypes.lazy_pattern ->
+ ProofEngineTypes.tactic
val cases_intros_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
exception WrongUriToConstant;;
exception RelToHiddenHypothesis;;
+module C = Cic
+module S = CicSubstitution
+
let alpha_equivalence =
- let module C = Cic in
let rec aux t t' =
if t = t' then true
else
(* "textual" replacement of several subterms with other ones *)
let replace ~equality ~what ~with_what ~where =
- let module C = Cic in
let find_image t =
let rec find_image_aux =
function
(* replaces in a term a term with another one. *)
(* Lifting are performed as usual. *)
let replace_lifting ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
let find_image what t =
let rec find_image_aux =
function
(* replaces in a term a list of terms with other ones. *)
(* Lifting are performed as usual. *)
let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
let find_image t =
let rec find_image_aux =
function
substaux 1 where
;;
+(* This is the inverse of the subst function. *)
+let subst_inv ~equality ~what =
+ let rec find_image t = function
+ | [] -> false
+ | hd :: tl -> equality t hd || find_image t tl
+ in
+ let rec subst_term k t =
+ if find_image t what then C.Rel k else inspect_term k t
+ and inspect_term k = function
+ | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Var (uri, enss) ->
+ let enss = List.map (subst_ens k) enss in
+ C.Var (uri, enss)
+ | C.Const (uri ,enss) ->
+ let enss = List.map (subst_ens k) enss in
+ C.Const (uri, enss)
+ | C.MutInd (uri, tyno, enss) ->
+ let enss = List.map (subst_ens k) enss in
+ C.MutInd (uri, tyno, enss)
+ | C.MutConstruct (uri, tyno, consno, enss) ->
+ let enss = List.map (subst_ens k) enss in
+ C.MutConstruct (uri, tyno, consno, enss)
+ | C.Meta (i, mss) ->
+ let mss = List.map (subst_ms k) mss in
+ C.Meta(i, mss)
+ | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
+ | C.Appl ts ->
+ let ts = List.map (subst_term k) ts in
+ C.Appl ts
+ | C.MutCase (uri, tyno, outty, t, cases) ->
+ let cases = List.map (subst_term k) cases in
+ C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
+ | C.Prod (n, v, t) ->
+ C.Prod (n, subst_term k v, subst_term (succ k) t)
+ | C.Lambda (n, v, t) ->
+ C.Lambda (n, subst_term k v, subst_term (succ k) t)
+ | C.LetIn (n, v, t) ->
+ C.LetIn (n, subst_term k v, subst_term (succ k) t)
+ | C.Fix (i, fixes) ->
+ let fixesno = List.length fixes in
+ let fixes = List.map (subst_fix fixesno k) fixes in
+ C.Fix (i, fixes)
+ | C.CoFix (i, cofixes) ->
+ let cofixesno = List.length cofixes in
+ let cofixes = List.map (subst_cofix cofixesno k) cofixes in
+ C.CoFix (i, cofixes)
+ and subst_ens k (uri, t) = uri, subst_term k t
+ and subst_ms k = function
+ | None -> None
+ | Some t -> Some (subst_term k t)
+ and subst_fix fixesno k (n, ind, ty, bo) =
+ n, ind, subst_term k ty, subst_term (k + fixesno) bo
+ and subst_cofix cofixesno k (n, ty, bo) =
+ n, subst_term k ty, subst_term (k + cofixesno) bo
+in
+subst_term
+
+
+
+
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
let reduce context =
let rec reduceaux context l =
- let module C = Cic in
- let module S = CicSubstitution in
function
C.Rel n as t ->
(match List.nth context (n-1) with
(*CSC: It does not perform simplification in a Case *)
let simpl context =
- let module C = Cic in
- let module S = CicSubstitution in
(* a simplified term is active if it can create a redex when used as an *)
(* actual parameter *)
let rec is_active =
List.map (function uri,t -> uri,reduceaux context [] t)
(**** Step 2 ****)
and try_delta_expansion context l term body =
- let module C = Cic in
- let module S = CicSubstitution in
try
let res,constant_args =
let rec aux rev_constant_args l =
val replace_lifting_csc :
int -> equality:(Cic.term -> Cic.term -> bool) ->
what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
+val subst_inv :
+ equality:(Cic.term -> Cic.term -> bool) ->
+ what:Cic.term list -> int -> Cic.term -> Cic.term
val reduce : Cic.context -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term
val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 1 10:25:04 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 12 13:47:11 CET 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
val destruct : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?depth:int ->
+ ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val elim_intros_simpl :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?depth:int ->
+ ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val elim_type :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
connect_button tbar#elimButton (tac_w_term
- (A.Elim (loc, hole, None, None, [])));
+ (A.Elim (loc, (Some hole, [], Some CicNotationPt.UserInput), None, None, [])));
connect_button tbar#elimTypeButton (tac_w_term
(A.ElimType (loc, hole, None, None, [])));
connect_button tbar#splitButton (tac (A.Split loc));
projects / helm.git / commitdiff