(**************************************************************************
* Proving functional programs through a deep embedding                    *
* Tactics for applying reasoning rules on embedded programs               *
***************************************************************************)

Set Implicit Arguments.
Require Export DeepReasoning.

(** This file contains a number of tactics that can be used to carry
    out verification of embedded code. Thanks to these tactics, the
    reasoning rules (in file [DeepReasoning.v]) never need to be
    applied manually. The tactics thereby help to make the proof 
    scripts shorter and more robust on change. 
    
    Tactics intended for use by the user start with letter "x",
    e.g. [xreturns] or [xapply] and are defined using 
    [Tactic Notation]. Other tactics, defined with [Ltac],
    are only there for implementation purposes. *)


(************************************************************)
(* ** Implication between behaviours: [ximpl] *)

(** [ximpl] expects a goal of the form [B1 ==> B2] or
    its unfolding [forall t, t >- B1 -> t >- B2].
    It applies the most appropriate reasoning rule for
    simplifying this goal, and possibly solves it.
    Some of the reasoning rules leave a subgoal of
    the form [forall X, P X -> ...], in which case
    the hypotheses can be introduced using the syntax
    [ximpl as X H]. The shorter form [ximpl as X] 
    is equivalent to [ximpl as X PX]. *)

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.


(************************************************************)
(* ** Helper function for analysing decoded values *)

(** [get_decoded v] applies when the value [v] is of the form
    [_A V] and [_A] is an encoder. It returns the pair 
    [(_A,V)] in this case. It fails otherwise. *)

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.


(************************************************************)
(* ** Behaviours of terminal terms: [xreturns] *)

(** [xreturns] applies to a goal of the form [t >- B] for a
    term [t] that has ended its evaluation, that is when
    [t] is a value or an exception.

    If the goal is [\_A V >- B] then [xreturns] will produce
    the goal [(>> _A st = V) ==> B]. If the goal is of the
    form [Exn V >- B] then [xreturns] will produce the goal
    [(>! v) ==> B].

    In both cases, tactic [ximpl] will be called on the 
    subgoal. Syntax [xreturns as X] and [xreturns as X PX]
    are provided to call [ximpl as X] and [ximpl as X PX].
    To avoid a call to [ximpl], use [xreturns_noximpl]. *)

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.


(************************************************************)
(* ** Helper functions for rule [trm-to-val] *)

(** [is_trm_value t] returns [true] if [t] can take a
    reduction step with rule [trm_to_val] (that is,
    if [t] is a value described in the syntax of terms).
    It returns [false] otherwise. *)

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.

(** [get_trm_value t] returns a value [v] that is the result
    of evaluating [trm_to_val t], whenever [t] describes
    a value in the syntax of terms. It fails otherwise. *)

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.


(************************************************************)
(* ** Reduction contexts *)

(** [prove_ctx] is a mini decision procedure which can
    solve any goal of the form [red_ctx C] when [C]
    is a composition of atomic contexts. *)

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.

(** [unfold_ctx] is a tactic that unfolds the definition
    of atomic contexts and context composition. 
    [unfold_ctx_all] is the same except that it performs
    the unfolding in the hypotheses as well as the goal. *)

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 *.


(************************************************************)
(* ** Find the reduction context *)

