1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: ppdecl_proof.ml 10739 2008-04-01 14:45:20Z herbelin $ *)
open Util
open Pp
open Decl_expr
open Names
open Nameops
let pr_constr = Printer.pr_constr_env
let pr_tac = Pptactic.pr_glob_tactic
let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
let pr_label = function
Anonymous -> mt ()
| Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
let pr_justification_items env = function
Some [] -> mt ()
| Some (_::_ as l) ->
spc () ++ str "by" ++ spc () ++
prlist_with_sep (fun () -> str ",") (pr_constr env) l
| None -> spc () ++ str "by *"
let pr_justification_method env = function
None -> mt ()
| Some tac ->
spc () ++ str "using" ++ spc () ++ pr_tac env tac
let pr_statement pr_it env st =
pr_label st.st_label ++ pr_it env st.st_it
let pr_or_thesis pr_this env = function
Thesis Plain -> str "thesis"
| Thesis (For id) ->
str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
| This c -> pr_this env c
let pr_cut pr_it env c =
hov 1 (pr_it env c.cut_stat) ++
pr_justification_items env c.cut_by ++
pr_justification_method env c.cut_using
let type_or_thesis = function
Thesis _ -> Term.mkProp
| This c -> c
let _I x = x
let rec print_hyps pconstr gtyp env sep _be _have hyps =
let pr_sep = if sep then str "and" ++ spc () else mt () in
match hyps with
(Hvar _ ::_) as rest ->
spc () ++ pr_sep ++ str _have ++
print_vars pconstr gtyp env false _be _have rest
| Hprop st :: rest ->
begin
let nenv =
match st.st_label with
Anonymous -> env
| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
spc() ++ pr_sep ++ pr_statement pconstr env st ++
print_hyps pconstr gtyp nenv true _be _have rest
end
| [] -> mt ()
and print_vars pconstr gtyp env sep _be _have vars =
match vars with
Hvar st :: rest ->
begin
let nenv =
match st.st_label with
Anonymous -> anomaly "anonymous variable"
| Name id -> Environ.push_named (id,None,st.st_it) env in
let pr_sep = if sep then pr_coma () else mt () in
spc() ++ pr_sep ++
pr_statement pr_constr env st ++
print_vars pconstr gtyp nenv true _be _have rest
end
| (Hprop _ :: _) as rest ->
let _st = if _be then
str "be such that"
else
str "such that" in
spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest
| [] -> mt ()
let pr_suffices_clause env (hyps,c) =
print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
let pr_elim_type = function
ET_Case_analysis -> str "cases"
| ET_Induction -> str "induction"
let pr_casee env =function
Real c -> str "on" ++ spc () ++ pr_constr env c
| Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
let pr_side = function
Lhs -> str "=~"
| Rhs -> str "~="
let rec pr_bare_proof_instr _then _thus env = function
| Pescape -> str "escape"
| Pthen i -> pr_bare_proof_instr true _thus env i
| Pthus i -> pr_bare_proof_instr _then true env i
| Phence i -> pr_bare_proof_instr true true env i
| Pcut c ->
begin
match _then,_thus with
false,false -> str "have" ++ spc () ++
pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
| false,true -> str "thus" ++ spc () ++
pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
| true,false -> str "then" ++ spc () ++
pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
| true,true -> str "hence" ++ spc () ++
pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
end
| Psuffices c ->
str "suffices" ++ pr_cut pr_suffices_clause env c
| Prew (sid,c) ->
(if _thus then str "thus" else str " ") ++ spc () ++
pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
| Passume hyps ->
str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
| Plet hyps ->
str "let" ++ print_vars pr_constr _I env false true "let" hyps
| Pclaim st ->
str "claim" ++ spc () ++ pr_statement pr_constr env st
| Pfocus st ->
str "focus on" ++ spc () ++ pr_statement pr_constr env st
| Pconsider (id,hyps) ->
str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
++ spc () ++ str "from " ++ pr_constr env id
| Pgiven hyps ->
str "given" ++ print_vars pr_constr _I env false false "given" hyps
| Ptake witl ->
str "take" ++ spc () ++
prlist_with_sep pr_coma (pr_constr env) witl
| Pdefine (id,args,body) ->
str "define" ++ spc () ++ pr_id id ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
pr_statement pr_constr env st ++ str ")") args ++ spc () ++
str "as" ++ (pr_constr env body)
| Pcast (id,typ) ->
str "reconsider" ++ spc () ++
pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
str "as" ++ spc () ++ (pr_constr env typ)
| Psuppose hyps ->
str "suppose" ++
print_hyps pr_constr _I env false false "we have" hyps
| Pcase (params,pat,hyps) ->
str "suppose it is" ++ spc () ++ pr_pat pat ++
(if params = [] then mt () else
(spc () ++ str "with" ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
pr_statement pr_constr env st ++ str ")") params ++ spc ()))
++
(if hyps = [] then mt () else
(spc () ++ str "and" ++
print_hyps (pr_or_thesis pr_constr) type_or_thesis
env false false "we have" hyps))
| Pper (et,c) ->
str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
pr_casee env c
| Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
| _ -> anomaly "unprintable instruction"
let pr_emph = function
0 -> str " "
| 1 -> str "* "
| 2 -> str "** "
| 3 -> str "*** "
| _ -> anomaly "unknown emphasis"
let pr_proof_instr env instr =
pr_emph instr.emph ++ spc () ++
pr_bare_proof_instr false false env instr.instr
|
