1use super::helpers_by_stmt::impossible_proof_error_message;
2use crate::prelude::*;
3
4impl Runtime {
5 pub fn exec_by_cases_stmt(&mut self, stmt: &ByCasesStmt) -> Result<StmtResult, RuntimeError> {
6 for fact in stmt.then_facts.iter() {
7 self.verify_fact_well_defined(fact, &VerifyState::new(0, false))
8 .map_err(|verify_error| {
9 short_exec_error(
10 stmt.clone().into(),
11 format!("by cases: failed to prove `{}`", fact),
12 Some(verify_error),
13 vec![],
14 )
15 })?;
16 }
17
18 if stmt
19 .then_facts
20 .iter()
21 .any(|f| matches!(f, Fact::ForallFactWithIff(_)))
22 {
23 return Err(short_exec_error(
24 stmt.clone().into(),
25 "by cases: `prove:` with `forall`/`iff` (forall-iff) is not supported; use a plain `forall` goal"
26 .to_string(),
27 None,
28 vec![],
29 ));
30 }
31 if stmt
32 .then_facts
33 .iter()
34 .filter(|f| matches!(f, Fact::ForallFact(_)))
35 .count()
36 > 1
37 {
38 return Err(short_exec_error(
39 stmt.clone().into(),
40 "by cases: `prove:` may contain at most one `forall` fact".to_string(),
41 None,
42 vec![],
43 ));
44 }
45 if stmt
46 .then_facts
47 .get(0)
48 .is_some_and(|f| !matches!(f, Fact::ForallFact(_)))
49 && stmt
50 .then_facts
51 .iter()
52 .any(|f| matches!(f, Fact::ForallFact(_)))
53 {
54 return Err(short_exec_error(
55 stmt.clone().into(),
56 "by cases: when `prove:` includes `forall`, the `forall` must be listed first"
57 .to_string(),
58 None,
59 vec![],
60 ));
61 }
62 if stmt
63 .then_facts
64 .iter()
65 .any(|f| matches!(f, Fact::ForallFact(_)))
66 && stmt.impossible_facts.iter().any(|o| o.is_some())
67 {
68 return Err(short_exec_error(
69 stmt.clone().into(),
70 "by cases: `prove:` with `forall` cannot be used in the same statement as a case arm that ends with `impossible`"
71 .to_string(),
72 None,
73 vec![],
74 ));
75 }
76
77 self.exec_by_cases_stmt_verify_cases_cover_all_situations(stmt)?;
78
79 for case_index in 0..stmt.cases.len() {
80 self.run_in_local_env(|rt| rt.exec_by_cases_stmt_for_one_case(stmt, case_index))?;
81 }
82
83 let mut infer_result = InferResult::new();
84 for then_fact in stmt.then_facts.iter() {
85 let one_then_fact_infer_result = self
86 .verify_well_defined_and_store_and_infer_with_default_verify_state(
87 then_fact.clone(),
88 )
89 .map_err(|store_fact_error| {
90 short_exec_error(
91 stmt.clone().into(),
92 format!("by cases: failed to release `{}`", then_fact),
93 Some(store_fact_error),
94 vec![],
95 )
96 })?;
97 infer_result.new_infer_result_inside(one_then_fact_infer_result);
98 }
99
100 Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
102 }
103
104 fn exec_by_cases_stmt_verify_cases_cover_all_situations(
105 &mut self,
106 stmt: &ByCasesStmt,
107 ) -> Result<(), RuntimeError> {
108 let all_cases_or_fact: Fact =
109 OrFact::new(stmt.cases.clone(), stmt.line_file.clone()).into();
110 let vs = VerifyState::new(0, false);
111 if let Some(Fact::ForallFact(ff)) = stmt.then_facts.first() {
112 self.run_in_local_env(|rt| {
113 rt.forall_assume_params_and_dom_in_current_env(ff, &vs)?;
114 rt.verify_fact_return_err_if_not_true(&all_cases_or_fact, &vs)
115 })
116 .map_err(|verify_error| {
117 short_exec_error(
118 stmt.clone().into(),
119 "by cases: cannot verify that all cases cover all situations".to_string(),
120 Some(verify_error),
121 vec![],
122 )
123 })?;
124 } else {
125 self.verify_fact_return_err_if_not_true(&all_cases_or_fact, &vs)
126 .map_err(|verify_error| {
127 short_exec_error(
128 stmt.clone().into(),
129 "by cases: cannot verify that all cases cover all situations".to_string(),
130 Some(verify_error),
131 vec![],
132 )
133 })?;
134 }
135 Ok(())
136 }
137
138 fn exec_by_cases_stmt_prove_then_facts_under_case(
139 &mut self,
140 stmt: &ByCasesStmt,
141 case_index: usize,
142 inside_results: &mut Vec<StmtResult>,
143 ) -> Result<(), RuntimeError> {
144 for then_fact in stmt.then_facts.iter() {
145 let exec_fact_result = self.exec_fact(then_fact).map_err(|statement_error| {
146 short_exec_error(
147 stmt.clone().into(),
148 format!(
149 "by cases: failed to prove `{}` under case `{}`",
150 then_fact, stmt.cases[case_index]
151 ),
152 Some(statement_error),
153 std::mem::take(inside_results),
154 )
155 })?;
156 inside_results.push(exec_fact_result);
157 }
158 Ok(())
159 }
160
161 fn exec_by_cases_stmt_for_one_case(
162 &mut self,
163 stmt: &ByCasesStmt,
164 case_index: usize,
165 ) -> Result<Vec<StmtResult>, RuntimeError> {
166 let case_fact = &stmt.cases[case_index];
167 let case_label = case_fact.to_string();
168 let mut inside_results: Vec<StmtResult> = Vec::new();
169 let vs = VerifyState::new(0, false);
170
171 if let Some(Fact::ForallFact(ff)) = stmt.then_facts.first() {
172 let mut infer_acc = self
173 .forall_assume_params_and_dom_in_current_env(ff, &vs)
174 .map_err(|e| {
175 short_exec_error(
176 stmt.clone().into(),
177 format!(
178 "by cases: failed to open `forall` parameters and dom for goal `{}`",
179 ff
180 ),
181 Some(e),
182 vec![],
183 )
184 })?;
185
186 self.store_and_chain_atomic_fact_without_well_defined_verified_and_infer(
187 case_fact.clone(),
188 )
189 .map_err(|store_fact_error| {
190 short_exec_error(
191 stmt.clone().into(),
192 format!("by cases: failed to assume case `{}`", case_fact),
193 Some(store_fact_error),
194 vec![],
195 )
196 })?;
197
198 for proof_stmt in stmt.proofs[case_index].iter() {
199 let exec_stmt_result = self.exec_stmt(proof_stmt);
200 match exec_stmt_result {
201 Ok(result) => inside_results.push(result),
202 Err(statement_error) => {
203 return Err(short_exec_error(
204 stmt.clone().into(),
205 format!(
206 "by cases: failed while executing proof under case `{}`",
207 case_fact
208 ),
209 Some(statement_error),
210 inside_results,
211 ));
212 }
213 }
214 }
215
216 let forall_then_result = self.forall_verify_then_facts_in_current_env(
217 ff,
218 &vs,
219 &mut infer_acc,
220 Some(&case_label),
221 )?;
222 if !forall_then_result.is_true() {
223 inside_results.push(forall_then_result);
224 return Err(short_exec_error(
225 stmt.clone().into(),
226 format!(
227 "by cases: failed to prove `forall` goal under case `{}`",
228 case_fact
229 ),
230 None,
231 inside_results,
232 ));
233 }
234 inside_results.push(forall_then_result);
235
236 for then_fact in stmt.then_facts.iter().skip(1) {
237 let exec_fact_result = self.exec_fact(then_fact).map_err(|statement_error| {
238 short_exec_error(
239 stmt.clone().into(),
240 format!(
241 "by cases: failed to prove `{}` under case `{}`",
242 then_fact, case_fact
243 ),
244 Some(statement_error),
245 std::mem::take(&mut inside_results),
246 )
247 })?;
248 inside_results.push(exec_fact_result);
249 }
250
251 return Ok(inside_results);
252 }
253
254 self.store_and_chain_atomic_fact_without_well_defined_verified_and_infer(case_fact.clone())
255 .map_err(|store_fact_error| {
256 short_exec_error(
257 stmt.clone().into(),
258 format!("by cases: failed to assume case `{}`", case_fact),
259 Some(store_fact_error),
260 vec![],
261 )
262 })?;
263
264 for proof_stmt in stmt.proofs[case_index].iter() {
265 let exec_stmt_result = self.exec_stmt(proof_stmt);
266 match exec_stmt_result {
267 Ok(result) => inside_results.push(result),
268 Err(statement_error) => {
269 return Err(short_exec_error(
270 stmt.clone().into(),
271 format!(
272 "by cases: failed while executing proof under case `{}`",
273 case_fact
274 ),
275 Some(statement_error),
276 inside_results,
277 ));
278 }
279 }
280 }
281
282 if let Some(impossible_fact) = &stmt.impossible_facts[case_index] {
283 let verify_state = VerifyState::new(0, false);
284 let verify_impossible_fact_result = self
285 .verify_atomic_fact(impossible_fact, &verify_state)
286 .map_err(|verify_error| {
287 short_exec_error(
288 stmt.clone().into(),
289 impossible_proof_error_message(
290 impossible_fact,
291 Some(case_fact.to_string()),
292 ),
293 Some(verify_error),
294 vec![],
295 )
296 })?;
297
298 if verify_impossible_fact_result.is_unknown() {
299 return Err(short_exec_error(
300 stmt.clone().into(),
301 impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
302 None,
303 vec![],
304 ));
305 }
306
307 let verify_reversed_impossible_fact_result = self
308 .verify_atomic_fact(&impossible_fact.make_reversed(), &verify_state)
309 .map_err(|verify_error| {
310 short_exec_error(
311 stmt.clone().into(),
312 impossible_proof_error_message(
313 impossible_fact,
314 Some(case_fact.to_string()),
315 ),
316 Some(verify_error),
317 vec![],
318 )
319 })?;
320
321 if verify_reversed_impossible_fact_result.is_unknown() {
322 return Err(short_exec_error(
323 stmt.clone().into(),
324 impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
325 None,
326 vec![],
327 ));
328 }
329
330 inside_results.push(
331 (NonFactualStmtSuccess::new(
332 stmt.clone().into(),
333 InferResult::new(),
334 vec![
335 verify_impossible_fact_result,
336 verify_reversed_impossible_fact_result,
337 ],
338 ))
339 .into(),
340 );
341
342 return Ok(inside_results);
343 }
344
345 self.exec_by_cases_stmt_prove_then_facts_under_case(stmt, case_index, &mut inside_results)?;
346 Ok(inside_results)
347 }
348}