(** [is_beta_redex t] returns [true] if [t] is of the form
    [\v1 ' \v2 ' .. ' \vN] for any [N >= 1]. It returns
    [false] otherwise. *)

Ltac is_beta_redex t :=
  match t with
  | (\?v) => ltac_true
  | (\?v1) ' (\?v2) => ltac_true
  | (?t1) ' (\?v2) => is_beta_redex t1
  | _ => ltac_false
  end.

(** [is_redex t] returns [false] if [t] contains a
    strict subterm in evaluation position that has not 
    fully reduced. It returns [true] otherwise. *)

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.

(** [get_red_ctx t] returns a pair [(C,t1)] of a 
    reduction context [C] and a subterm [t1] of [t] 
    such that [t = C t1]. Moreover, the context [C] 
    returned is as deep as possible, with the exception
    that it leaves N-ary applications and does not go
    as far as isolating the application of a function
    on its first argument only.
    Remark: [C] is [ctx_hole] whenever [is_redex t].    
    The tactic fails if it cannot find a reduction context, 
    but this should not happen for well-formed terms. *)

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.

(** [get_red_ctx_goal] applies to a goal of the form
    [t >- B] and returns the result of [get_red_ctx t],
    i.e. a pair [(C,t1)] such that [t = C t1]. *)

Ltac get_red_ctx_goal :=
  match goal with |- ?t >- ?B => get_red_ctx t end.

(** [get_ctx_arity N t] applies to a term [t] which should 
    be of the form [\f ' \v1 ' \v2 ' .. ' \vK] and to
    an integer [N] such that [1 <= N <= K]. It returns
    a pair [(C,t1)] such that [t = C t1] and [t1] is
    equal to [\f ' \v1 ' \v2 ' .. ' \vN]. *)

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.

(** [get_red_ctx_goal_arity N] returns a pair [(C,t1)] 
    of a reduction context [C] and a subterm [t1] of 
    [t] such that [t = C t1] and [t1] is of the form
    [\f ' \v1 ' \v2 ' .. ' \vN]. The integer [N] 
    should be between 1 and the number of arguments
    to which the function in reduction position is
    being applied to, inclusively. The tactic fails
    if [N] is not in this range or if the term in
    evaluation position is not an application. *)

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.


(************************************************************)
(* ** Expliciting the reduction context *)

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. 


(************************************************************)
(* ** Compute contraction of redexes: [xred] *)

(** [get_val_fix d v] is a tactic that unfolds the definition
    in the value [v] until it finds a function of the form
    built with constructor [val_fix]. If it reaches such 
    a value, it returns it, otherwise it fails.
    The parameter [d] denotes the maximal number of unfold to 
    perform. *)

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.

(** [xred_beta_instantiate t] applies when [t]
    is a beta-redex, of the form [(\F ' \V)].
    It returns a version of lemma [red_beta_explicit] 
    instantiated with all the appropriate parameters.
    This lemma can be used to prove that [t] takes a 
    reduction step, and it mentions the term to which
    [t] reduces. *)


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.

(** [xred_val_instantiate t] returns a version of 
    lemma [red_val] with the appropriate instantiation,
    showing that [t] reduces to a value [v].
    The tactic fails if [is_trm_value t] is not [true]. *)

Ltac xred_val_instantiate t :=
   let v := get_trm_value t in
   constr:(@red_val v).

(** [prove_red] expects a goal of the form [t --> t'],
    in which [t] is a known term and [t'] is either
    a known term or an unification variable. This tactic
    solves the goal, as soon as it is possible by
    applying one of the reduction rules which is not
    a "reduction under context" rule. 
    If [t'] was an unification variable, then it 
    instantiates it entirely. *)

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.

(** [xred] applies to a goal of the form [t >- B] and
    replaces it with the goal [t' >- B] whenever there
    exists a [t'] such that [t --> t']. This tactic
    works even if the reduction happens under a
    reduction context. It fails if there does not
    exists such a [t']. 
    
    The tactic [xreds n] applies [n] times the tactic
    [xred]. The tactic [xreds] (without argument) repeats
    [xred] as long as necessary to reach a value, 
    an exception, or be stuck. Remark: calling [xreds]
    on a term that diverges will cause the tactic to 
    loop forever. *)

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.


(************************************************************)
(* ** Reduction of pattern-matching: [xpat] and [xcase] *)

(** [xpat] applies to a goal of the form [t >- B]
    when the term in the reduction position in [t]
    is of the form ['match \v 'with ..]. It then
    beta-reduces this pattern-matching expression. 
    This tactic should only be applied when the value [v]
    is a constructed value and not just a meta-variable,
    so that the match expression has a chance to effectively 
    simplify. *)

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.

(** [xcase] applies to a goal of the form [t >- B]
    when the term in the reduction position in [t]
    is of the form ['match \_A V 'with ..]. 
    It calls [destruct V] to perform a case analysis
    on [V], and reduces the pattern using [xpat] in
    each case. The syntax [xcase as I] is available
    in order to apply [destruct V as I]. *)
  
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.


(************************************************************)
(* ** Introduction of function arguments: [xintros] *)

(** [xintros x] applies to a goal of the form
    [spec f \[x1:_A1\] = t is K] and simplifies it
    to [K x t], where [x] is a fresh meta-variable
    and [t] is the result of beta-reducing [f ' (_A1 x)].
    This generalizes to higher arities, with the syntax
    [xintros x1 .. xN]. *)

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.


(** [xintros_all x1 .. xN] is a variation on [xintros]
    that does not perform any beta-reduction. *)

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).



(************************************************************)
(* ** Naming tactics *)

(** [xname_func X] applies to a goal of the form [spec f ...] 
    and sets the name [X] for the piece of code [f]. *)

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.


(** [xname_spec X] applies to a goal of the form [spec f ...] 
    and sets the name [X] for this specification, that is,
    it abstracts [f] from the current goal. *)

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.


(************************************************************)
(* ** Analysis in reduction context: [xin] and [xout] *)

(** [xin B1] applies to a goal of the form [t >- B].
    First, it finds the reduction context [C]
    and [t1] such that [t = C t1]. Then, it replaces
    the current goal with two subgoals: [t1 >- B1]
    and [forall t1, (t1 >- B1) -> (C t1 >- B)].
    The first subgoal corresponds to the analysis
    of the subterm in evaluation position. The second
    subgoal is to be used to deduce the behaviour
    of the entire term from the behaviour of the
    subterm, which can be performed automatically
    by the tactic [xout] defined further on. 

    Tactic [xin] (without argument) is the same
    as [xin B1] with [B1] a fresh unification variable.
    Tactic [xin_arity N] is the same as [xin] excepts
    that it consider not the standard reduction context
    but instead a reduction context which contains only
    an N-ary application, which is useful for reasoning
    on over-applications (see documentation of tactic
    [get_red_ctx_goal_arity] for more details). *)

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.

(** [xout] applies to a goal of the form 
    [forall t, (t >- B1) -> (C t >- B)] when
    the behaviour [B1] is known. It simplifies
    the goal according to the behaviour, using 
    lemmas [ctx_returns], [ctx_throws], [ctx_diverges],
    or [ctx_unspecified]. For instance, if [B1] is
    of the form [>> _A st P], then the goal is simplified
    to [C (_A X) >- B] for a fresh variable [X] and an
    hypothesis [P X] added to the context.
    
    The tactic [xout as X PX] or simply [xout as X]
    allows to name the created hypothesis. In the 
    particular case where [B1] is of the form [>> _A st = V],
    the tactic [xouts] simplifies the goal directly
    towards [C (_A V) >- B], and introduces no intermediate
    variable. *)

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.

(** [xinout B] is a shorthand for calling [xin B] and
    then [xout] on the second generated subgoal. 
    Syntaxes [xinout B as X] and [xinout B as X PX]
    and [xinouts B] are also available.
    [xinout~] and [xinout~ as X] and [xinout~ as X PX]
    and [xintouts~] can also be used when the first
    subgoal of [xin] is solved by [eauto]. *)

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.



(************************************************************)
(* ** Weakening of term behaviour: [xweaken] *)

(** [xweaken] applies to a goal of the form [t >- B2],
    and produces two subgoals: [t >- B1] and [B1 ==> B2].
    The behaviour [B1] may be provided explicitely
    with the syntax [xweaken B1], otherwise [B1] is
    introduced as a unification variable.

    On the second subgoal, of the form [B1 ==> B2],
    the tactic [ximpl] will be applied. The syntax
    [xweaken as X] allows to call [ximpl as X] 
    instead of just [ximpl]. To avoid any invokation
    of [ximpl], use the form [xweaken_noximpl]. *)

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.


(************************************************************)
(* ** Exploiting the database specifications *)

(** [prove_spec] applies to a goal of the form 
    [SpecN _A1 .. _AN K f]. It solves the goal if it can 
    find a specification for function [f] in the 
    hint database of specifications. It fails otherwise.
    
    To add a specification to the database, write:
    [Hint Resolve my_spec_lemma : specs.].
    The interest of using this database is that it avoids
    the need to explicitly providing the name of a
    specification lemma when reasoning on an application
    (see tactic [xapply] further on for more details). *)

Ltac prove_spec :=
  solve [ eauto with specs ].

Ltac prove_spec_or_msg :=
  first [ prove_spec | fail 1 "-> cannot find a spec" ].


(************************************************************)
(* ** Useful variation on [fapply] from [LibTactics]. *)

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.


(************************************************************)
(* ** Reasoning on function application: [xapply] *)

(** [prove_behave_from_spec] is an auxiliary tactic
    that expects a goal of the form 
    [forall t, (forall ..., t >- B1) -> (t >- B2)]
    where [B2] is a unification variable.
    It introduces [t] and the hypothesis [Ht] and
    proves the goal by applying [Ht], causing [B2]
    to be unified with [B1]. It produces subgoals
    corresponding to the premises of [Ht] 
    (marked as dots above), which intuitively 
    correspond to the pre-conditions of the function
    being analysed by tactic [xapply]. *)

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.

(** [xapply_core e c] is an auxiliary tactic that
    applies the lemma [e] which is supposed to be
    an instantiated version of a [specN_elim] lemma.
    It leaves subgoals corresponding to the pre-condition
    appearing in the specification being eliminated,
    plus a subgoal to be resolved by [xout],
    on which tactic [c] is applied. *)

Ltac xapply_core lemma cont_spec cont_beh cont_out :=
  (* -> next line required for unification to work *)
  try get_red_ctx_visible; 
  eapply lemma;
    [ cont_spec
    | first [ prove_ctx | idtac "Warning: cannot prove ctx" ]
    | cont_beh
    | cont_out ].

(** [xapply_base c] applies to a goal of the form
    [t >- B] where the subterm [t1] of [t] in
    evaluation position is an application. This
    tactic instantiate an elimination lemma [e]
    for specifications, and calls [xapply_core e c]. *)

Ltac xapply_base_builder aux :=
  (* -> big pattern matching required for unification to work *)
  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.
  (* -> to debug, use (xapply_base_builder ltac:(fun e => lets: e)) *)

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.

(** [xapply] tactics applies to a goal of the form [t >- B] 
    where the subterm [t1] of [t] in evaluation position
    is an application. It chances [t1] with the result of
    the evaluation, and produces subgoals for pre-conditions
    appearing in the specification being eliminated.
    Variations:
    - [xapplys], based on [xouts],
    - [xapply as X] is based on [xout as X],
    - [xapply as X PX] is based on [xout as X PX],    
    Moreover, if the name of a lemma is mentionned 
    after [xapply], it will be used in the elimination. *)

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.


(************************************************************)
(* ** Weakening of function specification: [xweakens] *)

(** [xweakens] applies to a goal of the form 
    [SpecN _A1 .. _AN K2 f]. It replaces the goal
    with two subgoals: [SpecN _A1 .. _AN K1 f] and
    [forall X1 .. XN t, K1 X1 .. XN t -> K2 X1 .. XN t].
    This tactic is used to weaken specifications.

    Variations are:
    - [xweakens~] to find a specification to weaken from
      in the database,
    - [xweakens S] to weaken from specification lemma [S],
    
    These tactics can be suffixed with [as X1 .. XN] to
    provide introduction names for the second subgoal.
    In this case, tactic [ximpl] will be tried on the
    remaining subgoal, and if it fails the variable
    [t] and the assumption on [t] will be simply introduced
    under fresh names. *)

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.


(************************************************************)
(* ** Ltac trick: hints for decoders *)

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.


(************************************************************)
(* ** Decoding of values *)

(** [xdecode], also written [#] as prefix of tactics,
    is able to recover the logical value corresponding
    to a program value. *)

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.


(************************************************************)
(* ** Induction *)

(** [xinduction] is used to prove specification by 
    induction: it weakens the specification to be proved. *)

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 ].