Commit 284c99e4 authored by charguer's avatar charguer

xor_xand

parent e04c208a
......@@ -54,6 +54,7 @@ tools:
ln -sf $(CFML)/generator/makecmj.native $(TOOLS)/cfml_cmj
ln -sf $(CFML)/generator/myocamldep.native $(TOOLS)/cfml_dep
###############################################################################
# Clean
......
- rename xuntag_goal
- generate instance of comparable
- hint spec based on type args
(* DO not use; only used during the normalization phase *)
external ( & ) : bool -> bool -> bool = "%sequand"
external ( or ) : bool -> bool -> bool = "%sequor"
- xif sans argument pour pouvoir le forcer
- xifkeep ?
- xlet_keep
let H := cfml_get_precondition tt in
xlet (... \*+ H)
- "xapp as x" pratique sur xlet
- "xapps as x" pratique sur xlet
- xlet Q => xif Q mais avec branche
- xchanges
- hint spec based on type args
- implement xpush.
- xwhile: error reporting when arguments don't have the right types.
MAJOR TODAY
- implement xpush.
MAJOR NEXT
- Sys.max_array_length
- record with imperative
- partial/over application
MAJOR NEXT
- "xapp as x" pratique sur xlet
"xapps as x" pratique sur xlet
- xchanges
- Sys.max_array_length discuss with francois
- patterns and when clauses
......@@ -58,19 +44,12 @@ MAJOR NEXT
with : match r with T_intro x1 .. xN => T_intro x1 .. yI .. xN
=> requires the order of labels to be fixed as in the definition.
- record with imperative
- partial/over application
- xabstract => reimplement and rename as xgen
MAJOR NEXT NEXT
- xwhile: error reporting when arguments don't have the right types.
- eliminate notations for tags
- xlet_keep
let H := cfml_get_precondition tt in
xlet (... \*+ H)
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
......@@ -81,17 +60,13 @@ MAJOR NEXT NEXT
- realize array specification using single-cell array specifications
- see if we can get rid of make_cmj
- mutually recursive polymorhpic functions have too many type variables
quantified: we need one set of fvs for each def in the recursion.
- see if we can get rid of make_cmj, using -only-cmj
=> make_cmj seems to already be never used.
MAJOR POSTPONED
- support char
- support float
- support char, string, float
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
......@@ -102,7 +77,6 @@ MAJOR POSTPONED
- have a flag to control whether functions such as "min", "max", "abs", etc..
should be systematically let-bound; this would allow binding these names.
- mutual recursive definitions, polymophic type variables should be more precise
......
......@@ -6,65 +6,94 @@ Require Import Stdlib.
Open Scope tag_scope.
(*
todo: test xif new variants
todo: test xand
*)
(********************************************************************)
(* ** Lazy binary operators *)
Lemma lazyop_val_spec :
app lazyop_val [tt] \[] \[= 1].
Proof using.
xcf. xif. xrets~.
Qed.
Ltac xuntag_pre_post_core tt ::=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Ltac xcf_core tt ::=
intros;
xuntag_pre_post;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_top_value f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs) ?H ?Q => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf_show f as H], where [f] is the name of the definition"
end.
(* todo cleanup*)
(*
Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
*)
Lemma lazyop_term_spec :
app lazyop_term [tt] \[] \[= 1].
Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
(* we can do a simple proof if we are ready to duplicate the verification of [g] *)
Lemma rec_mutual_f_and_g_spec_inlining :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
xcf. xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets*. }
xapps.
xlet.
{ dup 3.
(* { xif_no_simpl \[= true]. xret. skip. skip. } *)
(* TODO:
xor \[= true].
with xif_base and 2 continuations
*)
{ xif_no_simpl \[= true].
{ xclean. false. }
{ xapps. xrets~. } }
{ xif. xapps. xrets~. }
{ xgo*. subst. xclean. auto. }
(* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
}
xpulls. xif. xrets~.
logic (forall (A B:Prop), A -> (A -> B) -> A /\ B).
{ intros x. induction_wf IH: (downto 0) x. intros Px.
xcf. xif. xrets~. xlet.
xcf. xapp. math. math. xpulls. xrets. math. }
{ intros Sg. introv Px. xcf. xapps. math. }
Qed.
Notation "'And_' v1 `&&` F2" :=
(!If (fun H Q => (v1 = true -> F2 H Q) /\ (v1 = false -> (Ret false) H Q)))
(at level 69, v1 at level 0) : charac.
(* the general approach is as follows, using a measure *)
Lemma lazyop_mixex_spec :
app lazyop_mixed [tt] \[] \[= 1].
Lemma rec_mutual_f_and_g_spec_measure :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
xcf.
xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets*. }
xlet \[= true].
{ xif. xapps. xlet \[= true].
{ xif. xapps. xlet \[= true].
{ xif. xrets~. }
{ intro_subst. xrets~. } }
{ intro_subst. xrets~. } }
{ intro_subst. xif. xrets~. }
intros. cuts G: (forall (m:int),
(forall x, -1 <= x /\ 2*x <= m -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x /\ 2*x+3 <= m -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P; specializes G (2*x+3);
destruct G as [G1 G2]; xapp; try math. }
=> m. induction_wf IH: (downto (-1)) m.
specializes IH (m-1). split; intros x (Lx&Px).
{ xcf. xif. xrets~. xapp. math. math.
intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
(* the general approach is as follows, using a lexicographical order
--- LATER
Lemma rec_mutual_f_and_g_spec :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
Search lexico2.
set (R := lexico2 (downto (-1)) (downto (-1))).
intros. cuts G: (forall p,
(forall x, -1 <= x /\ R (x,0) p -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x /\ R (x+1,1) p -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P.
{ specializes G (x+1,0). destruct G as [G1 G2]. xapp.
unfold R, lexico2. split. math. left. math. }
{ specializes G (x+2,0). destruct G as [G1 G2]. xapp.
unfold R, lexico2. split. math. left. math. } }
=> p. induction_wf IH: R p. split; intros x (Lx&Px).
destruct p as [a b]. unfolds R, @lexico2.
{ xcf. xif. xrets~. xapp (x-1,1).
(* todo: lexico2 is defined in a too strong way... *)
right. math. math.
intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
*)
......@@ -621,6 +650,62 @@ Qed.
(********************************************************************)
(* ** Lazy binary operators *)
Lemma lazyop_val_spec :
app lazyop_val [tt] \[] \[= 1].
Proof using.
xcf. xif. xrets~.
Qed.
(*
Ltac xauto_tilde ::= xauto_tilde_default ltac:(fun _ => auto_tilde).
*)
Lemma lazyop_term_spec :
app lazyop_term [tt] \[] \[= 1].
Proof using.
xcf. xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets*. }
xapps.
xlet \[=true].
{ dup 10.
{ xors. xapps. xsimpl~. subst. xclean. xauto*. }
{ xors \[=true]. xapps. xsimpl~. skip. }
{ xor \[=true]. xapps. xsimpl. skip. }
{ xif_no_simpl. skip. skip. }
{ xpost. xif_no_simpl \[= true]. skip. skip. skip. }
{ xpost. xif_no_simpl \[=true] as R.
{ xclean. false. }
{ xapps. xsimpl. subst. xclean. xauto*. }
xsimpl~. }
{ xpost. xif_no_intros \[=true]. intros R. skip. skip. }
{ xpost. xif_no_simpl_no_intros \[=true]. intros R. skip. skip. skip. }
{ xif. xapps. xsimpl. skip. }
{ xgo*. subst. xclean. auto. }
(* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
}
intro_subst. xif. xrets~.
Qed.
Lemma lazyop_mixed_spec :
app lazyop_mixed [tt] \[] \[= 1].
Proof using.
xcf.
xfun (fun f => forall (x:int),
app f [x] \[] \[= isTrue (x = 0)]).
{ xrets*. }
xlet \[= true].
{ xif. xapps. xors. xapps. xrets. extens. rew_refl. autos*. }
{ intro_subst. xif. xrets~. }
Qed.
(********************************************************************)
(* ** Comparison operators *)
......@@ -1162,55 +1247,7 @@ Proof using.
{ xrets. xif. math. xapps (k-1). math. math. xrets. math. } }
Qed.
Ltac xuntag_goal_core tt ::=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Ltac xcf_core tt ::=
intros;
xuntag_goal;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_top_value f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs) ?H ?Q => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf_show f as H], where [f] is the name of the definition"
end.
(* we can do a simple proof if we are ready to duplicate the verification of [g] *)
Lemma rec_mutual_f_and_g_spec_inlining :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
logic (forall (A B:Prop), A -> (A -> B) -> A /\ B).
{ intros x. induction_wf IH: (downto 0) x. intros Px.
xcf. xif. xrets~. xlet.
xcf. xapp. math. math. xpulls. xrets. math. }
{ intros Sg. introv Px. xcf. xapps. math. }
Qed.
(* the general approach is as follows *)
(* TODO: does not work yet
Lemma rec_mutual_f_and_g_spec :
(forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]).
Proof using.
intros. cuts G: (forall (m:int),
(forall x, 0 <= x <= m+1 -> app rec_mutual_f [x] \[] \[= x])
/\ (forall x, -1 <= x <= m-1 -> app rec_mutual_g [x] \[] \[= x+1])).
{ split; intros x P; specializes G (x+4);
destruct G as [G1 G2]; xapp; try math. }
=> m. induction_wf IH: (downto (-2)) m.
specializes IH (m-1). split; intros x (Lx&Px).
{ xcf. xif. xrets~. xapp.
math. split. math. skip. intro_subst. xrets. math. }
{ xcf. xapp. math. math. }
Qed.
*)
(********************************************************************)
......
......@@ -365,25 +365,36 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
assert (b0 = []); (* since e0 should be "&&" or "||" *)
let e1',b1 = aux ~as_value:true e1 in
let e2',b2 = aux ~as_value:true e2 in
if b1 = [] && b2 = [] then begin
(* produce: let <b1> in <e1> && <e2>
let <b1> in <e1> || <e2> *)
return (Pexp_apply (e0', [(l1,e1'); (l2,e2')])), []
end else if name = "&&" then begin
(* produce: let <b1> in if <e1'> then (let <b2> in <e2'>) else false *)
wrap_as_value (return (
Pexp_ifthenelse (
e1',
create_let loc b2 e2',
Some (mk_bool false)))) b1
end else if name = "||" then begin
(* produce: let <b1> in if <e1'> then true else (let <b2> in <e2'>) *)
wrap_as_value (return (
Pexp_ifthenelse (
e1',
mk_bool true,
Some (create_let loc b2 e2')))) b1
end else assert false
if b2 = [] then begin
if b1 = [] then begin
(* produce: <e1> && <e2>
<e1> || <e2> *)
return (Pexp_apply (e0', [(l1,e1'); (l2,e2')])), []
end else begin
(* produce: let <b1> in <e1> && <e2>
let <b1> in <e1> || <e2> *)
wrap_as_value (return (Pexp_apply (e0', [(l1,e1'); (l2,e2')]))) b1
end
end else begin
(* TODO: how to avoid the redundant computations of [aux e2]?
We need to return two results, one as a value, one not as a value. *)
let e2',b2 = aux ~as_value:false e2 in
if name = "&&" then begin
(* produce: let <b1> in if <e1'> then (let <b2> in <e2'>) else false *)
wrap_as_value (return (
Pexp_ifthenelse (
e1',
create_let loc b2 e2',
Some (mk_bool false)))) b1
end else if name = "||" then begin
(* produce: let <b1> in if <e1'> then true else (let <b2> in <e2'>) *)
wrap_as_value (return (
Pexp_ifthenelse (
e1',
mk_bool true,
Some (create_let loc b2 e2')))) b1
end else assert false
end
| Pexp_apply (e0, l) ->
let is_inlined = exp_is_inlined_primitive e0 l in
let e0',b0 = aux ~as_value:true e0 in
......
......@@ -82,17 +82,17 @@ Ltac xtag_pre_post_core tt :=
Tactic Notation "xtag_pre_post" :=
xtag_pre_post_core tt.
(** [xuntag_goal] removes [tag_goal] from the head of the goal,
(** [xuntag_pre_post] removes [tag_goal] from the head of the goal,
or does nothing if there is no such tag. *)
Ltac xuntag_goal_core tt :=
Ltac xuntag_pre_post_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Tactic Notation "xuntag_goal" :=
xuntag_goal_core tt.
Tactic Notation "xuntag_pre_post" :=
xuntag_pre_post_core tt.
(** [cfml_get_tag tt] returns the tag at the head of the goal *)
......@@ -121,10 +121,10 @@ Ltac cfml_check_not_tagged tt :=
(** [xuntag T] removes the tag [T] at the head of the goal,
and fails if it is not there. The tag [tag_goal] is
treated specially: it is automatically removed on the fly.
To remove only [tag_goal], use [xuntag_goal]. *)
To remove only [tag_goal], use [xuntag_pre_post]. *)
Ltac xuntag_core T :=
xuntag_goal;
xuntag_pre_post;
match goal with
| |- @tag T _ _ => unfold tag at 1
| |- @tag T _ _ _ _ => unfold tag at 1
......@@ -139,7 +139,7 @@ Tactic Notation "xuntag" constr(T) :=
removes the [tag_goal] at the head, if any. *)
Tactic Notation "xuntag" :=
xuntag_goal_core tt;
xuntag_pre_post_core tt;
match goal with
| |- @tag _ _ _ => unfold tag at 1
| |- @tag _ _ _ _ _ => unfold tag at 1
......
......@@ -79,7 +79,7 @@ Ltac cfml_get_goal_arity tt :=
match goal with
| |- spec ?f ?n ?P => constr:(n)
| |- app ?f ?xs ?H ?Q => aux xs
| |- tag tag_apply (app ?f ?xs ?H ?Q) => aux xs
| |- tag tag_apply (app ?f ?xs) ?H ?Q => aux xs
end .
(* [cfml_show_types_dyn_list L] displays the types of the
......@@ -1716,6 +1716,10 @@ Tactic Notation "xassert" :=
It leaves two subgoals [F1 H Q] under the assumption [v=true]
and [F2 H Q] under the assumption [v=false].
[xif] also applies to a goal of the form
[(Let x = (If v Then F1 Else F2) in ...) H Q].
In this case, it calls [xlet] first.
If [Q] is not instantiated, it will automatically be instantiated
with [if v then ?Q1 else ?Q2]. Without this behavior, when
the post-condition is not instantiated, then the post-condition will
......@@ -1730,6 +1734,10 @@ Tactic Notation "xassert" :=
- [xif_no_simpl] avoids proving false from obvious contradictions.
- [xif_no_intros] leaves the hypothesis in the goals.
- [xif_no_simpl_no_intros] combines the above two.
- [xif Q'] allows to specify the post-condition. It is useful
when the post [Q] is an evar. Equivalent to [xpost Q'; xif].
......@@ -1737,7 +1745,11 @@ Tactic Notation "xassert" :=
Also available;
- [xif Q' as X]
- [xif_no_simpl Q as X]
- [xif_no_simpl as X]
- [xif_no_simpl Q']
- [xif_no_simpl Q' as X]
- [xif_no_intros Q']
- [xif_no_simpl_no_intros Q']
*)
......@@ -1772,39 +1784,211 @@ Ltac xif_check_post_instantiated tt :=
| false => idtac
end.
Ltac xif_core H :=
apply local_erase; split; intro H.
Ltac xif_base H cont :=
Ltac xif_base cont1 cont2 :=
xpull_check_not_needed tt;
xif_check_post_instantiated tt;
xuntag tag_if;
xif_core H;
cont tt;
xtag_pre_post.
let cont tt :=
xuntag tag_if;
apply local_erase;
split; [ cont1 tt | cont2 tt ];
xtag_pre_post
in
match cfml_get_tag tt with
| tag_if => cont tt
| tag_let => xlet; [ cont tt | instantiate ]
end.
Ltac xif_then H :=
xif_base H ltac:(fun _ => xif_post H).
Ltac xif_assign_post_then Q cont :=
match cfml_get_tag tt with
| tag_if =>
match cfml_postcondition_is_evar tt with
| true => xpost Q; cont tt
| false => fail 2 "There is already a post-condition, so you shouldn't use [xif Q].\
To change the post, use [xpost Q] first."
end
| tag_let => xlet Q; [ cont tt | instantiate ]
end.
Ltac xif_base_sym cont :=
xif_base ltac:(cont) ltac:(cont).
Ltac xif_core H :=
xif_base_sym ltac:(fun _ => intro H; xif_post H).
Tactic Notation "xif" "as" ident(H) :=
xif_then H.
xif_core H.
Tactic Notation "xif" :=
let H := fresh "C" in xif as H.
Tactic Notation "xif" constr(Q) "as" ident(H) :=
xpost Q; xif as H.
xif_assign_post_then Q ltac:(fun _ => xif as H).
Tactic Notation "xif" constr(Q) :=
let H := fresh "C" in xif Q as H.
Ltac xif_no_simpl_core H :=
xif_base_sym ltac:(fun _ => intro H).
Tactic Notation "xif_no_simpl" "as" ident(H) :=
xif_base H ltac:(fun _ => idtac).
xif_no_simpl_core H.
Tactic Notation "xif_no_simpl" :=
let H := fresh "C" in xif_no_simpl as H.
Tactic Notation "xif_no_simpl" constr(Q) "as" ident(H) :=
xpost Q; xif_no_simpl as H.
xif_assign_post_then Q ltac:(fun _ => xif_no_simpl as H).
Tactic Notation "xif_no_simpl" constr(Q) :=
xpost Q; xif_no_simpl.
let H := fresh "C" in xif_no_simpl Q as H.
Ltac xif_no_intros_core tt :=
xif_base_sym ltac:(fun _ =>
let H := fresh in
intro H;
xif_post H;
revert H).
Tactic Notation "xif_no_intros" :=
xif_no_intros_core tt.
Tactic Notation "xif_no_intros" constr(Q) :=
xif_assign_post_then Q ltac:(fun _ => xif_no_intros).
Ltac xif_no_simpl_no_intros_core H :=
xif_base_sym ltac:(fun _ => idtac).
Tactic Notation "xif_no_simpl_no_intros" :=
xif_no_simpl_no_intros_core tt.
Tactic Notation "xif_no_simpl_no_intros" constr(Q) :=
xif_assign_post_then Q ltac:(fun _ => xif_no_simpl_no_intros).
(*--------------------------------------------------------*)
(* ** [xand] *)
(** [xand] applies to a goal of the form [(And v1 `&&` F2) H Q],
which is sugar for [(If v1 Then F2 Else (Ret false)) H Q].
It also applies to a goal of the form
[(Let x = (And v1 `&&` F2) in ...) H Q].
- [xand] is a shorthand for [xif] followed by [xret] in the
second branch.
- [xand as H] is similar; it allows naming the hypothesis.
- [xand Q] is short for [xlet Q] followed by [xand] in the
first branch.
- [xands] is similar, it calls [xrets] instead of [xret].
Variants:
- [xand Q as H]
- [xands Q]
- [xands Q as H]
- All [xif] variants are also applicable directly.
*)
Ltac xand_base H contRet :=
xif_base
ltac:(fun _ => intro H; xif_post H)
ltac:(fun _ => intro H; xif_post H; contRet tt).
Ltac xand_core H contRet :=
let cont tt := xand_base H contRet in
match cfml_get_tag tt with
| tag_if => cont tt
| tag_let => xlet; [ cont tt | instantiate ]
end.
Tactic Notation "xand" "as" ident(H) :=
xand_core H ltac:(fun _ => xret).
Tactic Notation "xand" :=
let H := fresh "C" in xand as H.
Ltac xand_with_core Q H contRet :=
let cont tt := xand_base H contRet in
match cfml_get_tag tt with
| tag_if => cont tt
| tag_let => xlet Q; [ cont tt | instantiate; try xpull ]
end.
Tactic Notation "xand" constr(Q) "as" ident(H) :=
xand_with_core Q H ltac:(fun _ => xret).
Tactic Notation "xand" constr(Q) :=
let H := fresh "C" in xand Q as H.
Tactic Notation "xands" "as" ident(H) :=
xand_core H ltac:(fun _ => xrets).
Tactic Notation "xands" :=
let H := fresh "C" in xands as H.
Tactic Notation "xands" constr(Q) "as" ident(H) :=
xand_with_core Q H ltac:(fun _ => xrets).
Tactic Notation "xands" constr(Q) :=
let H := fresh "C" in xands Q as H.
(*--------------------------------------------------------*)
(* ** [xor] *)
(** [xor] applies to a goal of the form [(Or v1 `||` F2) H Q],
which is sugar for [(If v1 Then (Ret true) Else F2) H Q].
It also applies to a goal of the form
[(Let x = (Or v1 `||` F2) in ...) H Q].
- [xor] is a shorthand for [xif] followed by [xret] in the
first branch.
- [xor as H] is similar; it allows naming the hypothesis.
- [xor Q] is short for [xlet Q] followed by [xor] in the
first branch.
- [xors] is similar, it calls [xrets] instead of [xret].
Variants:
- [xor Q as H]
- [xors Q]
- [xors Q as H]
- All [xif] variants are also applicable directly.
*)
Ltac xor_base H contRet :=
xif_base
ltac:(fun _ => intro H; xif_post H; contRet tt)
ltac:(fun _ => intro H; xif_post H).
Ltac xor_core H contRet :=
let cont tt := xor_base H contRet in
match cfml_get_tag tt with
| tag_if <