This file contains basic tactics and useful lemmas/types

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.

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.

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.

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.

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.