From ca2a604c2817deb118d595611b94a0d77978eab6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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 ++++++++++---------
.../software/components/grafite/grafiteAst.ml | 2 +-
.../components/grafite/grafiteAstPp.ml | 2 +-
.../grafite_parser/grafiteDisambiguate.ml | 3 +-
.../grafite_parser/grafiteParser.ml | 27 ++++++++++---
.../components/tactics/declarative.ml | 2 +
.../components/tactics/declarative.mli | 2 +-
helm/software/components/tactics/tactics.mli | 1 +
8 files changed, 50 insertions(+), 27 deletions(-)
diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 45e88ab0a..7d4839e03 100644
--- 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 0b54b68a4..b8a89e1b6 100644
--- 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 f689ff101..4828d0379 100644
--- 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 ececcf967..d4ab241cb 100644
--- 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 45a71f174..24d1b3feb 100644
--- 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 24801542d..b0615edb3 100644
--- 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 97514b684..8fd91b0e8 100644
--- 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 e9c265c8e..f46d53af9 100644
--- 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
--
2.39.5