(* Utilities (mostly tactics) used during the course *)

(* These are heavily work in progress, and understanding the
implementation shouldn't be required in order to use these. *)

(* Here be magic, beware *)



(*** Utils ***)

Ltac intro_clear :=
  let C := fresh "C" in
    intro C; clear C.

Ltac conv_error1 t1 t2 :=
  fail 1 t1 "is not convertible to" t2.

Ltac getgoal := match goal with |- ?G => G end.


Ltac check_change_goal goal :=
  first [change goal | let G := getgoal in conv_error1 G goal].
  



(*** Blocks ***)

Inductive Label (T : Type) := label.

Inductive End_Block {T : Type} (L : Label T) := end_block : Label T -> End_Block L.

Implicit Arguments end_block [T L].

(*
Ltac begin_label lab :=
  let G := getgoal in
    let L := lab in
      assert (lab : Label G); [exact (label G) | refine (block_result _ (block lab _ _))].
*)

Ltac begin_label lab :=
  let G := getgoal in
    let L := lab in
      let B := fresh "B" in
        let E := fresh "E" in
          assert (L : Label G); 
            [exact (label G) 
              | refine (let B : G := _ in let E : End_Block L := _ in B);
                [ |clear B]].

Ltac begin_label_with_type lab typ :=
  check_change_goal typ; begin_label lab.
      

Tactic Notation "begin" ident(lab) := begin_label lab.

Tactic Notation "begin" ident(lab) ":" constr(t) := begin_label_with_type lab t.

Ltac end_label lab :=
  match goal with 
  | |- End_Block lab => exact (end_block lab)
  | |- End_Block ?l => fail 1 "Currently at end of block" l
  | |- _ => fail 1 "Not at the end of a block"
  end.

Tactic Notation "end" hyp(lab) := end_label lab.

Goal True.
begin true.
exact I.
end true.
Abort.


(* Claims

Definition claim A B (a : forall L, Block A L) (f : A -> B) : B :=
  f (labeled _ a).

Ltac claim_tac' var typ :=
  refine (claim typ _ _ _); [intro var ; refine (block _ var _ _) |].

Ltac claim_tac'' var typ :=
  assert typ as var; 
  [assert Label as var; [exact label | refine (begin _ var _ _)] | ].

Ltac claim_tac var typ :=
  assert typ as var; 
  [ assert Label as var; 
    [ exact label 
    | let res := fresh var "_claim" in
      let endv := fresh var "_end" in
      assert typ as res; 
      [ 
      | assert (End_Block var) as endv; 
        [ clear res
        | exact res]]]
   | ].
  
Tactic Notation "claim" ident(var) ":" constr(typ) :=
  claim_tac var typ.


*)

Ltac solve_by_using hyps tac := generalize hyps; clear; intros; solve [tac].

Tactic Notation "solve" "using" tactic(tac) "on" constr_list(hyps) :=
  solve_by_using hyps tac.


(** * Induction **)

Definition ElimGoal {X Y} (A : X) (B : Y) := B.

Inductive ElimDep (T : Type) := elim_dep.

Definition ElimVar {T : Type} (t : T) := t.


Ltac push_dep a := 
  let T := type of a in
    revert a; assert (a : ElimDep T); [exact (elim_dep T)|].
Ltac push_deps0 := idtac.
Ltac push_deps1 a := push_dep a; push_deps0.
Ltac push_deps2 a b := push_dep b; push_deps1 a.
Ltac push_deps3 a b c := push_dep c; push_deps2 a b.



Ltac mark_goal term :=
  let G := getgoal in change (ElimGoal term G).
  
Ltac induction_on term push := 
  mark_goal term; push; elim term.


Ltac induction_on_as i v push := 
  let T := type of i in
    pose (v := (i : ElimVar T));
      change (i : ElimVar T) with i in v;
        induction_on i push.



Tactic Notation "per" "induction" "on" constr(a) := 
  induction_on a ltac:push_deps0.
Tactic Notation "per" "induction" "on" constr(a) "as" ident(IH) := 
  induction_on_as a IH ltac:push_deps0.
Tactic Notation "per" "induction" "on" constr(a) "as" ident(IH) "in" hyp(d1) := 
  induction_on_as a IH ltac:(push_deps1 d1).
Tactic Notation "per" "induction" "on" constr(a) "as" ident(IH) "in" hyp(d1) hyp(d2) := 
  induction_on_as a IH ltac:(push_deps2 d1 d2).
Tactic Notation "per" "induction" "on" constr(a) "in" hyp(d1) := 
  induction_on a ltac:(push_deps1 d1).
Tactic Notation "per" "induction" "on" constr(a) "in" hyp(d1) hyp(d2) := 
  induction_on a ltac:(push_deps2 d1 d2).

Ltac cases_on term push :=
  mark_goal term; push; case term.

Tactic Notation "per" "cases" "on" constr(a) :=
  cases_on a ltac:(push_deps0).

Tactic Notation "per" "cases" "on" constr(a) "in" hyp(d1) :=
  cases_on a ltac:(push_deps1 d1).

Tactic Notation "per" "cases" "on" constr(a) "in" hyp(d1) hyp(d2) :=
  cases_on a ltac:(push_deps2 d1 d2).








(** Induction cases **)


Ltac check_next_hyp truek falsek :=
  match goal with
  | |- ElimGoal _ _ -> _ => truek
  | |- (_ -> ElimGoal _ _) -> _ => truek
  | |- (_ -> _ -> ElimGoal _ _) -> _ => truek
  | |- (_ -> _ -> _ -> ElimGoal _ _) -> _ => truek
  | |- _ => falsek
  end.
  

Ltac getind m k :=
  intro m;
    let H := fresh "H" in
      check_next_hyp 
      ltac:(intro H; k; unfold ElimGoal in H; revert H)
      k.

Ltac getind0 k := k.
Ltac getind1 m0 k := getind m0 ltac:(getind0 k).
Ltac getind2 m0 m1 k := getind m0 ltac:(getind1 m1 k).
Ltac getind3 m0 m1 m2 k := getind m0 ltac:(getind2 m1 m2 k).




Ltac pop_deps :=
  match goal with 
  | |- ElimGoal _ _ => idtac
  | D : ElimDep _ |- _ -> _ => clear D; intro D; pop_deps
  | _ => fail 1 "Error when popping dependencies. Not in induction?"
  end.


Ltac check_ind := match goal with
  | |- ElimGoal _ _ => idtac
  | |- _ -> ElimGoal _ _ => idtac
  | |- _ -> _ -> ElimGoal _ _ => idtac
  | |- _ -> _ -> _ -> ElimGoal _ _ => idtac
  | |- _ -> _ -> _ -> _ -> ElimGoal _ _ => idtac
  | |- _ => fail 1 "not doing induction"
  end.

Ltac getcase k := match goal with
  | |- ElimGoal (?t _ _ _ _ _ _) _ => k (t, 6)
  | |- ElimGoal (?t _ _ _ _ _) _ => k (t, 5)
  | |- ElimGoal (?t _ _ _ _) _ => k (t, 4)
  | |- ElimGoal (?t _ _ _) _ => k (t, 3)
  | |- ElimGoal (?t _ _) _ => k (t, 2)
  | |- ElimGoal (?t _) _ => k (t, 1)
  | |- ElimGoal ?t _ => k (t, 0)
  | |- _ => fail 1 "Not in induction"
  end.

Ltac skip_till_indgoal := match goal with
  | |- _ -> _ => intro_clear; skip_till_indgoal
  end.

Ltac err_cont real_con real_arity := match real_arity with
  | 0 => fail "Now in case" real_con
  | 1 => fail "Now in case (" real_con "_)"
  | 2 => fail "Now in case (" real_con "_ _)"
  | 3 => fail "Now in case (" real_con "_ _ _)"
  | 4 => fail "Now in case (" real_con "_ _ _ _)"
  | 5 => fail "Now in case (" real_con "_ _ _ _ _)"
  end.
Ltac do_err c a :=
  skip_till_indgoal; getcase ltac:(err_cont).


Ltac getcase0 := match goal with
  | |- ElimGoal ?t _ => t
  | |- _ -> ElimGoal ?t _ => t
  | |- _ -> _ -> ElimGoal ?t _ => t
  | |- _ -> _ -> _ -> ElimGoal ?t _ => t
  | |- _ -> _ -> _ -> _ -> ElimGoal ?t _ => t
  | |- _ => fail 1 "bad arity"
  end.

Ltac getcase1 := match goal with
  | |- ElimGoal (?t _) _ => t
  | |- _ -> ElimGoal (?t _) _ => t
  | |- _ -> _ -> ElimGoal (?t _) _ => t
  | |- _ -> _ -> _ -> ElimGoal (?t _) _ => t
  | |- _ -> _ -> _ -> _ -> ElimGoal (?t _) _ => t
  | |- _ => fail 1 "bad arity"
  end.

Ltac checkcase actual expected := 
  match actual with
    | expected => idtac
    | _ => fail 1 "Now in case" actual ", not" expected
  end.

Ltac checkcase0 c := checkcase getcase0 c.

Ltac checkcase1 c := checkcase getcase1 c.

Ltac set_indvar val := match goal with
  | I : ElimVar _ |- _ => clear I; pose (I := val)
  | _ => idtac
  end.


Ltac check_goal val := match goal with
  | |- ElimGoal val _ => unfold ElimGoal
  | |- ElimGoal ?t  _ => fail 1 "wrong case:" t
  | |- _ => fail 1 "no goal in sight"
  end.

Ltac finish_suppose val :=
  pop_deps;
  set_indvar val;
  check_goal val.

Ltac suppose_tac checkget val :=
  checkget; set_indvar val; pop_deps; unfold ElimGoal.

Tactic Notation "suppose" "it" "is" constr(c) :=
  checkcase0 c; getind0 ltac:(set_indvar c; pop_deps); unfold ElimGoal.
Tactic Notation "suppose" "it" "is" "(" constr(c) ")" :=
  checkcase0 c; getind0 ltac:(set_indvar c; pop_deps); unfold ElimGoal.
Tactic Notation "suppose" "it" "is" "(" constr(c) ident(a) ")" :=
  checkcase1 c; getind1 a ltac:(set_indvar (c a); pop_deps); unfold ElimGoal.
Tactic Notation "suppose" "it" "is" "(" constr(c) ident(a) ident(b) ")" :=
  checkcase1 c; getind2 a b ltac:(set_indvar (c a b); pop_deps); unfold ElimGoal.



Ltac default_justify :=
  solve [auto | congruence | firstorder auto | firstorder congruence].

Ltac with_hyps hyps tac := 
  generalize hyps; clear; tac.

Ltac replace_goal_by newgoal :=
  let G := getgoal in
    let R := fresh "R" in
      assert (R : G = newgoal); [ | rewrite R; clear R].

Ltac prove_by_using hyps tac :=
  solve [with_hyps hyps tac] || fail "Couldn't solve the goal".


Tactic Notation (at level 3) "prove" "by" constr_list(reasons) "using" tactic(tac) 
  := prove_by_using reasons tac.

Tactic Notation (at level 3) 
"prove" constr(goal) "by" constr_list(reasons) "using" tactic(tac) 
  := check_change_goal(goal); prove_by_using reasons tac.

Tactic Notation (at level 3) "prove" "by" constr_list(reasons)
  := prove by reasons using default_justify.

Tactic Notation (at level 3) "prove" "using" tactic(tac) 
  := prove by using tac.

Tactic Notation (at level 3) "prove" constr(goal) "using" tactic(tac) 
  := check_change_goal(goal); prove using tac.

Tactic Notation (at level 3) "prove" "by" constr_list(reasons)
  := prove_by_using reasons default_justify.

Tactic Notation (at level 3) "prove" constr(goal) := 
  prove goal using default_justify.

Tactic Notation (at level 3) "prove" := 
  prove using default_justify.





Ltac let1 t H1 := intro H1; 
  first [(change t in H1; idtac) | let t1 := type of H1 in conv_error1 t1 t].
Ltac let2 t H1 H2 := let1 t H1; let1 t H2.
Ltac let3 t H1 H2 H3 := let1 t H1; let2 t H2 H3.
Ltac let4 t H1 H2 H3 H4 := let1 t H1; let3 t H2 H3 H4.




Tactic Notation "assume" ident(H1) ":" constr(t) := let1 t H1.
Tactic Notation "assume" ident(H1) ident(H2) ":" constr(t)  := let2 t H1 H2.
Tactic Notation "assume" ident(H1) ident(H2) ident(H3) ":" constr(t) := let3 t H1 H2 H3.



Ltac suffices1_as t H :=
  let G := getgoal in
    refine ((_ : t -> G) (_ : t)); [assume H : t |].

Tactic Notation "suffices" constr(t1) "as" ident(H1) :=
  suffices1_as t1 H1.

Ltac suffices2_as t1 H1 t2 H2 :=
  let G := getgoal in
    refine ((_ : t1 -> t2 -> G) (_ : t1) (_ : t2)); [assume H1 : t1; assume H2 : t2 |].

Tactic Notation "suffices" constr(t1) "as" ident(H1) "and" constr(t2) "as" ident(H2) :=
  suffices2_as t1 H1 t2 H2.