This file contains basic tactics and useful lemmas/types
Set Implicit Arguments.
Require Export Morphisms.

Usable version of iter: Taken from: http://www.ps.uni-saarland.de/courses/sem-ws17/confluence.v

Section Iter.
Variables (X: Type) (f: X -> X).

Fixpoint it n x : X :=
match n with
| 0 => x
| S n'=> f (it n' x)
end.

Fact it_shift n x :
f (it n x) = it n (f x).
Proof.
induction n; cbn; congruence.
Qed.

End Iter.

Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.

Type inhabitace – Conversion from Type to Prop due to restriction on elimination in Prop. Having typing judgements in Type we sometimes need to return a wrapped version of them to match on propositions. See progress.

Inductive inhab (X: Type) :Prop :=
| inhabited: X -> inhab X.

Pretty version of inversion
Ltac inv H := inversion H; subst; clear H.

Ltac invp R :=
match goal with
| [ H: R _ |- _] => inv H
| [ H: R _ _ |- _] => inv H
| [ H: R _ _ _ |- _] => inv H
| [ H: R _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ _ _ _ _ |- _] => inv H
| [ H: R _ _ _ _ _ _ _ _ _ _|- _] => inv H
end.

Ltac inject :=
repeat match goal with
| [H: ?C _ = ?C _ |- _] => injection H as ->
| [H: ?C _ _ = ?C _ _ |- _] => injection H as -> ->
| [H: ?C _ _ _ = ?C _ _ _ |- _] => injection H as -> -> ->
| [H: ?C _ _ _ _ = ?C _ _ _ _ |- _] => injection H as -> -> -> ->
| [H: ?C _ _ _ _ _ = ?C _ _ _ _ _ |- _] => injection H as -> -> -> -> ->
end.

Automatically destruct existential quantifier
Ltac exdestruct :=
match goal with
| [ H: ex ?P |- _] => destruct H
| [ H: ex2 ?P ?Q |- _] => destruct H
| [ H: sig ?P |- _] => destruct H
| [ H: sigT ?P |- _] => destruct H
end.

Ltac exintuition := intuition; repeat exdestruct; intuition.

Reduction tactic for beta reduction step
Ltac reduce := econstructor 2; [ solve [eauto] | cbn ].

Modus Ponens - applies to implications, will generate a subgoal for the premise of H and then specialize H with the result
Ltac mp H :=
let x := fresh "H" in
match type of H with
| ?Q -> ?P => assert P as x; [apply H | clear H; assert P as H by exact x; clear x]
end.