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

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 45e88ab0a26a9fc5626fc1a86bf6565d2477a9df..7d4839e035862a4b9671e3d5ee8f0ac47872b58d 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/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/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 0b54b68a4c6a1717b5d515f976cb2f40ce65be79..b8a89e1b6d885bf7293c8e5221f8d39e66eac22f 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/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/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index f689ff101d1c78561248b32c1a64dd7adeddde71..4828d037957a72e291de454bd361fd75e9726e55 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/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/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index ececcf967934f82ee5ccbbeb150b07b85e405b15..d4ab241cbbc64cfe8638980b81e4e051dcf9e57f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/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/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 45a71f174dea678322b79bd97fcaecf0e5a31b79..24d1b3feb441b864d977807b931196e1c3ea33f5 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 24801542dabcb76f57a6684a6d60fccaef31a488..b0615edb36c728415c5a03e8926278f03c3006a3 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/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/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index 97514b684b64bf8486b4fb8ddc9c8732c7ca40e5..8fd91b0e853f9c4a83c35d9604de5518aea571d9 100644 (file)
--- a/helm/software/components/tactics/declarative.mli
+++ b/helm/software/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/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index e9c265c8e3e451a3b45bccc699dc2c3ad97e77d9..f46d53af9d632ff51e9117e58fc02a3ef7a648fb 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/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