diff --git a/src/phl/README.md b/src/phl/README.md index d200fc609..388f1f969 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -105,11 +105,15 @@ equiv: one side at a time), parameterized by an entry of a catalogue: ("-transform") re-runs it on the goal's program and compares the subgoals up to conversion (programs up to alpha-equivalence). -Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`) and -`rmatch` (`EcTrRMatch`). Further entries come with the tactics that use -them. The framed form of `match C k` changes the precondition: it stays a -separate trusted rule of each logic, `t__rmatch_framed` -(`EcRMatch`). See `REFACTORING.md` §7f. +Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), +`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`) and `match-push` +(`EcTrMatchPush`), the last two pushing the continuation of a leading +conditional / `match` into its branches. The `if` and `match` tactics are +push + rule on the conditional alone (`EcIf`, `EcMatch`). +Further entries come with the tactics that use them. The framed form of +`match C k` changes the precondition: it stays a separate trusted rule of +each logic, `t__rmatch_framed` (`EcRMatch`). See +`REFACTORING.md` §7f. ## Directory layout @@ -125,7 +129,8 @@ src/phl/ Ec: one module per (logic, rule) transforms/ EcTr: catalogue entries of the program transformations ecPl*.ml computations shared by the rules of every logic: EcPlFrame, - EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform + EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform, + EcPlMatch ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index ae18315ce..fa49d6764 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -153,7 +153,8 @@ src/phl/ postcondition), EcPlWp (weakest precondition), EcPlRndSem (semantic sampling), EcPlRCond (deciding a conditional or a match), EcPlTransform (the transformation catalogue and - its obligations) + its obligations), EcPlMatch (branches of a `match` on + fresh program variables) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -374,11 +375,23 @@ Current catalogue: - `rmatch` (`EcTrRMatch`, deciding the `match` at a position, the arguments of the constructor being assigned to fresh program variables; obligation `OPrefixPost (hd, exists xs, e = C xs)`), used by `match C k` in every - logic (its unframed form, see below). + logic (its unframed form, see below); +- `if-push` (`EcTrIfPush`): `if b then c1 else c2; c` becomes the single + instruction `if b then { c1; c } else { c2; c }`; no obligation; +- `match-push` (`EcTrMatchPush`): `match e with C xs => b ...; c` becomes + the single instruction `match e with C xs => { b; c } ...`; no + obligation. The pattern variables are local identifiers bound in the + branch only: the binders of a branch are renamed apart when they occur + free in `c`, so that `c` is not captured. The decisions of a conditional or a match are computed by `EcPlRCond`. -Further entries come with the tactics that use them: if/match-push, then -swap, inline, kill/alias/cfold/set and proc rewrite. +The `if` and `match` tactics are push + rule on the conditional alone: they +push the continuation into the branches (when there is one) through the +transformation rule (on each side, for the two-sided equiv forms), then +apply the `if` / `match` rule of their logic (`EcIf`, +`EcMatch`), stated on the conditional alone. Further entries come +with the tactics that use them: swap, inline, kill/alias/cfold/set and +proc rewrite. Exception: the framed form of `match C k` (used when the variables of the discriminant `e` are neither read nor written by the prefix, and the diff --git a/src/phl/ecPhlCase.ml b/src/phl/ecPhlCase.ml index 531a15f41..f19a038ec 100644 --- a/src/phl/ecPhlCase.ml +++ b/src/phl/ecPhlCase.ml @@ -1,87 +1,42 @@ (* --------------------------------------------------------------------- *) -open EcFol -open EcCoreGoal -open EcLowPhlGoal open EcAst -(* --------------------------------------------------------------------- *) -let t_hoare_case_r ?(simplify = true) f tc = - let fand = if simplify then f_and_simpl else f_and in - let hs = tc1_as_hoareS tc in - let mt = snd hs.hs_m in - let concl1 = - f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs) - in - let concl2 = - f_hoareS - mt - (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f)) - hs.hs_s - (hs_po hs) - in - FApi.xmutate1 tc (`HlCase f) [concl1; concl2] - -(* --------------------------------------------------------------------- *) -let t_ehoare_case_r ?(simplify = true) f tc = - let _ = simplify in - let hs = tc1_as_ehoareS tc in - let mt = snd hs.ehs_m in - let concl1 = f_eHoareS mt (map_ss_inv2 f_interp_ehoare_form f (ehs_pr hs)) hs.ehs_s (ehs_po hs) in - let concl2 = f_eHoareS mt (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not f) (ehs_pr hs)) hs.ehs_s (ehs_po hs) in - FApi.xmutate1 tc (`HlCase f) [concl1; concl2] - -(* --------------------------------------------------------------------- *) -let t_bdhoare_case_r ?(simplify = true) f tc = - let fand = if simplify then f_and_simpl else f_and in - let bhs = tc1_as_bdhoareS tc in - let mt = snd bhs.bhs_m in - let concl1 = f_bdHoareS mt (map_ss_inv2 fand (bhs_pr bhs) f) bhs.bhs_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - let concl2 = f_bdHoareS mt - (map_ss_inv2 fand (bhs_pr bhs) (map_ss_inv1 f_not f)) bhs.bhs_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc (`HlCase f) [concl1; concl2] +open EcCoreGoal +open EcLowPhlGoal (* --------------------------------------------------------------------- *) -let t_equiv_case_r ?(simplify = true) f tc = - let fand = if simplify then f_and_simpl else f_and in - let es = tc1_as_equivS tc in - let mtl, mtr = snd es.es_ml, snd es.es_mr in - let concl1 = f_equivS mtl mtr (map_ts_inv2 fand (es_pr es) f) es.es_sl es.es_sr (es_po es) in - let concl2 = f_equivS mtl mtr (map_ts_inv2 fand (es_pr es) (map_ts_inv1 f_not f)) es.es_sl es.es_sr (es_po es) in - FApi.xmutate1 tc (`HlCase f) [concl1; concl2] +(* The [case] rules live, one module per logic, in [rules//]. This + module only keeps the legacy positional entry points (adapters onto + those rules, so that external callers and this module's interface are + unchanged) and the logic-agnostic dispatcher. *) (* --------------------------------------------------------------------- *) -let t_hoare_case ?simplify = - FApi.t_low1 "hoare-case" (t_hoare_case_r ?simplify) +let t_hoare_case ?(simplify = true) f = + EcHoareCase.(t_hoare_case { hca_cond = f; hca_simplify = simplify }) -let t_ehoare_case ?simplify = - FApi.t_low1 "ehoare-case" (t_ehoare_case_r ?simplify) +let t_bdhoare_case ?(simplify = true) f = + EcBdHoareCase.(t_bdhoare_case { bca_cond = f; bca_simplify = simplify }) -let t_bdhoare_case ?simplify = - FApi.t_low1 "bdhoare-case" (t_bdhoare_case_r ?simplify) - -let t_equiv_case ?simplify = - FApi.t_low1 "equiv-case" (t_equiv_case_r ?simplify) +let t_equiv_case ?(simplify = true) f = + EcEquivCase.(t_equiv_case { eca_cond = f; eca_simplify = simplify }) (* --------------------------------------------------------------------- *) -let t_hl_case_r ?simplify f tc = - match f with - | Inv_ss f -> - t_hS_or_bhS_or_eS - ~th:(t_hoare_case ?simplify f) - ~teh:(t_ehoare_case ?simplify f) - ~tbh:(t_bdhoare_case ?simplify f) - ~te:(fun _ -> tc_error !!tc "expecting a two sided formula") - tc - | Inv_ts f -> - let err _ = - tc_error !!tc "expecting a one sided formula" in - t_hS_or_bhS_or_eS - ~th:err - ~teh:err - ~tbh:err - ~te:(t_equiv_case ?simplify f) - tc - | _ -> assert false - -(* -------------------------------------------------------------------- *) -let t_hl_case ?simplify = FApi.t_low1 "hl-case" (t_hl_case_r ?simplify) +(* Dispatch on the formula kind and the goal kind. The ehoare rule has no + [simplify] option: its precondition is not a conjunction. *) +let t_hl_case ?simplify f tc = + match f, (FApi.tc1_goal tc).f_node with + | Inv_hs _, _ -> assert false + + | Inv_ss f, FhoareS _ -> t_hoare_case ?simplify f tc + | Inv_ss f, FeHoareS _ -> EcEHoareCase.(t_ehoare_case { ehca_cond = f }) tc + | Inv_ss f, FbdHoareS _ -> t_bdhoare_case ?simplify f tc + | Inv_ss _, FequivS _ -> tc_error !!tc "expecting a two sided formula" + + | Inv_ts f, FequivS _ -> t_equiv_case ?simplify f tc + | Inv_ts _, (FhoareS _ | FeHoareS _ | FbdHoareS _) -> + tc_error !!tc "expecting a one sided formula" + + | _, _ -> + tc_error_noXhl + ~kinds:[`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] + !!tc diff --git a/src/phl/ecPhlCond.ml b/src/phl/ecPhlCond.ml index baf9f449e..b6255b277 100644 --- a/src/phl/ecPhlCond.ml +++ b/src/phl/ecPhlCond.ml @@ -1,385 +1,19 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcTypes -open EcFol -open EcEnv -open EcAst - -open EcCoreGoal -open EcLowGoal -open EcLowPhlGoal - -module Sid = EcIdent.Sid - -(* -------------------------------------------------------------------- *) -module LowInternal = struct - - let t_finalize h h1 h2 = - FApi.t_seqs [t_elim_hyp h; - t_intros_i [h1;h2]; - t_apply_hyp h2] - - let t_finalize_ehoare h _h1 _h2 tc = - t_apply_hyp h tc - - let t_gen_cond ?(t_finalize=t_finalize) side e tc = - let hyps = FApi.tc1_hyps tc in - let fresh = ["&m"; "&m"; "_"; "_"; "_"] in - let fresh = LDecl.fresh_ids hyps fresh in - - let m1,m2,h,h1,h2 = as_seq5 fresh in - - let t_introm = if is_none side then t_id else t_intros_i [m1] in - - let t_sub b tc = - FApi.t_on1seq 0 - (EcPhlRCond.t_rcond side b (EcMatching.Position.cpos1 0)) - (FApi.t_seqs - [t_introm; EcPhlSkip.t_skip; t_intros_i [m2;h]; - t_finalize h h1 h2; t_simplify]) - tc - in - FApi.t_seqsub - (EcPhlCase.t_hl_case ~simplify:false e) - [t_sub true; t_sub false] tc -end (* -------------------------------------------------------------------- *) -let t_hoare_cond tc = - let hs = tc1_as_hoareS tc in - let (e,_,_) = fst (tc1_first_if tc hs.hs_s) in - LowInternal.t_gen_cond None (Inv_ss (ss_inv_of_expr (EcMemory.memory hs.hs_m) e)) tc - -(* -------------------------------------------------------------------- *) -let t_ehoare_cond tc = - let hs = tc1_as_ehoareS tc in - let (e,_,_) = fst (tc1_first_if tc hs.ehs_s) in - LowInternal.t_gen_cond ~t_finalize:LowInternal.t_finalize_ehoare - None (Inv_ss (ss_inv_of_expr (EcMemory.memory hs.ehs_m) e)) tc - -(* -------------------------------------------------------------------- *) -let t_bdhoare_cond tc = - let bhs = tc1_as_bdhoareS tc in - let (e,_,_) = fst (tc1_first_if tc bhs.bhs_s) in - LowInternal.t_gen_cond None (Inv_ss (ss_inv_of_expr (EcMemory.memory bhs.bhs_m) e)) tc - -(* -------------------------------------------------------------------- *) -let rec t_equiv_cond side tc = - let hyps = FApi.tc1_hyps tc in - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - - match side with - | Some s -> - let e = - match s with - | `Left -> - let (e,_,_) = fst (tc1_first_if tc es.es_sl) in - ss_inv_generalize_right (ss_inv_of_expr ml e) mr - | `Right -> - let (e,_,_) = fst (tc1_first_if tc es.es_sr) in - ss_inv_generalize_left (ss_inv_of_expr mr e) ml - in LowInternal.t_gen_cond side (Inv_ts e) tc - - | None -> - let el,_,_ = fst (tc1_first_if tc es.es_sl) in - let er,_,_ = fst (tc1_first_if tc es.es_sr) in - let el = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in - let er = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in - let fiff = - EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr - (map_ts_inv2 f_imp (es_pr es) (map_ts_inv2 f_iff el er)) in - - let fresh = ["hiff";"&m1";"&m2";"h";"h";"h"] in - let fresh = LDecl.fresh_ids hyps fresh in - - let hiff,m1,m2,h,h1,h2 = as_seq6 fresh in - - let t_aux = - let rwpt = - EcCoreGoal.ptlocal - ~args:[PAMemory m1; PAMemory m2; PASub None] - hiff in - - FApi.t_seqs [t_intros_i [m1] ; EcPhlSkip.t_skip; - t_intros_i [m2; h] ; t_elim_hyp h; - t_intros_i [h1; h2]; - FApi.t_seqsub - (t_rewrite rwpt (`RtoL, None)) - [t_apply_hyp h1; t_apply_hyp h2]] - in - FApi.t_on1seq 1 (t_cut fiff) - (t_intros_i_seq [hiff] - (FApi.t_seqsub - (t_equiv_cond (Some `Left)) - [FApi.t_seqsub - (EcPhlRCond.Low.t_equiv_rcond `Right true EcMatching.Position.cpos1_first) - [t_aux; t_clear hiff]; - FApi.t_seqsub - (EcPhlRCond.Low.t_equiv_rcond `Right false EcMatching.Position.cpos1_first) - [t_aux; t_clear hiff]])) - tc +(* The [if] and [match] rules live, one module per logic, in + [rules//]. This module only keeps the legacy entry points: + adapters onto the derived tactics there (the push transformation, then + the rule on the conditional alone), so that external callers and this + module's interface are unchanged. *) (* -------------------------------------------------------------------- *) -module LowMatchInternal : sig - val t_gen_match : side option -> FApi.backward -end = struct - let t_gen_match (side : side option) (tc : tcenv1) : tcenv = - let hyps = FApi.tc1_hyps tc in - let env = LDecl.toenv hyps in - let me, st = EcLowPhlGoal.tc1_get_stmt side tc in - - let (e, _), _ = tc1_first_match tc st in - let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in - let indt = oget (EcDecl.tydecl_as_datatype indt) in - let f = - let f = ss_inv_of_expr (EcMemory.memory me) e in - let pre = tc1_get_pre tc in - match pre, side with - | Inv_ts {mr}, Some `Left -> - Inv_ts (ss_inv_generalize_right f mr) - | Inv_ts {ml}, Some `Right -> - Inv_ts (ss_inv_generalize_left f ml) - | Inv_ss _, _ -> - Inv_ss f - | Inv_ts _, None -> tc_error !!tc "expecting a side" - | Inv_hs _, _ -> assert false - in - - let onsub (i : int) (tc : tcenv1) = - let cname, cargs = List.nth indt.tydt_ctors i in - let cargs = List.length cargs in - - let tc, names = t_intros_n_x cargs tc in - let tc = FApi.as_tcenv1 tc in - - let discharge (tc : tcenv1) = - let+ tc = - if Option.is_some side - then EcLowGoal.t_intros_n 1 tc - else t_id tc - in - - let+ tc = EcPhlSkip.t_skip tc in - let+ tc = EcLowGoal.t_intro_s `Fresh tc in - let+ tc = EcLowGoal.t_elim_and tc in - let e = EcEnv.LDecl.fresh_id (FApi.tc1_hyps tc) "e" in - - let+ tc = EcLowGoal.t_intros_i [e] tc in - let+ tc = EcLowGoal.t_intros_n ~clear:true 1 tc in - - let+ tc = - let hyps = FApi.tc1_hyps tc in - let args = - List.map - (fun x -> - let ty = EcEnv.LDecl.var_by_id x hyps in - PAFormula (f_local x ty)) - names in - EcLowGoal.t_exists_intro_s args tc in - - let+ tc = EcLowGoal.t_symmetry tc in - let+ tc = EcLowGoal.t_apply_hyp e ~args:[] ~sk:0 tc in - - t_id tc - in - - let clean (tc : tcenv1) = - let discharge_pre tc = - let+ tc = - if Option.is_some side - then EcLowGoal.t_intros_n 2 tc - else EcLowGoal.t_intros_n 1 tc - in - let+ tc = EcLowGoal.t_elim_and tc in - let+ tc = EcLowGoal.t_intro_s `Fresh tc in - let+ tc = EcLowGoal.t_elim_and tc in - let+ tc = EcLowGoal.t_intros_n ~clear:true 1 tc in - let+ tc = EcLowGoal.t_intro_s `Fresh tc in - tc - |> EcLowGoal.t_split - @! EcLowGoal.t_assumption `Alpha - in - let discharge_post tc = - let+ tc = - if Option.is_some side - then EcLowGoal.t_intros_n 2 tc - else EcLowGoal.t_intros_n 1 tc - in - let t_imp = EcLowGoal.t_intros_n 1 @! EcLowGoal.t_assumption `Alpha in - let t_iff = EcLowGoal.t_split @! t_imp in - tc |> FApi.t_or t_imp t_iff - in - - let pre = oget (EcLowPhlGoal.get_pre (FApi.tc1_goal tc)) in - let post = oget (EcLowPhlGoal.get_post (FApi.tc1_goal tc)) in - - let pre = map_inv1 (fun pre -> - let eq, _, pre = destr_and3 pre in - f_and eq pre) pre in - tc - |> EcPhlConseq.t_conseq pre post - @+ [discharge_pre; discharge_post; EcLowGoal.t_clears names] - in - - tc - |> EcPhlRCond.t_rcond_match side cname EcMatching.Position.cpos1_first - @+ [discharge; clean] - in - - let tc = FApi.as_tcenv1 (EcPhlExists.t_hr_exists_intro [f] tc) in - let tc = FApi.as_tcenv1 (EcPhlExists.t_hr_exists_elim_r ~bound:1 tc) in - let tc = EcLowGoal.t_elimT_ind `Case tc in - - FApi.t_onalli onsub tc -end - -(* -------------------------------------------------------------------- *) -let t_hoare_match (tc : tcenv1) : tcenv = - let _ : sHoareS = tc1_as_hoareS tc in - LowMatchInternal.t_gen_match None tc - -(* -------------------------------------------------------------------- *) -let t_bdhoare_match (tc : tcenv1) : tcenv = - let _ : bdHoareS = tc1_as_bdhoareS tc in - LowMatchInternal.t_gen_match None tc - -(* -------------------------------------------------------------------- *) -let t_equiv_match (s : side) (tc : tcenv1) : tcenv = - let _ : equivS = tc1_as_equivS tc in - LowMatchInternal.t_gen_match (Some s) tc - -(* -------------------------------------------------------------------- *) -let t_equiv_match_same_constr tc = - let hyps = FApi.tc1_hyps tc in - let env = LDecl.toenv hyps in - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - - let (el, bsl), sl = tc1_first_match tc es.es_sl in - let (er, bsr), sr = tc1_first_match tc es.es_sr in - - let pl, dt, tyl = oget (EcEnv.Ty.get_top_decl el.e_ty env) in - let pr, _ , tyr = oget (EcEnv.Ty.get_top_decl er.e_ty env) in - - if not (EcPath.p_equal pl pr) then - tc_error !!tc "match statements on different inductive types"; - - let dt = oget (EcDecl.tydecl_as_datatype dt) in - let fl = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in - let fr = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in - - let get_eqv_cond ((c, _), ((cl, _), (cr, _))) = - let bhl = List.map (fst_map EcIdent.fresh) cl in - let bhr = List.map (fst_map EcIdent.fresh) cr in - let cop = EcPath.pqoname (EcPath.prefix pl) c in - let copl = f_op cop tyl (toarrow (List.snd cl) fl.inv.f_ty) in - let copr = f_op cop tyr (toarrow (List.snd cr) fr.inv.f_ty) in - - let lhs = map_ts_inv1 (fun fl -> f_eq fl (f_app copl (List.map (curry f_local) bhl) fl.f_ty)) fl in - let lhs = map_ts_inv1 (f_exists (List.map (snd_map gtty) bhl)) lhs in - - let rhs = map_ts_inv1 (fun fr -> f_eq fr (f_app copr (List.map (curry f_local) bhr) fr.f_ty)) fr in - let rhs = map_ts_inv1 (f_exists (List.map (snd_map gtty) bhr)) rhs in - - EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr - (map_ts_inv2 f_imp_simpl (es_pr es) (map_ts_inv2 f_iff lhs rhs)) in - - let get_eqv_goal ((c, _), ((cl, bl), (cr, br))) = - let sb = Fsubst.f_subst_id in - let sb, bhl = add_elocals sb cl in - let sb, bhr = add_elocals sb cr in - let cop = EcPath.pqoname (EcPath.prefix pl) c in - let copl = f_op cop tyl (toarrow (List.snd cl) fl.inv.f_ty) in - let copr = f_op cop tyr (toarrow (List.snd cr) fr.inv.f_ty) in - let f_ands_simpl' f = f_ands_simpl (List.tl f) (List.hd f) in - let pre = map_ts_inv f_ands_simpl' - [es_pr es; map_ts_inv1 (fun fl -> f_eq fl (f_app copl (List.map (curry f_local) bhl) fl.f_ty)) fl; - map_ts_inv1 (fun fr -> f_eq fr (f_app copr (List.map (curry f_local) bhr) fr.f_ty)) fr ] - in - - f_forall - ( (List.map (snd_map gtty) bhl) @ - (List.map (snd_map gtty) bhr) ) - ( f_equivS (snd es.es_ml) (snd es.es_mr) pre - (EcModules.stmt ((s_subst sb bl).s_node @ sl.s_node)) - (EcModules.stmt ((s_subst sb br).s_node @ sr.s_node)) - (es_po es)) - - in - - let infos = - (List.combine dt.EcDecl.tydt_ctors (List.combine bsl bsr)) in - - let concl1 = List.map get_eqv_cond infos in - let concl2 = List.map get_eqv_goal infos in - - FApi.xmutate1 tc `Match (concl1 @ concl2) - -(* -------------------------------------------------------------------- *) -let t_equiv_match_eq tc = - let hyps = FApi.tc1_hyps tc in - let env = LDecl.toenv hyps in - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - - let (el, bsl), sl = tc1_first_match tc es.es_sl in - let (er, bsr), sr = tc1_first_match tc es.es_sr in - - let pl, dt, tyl = oget (EcEnv.Ty.get_top_decl el.e_ty env) in - let pr, _ , tyr = oget (EcEnv.Ty.get_top_decl er.e_ty env) in - - if not (EcPath.p_equal pl pr) then - tc_error !!tc "match statements on different inductive types"; - - if not (EcReduction.EqTest.for_type env el.e_ty er.e_ty) then - tc_error !!tc "synced match requires matches on the same type"; - - let dt = oget (EcDecl.tydecl_as_datatype dt) in - let fl = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in - let fr = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in - - let eqv_cond = - EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr - (map_ts_inv2 f_imp_simpl (es_pr es) (map_ts_inv2 f_eq fl fr)) in - - let get_eqv_goal ((c, _), ((cl, bl), (cr, br))) = - let sb = f_subst_init () in - let sb, bh = add_elocals sb cl in - - let sb = - List.fold_left2 - (fun sb (x, xty) (y, _) -> - bind_elocal sb y (e_subst sb (e_local x xty))) - sb cl cr in - - let cop = EcPath.pqoname (EcPath.prefix pl) c in - let copl = f_op cop tyl (toarrow (List.snd cl) fl.inv.f_ty) in - let copr = f_op cop tyr (toarrow (List.snd cr) fr.inv.f_ty) in - let f_ands_simpl' f = f_ands_simpl (List.tl f) (List.hd f) in - let pre = map_ts_inv f_ands_simpl' - [ es_pr es; map_ts_inv1 (fun fl -> f_eq fl (f_app copl (List.map (curry f_local) bh) fl.f_ty)) fl; - map_ts_inv1 (fun fr -> f_eq fr (f_app copr (List.map (curry f_local) bh) fr.f_ty)) fr ] in - - f_forall - (List.map (snd_map gtty) bh) - (f_equivS (snd es.es_ml) (snd es.es_mr) pre - (EcModules.stmt ((s_subst sb bl).s_node @ sl.s_node)) - (EcModules.stmt ((s_subst sb br).s_node @ sr.s_node)) - (es_po es)) - - in - - let infos = - (List.combine dt.EcDecl.tydt_ctors (List.combine bsl bsr)) in - - let concl2 = List.map get_eqv_goal infos in - - FApi.xmutate1 tc `Match ([eqv_cond] @ concl2) +let t_hoare_cond = EcHoareIf.t_hoare_if_head +let t_ehoare_cond = EcEHoareIf.t_ehoare_if_head +let t_bdhoare_cond = EcBdHoareIf.t_bdhoare_if_head +let t_equiv_cond = EcEquivIf.t_equiv_if_head (* -------------------------------------------------------------------- *) -let t_equiv_match infos tc = - match infos with - | `DSided `Eq -> t_equiv_match_eq tc - | `DSided `ConstrSynced -> t_equiv_match_same_constr tc - | `SSided s -> t_equiv_match s tc +let t_hoare_match = EcHoareMatch.t_hoare_match_head +let t_bdhoare_match = EcBdHoareMatch.t_bdhoare_match_head +let t_equiv_match = EcEquivMatch.t_equiv_match_head diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml index cb1995684..b8404b9ed 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/src/phl/ecPhlHiCond.ml @@ -1,47 +1,34 @@ (* -------------------------------------------------------------------- *) -open EcUtils +open EcParsetree +open EcAst + open EcCoreGoal -open EcLowGoal open EcLowPhlGoal -open EcPhlCond -open EcMatching.Position (* -------------------------------------------------------------------- *) -let process_cond (info : EcParsetree.pcond_info) tc = - let default_if (i : codegap1 option) s = - ofdfl (fun _ -> GapBefore (cpos1 (tc1_pos_last_if tc s))) i in - - match info with - | `Head side -> - t_hS_or_bhS_or_eS - ~th:t_hoare_cond - ~teh:t_ehoare_cond - ~tbh:t_bdhoare_cond - ~te:(t_equiv_cond side) tc - - | `Seq (side, (i1, i2), f) -> - let es = tc1_as_equivS tc in - let f = EcProofTyping.tc1_process_prhl_formula tc f in - let i1 = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i1)) i1 in - let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codegap1 tc (side, i2)) i2 in - let n1 = default_if i1 es.es_sl in - let n2 = default_if i2 es.es_sr in - FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f) - [ t_id; t_equiv_cond side ] tc - - | `SeqOne (s, i, f1, f2) -> - let es = tc1_as_equivS tc in - let i = Option.map (fun i1 -> EcLowPhlGoal.tc1_process_codegap1 tc (Some s, i1)) i in - let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in - let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in - let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in - FApi.t_seqsub - (EcPhlSeq.t_equiv_seq_onesided s n f1 f2) - [ t_id; t_bdhoare_cond] tc +(* Dispatch on the goal kind only; each logic owns its surface-syntax + handling and takes the whole parse info. *) +let process_cond (info : pcond_info) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareIf.process_hoare_if info tc + | FeHoareS _ -> EcEHoareIf.process_ehoare_if info tc + | FbdHoareS _ -> EcBdHoareIf.process_bdhoare_if info tc + | FequivS _ -> EcEquivIf.process_equiv_if info tc + | _ -> + let kinds = + match info with + | `Head _ -> + [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] + | `Seq _ | `SeqOne _ -> + [`Equiv `Stmt] in + tc_error_noXhl ~kinds !!tc (* -------------------------------------------------------------------- *) -let process_match infos tc = - t_hS_or_bhS_or_eS - ~th:t_hoare_match - ~tbh:t_bdhoare_match - ~te:(t_equiv_match infos) tc +(* There is no ehoare [match] tactic. *) +let process_match (infos : matchmode) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareMatch.process_hoare_match infos tc + | FbdHoareS _ -> EcBdHoareMatch.process_bdhoare_match infos tc + | FequivS _ -> EcEquivMatch.process_equiv_match infos tc + | _ -> + tc_error_noXhl ~kinds:[`Hoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] !!tc diff --git a/src/phl/rules/bdhoare/ecBdHoareCase.ml b/src/phl/rules/bdhoare/ecBdHoareCase.ml new file mode 100644 index 000000000..dd379f9dd --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareCase.ml @@ -0,0 +1,46 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [case] rule: the case formula, and whether it + is conjoined to the precondition with the simplifying conjunction. + Already typed, nothing to resolve: the same record is the rule argument + and the node payload. *) +type bdhoare_case = { + bca_cond : ss_inv; + bca_simplify : bool; +} + +type EcCoreGoal.rule += RBdHoareCase of bdhoare_case + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let bdhoare_case_subgoals (bhs : bdHoareS) (n : bdhoare_case) : form list = + let fand = if n.bca_simplify then f_and_simpl else f_and in + let f = ss_inv_rebind n.bca_cond (fst bhs.bhs_m) in + let mt = snd bhs.bhs_m in + let concl pre = + f_bdHoareS mt pre bhs.bhs_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in + let a = concl (map_ss_inv2 fand (bhs_pr bhs) f) in + let b = concl (map_ss_inv2 fand (bhs_pr bhs) (map_ss_inv1 f_not f)) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_case (r : bdhoare_case) (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + FApi.xrule1 tc (RBdHoareCase r) (bdhoare_case_subgoals bhs r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareCase n -> + Some (EcPlRecheck.checker_of "bdhoare-case" pf_as_bdhoareS + (fun _hyps bhs -> bdhoare_case_subgoals bhs n)) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoareCase.mli b/src/phl/rules/bdhoare/ecBdHoareCase.mli new file mode 100644 index 000000000..db47549ff --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareCase.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_case = { + bca_cond : ss_inv; (* case formula f *) + bca_simplify : bool; (* conjoin with the simplifying conjunction *) +} + +(* [t_bdhoare_case { bca_cond = f; bca_simplify }] — case analysis on [f], + with [~] the goal's comparison ([<=], [=] or [>=]): + + phoare [c : P /\ f ==> Q] ~ d phoare [c : P /\ !f ==> Q] ~ d + ---------------------------------------------------------------- + phoare [c : P ==> Q] ~ d + + where [/\] is [f_and_simpl] when [bca_simplify], [f_and] otherwise. + + Node: [RBdHoareCase { bca_cond = f; bca_simplify }]. + Checker: "bdhoare-case". *) +val t_bdhoare_case : bdhoare_case -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareIf.ml b/src/phl/rules/bdhoare/ecBdHoareIf.ml new file mode 100644 index 000000000..2da6ad21e --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareIf.ml @@ -0,0 +1,64 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [if] rule has no parameters: the statement is the + conditional. *) +type EcCoreGoal.rule += RBdHoareIf + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is a single conditional) is part of it, so the checker + re-validates it. *) +let bdhoare_if_subgoals (bhs : bdHoareS) : form list = + let e, c1, c2 = + match bhs.bhs_s.s_node with + | [{ i_node = Sif (e, c1, c2) }] -> (e, c1, c2) + | _ -> failwith "bdhoare-if: the statement is not a single conditional" in + let b = ss_inv_of_expr (fst bhs.bhs_m) e in + let mt = snd bhs.bhs_m in + let concl b s = + f_bdHoareS mt (map_ss_inv2 f_and (bhs_pr bhs) b) s + (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in + [concl b c1; concl (map_ss_inv1 f_not b) c2] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_if (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let sg = + try bdhoare_if_subgoals bhs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RBdHoareIf sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareIf -> + Some (EcPlRecheck.checker_of "bdhoare-if" pf_as_bdhoareS + (fun _hyps bhs -> bdhoare_if_subgoals bhs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [if b then c1 else c2; c], push [c] into the + branches (when not empty), then apply the rule. *) +let t_bdhoare_if_head (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let _, c = tc1_first_if tc bhs.bhs_s in + if List.is_empty c.s_node then t_bdhoare_if tc else + FApi.t_seq + (EcBdHoareTransform.t_bdhoare_transform { btr_tr = EcTrIfPush.TrIfPush }) + t_bdhoare_if tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. *) +let process_bdhoare_if (info : pcond_info) (tc : tcenv1) = + match info with + | `Head _ -> t_bdhoare_if_head tc + | `Seq _ | `SeqOne _ -> tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc diff --git a/src/phl/rules/bdhoare/ecBdHoareIf.mli b/src/phl/rules/bdhoare/ecBdHoareIf.mli new file mode 100644 index 000000000..968ea61f1 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareIf.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoare_if] — conditional, with [~] the goal's comparison ([<=], + [=] or [>=]): + + phoare [c1 : P /\ b ==> Q] ~ d phoare [c2 : P /\ !b ==> Q] ~ d + ------------------------------------------------------------------ + phoare [if b then c1 else c2 : P ==> Q] ~ d + + Side condition: the statement is the single conditional (otherwise + fails). + + Node: [RBdHoareIf]. Checker: "bdhoare-if". *) +val t_bdhoare_if : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_if_head] — on [phoare [if b then c1 else c2; c : P ==> Q] ~ d]: + 1. when [c] is not empty, [EcBdHoareTransform.t_bdhoare_transform] + with [EcTrIfPush.TrIfPush], giving + phoare [if b then { c1; c } else { c2; c } : P ==> Q] ~ d; + 2. [t_bdhoare_if]. + Visible goals: phoare [c1; c : P /\ b ==> Q] ~ d and + phoare [c2; c : P /\ !b ==> Q] ~ d. Fails if the first instruction is + not a conditional. Emits no node of its own. *) +val t_bdhoare_if_head : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [if] on a [bdHoareS] goal: applies [t_bdhoare_if_head]. The side, if + any, is ignored (behaviour preserved). The [seq]-ing forms are + rejected: they expect an [equivS] goal. *) +val process_bdhoare_if : pcond_info -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareMatch.ml b/src/phl/rules/bdhoare/ecBdHoareMatch.ml new file mode 100644 index 000000000..21ad442dd --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareMatch.ml @@ -0,0 +1,64 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [match] rule has no parameters: the statement is the + [match]. *) +type EcCoreGoal.rule += RBdHoareMatch + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is a single [match]) is part of it, so the checker + re-validates it. The constructors are read from the environment. *) +let bdhoare_match_subgoals (hyps : LDecl.hyps) (bhs : bdHoareS) : form list = + let e, bs = + match bhs.bhs_s.s_node with + | [{ i_node = Smatch (e, bs) }] -> (e, bs) + | _ -> failwith "bdhoare-match: the statement is not a single match" in + let concl (mb : EcPlMatch.match_branch) = + f_bdHoareS (snd mb.mb_mem) + (map_ss_inv2 f_and mb.mb_cond (bhs_pr bhs)) mb.mb_body + (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in + List.map concl + (EcPlMatch.match_branches (LDecl.toenv hyps) bhs.bhs_m e bs) + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_match (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let sg = + try bdhoare_match_subgoals (FApi.tc1_hyps tc) bhs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RBdHoareMatch sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareMatch -> + Some (EcPlRecheck.checker_of "bdhoare-match" pf_as_bdhoareS + bdhoare_match_subgoals) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [match e with ... end; c], push [c] into the + branches (when not empty), then apply the rule. *) +let t_bdhoare_match_head (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let _, c = tc1_first_match tc bhs.bhs_s in + if List.is_empty c.s_node then t_bdhoare_match tc else + FApi.t_seq + (EcBdHoareTransform.t_bdhoare_transform + { btr_tr = EcTrMatchPush.TrMatchPush }) + t_bdhoare_match tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. *) +let process_bdhoare_match (_ : matchmode) (tc : tcenv1) = + t_bdhoare_match_head tc diff --git a/src/phl/rules/bdhoare/ecBdHoareMatch.mli b/src/phl/rules/bdhoare/ecBdHoareMatch.mli new file mode 100644 index 000000000..6a65da2f9 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareMatch.mli @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoare_match] — pattern matching, with [~] the goal's comparison + ([<=], [=] or [>=]). With [C_1, ..., C_n] the constructors of the type + of [e], one premise per constructor, in declaration order: + + phoare{m + ys_i} [b_i[ys_i/xs_i] : e = C_i ys_i /\ P ==> Q] ~ d + ------------------------------------------------------- (i = 1..n) + phoare{m} [match e with | C_i xs_i => b_i end : P ==> Q] ~ d + + where [ys_i] are fresh program variables, named after the pattern + variables [xs_i] and of the same types, added to the memory [m] (see + [EcPlMatch.match_branches]). Side condition: the statement is the + single [match] (otherwise fails). + + Node: [RBdHoareMatch]. Checker: "bdhoare-match"; it recomputes the + constructors of the type of [e] from the goal's context. *) +val t_bdhoare_match : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_match_head] — on [phoare [match e with | C_i xs_i => b_i + end; c : P ==> Q] ~ d]: + 1. when [c] is not empty, [EcBdHoareTransform.t_bdhoare_transform] + with [EcTrMatchPush.TrMatchPush], giving + phoare [match e with | C_i xs_i => { b_i; c } end : P ==> Q] ~ d; + 2. [t_bdhoare_match]. + Visible goals, one per constructor: + phoare{m + ys_i} [b_i[ys_i/xs_i]; c : e = C_i ys_i /\ P ==> Q] ~ d. + Fails if the first instruction is not a [match]. Emits no node of its + own. *) +val t_bdhoare_match_head : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match] on a [bdHoareS] goal: applies [t_bdhoare_match_head]. The side + or [=], if any, is ignored (behaviour preserved). *) +val process_bdhoare_match : matchmode -> backward diff --git a/src/phl/rules/ecPlMatch.ml b/src/phl/rules/ecPlMatch.ml new file mode 100644 index 000000000..27c08175c --- /dev/null +++ b/src/phl/rules/ecPlMatch.ml @@ -0,0 +1,48 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcModules +open EcTypes +open EcFol + +(* -------------------------------------------------------------------- *) +type match_branch = { + mb_mem : memenv; + mb_cond : ss_inv; + mb_body : stmt; +} + +(* -------------------------------------------------------------------- *) +let match_branches env me e bs = + let typ, tydc, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in + let tyd = oget (EcDecl.tydecl_as_datatype tydc) in + let f = ss_inv_of_expr (fst me) e in + + let branch (cname, _) (cvars, body) = + let cname = EcPath.pqoname (EcPath.prefix typ) cname in + + let mb_mem, pvs = + let ovs = + List.map + (fun (x, xty) -> { ov_name = Some (EcIdent.name x); ov_type = xty; }) + cvars in + EcMemory.bindall_fresh ovs me in + + let subst, pvs = + List.fold_left_map (fun s ((x, xty), ov) -> + let pv = pv_loc (oget ov.ov_name) in + (bind_elocal s x (e_var pv xty), (pv, xty))) + Fsubst.f_subst_id (List.combine cvars pvs) in + + (* NB: the constructor is given the datatype as type, as before the + migration (behaviour preserved). *) + let mb_cond = + let vars = List.map (fun (pv, ty) -> f_pvar pv ty (fst mb_mem)) pvs in + let cop = f_op cname tyinst f.inv.f_ty in + let cop = map_ss_inv ~m:f.m (fun vs -> f_app cop vs f.inv.f_ty) vars in + map_ss_inv2 f_eq f cop in + + { mb_mem; mb_cond; mb_body = s_subst subst body; } + in + + List.map2 branch tyd.tydt_ctors bs diff --git a/src/phl/rules/ecPlMatch.mli b/src/phl/rules/ecPlMatch.mli new file mode 100644 index 000000000..66c6d72e7 --- /dev/null +++ b/src/phl/rules/ecPlMatch.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv + +(* -------------------------------------------------------------------- *) +(* Branches of a [match] instruction, instantiated on fresh program + variables. Shared by the single-sided [match] rules of every logic. *) + +type match_branch = { + mb_mem : memenv; (* memory, extended with the fresh variables ys *) + mb_cond : ss_inv; (* e = C ys, in that memory *) + mb_body : stmt; (* the branch, its pattern variables replaced by ys *) +} + +(* [match_branches env me e bs]: for [match e with | C_i xs_i => b_i end] + in memory [me], one [match_branch] per constructor [C_i] of the type of + [e], in declaration order. Each branch extends [me] with fresh program + variables [ys_i], named after [xs_i] and of the same types (not in [me], + hence not read by the judgement, nor written by [b_i]). *) +val match_branches : + env -> memenv -> expr -> ((EcIdent.t * ty) list * stmt) list + -> match_branch list diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index 6696a3160..ed52d2b69 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -29,11 +29,14 @@ open EcEnv logic's rule states them as premises of its own (see its [.mli]). Current catalogue: [EcTrRndSem] (semantic sampling of a straight-line - suffix), [EcTrRCond] (deciding an [if] / [while]) and [EcTrRMatch] - (deciding a [match], its unframed form). Entries live in - [rules/transforms/], as [EcTr]. The framed form of [match C k] - changes the precondition: it is not a transformation, but a separate - rule of each logic ([EcRMatch]). *) + suffix), [EcTrRCond] (deciding an [if] / [while]), [EcTrRMatch] + (deciding a [match], its unframed form), [EcTrIfPush] and + [EcTrMatchPush] (pushing the continuation of a leading conditional / + [match] into its branches; the [if] and [match] tactics are push + rule + on the conditional alone). Entries live in [rules/transforms/], as + [EcTr]. The framed form of [match C k] changes the precondition: + it is not a transformation, but a separate rule of each logic + ([EcRMatch]). *) (* -------------------------------------------------------------------- *) (* An entry of the catalogue, with its resolved parameters. *) diff --git a/src/phl/rules/ehoare/ecEHoareCase.ml b/src/phl/rules/ehoare/ecEHoareCase.ml new file mode 100644 index 000000000..be16ed771 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareCase.ml @@ -0,0 +1,42 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [case] rule: the case formula. Already typed, + nothing to resolve: the same record is the rule argument and the node + payload. *) +type ehoare_case = { + ehca_cond : ss_inv; +} + +type EcCoreGoal.rule += REHoareCase of ehoare_case + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let ehoare_case_subgoals (hs : eHoareS) (n : ehoare_case) : form list = + let f = ss_inv_rebind n.ehca_cond (fst hs.ehs_m) in + let mt = snd hs.ehs_m in + let pre f = map_ss_inv2 f_interp_ehoare_form f (ehs_pr hs) in + let a = f_eHoareS mt (pre f) hs.ehs_s (ehs_po hs) in + let b = f_eHoareS mt (pre (map_ss_inv1 f_not f)) hs.ehs_s (ehs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_case (r : ehoare_case) (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + FApi.xrule1 tc (REHoareCase r) (ehoare_case_subgoals hs r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareCase n -> + Some (EcPlRecheck.checker_of "ehoare-case" pf_as_ehoareS + (fun _hyps hs -> ehoare_case_subgoals hs n)) + | _ -> None) diff --git a/src/phl/rules/ehoare/ecEHoareCase.mli b/src/phl/rules/ehoare/ecEHoareCase.mli new file mode 100644 index 000000000..0f211df5a --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareCase.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_case = { + ehca_cond : ss_inv; (* case formula f *) +} + +(* [t_ehoare_case { ehca_cond = f }] — case analysis on [f]: + + ehoare [c : (f `|` P) ==> Q] ehoare [c : (!f `|` P) ==> Q] + ---------------------------------------------------------------- + ehoare [c : P ==> Q] + + where [(f `|` P)] is the expectation [P] where [f] holds, [+oo] + elsewhere. + + Node: [REHoareCase { ehca_cond = f }]. Checker: "ehoare-case". *) +val t_ehoare_case : ehoare_case -> backward diff --git a/src/phl/rules/ehoare/ecEHoareIf.ml b/src/phl/rules/ehoare/ecEHoareIf.ml new file mode 100644 index 000000000..0f3ba5871 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareIf.ml @@ -0,0 +1,63 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [if] rule has no parameters: the statement is the + conditional. *) +type EcCoreGoal.rule += REHoareIf + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is a single conditional) is part of it, so the checker + re-validates it. *) +let ehoare_if_subgoals (hs : eHoareS) : form list = + let e, c1, c2 = + match hs.ehs_s.s_node with + | [{ i_node = Sif (e, c1, c2) }] -> (e, c1, c2) + | _ -> failwith "ehoare-if: the statement is not a single conditional" in + let b = ss_inv_of_expr (fst hs.ehs_m) e in + let mt = snd hs.ehs_m in + let pre b = map_ss_inv2 f_interp_ehoare_form b (ehs_pr hs) in + [f_eHoareS mt (pre b) c1 (ehs_po hs); + f_eHoareS mt (pre (map_ss_inv1 f_not b)) c2 (ehs_po hs)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_if (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let sg = + try ehoare_if_subgoals hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REHoareIf sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareIf -> + Some (EcPlRecheck.checker_of "ehoare-if" pf_as_ehoareS + (fun _hyps hs -> ehoare_if_subgoals hs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [if b then c1 else c2; c], push [c] into the + branches (when not empty), then apply the rule. *) +let t_ehoare_if_head (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let _, c = tc1_first_if tc hs.ehs_s in + if List.is_empty c.s_node then t_ehoare_if tc else + FApi.t_seq + (EcEHoareTransform.t_ehoare_transform { ehtr_tr = EcTrIfPush.TrIfPush }) + t_ehoare_if tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS]. *) +let process_ehoare_if (info : pcond_info) (tc : tcenv1) = + match info with + | `Head _ -> t_ehoare_if_head tc + | `Seq _ | `SeqOne _ -> tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc diff --git a/src/phl/rules/ehoare/ecEHoareIf.mli b/src/phl/rules/ehoare/ecEHoareIf.mli new file mode 100644 index 000000000..2e40522fe --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareIf.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoare_if] — conditional: + + ehoare [c1 : (b `|` P) ==> Q] ehoare [c2 : (!b `|` P) ==> Q] + ------------------------------------------------------------------ + ehoare [if b then c1 else c2 : P ==> Q] + + where [(b `|` P)] is the expectation [P] where [b] holds, [+oo] + elsewhere. Side condition: the statement is the single conditional + (otherwise fails). + + Node: [REHoareIf]. Checker: "ehoare-if". *) +val t_ehoare_if : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoare_if_head] — on [ehoare [if b then c1 else c2; c : P ==> Q]]: + 1. when [c] is not empty, [EcEHoareTransform.t_ehoare_transform] with + [EcTrIfPush.TrIfPush], giving + ehoare [if b then { c1; c } else { c2; c } : P ==> Q]; + 2. [t_ehoare_if]. + Visible goals: ehoare [c1; c : (b `|` P) ==> Q] and + ehoare [c2; c : (!b `|` P) ==> Q]. Fails if the first instruction is + not a conditional. Emits no node of its own. *) +val t_ehoare_if_head : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [if] on an [eHoareS] goal: applies [t_ehoare_if_head]. The side, if + any, is ignored (behaviour preserved). The [seq]-ing forms are + rejected: they expect an [equivS] goal. *) +val process_ehoare_if : pcond_info -> backward diff --git a/src/phl/rules/equiv/ecEquivCase.ml b/src/phl/rules/equiv/ecEquivCase.ml new file mode 100644 index 000000000..15d3b9650 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCase.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [case] rule: the case relation, and whether it is + conjoined to the precondition with the simplifying conjunction. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type equiv_case = { + eca_cond : ts_inv; + eca_simplify : bool; +} + +type EcCoreGoal.rule += REquivCase of equiv_case + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let equiv_case_subgoals (es : equivS) (n : equiv_case) : form list = + let fand = if n.eca_simplify then f_and_simpl else f_and in + let f = ts_inv_rebind n.eca_cond (fst es.es_ml) (fst es.es_mr) in + let mtl, mtr = snd es.es_ml, snd es.es_mr in + let concl pre = f_equivS mtl mtr pre es.es_sl es.es_sr (es_po es) in + let a = concl (map_ts_inv2 fand (es_pr es) f) in + let b = concl (map_ts_inv2 fand (es_pr es) (map_ts_inv1 f_not f)) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_case (r : equiv_case) (tc : tcenv1) = + let es = tc1_as_equivS tc in + FApi.xrule1 tc (REquivCase r) (equiv_case_subgoals es r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivCase n -> + Some (EcPlRecheck.checker_of "equiv-case" pf_as_equivS + (fun _hyps es -> equiv_case_subgoals es n)) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivCase.mli b/src/phl/rules/equiv/ecEquivCase.mli new file mode 100644 index 000000000..7e946c42e --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCase.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_case = { + eca_cond : ts_inv; (* case relation f *) + eca_simplify : bool; (* conjoin with the simplifying conjunction *) +} + +(* [t_equiv_case { eca_cond = f; eca_simplify }] — case analysis on [f]: + + equiv [c ~ c' : P /\ f ==> Q] equiv [c ~ c' : P /\ !f ==> Q] + ---------------------------------------------------------------- + equiv [c ~ c' : P ==> Q] + + where [/\] is [f_and_simpl] when [eca_simplify], [f_and] otherwise. + + Node: [REquivCase { eca_cond = f; eca_simplify }]. Checker: "equiv-case". *) +val t_equiv_case : equiv_case -> backward diff --git a/src/phl/rules/equiv/ecEquivIf.ml b/src/phl/rules/equiv/ecEquivIf.ml new file mode 100644 index 000000000..cecc90f5c --- /dev/null +++ b/src/phl/rules/equiv/ecEquivIf.ml @@ -0,0 +1,153 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcModules + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* The two-sided equiv [if] rule has no parameters: the statements are the + conditionals. The one-sided rule is parameterized by its side, nothing + to resolve: the same record is the rule argument and the node + payload. *) +type equiv_if_onesided = { + eio_side : side; +} + +type EcCoreGoal.rule += + | REquivIf + | REquivIfOneSided of equiv_if_onesided + +(* -------------------------------------------------------------------- *) +(* The statement [s], a single conditional. *) +let single_if (who : string) (s : stmt) = + match s.s_node with + | [{ i_node = Sif (e, c1, c2) }] -> (e, c1, c2) + | _ -> failwith (who ^ ": the statement is not a single conditional") + +(* The condition [b] of the conditional of side [side], as a relation. *) +let side_cond (es : equivS) (side : side) (e : expr) : ts_inv = + let ml, mr = fst es.es_ml, fst es.es_mr in + match side with + | `Left -> ss_inv_generalize_right (ss_inv_of_expr ml e) mr + | `Right -> ss_inv_generalize_left (ss_inv_of_expr mr e) ml + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers. Their side + conditions (the statements are single conditionals) are part of them, + so the checkers re-validate them. *) +let equiv_if_subgoals (es : equivS) : form list = + let el, cl1, cl2 = single_if "equiv-if" es.es_sl in + let er, cr1, cr2 = single_if "equiv-if" es.es_sr in + let bl = side_cond es `Left el in + let br = side_cond es `Right er in + let fiff = + EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr + (map_ts_inv2 f_imp (es_pr es) (map_ts_inv2 f_iff bl br)) in + let concl b sl sr = + f_equivS (snd es.es_ml) (snd es.es_mr) + (map_ts_inv2 f_and (es_pr es) b) sl sr (es_po es) in + [fiff; concl bl cl1 cr1; concl (map_ts_inv1 f_not bl) cl2 cr2] + +let equiv_if_onesided_subgoals (es : equivS) (n : equiv_if_onesided) = + let side = n.eio_side in + let e, c1, c2 = + single_if "equiv-if-onesided" (sideif side es.es_sl es.es_sr) in + let b = side_cond es side e in + let concl b s = + let sl, sr = sideif side (s, es.es_sr) (es.es_sl, s) in + f_equivS (snd es.es_ml) (snd es.es_mr) + (map_ts_inv2 f_and (es_pr es) b) sl sr (es_po es) in + [concl b c1; concl (map_ts_inv1 f_not b) c2] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equiv_if (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_if_subgoals es + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REquivIf sg + +let t_equiv_if_onesided (r : equiv_if_onesided) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_if_onesided_subgoals es r + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivIfOneSided r) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivIf -> + Some (EcPlRecheck.checker_of "equiv-if" pf_as_equivS + (fun _hyps es -> equiv_if_subgoals es)) + | REquivIfOneSided n -> + Some (EcPlRecheck.checker_of "equiv-if-onesided" pf_as_equivS + (fun _hyps es -> equiv_if_onesided_subgoals es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): push the continuation of the conditional of + side [side] into its branches, when not empty. *) +let t_equiv_if_push (side : side) (c : stmt) = + if List.is_empty c.s_node then t_id else + EcEquivTransform.t_equiv_transform + { etr_side = side; etr_tr = EcTrIfPush.TrIfPush } + +(* Derived (no proof-node): on [if b then c1 else c2; c] (on one side, or + on both sides), push the continuations into the branches, then apply + the one-sided (resp. two-sided) rule. *) +let t_equiv_if_head (side : oside) (tc : tcenv1) = + let es = tc1_as_equivS tc in + match side with + | Some side -> + let _, c = tc1_first_if tc (sideif side es.es_sl es.es_sr) in + FApi.t_seq + (t_equiv_if_push side c) + (t_equiv_if_onesided { eio_side = side }) tc + + | None -> + let _, cl = tc1_first_if tc es.es_sl in + let _, cr = tc1_first_if tc es.es_sr in + FApi.t_seqs + [t_equiv_if_push `Left cl; t_equiv_if_push `Right cr; t_equiv_if] tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. *) +let process_equiv_if (info : pcond_info) (tc : tcenv1) = + (* By default, split before the last top-level conditional. *) + let default_if (i : EcMatching.Position.codegap1 option) s = + ofdfl (fun _ -> + EcMatching.Position.(GapBefore (cpos1 (tc1_pos_last_if tc s)))) i in + + match info with + | `Head side -> t_equiv_if_head side tc + + | `Seq (side, (i1, i2), f) -> + let es = tc1_as_equivS tc in + let f = TTC.tc1_process_prhl_formula tc f in + let i1 = Option.map (fun i1 -> tc1_process_codegap1 tc (side, i1)) i1 in + let i2 = Option.map (fun i2 -> tc1_process_codegap1 tc (side, i2)) i2 in + let n1 = default_if i1 es.es_sl in + let n2 = default_if i2 es.es_sr in + FApi.t_seqsub + (EcEquivSeq.t_equiv_seq { esr_at = (n1, n2); esr_mid = f }) + [t_id; t_equiv_if_head side] tc + + | `SeqOne (s, i, f1, f2) -> + let es = tc1_as_equivS tc in + let i = Option.map (fun i -> tc1_process_codegap1 tc (Some s, i)) i in + let n = default_if i (sideif s es.es_sl es.es_sr) in + let _, f1 = TTC.tc1_process_Xhl_formula ~side:s tc f1 in + let _, f2 = TTC.tc1_process_Xhl_formula ~side:s tc f2 in + FApi.t_seqsub + (EcEquivSeq.t_equiv_seq_onesided s n f1 f2) + [t_id; EcBdHoareIf.t_bdhoare_if_head] tc diff --git a/src/phl/rules/equiv/ecEquivIf.mli b/src/phl/rules/equiv/ecEquivIf.mli new file mode 100644 index 000000000..5650814b5 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivIf.mli @@ -0,0 +1,78 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equiv_if] — synchronized conditionals: + + forall &1 &2, P => (b<1> <=> b'<2>) + equiv [c1 ~ c1' : P /\ b<1> ==> Q] + equiv [c2 ~ c2' : P /\ !b<1> ==> Q] + --------------------------------------------------------------- + equiv [if b then c1 else c2 ~ if b' then c1' else c2' : P ==> Q] + + Side condition: each statement is a single conditional (otherwise + fails). + + Node: [REquivIf]. Checker: "equiv-if". *) +val t_equiv_if : backward + +type equiv_if_onesided = { + eio_side : side; (* side of the conditional *) +} + +(* [t_equiv_if_onesided { eio_side = `Left }] — one-sided conditional: + + equiv [c1 ~ c' : P /\ b<1> ==> Q] + equiv [c2 ~ c' : P /\ !b<1> ==> Q] + ----------------------------------------- + equiv [if b then c1 else c2 ~ c' : P ==> Q] + + (symmetrically for [`Right]). Side condition: the statement of that + side is a single conditional (otherwise fails). + + Node: [REquivIfOneSided { eio_side }]. Checker: "equiv-if-onesided". *) +val t_equiv_if_onesided : equiv_if_onesided -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_if_head side]: + - [side = Some `Left], on [equiv [if b then c1 else c2; c ~ c' : P ==> Q]] + (symmetrically for [`Right]): + 1. when [c] is not empty, [EcEquivTransform.t_equiv_transform] on that + side with [EcTrIfPush.TrIfPush], giving + equiv [if b then { c1; c } else { c2; c } ~ c' : P ==> Q]; + 2. [t_equiv_if_onesided]. + Visible goals: equiv [c1; c ~ c' : P /\ b<1> ==> Q] and + equiv [c2; c ~ c' : P /\ !b<1> ==> Q]. + - [side = None], on [equiv [if b then c1 else c2; c ~ + if b' then c1' else c2'; c' : P ==> Q]]: + 1. the push of step 1 above on the left (when [c] is not empty), then + on the right (when [c'] is not empty); + 2. [t_equiv_if]. + Visible goals: forall &1 &2, P => (b<1> <=> b'<2>), then + equiv [c1; c ~ c1'; c' : P /\ b<1> ==> Q] and + equiv [c2; c ~ c2'; c' : P /\ !b<1> ==> Q]. + Fails if the first instruction of a side is not a conditional (left + checked first). Emits no node of its own. *) +val t_equiv_if_head : oside -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* On an [equivS] goal: + - [if] / [if{i}]: applies [t_equiv_if_head]; + - [if{i}? k k' : R] (and [if := R], i.e. [if _ _ : R]): [t_equiv_seq] + before the conditionals at [(k, k')] (by default, the last top-level + conditional of each side) with the relation [R], then + [t_equiv_if_head] on the second premise; visible goals: the first + premise of [seq], then those of [t_equiv_if_head]; + - [if{i} k? : (_ : P ==> Q)]: [t_equiv_seq_onesided] on side [i] before + the conditional at [k] (by default, the last top-level one) with + [P] / [Q], then [EcBdHoareIf.t_bdhoare_if_head] on its [phoare] + premise; visible goals: the [equiv] premise of the one-sided [seq], + then those of [t_bdhoare_if_head]. *) +val process_equiv_if : pcond_info -> backward diff --git a/src/phl/rules/equiv/ecEquivMatch.ml b/src/phl/rules/equiv/ecEquivMatch.ml new file mode 100644 index 000000000..c3c3c5ba2 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivMatch.ml @@ -0,0 +1,261 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcModules +open EcEnv + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The one-sided equiv [match] rule is parameterized by its side, nothing + to resolve: the same record is the rule argument and the node payload. + The two-sided rules have no parameters: the statements are the + [match]es. *) +type equiv_match_onesided = { + emo_side : side; +} + +type EcCoreGoal.rule += + | REquivMatchOneSided of equiv_match_onesided + | REquivMatchSynced + | REquivMatchEq + +(* -------------------------------------------------------------------- *) +(* The statement [s], a single [match]. *) +let single_match (who : string) (s : stmt) = + match s.s_node with + | [{ i_node = Smatch (e, bs) }] -> (e, bs) + | _ -> failwith (who ^ ": the statement is not a single match") + +(* -------------------------------------------------------------------- *) +(* Pure core of the one-sided rule, shared by the rule and its checker. Its + side condition (the statement of that side is a single [match]) is part + of it, so the checker re-validates it. The constructors are read from + the environment. *) +let equiv_match_onesided_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_match_onesided) += + let side = n.emo_side in + let m, mo = sideif side (es.es_ml, es.es_mr) (es.es_mr, es.es_ml) in + let e, bs = + single_match "equiv-match-onesided" (sideif side es.es_sl es.es_sr) in + let generalize_other inv = + sideif side + (ss_inv_generalize_right inv (fst mo)) + (ss_inv_generalize_left inv (fst mo)) in + + let concl (mb : EcPlMatch.match_branch) = + let cond = generalize_other mb.mb_cond in + let (ml, mr), (sl, sr) = + sideif side + ((mb.mb_mem, es.es_mr), (mb.mb_body, es.es_sr)) + ((es.es_ml, mb.mb_mem), (es.es_sl, mb.mb_body)) in + f_equivS (snd ml) (snd mr) (map_ts_inv2 f_and cond (es_pr es)) + sl sr (es_po es) in + + List.map concl (EcPlMatch.match_branches (LDecl.toenv hyps) m e bs) + +(* -------------------------------------------------------------------- *) +(* The two-sided rules: the [match]es of both sides, and the datatype + (path, declaration, type instance of each side) they are on. *) +let single_matches (who : string) (env : env) (es : equivS) = + let el, bsl = single_match who es.es_sl in + let er, bsr = single_match who es.es_sr in + let pl, dt, tyl = oget (EcEnv.Ty.get_top_decl el.e_ty env) in + let pr, _ , tyr = oget (EcEnv.Ty.get_top_decl er.e_ty env) in + if not (EcPath.p_equal pl pr) then + failwith (who ^ ": matches on different inductive types"); + let dt = oget (EcDecl.tydecl_as_datatype dt) in + ((el, bsl), (er, bsr)), (pl, dt, tyl, tyr) + +(* The constructor [c] of the datatype [p], at type instance [tys], with + arguments of types [atys] and result type [rty]. *) +let f_ctor (p : EcPath.path) (tys : ty list) c (atys : ty list) (rty : ty) = + f_op (EcPath.pqoname (EcPath.prefix p) c) tys (toarrow atys rty) + +(* [f = cop xs]. *) +let f_eq_app (cop : form) (xs : (EcIdent.t * ty) list) (f : ts_inv) = + map_ts_inv1 + (fun f -> f_eq f (f_app cop (List.map (curry f_local) xs) f.f_ty)) f + +(* The precondition of a branch premise: [eql /\ eqr /\ P], simplifying. *) +let branch_pre (es : equivS) (eql : ts_inv) (eqr : ts_inv) = + map_ts_inv3 (fun p l r -> f_ands_simpl [l; r] p) (es_pr es) eql eqr + +(* Pure core of the synchronized rule, shared by the rule and its checker. + Its side conditions are part of it. The logical variables bound in the + premises are fresh at each call: the checker compares up to + alpha-conversion. *) +let equiv_match_synced_subgoals (hyps : LDecl.hyps) (es : equivS) = + let env = LDecl.toenv hyps in + let ml, mr = fst es.es_ml, fst es.es_mr in + let ((el, bsl), (er, bsr)), (p, dt, tyl, tyr) = + single_matches "equiv-match-synced" env es in + + let fl = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in + let fr = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in + + let copl c cl = f_ctor p tyl c (List.snd cl) fl.inv.f_ty in + let copr c cr = f_ctor p tyr c (List.snd cr) fr.inv.f_ty in + + (* forall &1 &2, P => ((exists xs, el = C xs) <=> (exists xs', er = C xs')) *) + let cond ((c, _), ((cl, _), (cr, _))) = + let xl = List.map (fst_map EcIdent.fresh) cl in + let xr = List.map (fst_map EcIdent.fresh) cr in + let ex xs = map_ts_inv1 (f_exists (List.map (snd_map gtty) xs)) in + let lhs = ex xl (f_eq_app (copl c cl) xl fl) in + let rhs = ex xr (f_eq_app (copr c cr) xr fr) in + EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr + (map_ts_inv2 f_imp_simpl (es_pr es) (map_ts_inv2 f_iff lhs rhs)) in + + (* forall xs xs', + equiv [bl ~ br : el = C xs /\ er = C xs' /\ P ==> Q] + (simplifying conjunction) *) + let goal ((c, _), ((cl, bl), (cr, br))) = + let sb = Fsubst.f_subst_id in + let sb, xl = add_elocals sb cl in + let sb, xr = add_elocals sb cr in + let pre = + branch_pre es (f_eq_app (copl c cl) xl fl) (f_eq_app (copr c cr) xr fr) in + f_forall (List.map (snd_map gtty) (xl @ xr)) + (f_equivS (snd es.es_ml) (snd es.es_mr) pre + (s_subst sb bl) (s_subst sb br) (es_po es)) in + + let infos = List.combine dt.EcDecl.tydt_ctors (List.combine bsl bsr) in + + List.map cond infos @ List.map goal infos + +(* Pure core of the rule on equal values, shared by the rule and its + checker. Its side conditions are part of it. The logical variables bound + in the premises are fresh at each call: the checker compares up to + alpha-conversion. *) +let equiv_match_eq_subgoals (hyps : LDecl.hyps) (es : equivS) = + let env = LDecl.toenv hyps in + let ml, mr = fst es.es_ml, fst es.es_mr in + let ((el, bsl), (er, bsr)), (p, dt, tyl, tyr) = + single_matches "equiv-match-eq" env es in + + if not (EcReduction.EqTest.for_type env el.e_ty er.e_ty) then + failwith "equiv-match-eq: matches on different types"; + + let fl = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in + let fr = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in + + (* forall &1 &2, P => el = er *) + let cond = + EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr + (map_ts_inv2 f_imp_simpl (es_pr es) (map_ts_inv2 f_eq fl fr)) in + + (* forall xs, + equiv [bl ~ br[xs/xs'] : el = C xs /\ er = C xs /\ P ==> Q] + (simplifying conjunction) *) + let goal ((c, _), ((cl, bl), (cr, br))) = + let sb = f_subst_init () in + let sb, xs = add_elocals sb cl in + let sb = + List.fold_left2 + (fun sb (x, xty) (y, _) -> + bind_elocal sb y (e_subst sb (e_local x xty))) + sb cl cr in + let copl = f_ctor p tyl c (List.snd cl) fl.inv.f_ty in + let copr = f_ctor p tyr c (List.snd cr) fr.inv.f_ty in + let pre = branch_pre es (f_eq_app copl xs fl) (f_eq_app copr xs fr) in + f_forall (List.map (snd_map gtty) xs) + (f_equivS (snd es.es_ml) (snd es.es_mr) pre + (s_subst sb bl) (s_subst sb br) (es_po es)) in + + let infos = List.combine dt.EcDecl.tydt_ctors (List.combine bsl bsr) in + + cond :: List.map goal infos + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equiv_match_onesided (r : equiv_match_onesided) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_match_onesided_subgoals (FApi.tc1_hyps tc) es r + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivMatchOneSided r) sg + +let t_equiv_match_synced (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_match_synced_subgoals (FApi.tc1_hyps tc) es + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REquivMatchSynced sg + +let t_equiv_match_eq (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_match_eq_subgoals (FApi.tc1_hyps tc) es + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REquivMatchEq sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivMatchOneSided n -> + Some (EcPlRecheck.checker_of "equiv-match-onesided" pf_as_equivS + (fun hyps es -> equiv_match_onesided_subgoals hyps es n)) + | REquivMatchSynced -> + Some (EcPlRecheck.checker_of "equiv-match-synced" pf_as_equivS + equiv_match_synced_subgoals) + | REquivMatchEq -> + Some (EcPlRecheck.checker_of "equiv-match-eq" pf_as_equivS + equiv_match_eq_subgoals) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): push the continuation of the [match] of side + [side] into its branches, when not empty. *) +let t_equiv_match_push (side : side) (c : stmt) = + if List.is_empty c.s_node then t_id else + EcEquivTransform.t_equiv_transform + { etr_side = side; etr_tr = EcTrMatchPush.TrMatchPush } + +(* The user-facing checks of the two-sided forms: both sides start with a + [match], on the same datatype (and, for [eq], on the same type). They + return the continuations. *) +let tc1_first_matches ~(eq : bool) (tc : tcenv1) (es : equivS) = + let env = FApi.tc1_env tc in + let (el, _), cl = tc1_first_match tc es.es_sl in + let (er, _), cr = tc1_first_match tc es.es_sr in + let pl, _, _ = oget (EcEnv.Ty.get_top_decl el.e_ty env) in + let pr, _, _ = oget (EcEnv.Ty.get_top_decl er.e_ty env) in + if not (EcPath.p_equal pl pr) then + tc_error !!tc "match statements on different inductive types"; + if eq && not (EcReduction.EqTest.for_type env el.e_ty er.e_ty) then + tc_error !!tc "synced match requires matches on the same type"; + (cl, cr) + +(* Derived (no proof-node): on [match e with ... end; c] (on one side, or + on both sides), push the continuations into the branches, then apply + the one-sided (resp. the synchronized, or on equal values) rule. *) +let t_equiv_match_head (mode : matchmode) (tc : tcenv1) = + let es = tc1_as_equivS tc in + match mode with + | `SSided side -> + let _, c = tc1_first_match tc (sideif side es.es_sl es.es_sr) in + FApi.t_seq + (t_equiv_match_push side c) + (t_equiv_match_onesided { emo_side = side }) tc + + | `DSided dmode -> + let cl, cr = tc1_first_matches ~eq:(dmode = `Eq) tc es in + let rule = + match dmode with + | `ConstrSynced -> t_equiv_match_synced + | `Eq -> t_equiv_match_eq in + FApi.t_seqs + [t_equiv_match_push `Left cl; t_equiv_match_push `Right cr; rule] tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. *) +let process_equiv_match (mode : matchmode) (tc : tcenv1) = + t_equiv_match_head mode tc diff --git a/src/phl/rules/equiv/ecEquivMatch.mli b/src/phl/rules/equiv/ecEquivMatch.mli new file mode 100644 index 000000000..313a00596 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivMatch.mli @@ -0,0 +1,101 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* Below, [M] is [match e with | C_i xs_i => b_i end] and [M'] is + [match e' with | C_i xs_i' => b_i' end], where [C_1, ..., C_n] are the + constructors of the datatype of [e] (and [e']), in declaration order. *) + +type equiv_match_onesided = { + emo_side : side; (* side of the [match] *) +} + +(* [t_equiv_match_onesided { emo_side = `Left }] — one-sided pattern + matching; one premise per constructor: + + equiv{&1 + ys_i} [b_i[ys_i/xs_i] ~ c' : e<1> = C_i ys_i<1> /\ P ==> Q] + --------------------------------------------------------- (i = 1..n) + equiv [M ~ c' : P ==> Q] + + (symmetrically for [`Right]), where [ys_i] are fresh program variables, + named after the pattern variables [xs_i] and of the same types, added + to the memory of that side (see [EcPlMatch.match_branches]). Side + condition: the statement of that side is the single [match] (otherwise + fails). + + Node: [REquivMatchOneSided { emo_side }]. + Checker: "equiv-match-onesided"; it recomputes the constructors from the + goal's context. *) +val t_equiv_match_onesided : equiv_match_onesided -> backward + +(* [t_equiv_match_synced] — synchronized pattern matching on the same + datatype (possibly at different type instances): + + (Ci) forall &1 &2, P => + ((exists xs, e<1> = C_i xs) <=> (exists xs', e'<2> = C_i xs')) + (Bi) forall xs_i xs_i', equiv [b_i ~ b_i' : + e<1> = C_i xs_i /\ e'<2> = C_i xs_i' /\ P ==> Q] + ------------------------------------------------------------- (i = 1..n) + equiv [M ~ M' : P ==> Q] + + where the pattern variables become universally quantified logical + variables, and [=>] in (Ci) and [/\] in (Bi) are simplifying. Premises, + in order: (C1)..(Cn), then (B1)..(Bn). Side conditions: each statement + is a single [match], both on the same datatype (otherwise fails). + + Node: [REquivMatchSynced]. Checker: "equiv-match-synced"; it recomputes + the datatype and its constructors from the goal's context. *) +val t_equiv_match_synced : backward + +(* [t_equiv_match_eq] — pattern matching on equal values: + + (C) forall &1 &2, P => e<1> = e'<2> + (Bi) forall xs_i, equiv [b_i ~ b_i'[xs_i/xs_i'] : + e<1> = C_i xs_i /\ e'<2> = C_i xs_i /\ P ==> Q] + ------------------------------------------------------------- (i = 1..n) + equiv [M ~ M' : P ==> Q] + + where the pattern variables become universally quantified logical + variables, and [=>] in (C) and [/\] in (Bi) are simplifying. Premises, + in order: (C), then (B1)..(Bn). Side conditions: each statement is a + single [match], both on the same type (otherwise fails). + + Node: [REquivMatchEq]. Checker: "equiv-match-eq"; it recomputes the + datatype and its constructors from the goal's context. *) +val t_equiv_match_eq : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_match_head mode]: + - [mode = `SSided `Left], on [equiv [M; c ~ c' : P ==> Q]] + (symmetrically for [`Right]): + 1. when [c] is not empty, [EcEquivTransform.t_equiv_transform] on that + side with [EcTrMatchPush.TrMatchPush], giving + equiv [match e with | C_i xs_i => { b_i; c } end ~ c' : P ==> Q]; + 2. [t_equiv_match_onesided]. + Visible goals, one per constructor: + equiv{&1 + ys_i} [b_i[ys_i/xs_i]; c ~ c' : + e<1> = C_i ys_i<1> /\ P ==> Q]. + - [mode = `DSided `ConstrSynced] (resp. [`DSided `Eq]), on + [equiv [M; c ~ M'; c' : P ==> Q]]: + 1. the push of step 1 above on the left (when [c] is not empty), then + on the right (when [c'] is not empty); + 2. [t_equiv_match_synced] (resp. [t_equiv_match_eq]). + Visible goals: those of the rule, the branches followed by [c] (resp. + [c']). + Fails if the first instruction of a side is not a [match] (left checked + first) and, for the two-sided forms, with "match statements on + different inductive types" or, for [`Eq], "synced match requires + matches on the same type". Emits no node of its own. *) +val t_equiv_match_head : matchmode -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* On an [equivS] goal: [match{i}], [match] and [match =] apply + [t_equiv_match_head] with the corresponding mode. *) +val process_equiv_match : matchmode -> backward diff --git a/src/phl/rules/hoare/ecHoareCase.ml b/src/phl/rules/hoare/ecHoareCase.ml new file mode 100644 index 000000000..e987f725b --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCase.ml @@ -0,0 +1,46 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [case] rule: the case formula, and whether it is + conjoined to the precondition with the simplifying conjunction. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type hoare_case = { + hca_cond : ss_inv; + hca_simplify : bool; +} + +type EcCoreGoal.rule += RHoareCase of hoare_case + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let hoare_case_subgoals (hs : sHoareS) (n : hoare_case) : form list = + let fand = if n.hca_simplify then f_and_simpl else f_and in + let f = ss_inv_rebind n.hca_cond (fst hs.hs_m) in + let mt = snd hs.hs_m in + let a = f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs) in + let b = f_hoareS mt + (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f)) + hs.hs_s (hs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_case (r : hoare_case) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + FApi.xrule1 tc (RHoareCase r) (hoare_case_subgoals hs r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareCase n -> + Some (EcPlRecheck.checker_of "hoare-case" pf_as_hoareS + (fun _hyps hs -> hoare_case_subgoals hs n)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareCase.mli b/src/phl/rules/hoare/ecHoareCase.mli new file mode 100644 index 000000000..fe416f3ae --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCase.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_case = { + hca_cond : ss_inv; (* case formula f *) + hca_simplify : bool; (* conjoin with the simplifying conjunction *) +} + +(* [t_hoare_case { hca_cond = f; hca_simplify }] — case analysis on [f]: + + hoare [c : P /\ f ==> Q | Q_e] hoare [c : P /\ !f ==> Q | Q_e] + -------------------------------------------------------------------- + hoare [c : P ==> Q | Q_e] + + where [/\] is [f_and_simpl] when [hca_simplify], [f_and] otherwise. + + Node: [RHoareCase { hca_cond = f; hca_simplify }]. Checker: "hoare-case". *) +val t_hoare_case : hoare_case -> backward diff --git a/src/phl/rules/hoare/ecHoareIf.ml b/src/phl/rules/hoare/ecHoareIf.ml new file mode 100644 index 000000000..a7317ff3e --- /dev/null +++ b/src/phl/rules/hoare/ecHoareIf.ml @@ -0,0 +1,63 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [if] rule has no parameters: the statement is the + conditional. *) +type EcCoreGoal.rule += RHoareIf + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is a single conditional) is part of it, so the checker + re-validates it. *) +let hoare_if_subgoals (hs : sHoareS) : form list = + let e, c1, c2 = + match hs.hs_s.s_node with + | [{ i_node = Sif (e, c1, c2) }] -> (e, c1, c2) + | _ -> failwith "hoare-if: the statement is not a single conditional" in + let b = ss_inv_of_expr (fst hs.hs_m) e in + let mt = snd hs.hs_m in + let pre = map_ss_inv2 f_and (hs_pr hs) in + [f_hoareS mt (pre b) c1 (hs_po hs); + f_hoareS mt (pre (map_ss_inv1 f_not b)) c2 (hs_po hs)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_if (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_if_subgoals hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RHoareIf sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareIf -> + Some (EcPlRecheck.checker_of "hoare-if" pf_as_hoareS + (fun _hyps hs -> hoare_if_subgoals hs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [if b then c1 else c2; c], push [c] into the + branches (when not empty), then apply the rule. *) +let t_hoare_if_head (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let _, c = tc1_first_if tc hs.hs_s in + if List.is_empty c.s_node then t_hoare_if tc else + FApi.t_seq + (EcHoareTransform.t_hoare_transform { htr_tr = EcTrIfPush.TrIfPush }) + t_hoare_if tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. *) +let process_hoare_if (info : pcond_info) (tc : tcenv1) = + match info with + | `Head _ -> t_hoare_if_head tc + | `Seq _ | `SeqOne _ -> tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc diff --git a/src/phl/rules/hoare/ecHoareIf.mli b/src/phl/rules/hoare/ecHoareIf.mli new file mode 100644 index 000000000..b95c089c4 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareIf.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_if] — conditional: + + hoare [c1 : P /\ b ==> Q | E] hoare [c2 : P /\ !b ==> Q | E] + -------------------------------------------------------------------- + hoare [if b then c1 else c2 : P ==> Q | E] + + Side condition: the statement is the single conditional (otherwise + fails). + + Node: [RHoareIf]. Checker: "hoare-if". *) +val t_hoare_if : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_if_head] — on [hoare [if b then c1 else c2; c : P ==> Q | E]]: + 1. when [c] is not empty, [EcHoareTransform.t_hoare_transform] with + [EcTrIfPush.TrIfPush], giving + hoare [if b then { c1; c } else { c2; c } : P ==> Q | E]; + 2. [t_hoare_if]. + Visible goals: hoare [c1; c : P /\ b ==> Q | E] and + hoare [c2; c : P /\ !b ==> Q | E]. Fails if the first instruction is + not a conditional. Emits no node of its own. *) +val t_hoare_if_head : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [if] on a [hoareS] goal: applies [t_hoare_if_head]. The side, if any, + is ignored (behaviour preserved). The [seq]-ing forms ([if _ _ : R], + [if := R], [if{i} : (_ : P ==> Q)]) are rejected: they expect an + [equivS] goal. *) +val process_hoare_if : pcond_info -> backward diff --git a/src/phl/rules/hoare/ecHoareMatch.ml b/src/phl/rules/hoare/ecHoareMatch.ml new file mode 100644 index 000000000..2b7947632 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareMatch.ml @@ -0,0 +1,63 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [match] rule has no parameters: the statement is the + [match]. *) +type EcCoreGoal.rule += RHoareMatch + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is a single [match]) is part of it, so the checker + re-validates it. The constructors are read from the environment. *) +let hoare_match_subgoals (hyps : LDecl.hyps) (hs : sHoareS) : form list = + let e, bs = + match hs.hs_s.s_node with + | [{ i_node = Smatch (e, bs) }] -> (e, bs) + | _ -> failwith "hoare-match: the statement is not a single match" in + let concl (mb : EcPlMatch.match_branch) = + f_hoareS (snd mb.mb_mem) + (map_ss_inv2 f_and mb.mb_cond (hs_pr hs)) mb.mb_body (hs_po hs) in + List.map concl + (EcPlMatch.match_branches (LDecl.toenv hyps) hs.hs_m e bs) + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_match (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_match_subgoals (FApi.tc1_hyps tc) hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RHoareMatch sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareMatch -> + Some (EcPlRecheck.checker_of "hoare-match" pf_as_hoareS + hoare_match_subgoals) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [match e with ... end; c], push [c] into the + branches (when not empty), then apply the rule. *) +let t_hoare_match_head (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let _, c = tc1_first_match tc hs.hs_s in + if List.is_empty c.s_node then t_hoare_match tc else + FApi.t_seq + (EcHoareTransform.t_hoare_transform + { htr_tr = EcTrMatchPush.TrMatchPush }) + t_hoare_match tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. *) +let process_hoare_match (_ : matchmode) (tc : tcenv1) = + t_hoare_match_head tc diff --git a/src/phl/rules/hoare/ecHoareMatch.mli b/src/phl/rules/hoare/ecHoareMatch.mli new file mode 100644 index 000000000..637346cbf --- /dev/null +++ b/src/phl/rules/hoare/ecHoareMatch.mli @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_match] — pattern matching. With [C_1, ..., C_n] the + constructors of the type of [e], one premise per constructor, in + declaration order: + + hoare{m + ys_i} [b_i[ys_i/xs_i] : e = C_i ys_i /\ P ==> Q | E] + ------------------------------------------------------ (i = 1..n) + hoare{m} [match e with | C_i xs_i => b_i end : P ==> Q | E] + + where [ys_i] are fresh program variables, named after the pattern + variables [xs_i] and of the same types, added to the memory [m] (see + [EcPlMatch.match_branches]). Side condition: the statement is the + single [match] (otherwise fails). + + Node: [RHoareMatch]. Checker: "hoare-match"; it recomputes the + constructors of the type of [e] from the goal's context. *) +val t_hoare_match : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_match_head] — on [hoare [match e with | C_i xs_i => b_i end; + c : P ==> Q | E]]: + 1. when [c] is not empty, [EcHoareTransform.t_hoare_transform] with + [EcTrMatchPush.TrMatchPush], giving + hoare [match e with | C_i xs_i => { b_i; c } end : P ==> Q | E]; + 2. [t_hoare_match]. + Visible goals, one per constructor: + hoare{m + ys_i} [b_i[ys_i/xs_i]; c : e = C_i ys_i /\ P ==> Q | E]. + Fails if the first instruction is not a [match]. Emits no node of its + own. *) +val t_hoare_match_head : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match] on a [hoareS] goal: applies [t_hoare_match_head]. The side or + [=], if any, is ignored (behaviour preserved). *) +val process_hoare_match : matchmode -> backward diff --git a/src/phl/rules/transforms/ecTrIfPush.ml b/src/phl/rules/transforms/ecTrIfPush.ml new file mode 100644 index 000000000..886563be9 --- /dev/null +++ b/src/phl/rules/transforms/ecTrIfPush.ml @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) +open EcModules +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* The [if-push] transformation has no parameters: it acts on the first + instruction of the statement. *) +type EcPlTransform.transform += TrIfPush + +(* -------------------------------------------------------------------- *) +(* Push the continuation [c] of the leading conditional into both of its + branches. *) +let if_push (ctxt : tr_ctxt) (s : stmt) = + match s.s_node with + | { i_node = Sif (e, c1, c2) } :: c -> + let c = stmt c in + { trr_me = ctxt.trc_me; + trr_s = stmt [i_if (e, s_seq c1 c, s_seq c2 c)]; + trr_obl = []; } + + | _ -> + raise (InvalidTransform "the first instruction is not a conditional") + +let () = + register (function + | TrIfPush -> Some if_push + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrIfPush.mli b/src/phl/rules/transforms/ecTrIfPush.mli new file mode 100644 index 000000000..a183b5138 --- /dev/null +++ b/src/phl/rules/transforms/ecTrIfPush.mli @@ -0,0 +1,14 @@ +(* -------------------------------------------------------------------- *) + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +(* [TrIfPush] — push the continuation of a conditional into its branches: + + c = if b then c1 else c2; c0 ~~> c' = if b then { c1; c0 } + else { c2; c0 } + + The conditional is the first instruction of [c], and [c'] is a single + instruction. No parameter, no obligation, the memory is unchanged. + Fails with "the first instruction is not a conditional" otherwise. *) +type EcPlTransform.transform += TrIfPush diff --git a/src/phl/rules/transforms/ecTrMatchPush.ml b/src/phl/rules/transforms/ecTrMatchPush.ml new file mode 100644 index 000000000..8098eab17 --- /dev/null +++ b/src/phl/rules/transforms/ecTrMatchPush.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcModules +open EcFol +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* The [match-push] transformation has no parameters: it acts on the first + instruction of the statement. *) +type EcPlTransform.transform += TrMatchPush + +(* -------------------------------------------------------------------- *) +(* Push the continuation [c] of the leading [match] into each of its + branches. The pattern variables of a branch are local identifiers bound + in its body; [c] lies outside of their scope, so a branch whose pattern + variables occur free in [c] is first renamed apart (fresh identifiers), + so that [c] is not captured. *) +let match_push (ctxt : tr_ctxt) (s : stmt) = + match s.s_node with + | { i_node = Smatch (e, bs) } :: c -> + let c = stmt c in + let fv = s_fv c in + + let push ((xs, b) : (EcIdent.t * ty) list * stmt) = + if List.exists (fun (x, _) -> EcIdent.Mid.mem x fv) xs then + let xs' = List.map (fst_map EcIdent.fresh) xs in + let sb = + List.fold_left2 + (fun sb (x, _) (x', ty) -> bind_elocal sb x (e_local x' ty)) + Fsubst.f_subst_id xs xs' in + (xs', s_seq (s_subst sb b) c) + else (xs, s_seq b c) in + + { trr_me = ctxt.trc_me; + trr_s = stmt [i_match (e, List.map push bs)]; + trr_obl = []; } + + | _ -> + raise (InvalidTransform "the first instruction is not a match") + +let () = + register (function + | TrMatchPush -> Some match_push + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrMatchPush.mli b/src/phl/rules/transforms/ecTrMatchPush.mli new file mode 100644 index 000000000..697436247 --- /dev/null +++ b/src/phl/rules/transforms/ecTrMatchPush.mli @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +(* [TrMatchPush] — push the continuation of a [match] into its branches: + + c = match e with | C_i xs_i => b_i end; c0 + ~~> + c' = match e with | C_i xs_i' => { b_i[xs_i'/xs_i]; c0 } end + + The [match] is the first instruction of [c], and [c'] is a single + instruction. No parameter, no obligation, the memory is unchanged. + Fails with "the first instruction is not a match" otherwise. + + Capture: the pattern variables [xs_i] are local identifiers (not + program variables) bound in [b_i] only, while [c0] is outside of their + scope and may mention local identifiers free (e.g. the logical + variables introduced by a two-sided [match]). Moving [c0] under the + binders [xs_i] would capture such an occurrence. The entry therefore + renames the binders of a branch to fresh identifiers [xs_i'] when one of + them occurs free in [c0] (and keeps them, [xs_i' = xs_i], otherwise), so + that [c0] keeps its meaning in every branch: each run of [c'] executes + the branch selected by the value of [e], with the same bindings, then + [c0], as [c] does. Program variables read or written by [c0] (even when + named like a pattern variable) are not affected. *) +type EcPlTransform.transform += TrMatchPush diff --git a/tests/if-match.ec b/tests/if-match.ec new file mode 100644 index 000000000..b39aa1493 --- /dev/null +++ b/tests/if-match.ec @@ -0,0 +1,665 @@ +require import AllCore Xreal. + +(* -------------------------------------------------------------------- *) +type t = [A | B of int | C of int & bool]. + +exception oops of int. + +module M = { + (* conditional, then a continuation *) + proc f(b : bool) : int = { + var x; + if (b) { x <- 1; } else { x <- 2; } + x <- x + 1; + return x; + } + + (* conditional alone (empty continuation) *) + proc f0(b : bool) : int = { + var x; + if (b) { x <- 1; } else { x <- 2; } + return x; + } + + (* conditional after a prefix, for the [seq]-ing forms *) + proc f1(b : bool) : int = { + var x; + x <- 0; + if (b) { x <- x + 1; } else { x <- x + 2; } + x <- x + 1; + return x; + } + + (* conditional raising an exception, then a continuation *) + proc fe(a : int) : int = { + var x; + x <- a; + if (x < 0) { raise (oops x); } + x <- x + 1; + return x; + } + + (* match, then a continuation *) + proc g(o : t) : int = { + var x; + match o with + | A => { x <- 1; } + | B y => { x <- y; } + | C y z => { x <- if z then y else 0; } + end; + x <- x + 1; + return x; + } + + (* match alone (empty continuation), on another datatype *) + proc h(o : int option) : int = { + var x; + match o with + | None => { x <- 1; } + | Some y => { x <- y; } + end; + return x; + } + + (* pattern variables named like program variables, read and written by + the continuation; wildcards *) + proc g2(o : t) : int = { + var x, y; + y <- 0; + match o with + | A => { x <- 1; } + | B y => { x <- y; } + | C _ z => { x <- if z then 1 else 0; } + end; + x <- x + y; + y <- x; + return x + y; + } + + (* match on another instance of the same datatype *) + proc k(o : bool option) : int = { + var x; + match o with + | None => { x <- 1; } + | Some y => { x <- 1; } + end; + return x; + } + + (* nested matches, the inner one followed by a continuation *) + proc n(o : int option, o' : int option) : int = { + var x; + x <- 0; + match o with + | None => { x <- 1; } + | Some y => { + match o' with + | None => { x <- y; } + | Some y' => { x <- y + y'; } + end; + x <- x + y; + } + end; + x <- x + 1; + return x; + } +}. + +(* a [match] duplicated by inlining (same binders in both copies) *) +module N = { + proc h1(o : int option) : int = { + var r; + r <- 0; + match o with + | None => { r <- 1; } + | Some y => { r <- y; } + end; + return r; + } + + proc h2(o : int option) : int = { + var a, b; + a <@ h1(o); + b <@ h1(o); + return a + b; + } +}. + +(* ==================================================================== *) +(* if *) + +lemma hoare_if : hoare [M.f : true ==> 1 < res]. +proof. +proc; if. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma hoare_if_alone : hoare [M.f0 : b ==> res = 1]. +proof. +proc; if. ++ by wp; skip. ++ by wp; skip; smt(). +qed. + +lemma hoare_if_prefix : hoare [M.f1 : b ==> res = 2]. +proof. +proc; sp 1; if. ++ by wp; skip. ++ by wp; skip; smt(). +qed. + +(* exceptional postconditions are kept in both branches *) +lemma hoare_if_raise (a0 : int) : + hoare [M.fe : a = a0 ==> res = a0 + 1 | oops x => x < 0 /\ x = a0]. +proof. +proc; sp; if. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +(* the side is ignored on a [hoare] goal *) +lemma hoare_if_side : hoare [M.f : true ==> 1 < res]. +proof. +proc; if{2}. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma ehoare_if : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. +proc; if. ++ by wp; skip => &hr; case: (b{hr}). ++ by wp; skip => &hr; case: (b{hr}). +qed. + +lemma ehoare_if_alone : ehoare [M.f0 : (1%xr) ==> (1%xr)]. +proof. +proc; if. ++ by wp; skip => &hr; case: (b{hr}). ++ by wp; skip => &hr; case: (b{hr}). +qed. + +lemma phoare_if_eq : phoare [M.f : true ==> 1 < res] = 1%r. +proof. +proc; if. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma phoare_if_alone : phoare [M.f0 : true ==> 0 < res] = 1%r. +proof. +proc; if. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma phoare_if_le : phoare [M.f : true ==> res = 0] <= 0%r. +proof. +proc; if. ++ by hoare; wp; skip. ++ by hoare; wp; skip. +qed. + +lemma phoare_if_ge : phoare [M.f : true ==> 1 < res] >= (1%r/2%r). +proof. +proc; if. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma equiv_if : equiv [M.f ~ M.f : ={b} ==> ={res}]. +proof. +proc; if. ++ by move=> &1 &2 ->. ++ by wp; skip. ++ by wp; skip. +qed. + +(* two-sided, a continuation on the left only *) +lemma equiv_if_alone_right : equiv [M.f ~ M.f0 : ={b} ==> res{1} = res{2} + 1]. +proof. +proc; if. ++ by move=> &1 &2 ->. ++ by wp; skip. ++ by wp; skip. +qed. + +(* two-sided, a continuation on the right only *) +lemma equiv_if_alone_left : equiv [M.f0 ~ M.f : ={b} ==> res{1} + 1 = res{2}]. +proof. +proc; if. ++ by move=> &1 &2 ->. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_alone_both : equiv [M.f0 ~ M.f0 : ={b} ==> ={res}]. +proof. +proc; if. ++ by move=> &1 &2 ->. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_left : equiv [M.f ~ M.f0 : ={b} ==> 1 < res{1}]. +proof. +proc; if{1}. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_right : equiv [M.f0 ~ M.f : ={b} ==> 1 < res{2}]. +proof. +proc; if{2}. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_left_alone : equiv [M.f0 ~ M.f : ={b} ==> 0 < res{1}]. +proof. +proc; if{1}. ++ by wp; skip. ++ by wp; skip. +qed. + +(* [if] after [seq], at the last conditional *) +lemma equiv_if_seq : equiv [M.f1 ~ M.f1 : ={b} ==> ={res}]. +proof. +proc; if _ _ : (={b, x}). ++ by wp; skip. ++ by move=> &1 &2 [->]. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_seq_eq : equiv [M.f1 ~ M.f1 : ={b} ==> ={res}]. +proof. +proc; if := (={b, x}). ++ by wp; skip. ++ by move=> &1 &2 [->]. ++ by wp; skip. ++ by wp; skip. +qed. + +(* explicit positions: typed on the given side *) +lemma equiv_if_seq_pos : equiv [M.f1 ~ M.f1 : ={b} ==> ={res}]. +proof. +proc. +fail if 2 2 : (={b, x}). +if{1} 2 2 : (={b, x}). ++ by wp; skip. ++ by wp; skip. ++ by wp; skip. +abort. + +lemma equiv_if_seq_left : equiv [M.f1 ~ M.f1 : ={b} ==> true]. +proof. +proc; if{2} _ _ : (={b}). ++ by wp; skip. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_seqone : equiv [M.f1 ~ M.f1 : ={b} ==> true]. +proof. +proc; if{1} : (_ : true ==> true). ++ by wp; skip. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_if_seqone_right : equiv [M.f1 ~ M.f1 : ={b} ==> true]. +proof. +proc; if{2} 2 : (_ : true ==> true). ++ by wp; skip. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma if_errors : equiv [M.f1 ~ M.f : ={b} ==> true]. +proof. +proc. +fail if. +fail if{1}. +if{2}. +fail if _ _ : true. +abort. + +lemma if_errors_right : equiv [M.f ~ M.f1 : ={b} ==> true]. +proof. +proc. +fail if. +fail if{2}. +abort. + +lemma if_errors_hoare : hoare [M.f1 : true ==> true]. +proof. +proc. +fail if. +fail if _ _ : true. +fail if{1} : (_ : true ==> true). +abort. + +lemma if_errors_ehoare : ehoare [M.f1 : (1%xr) ==> (1%xr)]. +proof. +proc. +fail if. +fail if := true. +abort. + +lemma if_errors_phoare : phoare [M.f1 : true ==> true] = 1%r. +proof. +proc. +fail if. +fail if{1} : (_ : true ==> true). +abort. + +lemma if_errors_ambient : true. +proof. +fail if. +fail if := true. +abort. + +lemma if_errors_pred : hoare [M.f : true ==> true]. +proof. +fail if. +abort. + +(* ==================================================================== *) +(* match *) + +lemma hoare_match : hoare [M.g : o = A ==> res = 2]. +proof. +proc; match. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma hoare_match_alone : hoare [M.h : o = None ==> res = 1]. +proof. +proc; match. ++ by wp; skip. ++ by wp; skip => /> /#. +qed. + +lemma hoare_match_clash : hoare [M.g2 : o = A ==> res = 2]. +proof. +proc; sp 1; match. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma hoare_match_nested : hoare [M.n : o = None ==> res = 2]. +proof. +proc; sp 1; match. ++ by wp; skip. ++ match. + + by wp; skip => /> /#. + + by wp; skip => /> /#. +qed. + +(* the side or [=] is ignored on a [hoare] goal *) +lemma hoare_match_side : hoare [M.g : o = A ==> res = 2]. +proof. +proc; match{2}. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma hoare_match_eq : hoare [M.g : o = A ==> res = 2]. +proof. +proc; match =. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma phoare_match_eq : phoare [M.g : true ==> true] = 1%r. +proof. +proc; match. ++ by wp; skip. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma phoare_match_alone : phoare [M.h : true ==> true] = 1%r. +proof. +proc; match. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma phoare_match_le : phoare [M.g : o = A ==> res = 0] <= 0%r. +proof. +proc; match. ++ by hoare; wp; skip. ++ by hoare; wp; skip => /> /#. ++ by hoare; wp; skip => /> /#. +qed. + +lemma phoare_match_ge : phoare [M.g : o = A ==> res = 2] >= 1%r. +proof. +proc; match. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma phoare_match_clash : phoare [M.g2 : o = A ==> res = 2] = 1%r. +proof. +proc; sp 1; match. ++ by wp; skip. ++ by wp; skip => /> /#. ++ by wp; skip => /> /#. +qed. + +lemma equiv_match_sided : equiv [M.g ~ M.g : ={o} ==> ={res}]. +proof. +proc; match{1}. ++ match{2}. + + by wp; skip. + + by wp; skip => /> /#. + + by wp; skip => /> /#. ++ match{2}. + + by wp; skip => /> /#. + + by wp; skip => /> /#. + + by wp; skip => /> /#. ++ match{2}. + + by wp; skip => /> /#. + + by wp; skip => /> /#. + + by wp; skip => /> /#. +qed. + +lemma equiv_match_sided_alone : equiv [M.h ~ M.g : o{1} = None /\ o{2} = A ==> res{1} + 1 = res{2}]. +proof. +proc; match{1}. ++ match{2}. + + by wp; skip. + + by wp; skip => /> /#. + + by wp; skip => /> /#. ++ by exfalso => /> /#. +qed. + +lemma equiv_match_sided_right : equiv [M.g2 ~ M.g2 : ={o} ==> ={res}]. +proof. +proc; sp 1 1; match{2}. ++ by match{1}; [wp; skip | wp; skip => /> /# | wp; skip => /> /#]. ++ by match{1}; [wp; skip => /> /# | wp; skip => /> /# | wp; skip => /> /#]. ++ by match{1}; [wp; skip => /> /# | wp; skip => /> /# | wp; skip => /> /#]. +qed. + +lemma equiv_match_synced : equiv [M.g ~ M.g : ={o} ==> ={res}]. +proof. +proc; match. ++ smt(). ++ smt(). ++ smt(). ++ by wp; skip. ++ by move=> y1 y2; wp; skip => /> /#. ++ by move=> y1 z1 y2 z2; wp; skip => /> /#. +qed. + +lemma equiv_match_eq : equiv [M.g ~ M.g : ={o} ==> ={res}]. +proof. +proc; match =. ++ done. ++ by wp; skip. ++ by move=> y; wp; skip. ++ by move=> y z; wp; skip. +qed. + +lemma equiv_match_eq_clash : equiv [M.g2 ~ M.g2 : ={o} ==> ={res}]. +proof. +proc; sp 1 1; match =. ++ done. ++ by wp; skip. ++ by move=> y; wp; skip. ++ by move=> y z; wp; skip. +qed. + +(* two-sided, a continuation on one side only *) +lemma equiv_match_synced_inst : equiv [M.h ~ M.k : o{1} = None <=> o{2} = None ==> res{1} = 1 => res{2} = 1]. +proof. +proc; match. ++ by move=> &1 &2 /#. ++ by move=> &1 &2 /#. ++ by wp; skip. ++ by move=> y1 y2; wp; skip. +qed. + +lemma equiv_match_eq_alone : equiv [M.h ~ M.h : ={o} ==> ={res}]. +proof. +proc; match =. ++ done. ++ by wp; skip. ++ by move=> y; wp; skip. +qed. + +lemma equiv_match_nested : equiv [M.n ~ M.n : ={o, o'} ==> ={res}]. +proof. +proc; sp 1 1; match =. ++ done. ++ by wp; skip. ++ move=> y; match =. + + done. + + by wp; skip. + + by move=> y'; wp; skip. +qed. + +(* a free logical variable named like the pattern variables, in the + continuation of a match *) +lemma equiv_match_dup : equiv [N.h2 ~ N.h2 : ={o} ==> ={res}]. +proof. +proc; inline *; sp. +match =. ++ done. ++ admit. +move=> y. +swap{1} [3..5] -2. +sp 2 0. +match{1}. ++ admit. +admit. +abort. + +lemma match_errors : equiv [M.g ~ M.h : true ==> true]. +proof. +proc. +fail match. +fail match =. +abort. + +lemma match_errors_inst : equiv [M.h ~ M.k : true ==> true]. +proof. +proc. +fail match =. +abort. + +lemma match_errors_nomatch : equiv [M.f ~ M.g : true ==> true]. +proof. +proc. +fail match. +fail match =. +fail match{1}. +match{2}. +abort. + +lemma match_errors_nomatch_right : equiv [M.g ~ M.f : true ==> true]. +proof. +proc. +fail match. +fail match{2}. +abort. + +lemma match_errors_hoare : hoare [M.f : true ==> true]. +proof. +proc. +fail match. +abort. + +lemma match_errors_phoare : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +fail match. +abort. + +lemma match_errors_ehoare : ehoare [M.g : (1%xr) ==> (1%xr)]. +proof. +proc. +fail match. +abort. + +lemma match_errors_ambient : true. +proof. +fail match. +abort. + +(* ==================================================================== *) +(* case *) + +lemma hoare_case : hoare [M.f : true ==> 1 < res]. +proof. +proc; case (b). ++ by rcondt 1 => //; wp; skip. ++ by rcondf 1 => //; wp; skip. +qed. + +lemma ehoare_case : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. +proc; case (b). ++ by if; wp; skip => &hr; case: (b{hr}). ++ by if; wp; skip => &hr; case: (b{hr}). +qed. + +lemma phoare_case : phoare [M.f : true ==> 1 < res] = 1%r. +proof. +proc; case (b). ++ by rcondt 1 => //; wp; skip. ++ by rcondf 1 => //; wp; skip. +qed. + +lemma equiv_case : equiv [M.f ~ M.f : ={b} ==> ={res}]. +proof. +proc; case (b{1}). ++ by rcondt{1} 1 => //; rcondt{2} 1; auto => /> /#. ++ by rcondf{1} 1 => //; rcondf{2} 1; auto => /> /#. +qed. + +(* the case formula is simplified away when trivial *) +lemma hoare_case_true : hoare [M.f : true ==> true]. +proof. +proc; case true. ++ by wp; skip. ++ by wp; skip. +qed. + +lemma equiv_case_true : equiv [M.f ~ M.f : true ==> true]. +proof. +proc; case true. ++ by wp; skip. ++ by wp; skip. +qed.