(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export bg_require.

(*#* #stop file *)

      Tactic Definition XLApply H :=
         LApply H; [ Clear H; Intros H | XAuto ].

      Tactic Definition XAuto := Auto with ld.

      Tactic Definition XDEAuto d := EAuto d with ld.

      Tactic Definition XElimUsing e v :=
         Try Intros until v; Elim v using e; Try Clear v.

      Tactic Definition XElim v := Try Intros until v; Elim v; Try Clear v.

      Tactic Definition XInv :=
         Try Match Context With
            | [ H: ?0 = ?0 |- ? ] -> Clear H
            | [ H: ? = ? |- ? ] -> Discriminate H Orelse (Injection H; Clear H; Intros).

      Tactic Definition XReplaceIn Z0 y1 y2 :=
         Cut y1=y2; [ Intros Z; Rewrite Z in Z0; Clear Z | XAuto ].

(*#* #start file *)

      Lemma insert_eq: (S:Set; x:S; P:S->Prop; G:S->Prop)
                       ((y:S) (P y) -> y = x -> (G y)) -> (P x) -> (G x).
      Proof.
      XAuto.
      Qed.

(*#* #stop file *)

      Tactic Definition InsertEq H y :=
         Pattern 1 y in H; Match Context With [ _: (?1 y) |- ? ] ->
         Apply insert_eq with x:=y P:=?1;
         [ Clear H; Intros until 1 | Pattern y; Apply H ].

(*#* #start file *)

      Lemma unintro : (A:Set; a:A; P:A->Prop) ((x:A) (P x)) -> (P a).
      Proof.
      XAuto.
      Qed.

(*#* #stop file *)

      Tactic Definition UnIntroLast :=
         Match Context With [ y: ?1 |- ?2 ] ->
            Apply (unintro ?1 y); Clear y.

      Tactic Definition UnIntro Last H :=
         Move H after Last; UnIntroLast.

      Tactic Definition DecFalse := Right; Intros; XInv; Subst.

      Tactic Definition XPose H t :=
         Pose H := t; ClearBody H.

      Tactic Definition XPoseClear H t :=
         XPose H_y t; Clear H; Rename H_y into H.

      Tactic Definition ImplLast :=
         Match Context With
            | [ H: ?1 |- ? ] -> Cut ?1; [ Clear H | Assumption ].

      Tactic Definition Impl Last H :=
         Move H after Last; ImplLast.

      Tactic Definition NonLinear :=
         Match Context With
            [ H: ?1 |- ? ] -> Cut ?1; [ Intro | XAuto ].

      Tactic Definition XRewrite x :=
         Match Context With
            | [ H0: x = ? |- ? ] -> Try Rewrite H0
            | [ H0: ? = x |- ? ] -> Try Rewrite <- H0
            | _                  -> Idtac.

(*#* #start file *)

      Lemma xinduction: (A:Set; t:A; P:A->Prop)
                        ((x:A) t=x -> (P x)) -> (P t).
      Proof.
      XAuto.
      Qed.

      Tactic Definition XInduction t :=
         Apply (xinduction ? t); Intros x_x; XElim x_x; Intros.