quantifier and elimination of conjunciton implemented.
| 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
+ | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
+ | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
+ | RewritingStep of
+ loc * 'term option * 'term * 'term option * Cic.name option
type search_kind = [ `Locate | `Hint | `Match | `Elim ]
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 7
+let magic = 8
type 'obj command =
| Default of loc * string * UriManager.uri list
| 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 )
+ | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
+ | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")"
+ | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")"
+ | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id)
| Case (_, id, args) ->
"case" ^ id ^
String.concat " "
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.ExistsElim (_, t, id1, t1, id2, t2) ->
+ Declarative.existselim t id1 t1 id2 t2
| 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
+ | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
+ | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
+ Declarative.rewritingstep termine t1 t2 cont
let classify_tactic tactic =
match tactic with
| GrafiteAst.Thesisbecomes (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Thesisbecomes (loc, cic)
- | GrafiteAst.Let1 (loc, id, term, term1) ->
+ | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
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.ExistsElim(loc, cic, id1, cic', id2, cic'')
+ | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
+ let metasenv,cic = disambiguate_term context metasenv term 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)
+ metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')
| GrafiteAst.Case (loc, id, params) ->
let metasenv,params' =
List.fold_right
) params (metasenv,[])
in
metasenv,GrafiteAst.Case(loc, id, params')
- | GrafiteAst.RewritingStep (loc, term1, term2, term3) ->
+ | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
let metasenv,cic =
match term1 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'')
+ metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
let default_precedence = 50
let default_associativity = Gramext.NonA
+type by_continuation =
+ BYC_done
+ | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
+ | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+
EXTEND
GLOBAL: term statement;
arg: [
GrafiteAst.Assume (loc, id, 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];
+ | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
cont=by_continuation ->
+ let t' = match t with LNone _ -> None | LSome t -> Some t in
(match cont with
- None -> GrafiteAst.Bydone (loc, t)
- | Some (ty,id,t1) ->
- GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+ BYC_done -> GrafiteAst.Bydone (loc, t')
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
| 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 ->
| 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)
+ | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
+ | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
]
];
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
+ [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1)
+ | IDENT "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)
+ | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;
+ "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+ BYC_wehaveand (id1,t1,id2,t2)
+ ]
+];
+ rewriting_step_continuation : [
+ [ IDENT "done" -> None
+ | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
+ | -> Some Cic.Anonymous
]
];
atomic_tactical:
;;
let suppose t id ty =
+(*BUG: ty not used *)
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))
+ (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph))
;;
let by_term_we_proved t ty id ty' =
+(*BUG: ty' not used *)
match t with
None -> assert false
| Some t ->
;;
let we_need_to_prove t id ty =
+(*BUG: ty not used *)
let aux status =
let proof,goals =
ProofEngineTypes.apply_tactic
ProofEngineTypes.mk_tactic aux
;;
-let prova _ = assert false
-;;
-let bywehave _ = assert false
+let existselim t id1 t1 id2 t2 =
+(*BUG: t1 and t2 not used *)
+(*PARSING BUG: t2 is parsed in the current context, but it may
+ have occurrences of id1 in it *)
+ Tactics.elim_intros t
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2)
+
+let andelim = existselim;;
+
+let rewritingstep lhs rhs just conclude =
+ let aux ((proof,goal) as status) =
+ let (curi,metasenv,proofbo,proofty) = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let eq,trans =
+ match LibraryObjects.eq_URI () with
+ None -> assert false (*TODO*)
+ | Some uri ->
+ Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
+ in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+ let just =
+ match just with
+ None -> assert false (*TOOD*)
+ | Some just -> just
+ in
+ match lhs with
+ None ->
+ let plhs,prhs =
+ match
+ fst
+ (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
+ CicUniv.empty_ugraph)
+ with
+ Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
+ | _ -> assert false in
+ let last_hyp_name =
+ match context with
+ (Some (Cic.Name id,_))::_ -> id
+ | _ -> assert false
+ in
+ (match conclude with
+ None ->
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens
+ ~start:(Tactics.apply ~term:trans)
+ ~continuations:
+ [ Tactics.apply prhs ;
+ Tactics.apply (Cic.Rel 1) ;
+ Tactics.apply just]) status
+ | Some name ->
+ let mk_fresh_name_callback =
+ fun metasenv context _ ~typ ->
+ FreshNamesGenerator.mk_fresh_name ~subst:[]
+ metasenv context name ~typ
+ in
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens
+ ~start:(Tactics.cut ~mk_fresh_name_callback
+ (Cic.Appl [eq ; ty ; plhs ; rhs]))
+ ~continuations:
+ [ Tactics.clear ~hyps:[last_hyp_name] ;
+ Tacticals.thens
+ ~start:(Tactics.apply ~term:trans)
+ ~continuations:
+ [ Tactics.apply prhs ;
+ Tactics.apply (Cic.Rel 1) ;
+ Tactics.apply just]
+ ]) status)
+ | Some lhs ->
+ match conclude with
+ None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
+ | Some name ->
+ let mk_fresh_name_callback =
+ fun metasenv context _ ~typ ->
+ FreshNamesGenerator.mk_fresh_name ~subst:[]
+ metasenv context name ~typ
+ in
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens
+ ~start:
+ (Tactics.cut ~mk_fresh_name_callback
+ (Cic.Appl [eq ; ty ; lhs ; rhs]))
+ ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
+ in
+ ProofEngineTypes.mk_tactic aux
;;
+
let case _ = assert false
;;
let thesisbecomes _ = assert false
;;
let we_proceed_by_induction_on _ = assert false
;;
-let let1 _ = assert false
val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
-val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic
+val existselim :
+ Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
-val bywehave :
- Cic.term option -> Cic.term -> string -> Cic.term -> string ->
- ProofEngineTypes.tactic
+val andelim :
+ Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
-val prova :
- Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic
+val rewritingstep :
+ Cic.term option -> Cic.term -> Cic.term option -> Cic.name option ->
+ ProofEngineTypes.tactic
<keyword>know</keyword>
<keyword>case</keyword>
<keyword>obtain</keyword>
+ <keyword>done</keyword>
</keyword-list>
<keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
]
]
qed.
-
\ No newline at end of file
+
+
+theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
+ assume P: Prop.
+ suppose (P ∧ ∃m:nat.m ≠ m) (H).
+ by H we have P (H1) and (∃x:nat.x≠x) (H2).
+ (*BUG:
+ by H2 let q:nat such that (q ≠ q) (Ineq).
+ *)
+ (* the next line is wrong, but for the moment it does the job *)
+ by H2 let q:nat such that False (Ineq).
+ by I done.
+qed.
+
+theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
+assume n: nat.
+assume m:nat.
+assume p:nat.
+suppose (n=m) (H).
+suppose (S m = S p) (K).
+suppose (n = S p) (L).
+obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+ = (S p) by K.
+ = n by (sym_eq ? ? ? L)
+done.
+qed.
projects / helm.git / commitdiff