| Transitivity of loc * 'term
(* Costruttori Aggiunti *)
| Assume of loc * 'ident * 'term
- | Suppose of loc * 'term *'ident
- | By_term_we_proved of loc * 'term * 'term * 'ident
- | We_need_to_prove of loc * 'term * 'ident
- | Bydone of loc * 'term
-
+ | Suppose of loc * 'term *'ident * 'term option
+ | By_term_we_proved of loc *'term option * 'term * 'ident * 'term option
+ | We_need_to_prove of loc * 'term * 'ident * 'term option
+ | Bydone of loc * 'term option
+ | We_proceed_by_induction_on of loc * 'term * 'term
+ | Byinduction of loc * 'term * 'ident
+ | Thesisbecomes of loc * 'term
+ | Case of loc * string * (string * 'term) list
+ | Let1 of loc * 'ident * 'term * 'term
+ | Bywehave of loc * 'term option * 'term * 'ident * 'term * 'ident
+ | RewritingStep of loc * 'term option * 'term * 'term option
+
type search_kind = [ `Locate | `Hint | `Match | `Elim ]
type print_kind = [ `Env | `Coer ]
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 6
+let magic = 7
type 'obj command =
| Default of loc * string * UriManager.uri list
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
-
- let pp_search_kind = function
+ (* Tattiche Aggiunte *)
+ | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term
+ | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+ | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
+ | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^
+ (match term2 with None -> " " | Some term2 -> term_pp term2)
+ | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+ | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
+ | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
+ | Thesisbecomes (_, term) -> "the thesis becomes" ^ term_pp term
+ | Let1 (_, ident, term, term1) -> "let" ^ ident ^ ":" ^ term_pp term ^ "such that" ^ term_pp term1
+ | Bywehave (_, term, term1, ident, term2, ident1) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we have" ^ term_pp term1 ^ "(" ^ ident ^ ")" ^ "and" ^ term_pp term2 ^ "(" ^ ident1 ^ ")"
+ | RewritingStep (_, term, term1, term2 ) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2 )
+ | Case (_, id, args) ->
+ "case" ^ id ^
+ String.concat " "
+ (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")")
+ args)
+
+ let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| `Match -> "match"
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
(* Implementazioni Aggiunte *)
| GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
- | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
- | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
- Declarative.by_term_we_proved t ty id
- | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
- | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
+ | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
+ | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
+ Declarative.by_term_we_proved t ty id t1
+ | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
+ Declarative.we_need_to_prove t id t2
+ | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
+ | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+ Declarative.we_proceed_by_induction_on t t1
+ | GrafiteAst.Byinduction (_, t, id) -> Declarative.assume id t
+ | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
+ | GrafiteAst.Let1 (_, id, t, t1) -> Declarative.let1 id t t1
+ | GrafiteAst.Case (_,id,params) -> Declarative.case id params
+ | GrafiteAst.Bywehave(_,t,t1,id,t2,id1) -> Declarative.bywehave t t1 id t2 id1
+ | GrafiteAst.RewritingStep (_,termine,t1,t2) -> Declarative.prova termine t1 t2
-(* maybe we only need special cases for apply and goal *)
let classify_tactic tactic =
match tactic with
(* tactics that can't close the goal (return a goal we want to "select") *)
-(* Copyright (C) 2005, HELM Team.
+(*
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
| GrafiteAst.Assume (loc, id, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Assume (loc, id, cic)
- | GrafiteAst.Suppose (loc, term, id) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Suppose (loc, cic, id)
+ | GrafiteAst.Suppose (loc, term, id, term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' =
+ match term' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
| GrafiteAst.Bydone (loc,term) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ |Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.Bydone (loc, cic)
+ | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Bydone (loc, cic)
- | GrafiteAst.We_need_to_prove (loc,term,id) ->
+ let metasenv,cic' =
+ match term' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
+ | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ let metasenv,cic'' =
+ match term'' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+ | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.We_need_to_prove (loc,cic,id)
- | GrafiteAst.By_term_we_proved (loc,term,term',id) ->
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
+ | GrafiteAst.Byinduction (loc, term, id) ->
let metasenv,cic = disambiguate_term context metasenv term in
- let metasenv,cic' = disambiguate_term context metasenv term' in
- metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id)
+ metasenv,GrafiteAst.Byinduction(loc, cic, id)
+ | GrafiteAst.Thesisbecomes (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Thesisbecomes (loc, cic)
+ | GrafiteAst.Let1 (loc, id, term, term1) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic'= disambiguate_term context metasenv term1 in
+ metasenv,GrafiteAst.Let1(loc, id, cic, cic')
+ | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic'= disambiguate_term context metasenv term1 in
+ let metasenv,cic''= disambiguate_term context metasenv term2 in
+ metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1)
+ | GrafiteAst.Case (loc, id, params) ->
+ let metasenv,params' =
+ List.fold_right
+ (fun (id,term) (metasenv,params) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,(id,cic)::params
+ ) params (metasenv,[])
+ in
+ metasenv,GrafiteAst.Case(loc, id, params')
+ | GrafiteAst.RewritingStep (loc, term1, term2, term3) ->
+ let metasenv,cic =
+ match term1 with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic'= disambiguate_term context metasenv term2 in
+ let metasenv,cic'' =
+ match term3 with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'')
+
let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
let uri =
(* Produzioni Aggiunte *)
| IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
GrafiteAst.Assume (loc, id, t)
- | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
- GrafiteAst.Suppose (loc, t, id)
- | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
- GrafiteAst.By_term_we_proved (loc, t, ty, id)
- | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
- GrafiteAst.We_need_to_prove (loc, t, id)
- | IDENT "by" ; t = tactic_term ; IDENT "done" ->
- GrafiteAst.Bydone (loc, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']->
+ GrafiteAst.Suppose (loc, t, id, t1)
+ | IDENT "by" ; t = [t' = tactic_term -> Some t' | SYMBOL "_" -> None];
+ cont=by_continuation ->
+ (match cont with
+ None -> GrafiteAst.Bydone (loc, t)
+ | Some (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ GrafiteAst.We_need_to_prove (loc, t, id, t1)
+ | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
+ | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Byinduction(loc, t, id)
+ | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
+ GrafiteAst.Thesisbecomes(loc, t)
+ | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
+ SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
+ GrafiteAst.Case(loc,id,params)
+ | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term ->
+ GrafiteAst.Let1 (loc, id, t, t1)
+ | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ->
+ GrafiteAst.Bywehave (loc, t, t1, id, t2, id1)
+ | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
+ GrafiteAst.RewritingStep(loc, Some termine, t1, t2)
+ | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2)
+ ]
+];
+ by_continuation: [
+ [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> Some (ty,id,t1)
+ | IDENT "done" -> None
]
- ];
+];
atomic_tactical:
[ "sequence" LEFTA
[ t1 = SELF; SYMBOL ";"; t2 = SELF ->
*)
let assume id t =
- Tacticals.then_
- ~start:
- (Tactics.intros ~howmany:1
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
- ~continuation:
- (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
- (fun _ metasenv ugraph -> t,metasenv,ugraph))
+ Tacticals.then_
+ ~start:
+ (Tactics.intros ~howmany:1
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+ ~continuation:
+ (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph))
;;
-let suppose t id =
+let suppose t id ty =
Tacticals.then_
~start:
(Tactics.intros ~howmany:1
(fun _ metasenv ugraph -> t,metasenv,ugraph))
;;
-let by_term_we_proved t ty id =
- Tacticals.thens
- ~start:
- (Tactics.cut ty
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
- ~continuations:
- [ Tacticals.id_tac ; Tactics.apply t ]
+let by_term_we_proved t ty id ty' =
+ match t with
+ None -> assert false
+ | Some t ->
+ Tacticals.thens
+ ~start:
+ (Tactics.cut ty
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:
+ [ Tacticals.id_tac ; Tactics.apply t ]
;;
let bydone t =
- (Tactics.apply ~term:t)
+ match t with
+ None -> assert false
+ | Some t ->
+ (Tactics.apply ~term:t)
;;
-let we_need_to_prove t id =
+let we_need_to_prove t id ty =
let aux status =
let proof,goals =
ProofEngineTypes.apply_tactic
in
ProofEngineTypes.mk_tactic aux
;;
+
+let prova _ = assert false
+;;
+let bywehave _ = assert false
+;;
+let case _ = assert false
+;;
+let thesisbecomes _ = assert false
+;;
+let byinduction _ = assert false
+;;
+let we_proceed_by_induction_on _ = assert false
+;;
+let let1 _ = assert false
*)
val assume : string -> Cic.term -> ProofEngineTypes.tactic
-val suppose : Cic.term -> string -> ProofEngineTypes.tactic
-val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
-val bydone : Cic.term -> ProofEngineTypes.tactic
-val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic
+
+val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+
+val by_term_we_proved : Cic.term option -> Cic.term -> string -> Cic.term option ->ProofEngineTypes.tactic
+
+val bydone : Cic.term option -> ProofEngineTypes.tactic
+
+val we_need_to_prove :
+ Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+
+val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic
+
+val byinduction : Cic.term -> string -> ProofEngineTypes.tactic
+
+val thesisbecomes : Cic.term -> ProofEngineTypes.tactic
+
+val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
+
+val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic
+
+val bywehave :
+ Cic.term option -> Cic.term -> string -> Cic.term -> string ->
+ ProofEngineTypes.tactic
+
+val prova :
+ Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic
<keyword>transitivity</keyword>
<keyword>unfold</keyword>
<keyword>whd</keyword>
- </keyword-list>
+ (* Tattiche Aggiunte *)
+ <keyword>assume</keyword>
+ <keyword>suppose</keyword>
+ <keyword>by</keyword>
+ <keyword>we</keyword>
+ <keyword>prove</keyword>
+ <keyword>proved</keyword>
+ <keyword>need</keyword>
+ <keyword>proceed</keyword>
+ <keyword>induction</keyword>
+ <keyword>inductive</keyword>
+ <keyword>case</keyword>
+ <keyword>base</keyword>
+ <keyword>let</keyword>
+ <keyword>such</keyword>
+ <keyword>that</keyword>
+ <keyword>by</keyword>
+ <keyword>have</keyword>
+ <keyword>and</keyword>
+ <keyword>the</keyword>
+ <keyword>thesis</keyword>
+ <keyword>becomes</keyword>
+ <keyword>hypothesis</keyword>
+ <keyword>know</keyword>
+ <keyword>case</keyword>
+ <keyword>obtain</keyword>
+</keyword-list>
<keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
<keyword>try</keyword>
projects / helm.git / commitdiff