diff --git a/src/phl/ecPhlTAuto.ml b/src/phl/ecPhlTAuto.ml index e06514f4a..47f0cfcea 100644 --- a/src/phl/ecPhlTAuto.ml +++ b/src/phl/ecPhlTAuto.ml @@ -6,52 +6,28 @@ open EcCoreGoal open EcLowPhlGoal (* -------------------------------------------------------------------- *) - -let t_hoare_true_r tc = - match (FApi.tc1_goal tc).f_node with - | FhoareF hf when POE.forall (f_equal f_true) (hf_po hf).hsi_inv -> - FApi.xmutate1 tc `HoareTrue [] - - | FhoareS hs when POE.forall (f_equal f_true) (hs_po hs).hsi_inv -> - FApi.xmutate1 tc `HoareTrue [] - - | _ -> - tc_error !!tc - "the conclusion is not of the form %s" - "hoare[_ : _ ==> true]" - -let t_hoare_true = FApi.t_low0 "hoare-true" t_hoare_true_r +(* The rules closing trivially valid judgements live, one module per rule + and logic, in [rules//]: [true] (hoare), [zero] (ehoare) and + [exfalso] (hoare, bdhoare, equiv). This module only keeps the legacy + entry points and the logic-agnostic [exfalso] dispatcher. *) (* -------------------------------------------------------------------- *) -let f_xr0 = f_r2xr f_r0 +let t_hoare_true = EcHoareTrue.t_hoare_true -let t_ehoare_zero_r tc = - match (FApi.tc1_goal tc).f_node with - | FeHoareF hf when f_equal (ehf_po hf).inv f_xr0 -> - FApi.xmutate1 tc `eHoareZero [] - - | FeHoareS hs when f_equal (ehs_po hs).inv f_xr0 -> - FApi.xmutate1 tc `eHoareZero [] - | _ -> - tc_error !!tc - "the conclusion is not of the form %s" - "ehoare[_ : _ ==> 0%xr]" - -let t_ehoare_zero = FApi.t_low0 "hoare-zero" t_ehoare_zero_r +let t_ehoare_zero = EcEHoareZero.t_ehoare_zero (* -------------------------------------------------------------------- *) -let t_core_exfalso_r tc = - let pre = tc1_get_pre tc in - if not (f_equal (inv_of_inv pre) f_false) then - tc_error !!tc "pre-condition is not `false'"; - match (FApi.tc1_goal tc).f_node with - | FbdHoareS bhs -> - FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv bhs.bhs_m - (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))] - | FbdHoareF bhf -> - let (me, _) = EcEnv.Fun.hoareF_memenv (bhf.bhf_m) bhf.bhf_f (FApi.tc1_env tc) in - FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv me - (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))] - | _ -> FApi.xmutate1 tc `ExFalso [] - -let t_core_exfalso = FApi.t_low0 "core-exfalso" t_core_exfalso_r +(* An ehoare precondition is an expectation, never [false]: [exfalso] has no + ehoare rule, and such goals are rejected by the precondition check. *) +let t_core_exfalso (tc : tcenv1) = + let pre = tc1_get_pre tc in + if not (f_equal (inv_of_inv pre) f_false) then + tc_error !!tc "pre-condition is not `false'"; + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareExfalso.t_hoareS_exfalso tc + | FhoareF _ -> EcHoareExfalso.t_hoareF_exfalso tc + | FbdHoareS _ -> EcBdHoareExfalso.t_bdhoareS_exfalso tc + | FbdHoareF _ -> EcBdHoareExfalso.t_bdhoareF_exfalso tc + | FequivS _ -> EcEquivExfalso.t_equivS_exfalso tc + | FequivF _ -> EcEquivExfalso.t_equivF_exfalso tc + | _ -> tc_error !!tc "pre-condition is not `false'" diff --git a/src/phl/rules/bdhoare/ecBdHoareExfalso.ml b/src/phl/rules/bdhoare/ecBdHoareExfalso.ml new file mode 100644 index 000000000..811128dc8 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareExfalso.ml @@ -0,0 +1,57 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [exfalso] rules have no parameters. *) +type EcCoreGoal.rule += + | RBdHoareSExfalso + | RBdHoareFExfalso + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers. The side condition + (the precondition is syntactically [false]) is part of them, so the + checker re-validates it. *) +let bdhoareS_exfalso_subgoals (bhs : bdHoareS) : form list = + if not (f_equal (bhs_pr bhs).inv f_false) then + failwith "bdhoareS-exfalso: the precondition is not false"; + [EcSubst.f_forall_mems_ss_inv bhs.bhs_m + (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))] + +let bdhoareF_exfalso_subgoals (hyps : LDecl.hyps) (bhf : bdHoareF) : form list = + if not (f_equal (bhf_pr bhf).inv f_false) then + failwith "bdhoareF-exfalso: the precondition is not false"; + let me, _ = Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f (LDecl.toenv hyps) in + [EcSubst.f_forall_mems_ss_inv me + (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))] + +(* -------------------------------------------------------------------- *) +let not_false tc = tc_error !!tc "pre-condition is not `false'" + +(* Rules (TCB). *) +let t_bdhoareS_exfalso (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + if not (f_equal (bhs_pr bhs).inv f_false) then not_false tc; + FApi.xrule1 tc RBdHoareSExfalso (bdhoareS_exfalso_subgoals bhs) + +let t_bdhoareF_exfalso (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + if not (f_equal (bhf_pr bhf).inv f_false) then not_false tc; + FApi.xrule1 tc RBdHoareFExfalso + (bdhoareF_exfalso_subgoals (FApi.tc1_hyps tc) bhf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareSExfalso -> + Some (EcPlRecheck.checker_of "bdhoareS-exfalso" pf_as_bdhoareS + (fun _hyps bhs -> bdhoareS_exfalso_subgoals bhs)) + | RBdHoareFExfalso -> + Some (EcPlRecheck.checker_of "bdhoareF-exfalso" pf_as_bdhoareF + (fun hyps bhf -> bdhoareF_exfalso_subgoals hyps bhf)) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoareExfalso.mli b/src/phl/rules/bdhoare/ecBdHoareExfalso.mli new file mode 100644 index 000000000..c8aeb7cca --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareExfalso.mli @@ -0,0 +1,28 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareS_exfalso] — false precondition, with [~] the goal's + comparison: + + forall &m, 0%r <= d + ------------------------------- + phoare [c : false ==> Q] ~ d + + Side condition: the precondition is syntactically [false] (otherwise + fails). + + Node: [RBdHoareSExfalso]. Checker: "bdhoareS-exfalso". *) +val t_bdhoareS_exfalso : backward + +(* [t_bdhoareF_exfalso] — same for a procedure (the premise quantifies over + the procedure's initial memory): + + forall &m, 0%r <= d + ------------------------------- + phoare [f : false ==> Q] ~ d + + Node: [RBdHoareFExfalso]. Checker: "bdhoareF-exfalso". *) +val t_bdhoareF_exfalso : backward diff --git a/src/phl/rules/ehoare/ecEHoareZero.ml b/src/phl/rules/ehoare/ecEHoareZero.ml new file mode 100644 index 000000000..e55f3f3ac --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareZero.ml @@ -0,0 +1,63 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [zero] rules have no parameters. *) +type EcCoreGoal.rule += + | REHoareSZero + | REHoareFZero + +(* -------------------------------------------------------------------- *) +let f_xr0 = f_r2xr f_r0 + +(* Pure cores shared by the rules and their checkers: no premise; the side + condition (the postcondition is syntactically [0%xr]) is part of them, so + the checker re-validates it. *) +let ehoareS_zero_subgoals (hs : eHoareS) : form list = + if not (f_equal (ehs_po hs).inv f_xr0) then + failwith "ehoareS-zero: the postcondition is not 0%xr"; + [] + +let ehoareF_zero_subgoals (hf : eHoareF) : form list = + if not (f_equal (ehf_po hf).inv f_xr0) then + failwith "ehoareF-zero: the postcondition is not 0%xr"; + [] + +(* -------------------------------------------------------------------- *) +let not_of_the_form tc = + tc_error !!tc "the conclusion is not of the form %s" "ehoare[_ : _ ==> 0%xr]" + +(* Rules (TCB). *) +let t_ehoareS_zero (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + if not (f_equal (ehs_po hs).inv f_xr0) then not_of_the_form tc; + FApi.xrule1 tc REHoareSZero (ehoareS_zero_subgoals hs) + +let t_ehoareF_zero (tc : tcenv1) = + let hf = tc1_as_ehoareF tc in + if not (f_equal (ehf_po hf).inv f_xr0) then not_of_the_form tc; + FApi.xrule1 tc REHoareFZero (ehoareF_zero_subgoals hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareSZero -> + Some (EcPlRecheck.checker_of "ehoareS-zero" pf_as_ehoareS + (fun _hyps hs -> ehoareS_zero_subgoals hs)) + | REHoareFZero -> + Some (EcPlRecheck.checker_of "ehoareF-zero" pf_as_ehoareF + (fun _hyps hf -> ehoareF_zero_subgoals hf)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Dispatcher (no node of its own). *) +let t_ehoare_zero (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FeHoareS _ -> t_ehoareS_zero tc + | FeHoareF _ -> t_ehoareF_zero tc + | _ -> not_of_the_form tc diff --git a/src/phl/rules/ehoare/ecEHoareZero.mli b/src/phl/rules/ehoare/ecEHoareZero.mli new file mode 100644 index 000000000..1254050f8 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareZero.mli @@ -0,0 +1,31 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoareS_zero] — null expectation: + + -------------------------- + ehoare [c : P ==> 0%xr] + + No premise. Side condition: the postcondition is syntactically [0%xr] + (otherwise fails). + + Node: [REHoareSZero]. Checker: "ehoareS-zero". *) +val t_ehoareS_zero : backward + +(* [t_ehoareF_zero] — same for a procedure: + + -------------------------- + ehoare [f : P ==> 0%xr] + + Node: [REHoareFZero]. Checker: "ehoareF-zero". *) +val t_ehoareF_zero : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoare_zero] — [t_ehoareS_zero] or [t_ehoareF_zero], depending on the + goal. *) +val t_ehoare_zero : backward diff --git a/src/phl/rules/equiv/ecEquivExfalso.ml b/src/phl/rules/equiv/ecEquivExfalso.ml new file mode 100644 index 000000000..3755e1a50 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivExfalso.ml @@ -0,0 +1,52 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [exfalso] rules have no parameters. *) +type EcCoreGoal.rule += + | REquivSExfalso + | REquivFExfalso + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers: no premise; the side + condition (the precondition is syntactically [false]) is part of them, so + the checker re-validates it. *) +let equivS_exfalso_subgoals (es : equivS) : form list = + if not (f_equal (es_pr es).inv f_false) then + failwith "equivS-exfalso: the precondition is not false"; + [] + +let equivF_exfalso_subgoals (ef : equivF) : form list = + if not (f_equal (ef_pr ef).inv f_false) then + failwith "equivF-exfalso: the precondition is not false"; + [] + +(* -------------------------------------------------------------------- *) +let not_false tc = tc_error !!tc "pre-condition is not `false'" + +(* Rules (TCB). *) +let t_equivS_exfalso (tc : tcenv1) = + let es = tc1_as_equivS tc in + if not (f_equal (es_pr es).inv f_false) then not_false tc; + FApi.xrule1 tc REquivSExfalso (equivS_exfalso_subgoals es) + +let t_equivF_exfalso (tc : tcenv1) = + let ef = tc1_as_equivF tc in + if not (f_equal (ef_pr ef).inv f_false) then not_false tc; + FApi.xrule1 tc REquivFExfalso (equivF_exfalso_subgoals ef) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivSExfalso -> + Some (EcPlRecheck.checker_of "equivS-exfalso" pf_as_equivS + (fun _hyps es -> equivS_exfalso_subgoals es)) + | REquivFExfalso -> + Some (EcPlRecheck.checker_of "equivF-exfalso" pf_as_equivF + (fun _hyps ef -> equivF_exfalso_subgoals ef)) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivExfalso.mli b/src/phl/rules/equiv/ecEquivExfalso.mli new file mode 100644 index 000000000..83acc5e5c --- /dev/null +++ b/src/phl/rules/equiv/ecEquivExfalso.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equivS_exfalso] — false precondition: + + ------------------------------ + equiv [c ~ c' : false ==> Q] + + No premise. Side condition: the precondition is syntactically [false] + (otherwise fails). + + Node: [REquivSExfalso]. Checker: "equivS-exfalso". *) +val t_equivS_exfalso : backward + +(* [t_equivF_exfalso] — same for procedures: + + ------------------------------ + equiv [f ~ f' : false ==> Q] + + Node: [REquivFExfalso]. Checker: "equivF-exfalso". *) +val t_equivF_exfalso : backward diff --git a/src/phl/rules/hoare/ecHoareExfalso.ml b/src/phl/rules/hoare/ecHoareExfalso.ml new file mode 100644 index 000000000..52849796f --- /dev/null +++ b/src/phl/rules/hoare/ecHoareExfalso.ml @@ -0,0 +1,52 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [exfalso] rules have no parameters. *) +type EcCoreGoal.rule += + | RHoareSExfalso + | RHoareFExfalso + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers: no premise; the side + condition (the precondition is syntactically [false]) is part of them, so + the checker re-validates it. *) +let hoareS_exfalso_subgoals (hs : sHoareS) : form list = + if not (f_equal (hs_pr hs).inv f_false) then + failwith "hoareS-exfalso: the precondition is not false"; + [] + +let hoareF_exfalso_subgoals (hf : sHoareF) : form list = + if not (f_equal (hf_pr hf).inv f_false) then + failwith "hoareF-exfalso: the precondition is not false"; + [] + +(* -------------------------------------------------------------------- *) +let not_false tc = tc_error !!tc "pre-condition is not `false'" + +(* Rules (TCB). *) +let t_hoareS_exfalso (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (f_equal (hs_pr hs).inv f_false) then not_false tc; + FApi.xrule1 tc RHoareSExfalso (hoareS_exfalso_subgoals hs) + +let t_hoareF_exfalso (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + if not (f_equal (hf_pr hf).inv f_false) then not_false tc; + FApi.xrule1 tc RHoareFExfalso (hoareF_exfalso_subgoals hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareSExfalso -> + Some (EcPlRecheck.checker_of "hoareS-exfalso" pf_as_hoareS + (fun _hyps hs -> hoareS_exfalso_subgoals hs)) + | RHoareFExfalso -> + Some (EcPlRecheck.checker_of "hoareF-exfalso" pf_as_hoareF + (fun _hyps hf -> hoareF_exfalso_subgoals hf)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareExfalso.mli b/src/phl/rules/hoare/ecHoareExfalso.mli new file mode 100644 index 000000000..c9e58d501 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareExfalso.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoareS_exfalso] — false precondition: + + --------------------------- + hoare [c : false ==> Q | Q_e] + + No premise. Side condition: the precondition is syntactically [false] + (otherwise fails). + + Node: [RHoareSExfalso]. Checker: "hoareS-exfalso". *) +val t_hoareS_exfalso : backward + +(* [t_hoareF_exfalso] — same for a procedure: + + --------------------------- + hoare [f : false ==> Q | Q_e] + + Node: [RHoareFExfalso]. Checker: "hoareF-exfalso". *) +val t_hoareF_exfalso : backward diff --git a/src/phl/rules/hoare/ecHoareTrue.ml b/src/phl/rules/hoare/ecHoareTrue.ml new file mode 100644 index 000000000..7ab67a0a7 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareTrue.ml @@ -0,0 +1,64 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [true] rules have no parameters. *) +type EcCoreGoal.rule += + | RHoareSTrue + | RHoareFTrue + +(* -------------------------------------------------------------------- *) +(* Every postcondition, normal and exceptional, is syntactically [true]. *) +let is_true_post (po : hs_inv) = + POE.forall (f_equal f_true) po.hsi_inv + +(* Pure cores shared by the rules and their checkers: no premise; the side + condition is part of them, so the checker re-validates it. *) +let hoareS_true_subgoals (hs : sHoareS) : form list = + if not (is_true_post (hs_po hs)) then + failwith "hoareS-true: the postcondition is not true"; + [] + +let hoareF_true_subgoals (hf : sHoareF) : form list = + if not (is_true_post (hf_po hf)) then + failwith "hoareF-true: the postcondition is not true"; + [] + +(* -------------------------------------------------------------------- *) +let not_of_the_form tc = + tc_error !!tc "the conclusion is not of the form %s" "hoare[_ : _ ==> true]" + +(* Rules (TCB). *) +let t_hoareS_true (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (is_true_post (hs_po hs)) then not_of_the_form tc; + FApi.xrule1 tc RHoareSTrue (hoareS_true_subgoals hs) + +let t_hoareF_true (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + if not (is_true_post (hf_po hf)) then not_of_the_form tc; + FApi.xrule1 tc RHoareFTrue (hoareF_true_subgoals hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareSTrue -> + Some (EcPlRecheck.checker_of "hoareS-true" pf_as_hoareS + (fun _hyps hs -> hoareS_true_subgoals hs)) + | RHoareFTrue -> + Some (EcPlRecheck.checker_of "hoareF-true" pf_as_hoareF + (fun _hyps hf -> hoareF_true_subgoals hf)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Dispatcher (no node of its own). *) +let t_hoare_true (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> t_hoareS_true tc + | FhoareF _ -> t_hoareF_true tc + | _ -> not_of_the_form tc diff --git a/src/phl/rules/hoare/ecHoareTrue.mli b/src/phl/rules/hoare/ecHoareTrue.mli new file mode 100644 index 000000000..3176bb013 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareTrue.mli @@ -0,0 +1,31 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoareS_true] — trivial postcondition: + + ------------------------------- + hoare [c : P ==> true | true_e] + + No premise. Side condition: every postcondition, normal and exceptional, + is syntactically [true] (otherwise fails). + + Node: [RHoareSTrue]. Checker: "hoareS-true". *) +val t_hoareS_true : backward + +(* [t_hoareF_true] — same for a procedure: + + ------------------------------- + hoare [f : P ==> true | true_e] + + Node: [RHoareFTrue]. Checker: "hoareF-true". *) +val t_hoareF_true : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_true] — [t_hoareS_true] or [t_hoareF_true], depending on the + goal. *) +val t_hoare_true : backward diff --git a/tests/true-zero-exfalso.ec b/tests/true-zero-exfalso.ec new file mode 100644 index 000000000..9ab6871aa --- /dev/null +++ b/tests/true-zero-exfalso.ec @@ -0,0 +1,42 @@ +require import AllCore Xreal. + +module M = { + proc f() : int = { + var x; + x <- 1; + return x; + } +}. + +(* [true]: trivial postcondition, procedure and statement forms. *) +lemma hoareF_true : hoare [M.f : true ==> true]. +proof. by auto. qed. + +lemma hoareS_true : hoare [M.f : true ==> true]. +proof. by proc; auto. qed. + +(* [zero]: null expectation, procedure and statement forms. *) +lemma ehoareF_zero : ehoare [M.f : (1%xr) ==> (0%xr)]. +proof. by auto. qed. + +lemma ehoareS_zero : ehoare [M.f : (1%xr) ==> (0%xr)]. +proof. by proc; auto. qed. + +(* [exfalso]: false precondition, in every logic and both forms. *) +lemma hoareF_exfalso : hoare [M.f : false ==> res = 2]. +proof. by exfalso. qed. + +lemma hoareS_exfalso : hoare [M.f : false ==> res = 2]. +proof. by proc; exfalso. qed. + +lemma bdhoareF_exfalso : phoare [M.f : false ==> res = 2] = 1%r. +proof. by exfalso. qed. + +lemma bdhoareS_exfalso : phoare [M.f : false ==> res = 2] = 1%r. +proof. by proc; exfalso. qed. + +lemma equivF_exfalso : equiv [M.f ~ M.f : false ==> res{1} <> res{2}]. +proof. by exfalso. qed. + +lemma equivS_exfalso : equiv [M.f ~ M.f : false ==> res{1} <> res{2}]. +proof. by proc; exfalso. qed.