Set Implicit Arguments.
Require Export DeepReasoning.
Ltac ximpl_base :=
first
[ eapply bimpl_refl
| rapply 1 bimpl_refl
| rapply 1 bimpl_bottom
| rapply 5 bimpl_nocast_leq_req
| rapply 5 bimpl_nocast_leq
| rapply 5 bimpl_nocast
| rapply 5 bimpl_cast_lval
| rapply 7 bimpl_cast_lval_leq
| rapply 5 bimpl_cast_lval_leq_req
| rapply 5 bimpl_cast_rval
| rapply 5 bimpl_cast_rval_leq
| rapply 5 bimpl_cast_rval_leq_req
| rapply 7 bimpl_cast
| rapply 9 bimpl_cast_leq
| rapply 8 bimpl_cast_leq_req ].
Tactic Notation "ximpl" :=
ximpl_base.
Tactic Notation "ximpl" "~" :=
ximpl; eauto.
Tactic Notation "ximpl" "as" ident(I1) simple_intropattern(I2) :=
ximpl; intros I1 I2.
Tactic Notation "ximpl" "as" ident(I1) :=
let I2 := fresh "P" I1 in ximpl as I1 I2.
Ltac get_decoded v :=
match v with
| ?_A1 ?V => constr:(_A1,V)
| ?_A1 ?_A2 ?V => constr:(_A1 _A2, V)
| ?_A1 ?_A2 ?_A3 ?V => constr:(_A1 _A2 _A3, V)
| ?_A1 ?_A2 ?_A3 ?_A4 ?V => constr:(_A1 _A2 _A3 _A4, V)
| ?_A1 ?_A2 ?_A3 ?_A4 ?_A5 ?V => constr:(_A1 _A2 _A3 _A4 _A5, V)
end.
Ltac xreturns_core :=
match goal with
| |- ?t >- ?B =>
match t with
| (\?v) => match get_decoded v with (?_A,?V) =>
apply (@bimpl_elim (>> _A st = V));
[ apply prove_returns | ] end
| (Exn ?C) => apply (@bimpl_elim (>! C));
[ apply prove_throws | ]
| _ => fail 1 "> xreturns does not apply to this goal"
end
| |- ?t >- Unspecified => apply behave_unspecified
end.
Tactic Notation "xreturns" :=
xreturns_core; try ximpl.
Tactic Notation "xreturns" "~" :=
xreturns; auto_tilde.
Tactic Notation "xreturns" "*" :=
xreturns; auto_star.
Tactic Notation "xreturns" "as" ident(I1) :=
xreturns_core; first [ ximpl as I1 | fail 1 "-> ximpl failed" ].
Tactic Notation "xreturns" "as" ident(I1) simple_intropattern(I2) :=
xreturns_core; first [ ximpl as I1 I2 | fail 1 "-> ximpl failed" ].
Tactic Notation "xreturns_noximpl" :=
xreturns_core.
Ltac is_trm_value t :=
let R := constr:(trm_to_val t) in
let R' := eval simpl in R in
match R' with
| Some ?v => ltac_true
| None => ltac_false
end.
Ltac get_trm_value t :=
let R := constr:(trm_to_val t) in
let R' := eval simpl in R in
match R' with
| Some ?v => v
| None => fail "term is not a value"
end.
Ltac prove_ctx :=
match goal with |- red_ctx ?C =>
match C with
| ctx_hole => apply red_ctx_hole
| ctx_app_1 _ => apply red_ctx_app_1
| ctx_app_2 _ => apply red_ctx_app_2
| ctx_try _ => apply red_ctx_try
| ctx_con_1_1 _ => apply red_ctx_con_1_1
| ctx_con_2_1 _ _ => apply red_ctx_con_2_1
| ctx_con_2_2 _ _ => apply red_ctx_con_2_2
| ctx_con_3_1 _ _ _ => apply red_ctx_con_3_1
| ctx_con_3_2 _ _ _ => apply red_ctx_con_3_2
| ctx_con_3_3 _ _ _ => apply red_ctx_con_3_3
| ctx_comp _ _ => apply red_ctx_comp; prove_ctx
end end.
Ltac unfold_ctx :=
unfold ctx_hole, ctx_try,
ctx_app_1, ctx_app_2, ctx_comp,
ctx_con_1_1, ctx_con_2_1, ctx_con_2_2,
ctx_con_3_1, ctx_con_3_2, ctx_con_3_3.
Ltac unfold_ctx_all :=
unfold ctx_hole, ctx_try,
ctx_app_1, ctx_app_2, ctx_comp,
ctx_con_1_1, ctx_con_2_1, ctx_con_2_2,
ctx_con_3_1, ctx_con_3_2, ctx_con_3_3 in *.
Ltac is_beta_redex t :=
match t with
| (\?v) => ltac_true
| (\?v1) ' (\?v2) => ltac_true
| (?t1) ' (\?v2) => is_beta_redex t1
| _ => ltac_false
end.
Ltac is_redex t :=
match t with
| (exn ?v1) ' (\?v2) => ltac_true
| ?t1 ' (exn ?v2) => ltac_true
| (\?v1) ' (\?v2) => ltac_true
| (?t1) ' (\?v2) => is_beta_redex t1
| ('try (exn ?v1) 'catch ?t2) => ltac_true
| 'try (\?v1) 'catch ?t2 => ltac_true
| trm_con ?c nil => ltac_true
| trm_con ?c ((exn ?v1)::?ts) => ltac_true
| trm_con ?c ((\?v1)::?ts) => is_redex (trm_con c ts)
| _ => is_trm_value t
end.
Definition ctx_marker (t:trm) := t.
Ltac get_red_ctx t :=
let get_ctx_comp C1t1 C2 :=
match C1t1 with (?C1,?T) =>
constr:(ctx_comp C2 C1, T) end in
match is_redex t with
| true => constr:(ctx_hole,t)
| false => match t with
| ?t1 ' \?v2 =>
let x := get_red_ctx t1 in
get_ctx_comp x (ctx_app_1 v2)
| ?t1 ' ?t2 =>
let x := get_red_ctx t2 in
get_ctx_comp x (ctx_app_2 t1)
| 'try ?t1 'catch ?t2 =>
let x := get_red_ctx t1 in
get_ctx_comp x (ctx_try t2)
| ?c#(?t1) =>
let x := get_red_ctx t1 in
get_ctx_comp x (ctx_con_1_1 c)
| ?c#(\?v1,?t2) =>
let x := get_red_ctx t2 in
get_ctx_comp x (ctx_con_2_2 c v1)
| ?c#(?t1,?t2) =>
let x := get_red_ctx t1 in
get_ctx_comp x (ctx_con_2_1 c t2)
| ?c#(\?v1,\?v2,?t3) =>
let x := get_red_ctx t3 in
get_ctx_comp x (ctx_con_3_3 c v1 v2)
| ?c#(\?v1,?t2,?t3) =>
let x := get_red_ctx t2 in
get_ctx_comp x (ctx_con_3_2 c v1 t3)
| ?c#(?t1,?t2,?t3) =>
let x := get_red_ctx t1 in
get_ctx_comp x (ctx_con_3_1 c t2 t3)
| ctx_marker ?t' => constr:(ctx_hole,t')
| _ => fail 2 "-> cannot find reduction context"
end end.
Ltac get_red_ctx_goal :=
match goal with |- ?t >- ?B => get_red_ctx t end.
Ltac get_ctx_arity N t :=
let rec aux t :=
match t with
| (?t1 ' \ ?v2) =>
match aux t1 with
| (?C,?T) => constr:(ctx_comp (ctx_app_1 v2) C, T)
| N => constr:(ctx_hole, t)
| ?k => constr:(S k)
end
| _ => constr:(1)
end in
match aux t with
| (?C,?t1) => constr:(C,t1)
| _ => fail 1 "-> error in get_ctx_arity"
end.
Ltac get_red_ctx_goal_arity N :=
match get_red_ctx_goal with (?C1,?t1) =>
match get_ctx_arity N t1 with (?C2,?t2) =>
constr:(ctx_comp C1 C2, t2) end end.
Ltac get_ctx_visible C t1 :=
match goal with |- ?t >- ?B =>
let H := fresh in
asserts H: ((C t1) >- B); [ | exact H ] end.
Ltac get_red_ctx_visible :=
match get_red_ctx_goal with (?C,?t1) =>
get_ctx_visible C t1 end.
Ltac get_val_fix max_depth v :=
match max_depth with
| O => fail
| S ?max_depth' =>
match v with
| val_fix _ _ _ _ => v
| _Val ?v' => get_val_fix max_depth' v'
| ?f => let v' := (eval unfold f in v) in
get_val_fix max_depth' v'
end end.
Ltac xred_beta_instantiate t :=
match t with (\ ?F ' \ ?v) =>
let FU := get_val_fix 5 F in
match FU with
| val_fix novar ?p ?t1 ?t2 =>
let rbase := constr:(match matching p v with
| None => t2 ' v
| Some m => subst m t1
end) in
let r := (eval simpl in rbase) in
constr:(@red_beta_explicit r p t1 t2 v F)
| val_fix ?f ?p ?t1 ?t2 =>
let rbase := constr:(match matching p v with
| None => (subst (f ~> F) t2) ' v
| Some m => subst (m \U (f ~> F)) t1
end) in
let r := (eval simpl in rbase) in
constr:(@red_beta_fix_explicit r f p t1 t2 v F) end
end.
Ltac xred_val_instantiate t :=
let v := get_trm_value t in
constr:(@red_val v).
Ltac prove_red :=
match goal with |- ?t --> _ =>
first
[ let red_beta_inst := xred_beta_instantiate t in
sapply red_beta_inst; try solve [ unfold is_true; reflexivity ]
| let red_val_inst := xred_val_instantiate t in
sapply red_val_inst; try reflexivity
| match t with ((\ val_builtin ?b) ' ?t2) =>
first [ sapply red_throw
| sapply red_add
| sapply red_sub
| sapply red_mul
| sapply red_sub
| sapply red_div
| sapply red_equ
| sapply red_leq ]
end
| sapply red_exn_app_2
| sapply red_exn_app_1
| sapply red_exn_con
| sapply red_try_exn
| sapply red_try_val
]
end.
Ltac xred_ctx C t1 :=
eapply (@ctx_behave_red C t1);
[ first [ prove_red | fail 2 "-> No reduction possible" ]
| try prove_ctx
| try unfold_ctx ].
Ltac xredfun :=
apply behave_red_beta_fun_val ||
(apply behave_red_beta_fun_trm; [ reflexivity | ]);
simpl subst.
Ltac xredfail := apply behave_red_beta_fail.
Ltac xred_base :=
xredfun ||
match get_red_ctx_goal with (?C,?t1) => xred_ctx C t1 end.
Ltac xreds_step :=
match goal with
| |- \?v >- ?B => fail 1
| |- exn ?v >- ?B => fail 1
| _ => xred_base
end.
Tactic Notation "xred" :=
xred_base.
Tactic Notation "xred" "*" :=
xred; auto*.
Tactic Notation "xreds" integer(n) :=
do n xred.
Tactic Notation "xreds" "*" integer(n) :=
do n xred; auto*.
Tactic Notation "xreds" :=
repeat xreds_step.
Ltac xred_arity N :=
match get_red_ctx_goal_arity N with (?C,?t1) =>
xred_ctx C t1 end.
Tactic Notation "xred1" :=
xred_arity 1.
Ltac xreds1_base N :=
match N with
| 0 => fail 2
| S 0 => xred1
| S ?N' => xred1; xred; xreds1_base N'
end.
Tactic Notation "xreds1" constr(N) :=
xreds1_base N.
Ltac xpat_base :=
match get_red_ctx_goal with
| (?C, \ ?F ' \ ?v) =>
match get_val_fix 5 F with val_fix ?f ?p ?t1 ?t2 =>
first
[ let r1 := constr:(matching p v) in
let r2 := eval simpl in r1 in
match r2 with
| None => xred; xpat_base
| Some _ => xred
end
| fail 3 "-> error in xpat_base" ]
end
| (?C, trm_fix novar _ _ _) => xred; xpat_base
| _ => fail 1 "-> cannot find a match to reduce"
end.
Tactic Notation "xpat" :=
xpat_base.
Ltac xcase_cont hasI I :=
match get_red_ctx_goal with
| (?C, (\ ?F ' \ ?v)) =>
match get_decoded v with
| (_Bool, ?V) => match hasI with
| true => testb I: V
| false => testb: V
end
| (?_A, ?V) => match hasI with
| true => destruct V as I
| false => destruct V
end
| _ => fail 2 "-> matched value should be decoded"
end
| (?C, ?t) => xred; xcase_cont hasI I
| _ => fail 1 "-> cannot find a value as argument of match"
end.
Tactic Notation "xcase" :=
xcase_cont false ltac_no_arg; xpat_base.
Tactic Notation "xcase" "as" simple_intropattern(I) :=
xcase_cont true I; xpat_base.
Ltac xfct :=
xred; try xred; apply prove_returns_fun.
Tactic Notation "xintros" simple_intropattern(X1) :=
intros X1.
Tactic Notation "xintros" simple_intropattern(X1)
simple_intropattern(X2) :=
intros X1; xfct; xintros X2.
Tactic Notation "xintros" simple_intropattern(X1)
simple_intropattern(X2) simple_intropattern(X3) :=
intros X1; xfct; xintros X2 X3.
Tactic Notation "xintros" simple_intropattern(X1)
simple_intropattern(X2) simple_intropattern(X3)
simple_intropattern(X4) :=
intros X1; xfct; xintros X2 X3 X4.
Ltac prove_curry :=
solve [
let x1 := fresh "arg" in let x2 := fresh "arg" in
let x3 := fresh "arg" in let x4 := fresh "arg" in
match goal with
| |- curried1 _ _ => xintros x1; auto
| |- curried2 _ _ _ => xintros x1 x2; auto
| |- curried3 _ _ _ _ => xintros x1 x2 x3; auto
| |- curried4 _ _ _ _ _ => xintros x1 x2 x3 x4; auto
end ].
Ltac prove_descr :=
solve [ split; intros; [ apply* behave_red_back
| apply* behave_red ] ].
Ltac prove_descr_precise :=
let t := fresh "t" in let t' := fresh "t'" in
let Red := fresh "Red" in let P := fresh "P" in
intros; cbv beta; intros t t' Red; split;
intros Pt; intros_all;
[ apply (@behave_red_back t) | apply (@behave_red t') ];
solve [ eauto ].
Ltac xintros_all_base cont :=
first [ apply spec1_intro
| apply spec2_intro
| apply spec3_intro ];
[ try prove_curry | try prove_descr | cont ].
Tactic Notation "xintros_all" ident(X1) :=
xintros_all_base ltac:(intros X1).
Tactic Notation "xintros_all" ident(X1) ident(X2) :=
xintros_all_base ltac:(intros X1 X2).
Tactic Notation "xintros_all" ident(X1) ident(X2) ident(X3) :=
xintros_all_base ltac:(intros X1 X2 X3).
Ltac xname_func_base X :=
let name f := (set (X := f)) in
match goal with
| |- Spec1 _ _ ?f => name f
| |- Spec2 _ _ _ ?f => name f
| |- Spec3 _ _ _ _ ?f => name f
| |- Spec4 _ _ _ _ _ ?f => name f
| _ => progress (unfolds); xname_func_base X
end.
Tactic Notation "xname_func" ident(X) :=
xname_func_base X.
Ltac xname_spec_base X :=
let name f :=
pattern f;
match goal with |- ?P _ => set (X := P) in |- end;
(unfold X)
in
match goal with
| |- Spec1 _ _ ?f => name f
| |- Spec2 _ _ _ ?f => name f
| |- Spec3 _ _ _ _ ?f => name f
| |- Spec4 _ _ _ _ _ ?f => name f
| _ => progress (unfolds); xname_spec_base X
end.
Tactic Notation "xname_spec" ident(X) :=
xname_spec_base X.
Ltac xin_base arg :=
match get_red_ctx_goal with (?C,?t1) => first
[ apply (@ctx_focus C t1 arg)
| refine (@ctx_focus C t1 _ _ arg _) ]
end.
Ltac xin_arity_base N B1 :=
match get_red_ctx_goal_arity N with (?C,?t) =>
apply (@ctx_focus C t B1) end.
Tactic Notation "xin" constr(B1) :=
xin_base B1.
Tactic Notation "xin" :=
let B1 := fresh in evar(B1:behaviour); xin B1; subst B1.
Tactic Notation "xin_arity" constr(N) :=
let B1 := fresh in evar(B1:behaviour); xin_arity_base N B1; subst B1.
Ltac xout_base X PX :=
let t1r := fresh in let Beh := fresh in
intros t1r Beh;
match type of Beh with
| _ >> _ st _ => apply (ctx_returns Beh);
[ prove_ctx | intros X PX ]
| _ >! _ => apply (ctx_throws Beh); [ prove_ctx | ]
| _ >oo => apply (ctx_diverges Beh); [ prove_ctx ]
| _ >? => apply (ctx_unspecified Beh)
| _ => fail 1 "-> xout requires the behaviour to be known (try simpl?)"
end; clear t1r Beh; unfold_ctx.
Tactic Notation "xout" "as"
simple_intropattern(X) simple_intropattern(PX) :=
xout_base X PX.
Tactic Notation "xout" "as" simple_intropattern(X) :=
let PX := fresh "P" X in xout as X PX.
Tactic Notation "xout" :=
let X := fresh "X" in xout as X.
Tactic Notation "xouts" :=
let X := fresh "X" in xout as X; subst X.
Tactic Notation "xinout" constr(B1) :=
xin B1; [ | xout ].
Tactic Notation "xinout" constr(B1) "as" simple_intropattern(X) :=
xin B1; [ | xout as X ].
Tactic Notation "xinout" constr(B1) "as" simple_intropattern(X)
simple_intropattern(PX) :=
xin B1; [ | xout as X PX ].
Tactic Notation "xinouts" constr(B1) :=
xin B1; [ | xouts ].
Tactic Notation "xinout" "~" :=
xin; [ eauto | xout ].
Tactic Notation "xinout" "~" "as" simple_intropattern(X) :=
xin; [ eauto | xout as X ].
Tactic Notation "xinout" "~" "as" simple_intropattern(X)
simple_intropattern(PX) :=
xin; [ eauto | xout as X PX ].
Tactic Notation "xinouts" "~" :=
xin; [ eauto | xouts ].
Ltac xinfun_base Sof X SX :=
xin (>> _Val st Sof);
[ try xred; apply prove_returns_fun; xname_func X
| xout as X SX; try xred ].
Tactic Notation "xinfun" constr(Sof) "as" ident(X) ident(SX) :=
xinfun_base Sof X SX.
Tactic Notation "xinfun" constr(B1) "as" ident(X) :=
let SX := fresh "S" X in xinfun B1 as X SX.
Tactic Notation "xinfun" constr(B1) :=
let X := fresh "aux" in xinfun B1 as X.
Ltac xweaken_base arg cont1 cont2 :=
match type of arg with
| ltac_no_arg_type => eapply bimpl_elim; [ cont1 | cont2 ]
| behaviour => apply (@bimpl_elim arg); [ cont1 | cont2 ]
| ?t >- ?B => apply (bimpl_elim arg); cont2
| _ => fail 1 "-> invalid argument for ximpl_from"
end.
Tactic Notation "xweaken" :=
xweaken_base ltac_no_arg idtac idtac.
Tactic Notation "xweaken" "~" :=
xweaken_base ltac_no_arg ltac:(solve[eauto]) ltac:(ximpl).
Tactic Notation "xweaken" constr(A) :=
xweaken_base A idtac ltac:(ximpl).
Tactic Notation "xweaken" "~" "as" ident(I1) :=
xweaken_base ltac_no_arg ltac:(eauto) ltac:(ximpl as I1).
Tactic Notation "xweaken" constr(A) "as" ident(I1) :=
xweaken_base A idtac ltac:(ximpl as I1).
Tactic Notation "xweaken_noximpl" "~" :=
xweaken_base ltac_no_arg ltac:(solve [eauto]) idtac.
Tactic Notation "xweaken_noximpl" constr(A) :=
xweaken_base A idtac idtac.
Ltac prove_spec :=
solve [ eauto with specs ].
Ltac prove_spec_or_msg :=
first [ prove_spec | fail 1 "-> cannot find a spec" ].
Ltac fapplys_base E :=
let H := fresh in forwards H: E; try apply H.
Tactic Notation "fapplys" constr(E) :=
fapplys_base E.
Tactic Notation "fapplys" "~" constr(E) :=
fapplys E; auto_tilde.
Tactic Notation "fapplys" "*" constr(E) :=
fapplys E; auto_star.
Ltac prove_behave_from_spec :=
let t := fresh "t" in let H := fresh "Ht" in
cbv beta; intros t Ht;
first [ eapply Ht | fapplys Ht ]; try clear t Ht.
Ltac xapply_core lemma cont_spec cont_beh cont_out :=
try get_red_ctx_visible;
eapply lemma;
[ cont_spec
| first [ prove_ctx | idtac "Warning: cannot prove ctx" ]
| cont_beh
| cont_out ].
Ltac xapply_base_builder aux :=
match get_red_ctx_goal with (?C,?t) => match t with
| (\?F ' \?v1) =>
match get_decoded v1 with (?_A1,?V1) =>
aux (@spec1_elim_ctx C _ _A1) end
| (\?F ' \?v1 ' \?v2) =>
match get_decoded v1 with (?_A1,?V1) =>
match get_decoded v2 with (?_A2,?V2) =>
aux (@spec2_elim_ctx C _ _ _A1 _A2) end end
| (\?F ' \?v1 ' \?v2 ' \?v3) =>
match get_decoded v1 with (?_A1,?V1) =>
match get_decoded v2 with (?_A2,?V2) =>
match get_decoded v3 with (?_A3,?V3) =>
aux (@spec3_elim_ctx C _ _ _ _A1 _A2 _A3) end end end
| (\?F ' \?v1 ' \?v2 ' \?v3 ' \?v4) =>
match get_decoded v1 with (?_A1,?V1) =>
match get_decoded v2 with (?_A2,?V2) =>
match get_decoded v3 with (?_A3,?V3) =>
match get_decoded v4 with (?_A4,?V4) =>
aux (@spec4_elim_ctx C _ _ _ _ _A1 _A2 _A3 _A4) end end end end
end end.
Ltac xapply_base cont_spec cont_beh cont_out :=
let aux lemma :=
xapply_core lemma cont_spec cont_beh cont_out in
xapply_base_builder aux.
Ltac try_beh :=
try prove_behave_from_spec.
Tactic Notation "xapply_debug" :=
xapply_base ltac:(idtac) ltac:(idtac) ltac:(idtac).
Tactic Notation "xapply" :=
first
[ xapply_base ltac:(prove_spec_or_msg) ltac:(try_beh) ltac:(try xout)
| xapply_base ltac:(idtac) ltac:(idtac) ltac:(idtac) ].
Tactic Notation "xapply" "as" simple_intropattern(X) :=
xapply_base ltac:(prove_spec_or_msg) ltac:(try_beh) ltac:(xout as X).
Tactic Notation "xapply" "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply_base ltac:(prove_spec_or_msg) ltac:(try_beh) ltac:(xout as X PX).
Tactic Notation "xapplys" :=
xapply_base ltac:(prove_spec_or_msg) ltac:(try_beh) ltac:(xouts).
Tactic Notation "xapply" constr(E) :=
xapply_base ltac:(apply E) ltac:(try_beh) ltac:(try xout).
Tactic Notation "xapply" constr(E) "as" simple_intropattern(X) :=
xapply_base ltac:(apply E) ltac:(try_beh) ltac:(xout as X).
Tactic Notation "xapply" constr(E) "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply_base ltac:(apply E) ltac:(try_beh) ltac:(xout as X PX).
Tactic Notation "xapplys" constr(E) :=
xapply_base ltac:(apply E) ltac:(try_beh) ltac:(xouts).
Tactic Notation "xapply_noxout" constr(E) :=
xapply_base ltac:(apply E) ltac:(try_beh) ltac:(idtac).
Tactic Notation "xapply" "~" :=
xapply; auto_tilde.
Tactic Notation "xapply" "*" :=
xapply; auto_star.
Tactic Notation "xapplys" "~" :=
xapplys; auto_tilde.
Tactic Notation "xapplys" "*" :=
xapplys; auto_star.
Tactic Notation "xapplys" "~" constr(E) :=
xapplys E; auto_tilde.
Tactic Notation "xapplys" "*" constr(E) :=
xapplys E; auto_star.
Tactic Notation "xapply" "~" "as" simple_intropattern(X) :=
xapply as X; auto_tilde.
Tactic Notation "xapply" "*" "as" simple_intropattern(X) :=
xapply as X; auto_star.
Tactic Notation "xapply" "~" "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply as X PX; auto_tilde.
Tactic Notation "xapply" "*" "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply as X PX; auto_star.
Tactic Notation "xapply" "~" constr(E) :=
xapply E; auto_tilde.
Tactic Notation "xapply" "*" constr(E) :=
xapply E; auto_star.
Tactic Notation "xapply" "~" constr(E) "as" simple_intropattern(X) :=
xapply E as X; auto_tilde.
Tactic Notation "xapply" "*" constr(E) "as" simple_intropattern(X) :=
xapply E as X; auto_star.
Tactic Notation "xapply" "~" constr(E) "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply E as X PX; auto_tilde.
Tactic Notation "xapply" "*" constr(E) "as" simple_intropattern(X) simple_intropattern(PX) :=
xapply E as X PX; auto_star.
Ltac xweakens_base arg cont1 cont2 :=
match type of arg with
| ltac_no_arg_type => first
[ eapply spec4_weaken
| eapply spec3_weaken
| eapply spec2_weaken
| eapply spec1_weaken ]; [ cont1 | cont2 ]
| Spec1 _ _ _ => apply (spec1_weaken arg); cont2
| Spec2 _ _ _ _ => apply (spec2_weaken arg); cont2
| Spec3 _ _ _ _ _ => apply (spec3_weaken arg); cont2
| Spec4 _ _ _ _ _ _ => apply (spec4_weaken arg); cont2
| _ -> trm -> Prop =>
eapply spec1_weaken with (K1 := arg);
[ cont1 | cont2 ]
| _ -> behaviour =>
eapply spec1_weaken with (K1 := fun x1 t => t >- arg x1);
[ cont1 | cont2 ]
end.
Ltac xweaken_end :=
first [ ximpl
| let t := fresh "t" in let Pt := fresh "Pt" in
intros t Pt; hnf in Pt ].
Tactic Notation "xweakens_debug" :=
xweakens_base ltac_no_arg idtac idtac.
Tactic Notation "xweakens" :=
xweakens_base ltac_no_arg ltac:(prove_spec) idtac.
Tactic Notation "xweakens" constr(A) :=
xweakens_base A idtac idtac.
Tactic Notation "xweakens" "as" ident(X1) :=
xweakens_base ltac_no_arg ltac:(try prove_spec) ltac:(intros X1; xweaken_end).
Tactic Notation "xweakens" "as" ident(X1) ident(X2) :=
xweakens_base ltac_no_arg ltac:(try prove_spec) ltac:(intros X1 X2; xweaken_end).
Tactic Notation "xweakens" "as" ident(X1) ident(X2) ident(X3) :=
xweakens_base ltac_no_arg ltac:(try prove_spec) ltac:(intros X1 X2 X3; xweaken_end).
Tactic Notation "xweakens" "as" ident(X1) ident(X2) ident(X3) ident(X4) :=
xweakens_base ltac_no_arg ltac:(try prove_spec) ltac:(intros X1 X2 X3 X4; xweaken_end).
Tactic Notation "xweakens" constr(A) "as" ident(X1) :=
xweakens_base A idtac ltac:(intros X1; xweaken_end).
Tactic Notation "xweakens" constr(A) "as" ident(X1) ident(X2) :=
xweakens_base A idtac ltac:(intros X1 X2; xweaken_end).
Tactic Notation "xweakens" constr(A) "as" ident(X1) ident(X2) ident(X3) :=
xweakens_base A idtac ltac:(intros X1 X2 X3; xweaken_end).
Tactic Notation "xweakens" constr(A) "as" ident(X1) ident(X2) ident(X3) ident(X4) :=
xweakens_base A idtac ltac:(intros X1 X2 X3 X4; xweaken_end).
Tactic Notation "xweakens" "~" :=
xweakens; auto_tilde.
Tactic Notation "xweakens" "*" :=
xweakens; auto_star.
Tactic Notation "xweakens" "~" constr(A) :=
xweakens A; auto_tilde.
Tactic Notation "xweakens" "*" constr(A) :=
xweakens A; auto_star.
Inductive hint_type : forall A, A -> Type :=
| hint_intro : forall A x, @hint_type A x.
Inductive hint_code_type : Type :=
| hint : forall (A:Type) (x:code A), hint_code_type.
Ltac _hints hs :=
lets: (@hint_intro _ hs).
Ltac _next_hint :=
match goal with H: hint_type (?h::?hs) |- _ =>
clear H;
_hints hs;
_put h end.
Ltac _rem_hints :=
match goal with H: hint_type ?t |- _ => clear H end.
Ltac decode1 dec v :=
match v with
| val_nat ?n => _put2 _Int n
| val_int ?n => _put2 _Int n
| val_fix _ _ _ _ => _put2 _Val v
| val_con con_true nil => _put2 _Bool true
| val_con con_false nil => _put2 _Bool false
| (#(?v1,?v2))%val =>
dec v1; let _A1 := _get in _rem; let V1 := _get in _rem;
dec v2; let _A2 := _get in _rem; let V2 := _get in _rem;
_put2 (_Tup2 _A1 _A2) (V1,V2)
| (#(?v1,?v2,?v3))%val =>
dec v1; let _A1 := _get in _rem; let V1 := _get in _rem;
dec v2; let _A2 := _get in _rem; let V2 := _get in _rem;
dec v3; let _A3 := _get in _rem; let V3 := _get in _rem;
_put2 (_Tup3 _A1 _A2 _A3) (V1,V2,V3)
| ?_A1 ?v => _put2 _A1 v
| ?_A1 ?_A2 ?v => _put2 (_A1 _A2) v
| ?_A1 ?_A2 ?_A3 ?v => _put2 (_A1 _A2 _A3) v
| ?_A1 ?_A2 ?_A3 ?_A4 ?v => _put2 (_A1 _A2 _A3 _A4) v
| ?_A1 ?_A2 ?_A3 ?_A4 ?_A5 ?v => _put2 (_A1 _A2 _A3 _A4 _A5) v
| ?v => _put2 _Val v
end.
Ltac decode2 dec v :=
match v with
| val_con con_nil nil =>
match goal with
| H: hint_type ((@hint ?A ?_A)::?hs) |- _ =>
clear H; _hints hs; _put2 (_List _A) (@nil A)
| _ =>
let A := fresh in let _A := fresh in
evar (A:Type); evar (_A:A->val);
_put2 (_List _A) (@nil A); subst A _A
end
| val_con con_cons (?h::?t::nil) =>
first [
dec h; let _A := _get in _rem; let H := _get in _rem;
dec t; let _LA := _get in _rem; let T := _get in _rem;
_put2 (_List _A) (H::T)
| fail 10 "error on cons" ]
| _ => decode1 dec v
end.
Ltac decode_trm dec t :=
match t with
| \ ?v =>
dec v;
let _A := _get in _rem; let V := _get in _rem;
_put (\_A V)
| ?t1 ' ?t2 =>
decode_trm dec t1; let t1d := _get in _rem;
decode_trm dec t2; let t2d := _get in _rem;
_put (t1d ' t2d)
| _ => _put t
end.
Ltac get_decode_ctx :=
match goal with
| |- ?t >- ?B => get_red_ctx t
| |- ?t >- ?B => constr:(ctx_hole,t)
end.
Ltac xdecode_core decfct :=
match get_decode_ctx with (?C,?t1) =>
let rec dec v := decfct dec v in
decode_trm dec t1;
let t1d := _get in _rem;
apply (@ctx_rewrite C t1 t1d);
[ try reflexivity | unfold_ctx ]
end.
Ltac xdecode_with decfct hs :=
_hints hs; xdecode_core decfct;
match goal with
| H: hint_type (?h::?hs) |- _ =>
idtac "Warning: too many decoders"
| H: hint_type nil |- _ => clear H
end.
Ltac decode hs := xdecode_with decode2 hs.
Tactic Notation "xdecode" :=
decode (@nil hint_code_type).
Tactic Notation "xdecode" constr(h1) :=
decode ((hint h1)::nil).
Tactic Notation "#" tactic(tac) :=
xreds; xdecode; tac.
Ltac xinduction_base_lt lt :=
first
[ apply (@spec1_induction _ lt)
| apply (@spec2_induction _ _ lt)
| apply (@spec3_induction _ _ _ lt)
| apply (@spec4_induction _ _ _ _ lt)
| apply (@spec2_induction _ _ (decurrifyp2 lt))
| apply (@spec3_induction _ _ _ (decurrifyp3 lt))
| apply (@spec4_induction _ _ _ _ (decurrifyp4 lt)) ];
[ try prove_wf
| try prove_curry
| try prove_descr
| unfolds_wf ].
Ltac xinduction_base_wf wf :=
first
[ apply (spec1_induction wf)
| apply (spec2_induction wf)
| apply (spec3_induction wf)
| apply (spec4_induction wf) ];
[ try prove_curry | try prove_descr | unfolds_wf ].
Ltac xinduction_base_measure m :=
first
[ apply (spec1_induction (measure_wf m))
| apply (spec2_induction (measure_wf m))
| apply (spec3_induction (measure_wf m))
| apply (spec4_induction (measure_wf m))
| apply (spec2_induction (measure_wf (decurrify2 m)))
| apply (spec3_induction (measure_wf (decurrify3 m)))
| apply (spec4_induction (measure_wf (decurrify4 m))) ];
[ try prove_curry | try prove_descr | unfolds_wf ].
Tactic Notation "xinduction" constr(arg) :=
first [ xinduction_base_lt arg
| xinduction_base_wf arg
| xinduction_base_measure arg ].