From 78ed249d75b6b65847e4739dabf7c18b8288c7d8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:13:49 +0000 Subject: [PATCH] 1. "by proof" now allowed as a justification in equality chains. It opens a side-proof to be proved immediately. 2. Side proofs restored in equality chains in content2pres.ml --- components/content_pres/content2pres.ml | 38 ++++++++++--------- components/grafite/grafiteAst.ml | 2 +- components/grafite/grafiteAstPp.ml | 2 +- .../grafite_parser/grafiteDisambiguate.ml | 3 +- components/grafite_parser/grafiteParser.ml | 27 ++++++++++--- components/tactics/declarative.ml | 2 + components/tactics/declarative.mli | 2 +- components/tactics/tactics.mli | 1 + 8 files changed, 50 insertions(+), 27 deletions(-) diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml index 45e88ab0a..7d4839e03 100644 --- a/components/content_pres/content2pres.ml +++ b/components/content_pres/content2pres.ml @@ -132,9 +132,8 @@ let rec justification term2pres p = (B.b_kw "by")::B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")]), None else - (*(B.b_kw "by"), - Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])*) - proof2pres true term2pres p, None + B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"]), + Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = @@ -336,6 +335,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = if conclude.Con.conclude_method = "Intros+LetTac" || conclude.Con.conclude_method = "ByInduction" || conclude.Con.conclude_method = "TD_Conversion" + || conclude.Con.conclude_method = "Eq_chain" then B.Text([],"") else if omit_conclusion then @@ -435,6 +435,11 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (match (List.nth conclude.Con.conclude_args 6) with Con.ArgProof p -> justification term2pres p | _ -> assert false) in + let justif = + match justif2 with + None -> justif1 + | Some j -> j + in let term1 = (match List.nth conclude.Con.conclude_args 2 with Con.Term (_,t) -> term2pres t @@ -453,30 +458,27 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.b_space; justif1]):: match justif2 with None -> [] | Some j -> [B.indent j]) *) - if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) - || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then - B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"]) - else - B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"]) + if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) + || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then + B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"]) + else + B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"]) (*CSC: bad idea B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1; B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = -(* - if skip_initial_lambdas <> None (* cheating *) then - [B.b_kw "by _"] - else -*) - let j1,j2 = justification term2pres p in - j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> []) + let j1,j2 = justification term2pres p in + [j1], match j2 with Some j -> [j] | None -> [] in let rec aux args = match args with | [] -> [] | (Con.ArgProof p)::(Con.Term (_,t))::tl -> - B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw - "=";B.b_space;term2pres t;B.b_space]@justification p@ - (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl) + let justif1,justif2 = justification p in + B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw + "=";B.b_space;term2pres t;B.b_space]@justif1@ + (if tl <> [] then [B.Text ([],".")] else [B.b_space; B.b_kw "done" ; B.Text([],".")])@ + justif2))::(aux tl) | _ -> assert false in let hd = diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 0b54b68a4..b8a89e1b6 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -114,7 +114,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term | RewritingStep of loc * (string option * 'term) option * 'term * - [ `Term of 'term | `Auto of (string * string) list ] * + [ `Term of 'term | `Auto of (string * string) list | `Proof ] * bool (* last step*) type search_kind = [ `Locate | `Hint | `Match | `Elim ] diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index f689ff101..4828d0379 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -187,7 +187,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_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 (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "") + | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ " by " ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2 | `Proof -> "proof") ^ (if cont then " done" else "") | Case (_, id, args) -> "case" ^ id ^ String.concat " " diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index ececcf967..d4ab241cb 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -397,7 +397,8 @@ let rec disambiguate_tactic `Auto _ as t -> metasenv,t | `Term t -> let metasenv,t = disambiguate_term context metasenv t in - metasenv,`Term t in + metasenv,`Term t + | `Proof as t -> metasenv,t in metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 45a71f174..24d1b3feb 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -291,11 +291,28 @@ EXTEND | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> GrafiteAst.Case(loc,id,params) - | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont) - | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; - cont=rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, None, t1, t2, cont) + | start = + [ IDENT "conclude" -> None + | IDENT "obtain" ; name = IDENT -> Some name ] ; + termine = tactic_term ; + SYMBOL "=" ; + t1=tactic_term ; + IDENT "by" ; + t2 = + [ t=tactic_term -> `Term t + | SYMBOL "_" ; params = auto_params' -> `Auto params + | IDENT "proof" -> `Proof] ; + cont = rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont) + | SYMBOL "=" ; + t1=tactic_term ; + IDENT "by" ; + t2= + [ t=tactic_term -> `Term t + | SYMBOL "_" ; params = auto_params' -> `Auto params + | IDENT "proof" -> `Proof] ; + cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, None, t1, t2, cont) ] ]; auto_params: [ diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 24801542d..b0615edb3 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -193,6 +193,8 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = ~universe:(Universe.index Universe.empty (Universe.key ty) just) ~steps:1 () (* Tactics.apply just *) + | `Proof -> + Tacticals.id_tac in let plhs,prhs,prepare = match lhs with diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index 97514b684..8fd91b0e8 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -57,5 +57,5 @@ val andelim : val rewritingstep : dbd:HSql.dbd -> universe:Universe.universe -> (string option * Cic.term) option -> Cic.term -> - [ `Term of Cic.term | `Auto of (string * string) list ] -> + [ `Term of Cic.term | `Auto of (string * string) list | `Proof ] -> bool (* last step *) -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index e9c265c8e..f46d53af9 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -16,6 +16,7 @@ val cases_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic val change : + ?with_cast:bool -> pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic val clear : hyps:string list -> ProofEngineTypes.tactic -- 2.39.2