Add drafts for assume, suppose, we_need_to_prove.
Add a just type to handle justfications in tactics.
Add drafts for the by_done and by_just_we_proved tactics.
Everything needs testing
type auto_params = nterm list option * (string*string) list
+(* The additional a is for abstract *)
+type 'term aauto_params = 'term list option * (string*string) list
+
+type 'term just = [`Term of 'term | `Auto of 'term aauto_params]
+
type ntactic =
| NApply of loc * nterm
| NSmartApply of loc * nterm
| NBlock of loc * ntactic list
(* Declarative langauge *)
(* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
- | Assume of loc * string * nterm (* loc, identifier, term *)
- | Suppose of loc * nterm *string * nterm option
+ | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
+ | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
+ | By_just_we_proved of loc * nterm just * nterm * string option * nterm option (* loc,
+ justification, conclusion, identifier, eqconcl *)
+ | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
+ identifier, equivnewcon *)
+ | Bydone of loc * nterm just
+ (*
+ | ExistsElim of loc * nterm just * string * nterm * nterm * string
+ | AndElim of loc * nterm just * nterm * string * nterm * string
+ *)
type nmacro =
| NCheck of loc * nterm
in
Printf.sprintf "%sin %s%s" what_text hyp_text goal_text
+let pp_auto_params params status =
+ match params with
+ | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+ | (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags)
+;;
+
+let pp_just status just =
+ match just with
+ `Term term -> "exact " ^ NotationPp.pp_term status term
+ | `Auto params -> pp_auto_params params status
+;;
+
let rec pp_ntactic status ~map_unicode_to_tex =
let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
function
| NBlock (_,l) ->
"(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
| NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
- | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
+ | Assume (_, ident, term, term1) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term ^
+ (match term1 with None -> " " | Some t1 -> " that is eqivalent to " ^ NotationPp.pp_term status t1)
| Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match
- term1 with None -> "" | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
+ term1 with None -> " " | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
+ | By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just ^ "we proved" ^
+ NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match
+ term2 with None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2)
+ | We_need_to_prove (_,term,ident,term1) -> "we need to prove" ^ NotationPp.pp_term status term ^
+ (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match term1 with None -> " " | Some t1
+ -> "or equivalently" ^ NotationPp.pp_term status t1)
+ | Bydone (_, just) -> pp_just status just ^ "done"
+ (*
+ | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":"
+ ^ NotationPp.pp_term term ^ "such that " ^ NotationPp.pp_term term1 ^ "(" ^ ident1 ^ ")"
+ | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just ~NotationPp.pp_term just ^ "we have " ^ NotationPp.pp_term term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term term2 ^ " (" ^ ident2 ^ ")"
+ *)
;;
let pp_nmacro status = function
;;
let eval_ng_tac tac =
+ let just_to_tacstatus_just just text prefix_len =
+ match just with
+ | `Term t -> `Term (text,prefix_len,t)
+ | `Auto (l,params) ->
+ (
+ match l with
+ | None -> `Auto (None,params)
+ | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params)
+ )
+ in
let rec aux f (text, prefix_len, tac) =
match tac with
| GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
|GrafiteAst.NRepeat (_,tac) ->
NTactics.repeat_tac (f f (text, prefix_len, tac))
- |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t
- |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1
+ |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
+ None | Some t1 -> (Some (text,prefix_len,t1)))
+ |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
+ -> None | Some t1 -> (Some (text,prefix_len,t1)))
+ |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
+ (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
+ Some t2 -> (Some (text,prefix_len,t2)))
+ |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+ (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+ | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
+ (*
+ | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
+ Declarative.existselim just id1 t1 t2 id2
+ | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) ->
+ Declarative.andelim just t1 id1 t2 id2
+ *)
in
aux aux tac (* trick for non uniform recursion call *)
;;
type by_continuation =
BYC_done
| BYC_weproved of N.term * string option * N.term option
- | BYC_letsuchthat of string * N.term * string * N.term
+ | BYC_letsuchthat of string * N.term * N.term * string
| BYC_wehaveand of string * N.term * string * N.term
let mk_parser statement lstatus =
| SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
| SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
| SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
- | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+ | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term ; t1 = OPT [IDENT "that"; IDENT "is";
+ IDENT "equivalent"; "to"; t' = tactic_term -> t']-> G.NTactic (loc,[G.Assume (loc,id,t,t1)])
| IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT
"is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
+ | just =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | params = auto_params ->
+ let just,params = params in
+ `Auto
+ (match just with
+ | None -> (None,params)
+ | Some (`Univ univ) -> (Some univ,params)
+ (* `Trace behaves exaclty like None for the moment being *)
+ | Some (`Trace) -> (None,params)
+ )
+ ];
+ cont=by_continuation -> G.NTactic (loc,[
+ (match cont with
+ BYC_done -> G.Bydone (loc, just)
+ | BYC_weproved (ty,id,t1) ->
+ G.By_just_we_proved(loc, just, ty, id, t1)
+ (*
+ | BYC_letsuchthat (id1,t1,t2,id2) ->
+ G.ExistsElim (loc, just, id1, t1, t2, id2)
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ G.AndElim (loc, just, id1, t1, id2, t2)*))
+ ])
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])
]
];
auto_fixed_param: [
]
];
-(* MATITA 1.0
by_continuation: [
[ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
| WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
| "done" -> BYC_done
| "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
- id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
+ id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,t2,id2)
| WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
BYC_wehaveand (id1,t1,id2,t2)
]
];
-*)
-(* MATITA 1.0
+
rewriting_step_continuation : [
[ "done" -> true
| -> false
]
];
-*)
+
(* MATITA 1.0
atomic_tactical:
[ "sequence" LEFTA
nTacStatus.mli \
nCicElim.mli \
nTactics.mli \
- declarative.mli \
nnAuto.mli \
+ declarative.mli \
nDestructTac.mli \
nInversion.mli
module Ast = NotationPt
open NTactics
+open NTacStatus
-let assume name ty =
- exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne)))
+type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ]
-let suppose t id t1 =
- let t1 = match t1 with None -> t | Some t1 -> t1 in
- exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit `JustOne)))
+let mk_just =
+ function
+ `Auto (l,params) -> NnAuto.auto_tac ~params:(l,params) ?trace_ref:None
+ | `Term t -> apply_tac t
+
+let extract_conclusion_type status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let status,gty = term_of_cic_term status gty ctx in
+ gty
+;;
+
+let same_type_as_conclusion ty t status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
+ let (_,_,metasenv,subst,_) = status#obj in
+ let status,ty = term_of_cic_term status cicterm ctx in
+ if NCicReduction.alpha_eq status metasenv subst ctx t ty then
+ true
+ else
+ false
+;;
+
+let same_type t1 t2 status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let status1,cicterm1 = disambiguate status ctx t1 `XTNone in
+ let status1,term1 = term_of_cic_term status cicterm1 (ctx_of cicterm1) in
+ let status2,cicterm2 = disambiguate status ctx t2 `XTNone in
+ let status2,term2 = term_of_cic_term status cicterm2 (ctx_of cicterm2) in
+ let (_,_,metasenv,subst,_) = status#obj in
+ if NCicReduction.alpha_eq status1 metasenv subst ctx term1 term2 then
+ true
+ else
+ false
+;;
+
+let assume name ty eqty =
+ distribute_tac (fun status goal ->
+ match extract_conclusion_type status goal with
+ | NCic.Prod (_,t,_) ->
+ if same_type_as_conclusion ty t status goal then
+ match eqty with
+ | None ->
+ let (_,_,ty) = ty in
+ exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit
+ `JustOne)))) status goal
+
+ | Some eqty ->
+ if same_type ty eqty status goal then
+ let (_,_,eqty) = eqty in
+ exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some eqty),Ast.Implicit
+ `JustOne)))) status goal
+ else
+ fail (lazy "The two given types are not equivalent")
+ else
+ fail (lazy "The assumed type is wrong")
+ | _ -> fail (lazy "You can't assume without an universal quantification")
+ )
+;;
+
+let suppose t1 id t2 =
+ distribute_tac (fun status goal ->
+ match extract_conclusion_type status goal with
+ | NCic.Prod (_,t,_) ->
+ if same_type_as_conclusion t1 t status goal then
+ match t2 with
+ | None ->
+ let (_,_,t1) = t1 in
+ exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+ `JustOne)))) status goal
+
+ | Some t2 ->
+ if same_type t1 t2 status goal then
+ let (_,_,t2) = t2 in
+ exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
+ `JustOne)))) status goal
+ else
+ fail (lazy "The two given proposition are not equivalent")
+ else
+ fail (lazy "The supposed proposition is different from the premise")
+ | _ -> fail (lazy "You can't suppose without a logical implication")
+ )
+
+let we_need_to_prove t id t1 =
+ distribute_tac (fun status goal ->
+ match id with
+ | None ->
+ (
+ match t1 with
+ (* Change the conclusion of the sequent with t *)
+ (* Is the pattern correct? Probably not *)
+ | None -> (* We need to prove t *)
+ exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t) status goal
+ | Some t1 -> (* We need to prove t or equivalently t1 *)
+ if same_type t1 t status goal then
+ exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) status goal
+ else
+ fail (lazy "The two conclusions are not equivalent")
+ )
+ | Some id ->
+ (
+ let (_,_,npt_t) = t in
+ match t1 with
+ | None -> (* We need to prove t (id) *)
+ exec (block_tac [cut_tac t; exact_tac ("",0,(Ast.LetIn ((Ast.Ident
+ (id,None),None),npt_t,Ast.Implicit
+ `JustOne)))]) status goal
+ | Some t1 -> (* We need to prove t (id) or equivalently t1 *)
+ exec (block_tac [cut_tac t; change_tac ~where:("",0,(None,[],Some Ast.UserInput))
+ ~with_what:t1; exact_tac ("",0,(Ast.LetIn ((Ast.Ident (id,None),None),npt_t,Ast.Implicit
+ `JustOne)))]) status goal
+ )
+ )
+;;
+
+let by_just_we_proved just ty id ty' =
+ let just = mk_just just in
+ match id with
+ | None ->
+ (match ty' with
+ | None -> (* just we proved P done *)
+ just
+ | Some ty' -> (* just we proved P that is equivalent to P' done *)
+ (* I should probably check that ty' is the same thing as the conclusion of the
+ sequent of the open goal and that ty and ty' are equivalent *)
+ block_tac [ change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just]
+ )
+ | Some id ->
+ let ty',continuation =
+ match ty' with
+ | None -> ty,just
+ | Some ty' -> ty', block_tac [change_tac ~where:("",0,(None,[id,Ast.Implicit `JustOne],None))
+ ~with_what:ty; just]
+ in block_tac [cut_tac ty'; continuation ]
+;;
+
+let bydone just =
+ mk_just just
+;;
+
+(*
+let existselim just id1 t1 t2 id2 =
+ let aux (proof, goal) =
+ let (n,metasenv,_subst,bo,ty,attrs) = proof in
+ 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,_subst,bo,ty,attrs) 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)
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
+ (mk_just ~dbd ~automation_cache just)
+ ]) (proof', goal)
+ in
+ ProofEngineTypes.mk_tactic aux
+;;
+
+let andelim just t1 id1 t2 id2 =
+ Tacticals.thens
+ ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
+ ~continuations:
+ [ Tactics.elim_intros (Cic.Rel 1)
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
+ (mk_just ~dbd ~automation_cache just) ]
+;;
+ *)
* http://cs.unibo.it/helm/.
*)
-val assume : string -> NotationPt.term -> 's NTacStatus.tactic
-val suppose : NotationPt.term -> string -> NotationPt.term option -> 's NTacStatus.tactic
+type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ]
+
+val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val bydone : just -> 's NTacStatus.tactic
+val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term
+option -> 's NTacStatus.tactic
<keyword>is</keyword>
<keyword>equivalent</keyword>
<keyword>to</keyword>
+ <keyword>we</keyword>
+ <keyword>need</keyword>
+ <keyword>prove</keyword>
+ <keyword>or</keyword>
+ <keyword>equivalently</keyword>
+ <keyword>by</keyword>
+ <keyword>done</keyword>
+ <keyword>proved</keyword>
<!-- commands -->
<keyword>alias</keyword>
projects / helm.git / commitdiff