# Library Coq.Program.Tactics

This module implements various tactics used to simplify the goals produced by Program,
which are also generally useful.
Debugging tactics to show the goal during evaluation.

Ltac show_goal := match goal with [ |- ?T ] => idtac T end.

Ltac show_hyp id :=

match goal with

| [ H := ?b : ?T |- _ ] =>

match H with

| id => idtac id ":=" b ":" T

end

| [ H : ?T |- _ ] =>

match H with

| id => idtac id ":" T

end

end.

Ltac show_hyps :=

try match reverse goal with

| [ H : ?T |- _ ] => show_hyp H ; fail

end.

The do tactic but using a Coq-side nat.

Do something on the last hypothesis, or fail

Ltac on_last_hyp tac :=

lazymatch goal with [ H : _ |- _ ] => tac H end.

Destructs one pair, without care regarding naming.

Ltac destruct_one_pair :=

match goal with

| [H : (_ /\ _) |- _] => destruct H

| [H : prod _ _ |- _] => destruct H

end.

Repeateadly destruct pairs.

Ltac destruct_pairs := repeat (destruct_one_pair).

Destruct one existential package, keeping the name of the hypothesis for the first component.

Ltac destruct_one_ex :=

let tac H := let ph := fresh "H" in (destruct H as [H ph]) in

let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in

(destruct H as [H ph ph'])

in

let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in

let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in

(destruct H as [H ph ph'])

in

match goal with

| [H : (ex _) |- _] => tac H

| [H : (sig ?P) |- _ ] => tac H

| [H : (sigT ?P) |- _ ] => tacT H

| [H : (ex2 _ _) |- _] => tac2 H

| [H : (sig2 ?P _) |- _ ] => tac2 H

| [H : (sigT2 ?P _) |- _ ] => tacT2 H

end.

Repeateadly destruct existentials.

Ltac destruct_exists := repeat (destruct_one_ex).

Repeateadly destruct conjunctions and existentials.

Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).

Destruct an existential hypothesis t keeping its name for the first component
and using Ht for the second

Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].

Destruct a disjunction keeping its name in both subgoals.

Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].

Discriminate that also work on a x <> x hypothesis.

Ltac discriminates :=

match goal with

| [ H : ?x <> ?x |- _ ] => elim H ; reflexivity

| _ => discriminate

end.

Revert the last hypothesis.

Ltac revert_last :=

match goal with

[ H : _ |- _ ] => revert H

end.

Repeatedly reverse the last hypothesis, putting everything in the goal.

Ltac reverse := repeat revert_last.

Reverse everything up to hypothesis id (not included).

Ltac revert_until id :=

on_last_hyp ltac:(fun id' =>

match id' with

| id => idtac

| _ => revert id' ; revert_until id

end).

Clear duplicated hypotheses

Ltac clear_dup :=

match goal with

| [ H : ?X |- _ ] =>

match goal with

| [ H' : ?Y |- _ ] =>

match H with

| H' => fail 2

| _ => unify X Y ; (clear H' || clear H)

end

end

end.

Ltac clear_dups := repeat clear_dup.

Try to clear everything except some hyp

Ltac clear_except hyp :=

repeat match goal with [ H : _ |- _ ] =>

match H with

| hyp => fail 1

| _ => clear H

end

end.

A non-failing subst that substitutes as much as possible.

Ltac subst_no_fail :=

repeat (match goal with

[ H : ?X = ?Y |- _ ] => subst X || subst Y

end).

Tactic Notation "subst" "*" := subst_no_fail.

Ltac on_application f tac T :=

match T with

| context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c)

| context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b)

| context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a)

| context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)

| context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)

| context [f ?x ?y ?z ?w] => tac (f x y z w)

| context [f ?x ?y ?z] => tac (f x y z)

| context [f ?x ?y] => tac (f x y)

| context [f ?x] => tac (f x)

end.

A variant of apply using refine, doing as much conversion as necessary.

Ltac rapply p :=

before we try to add more underscores, first ensure that adding such underscores is valid

(assert_succeeds (idtac; let __ := open_constr:(p _) in idtac);

rapply uconstr:(p _))

|| refine p.

rapply uconstr:(p _))

|| refine p.

Tactical on_call f tac applies tac on any application of f in the hypothesis or goal.

Ltac on_call f tac :=

match goal with

| |- ?T => on_application f tac T

| H : ?T |- _ => on_application f tac T

end.

Ltac destruct_call f :=

let tac t := (destruct t) in on_call f tac.

Ltac destruct_calls f := repeat destruct_call f.

Ltac destruct_call_in f H :=

let tac t := (destruct t) in

let T := type of H in

on_application f tac T.

Ltac destruct_call_as f l :=

let tac t := (destruct t as l) in on_call f tac.

Ltac destruct_call_as_in f l H :=

let tac t := (destruct t as l) in

let T := type of H in

on_application f tac T.

Tactic Notation "destruct_call" constr(f) := destruct_call f.

Permit to name the results of destructing the call to f.

Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) :=

destruct_call_as f l.

Specify the hypothesis in which the call occurs as well.

Tactic Notation "destruct_call" constr(f) "in" hyp(id) :=

destruct_call_in f id.

Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) :=

destruct_call_as_in f l id.

A marker for prototypes to destruct.

Definition fix_proto {A : Type} (a : A) := a.

Register fix_proto as program.tactic.fix_proto.

Ltac destruct_rec_calls :=

match goal with

| [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H

end.

Ltac destruct_all_rec_calls :=

repeat destruct_rec_calls ; unfold fix_proto in *.

Try to inject any potential constructor equality hypothesis.

Ltac autoinjection tac :=

match goal with

| [ H : ?f ?a = ?f' ?a' |- _ ] => tac H

end.

Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.

Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)).

Destruct an hypothesis by first copying it to avoid dependencies.

Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.

If bang appears in the goal, it means that we have a proof of False and the goal is solved.

A tactic to show contradiction by first asserting an automatically provable hypothesis.

Tactic Notation "contradiction" "by" constr(t) :=

let H := fresh in assert t as H by auto with * ; contradiction.

let H := fresh in assert t as H by auto with * ; contradiction.

A tactic that adds H:=p:typeof(p) to the context if no hypothesis of the same type appears in the goal.
Useful to do saturation using tactics.

Ltac add_hypothesis H' p :=

match type of p with

?X =>

match goal with

| [ H : X |- _ ] => fail 1

| _ => set (H':=p) ; try (change p with H') ; clearbody H'

end

end.

A tactic to replace an hypothesis by another term.

Ltac replace_hyp H c :=

let H' := fresh "H" in

assert(H' := c) ; clear H ; rename H' into H.

A tactic to refine an hypothesis by supplying some of its arguments.

Ltac refine_hyp c :=

let tac H := replace_hyp H c in

match c with

| ?H _ => tac H

| ?H _ _ => tac H

| ?H _ _ _ => tac H

| ?H _ _ _ _ => tac H

| ?H _ _ _ _ _ => tac H

| ?H _ _ _ _ _ _ => tac H

| ?H _ _ _ _ _ _ _ => tac H

| ?H _ _ _ _ _ _ _ _ => tac H

end.

The default simplification tactic used by Program is defined by program_simpl, sometimes auto
is not enough, better rebind using Obligation Tactic := tac in this case,
possibly using program_simplify to use standard goal-cleaning tactics.

Ltac program_simplify :=

simpl; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in * );

subst*; autoinjections ; try discriminates ;

try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).

Restrict automation to propositional obligations.

Ltac program_solve_wf :=

match goal with

| |- well_founded _ => auto with *

| |- ?T => match type of T with Prop => auto end

end.

Create HintDb program discriminated.

Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf.

#[global] Obligation Tactic := program_simpl.

#[export] Obligation Tactic := program_simpl.