# Library HoTT.Overture

# Basic definitions of homotopy type theory, particularly the groupoid structure of identity types.

## Type classes

TODO: Should we make reflexivity, symmetry, and transitivity unfold under simpl, to, e.g., idpath, inverse, and concat?

Class Reflexive {A} (R : relation A) :=

reflexivity : ∀ x : A, R x x.

Class Symmetric {A} (R : relation A) :=

symmetry : ∀ x y, R x y → R y x.

Class Transitive {A} (R : relation A) :=

transitivity : ∀ x y z, R x y → R y z → R x z.

reflexivity : ∀ x : A, R x x.

Class Symmetric {A} (R : relation A) :=

symmetry : ∀ x y, R x y → R y x.

Class Transitive {A} (R : relation A) :=

transitivity : ∀ x y z, R x y → R y z → R x z.

A PreOrder is both Reflexive and Transitive.

Class PreOrder {A} (R : relation A) :=

{ PreOrder_Reflexive :> Reflexive R | 2 ;

PreOrder_Transitive :> Transitive R | 2 }.

Tactic Notation "etransitivity" open_constr(y) :=

let R := match goal with |- ?R ?x ?z ⇒ constr:(R) end in

let x := match goal with |- ?R ?x ?z ⇒ constr:(x) end in

let z := match goal with |- ?R ?x ?z ⇒ constr:(z) end in

refine (@transitivity _ R _ x y z _ _).

Tactic Notation "etransitivity" := etransitivity _.

{ PreOrder_Reflexive :> Reflexive R | 2 ;

PreOrder_Transitive :> Transitive R | 2 }.

Tactic Notation "etransitivity" open_constr(y) :=

let R := match goal with |- ?R ?x ?z ⇒ constr:(R) end in

let x := match goal with |- ?R ?x ?z ⇒ constr:(x) end in

let z := match goal with |- ?R ?x ?z ⇒ constr:(z) end in

refine (@transitivity _ R _ x y z _ _).

Tactic Notation "etransitivity" := etransitivity _.

We redefine transitivity to work without needing to include Setoid or be using Leibniz equality, and to give proofs that unfold to concat.

Ltac transitivity x := etransitivity x.

We redefine symmetry, which is too smart for its own good.

Define Type₁ (really, Type_i for any i > 0) so that we can enforce having universes that are not Set. In trunk, universes will not be unified with Set in most places, so we want to never use Set at all.

Definition Type1 := Eval hnf in let U := Type in let gt := (Set : U) in U.

Arguments Type1 / .

Identity Coercion unfold_Type1 : Type1 >-> Sortclass.

Arguments Type1 / .

Identity Coercion unfold_Type1 : Type1 >-> Sortclass.

We make the identity map a notation so we do not have to unfold it,
or complicate matters with its type.

We define notation for dependent pairs because it is too annoying to write and see existT P x y all the time. However, we put it in its own scope, because sometimes it is necessary to give the particular dependent type, so we'd like to be able to turn off this notation selectively.

We have unified sig and sigT of the standard Coq, and so we introduce a new notation to not annoy newcomers with the T in projT1 and projT2 nor the _sig in proj1_sig and proj2_sig, and to not confuse Coq veterans by stealing proj1 and proj2, which Coq uses for and.

The following notation is very convenient, although it unfortunately clashes with Proof General's "electric period". We add format specifiers so that it will display without an extra space, as x.1 rather than as x .1.

Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.

Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.

Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.

Composition of functions.

We put the following notation in a scope because leaving it unscoped causes it to override identical notations in other scopes. It's convenient to use the same notation for, e.g., function composition, morphism composition in a category, and functor composition, and let Coq automatically infer which one we mean by scopes. We can't do this if this notation isn't scoped. Unfortunately, Coq doesn't have a built-in function_scope like type_scope; type_scope is automatically opened wherever Coq is expecting a Sort, and it would be nice if function_scope were automatically opened whenever Coq expects a thing of type ∀ _, _ or _ → _. To work around this, we open function_scope globally.

Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.

Open Scope function_scope.

Open Scope function_scope.

Dependent composition of functions.

Definition composeD {A B C} (g : ∀ b, C b) (f : A → B) := fun x : A ⇒ g (f x).

Hint Unfold composeD.

Notation "g 'oD' f" := (composeD g f) (at level 40, left associativity) : function_scope.

Hint Unfold composeD.

Notation "g 'oD' f" := (composeD g f) (at level 40, left associativity) : function_scope.

## The groupoid structure of identity types.

Inductive paths {A : Type} (a : A) : A → Type :=

idpath : paths a a.

Arguments idpath {A a} , [A] a.

Arguments paths_ind [A] a P f y p.

Arguments paths_rec [A] a P f y p.

Arguments paths_rect [A] a P f y p.

Notation "x = y :> A" := (@paths A x y) : type_scope.

Notation "x = y" := (x = y :>_) : type_scope.

idpath : paths a a.

Arguments idpath {A a} , [A] a.

Arguments paths_ind [A] a P f y p.

Arguments paths_rec [A] a P f y p.

Arguments paths_rect [A] a P f y p.

Notation "x = y :> A" := (@paths A x y) : type_scope.

Notation "x = y" := (x = y :>_) : type_scope.

Ensure internal_paths_rew and internal_paths_rew_r are defined outside sections, so they are not unnecessarily polymorphic.

Lemma paths_rew A a y P (X : P a) (H : a = y :> A) : P y.

Proof. rewrite <- H. exact X. Defined.

Lemma paths_rew_r A a y P (X : P y) (H : a = y :> A) : P a.

Proof. rewrite → H. exact X. Defined.

Instance reflexive_paths {A} : Reflexive (@paths A) | 0 := @idpath A.

Proof. rewrite <- H. exact X. Defined.

Lemma paths_rew_r A a y P (X : P y) (H : a = y :> A) : P a.

Proof. rewrite → H. exact X. Defined.

Instance reflexive_paths {A} : Reflexive (@paths A) | 0 := @idpath A.

Our identity type is the Paulin-Mohring style. We derive the Martin-Lof eliminator.

Definition paths_rect' {A : Type} (P : ∀ (a b : A), (a = b) → Type)

: (∀ (a : A), P a a idpath) → ∀ (a b : A) (p : a = b), P a b p.

Proof.

intros H ? ? [].

apply H.

Defined.

We declare a scope in which we shall place path notations. This way they can be turned on and off by the user.

Delimit Scope path_scope with path.

Local Open Scope path_scope.

We define equality concatenation by destructing on both its arguments, so that it only computes when both arguments are idpath. This makes proofs more robust and symmetrical. Compare with the definition of identity_trans.

Arguments transitivity {A R _ x y z} _ _: simpl nomatch.

Instance transitive_paths {A} : Transitive (@paths A) | 0

:= fun x y z (p : x = y) (q : y = z) ⇒ match p, q with idpath, idpath ⇒ idpath end.

Arguments transitive_paths {A x y z} p q : simpl nomatch.

Notation concat := (transitivity (R := @paths _)) (only parsing).

Infix "@" := (@transitivity _ _ _ _ _ _) (at level 20).

Instance transitive_paths {A} : Transitive (@paths A) | 0

:= fun x y z (p : x = y) (q : y = z) ⇒ match p, q with idpath, idpath ⇒ idpath end.

Arguments transitive_paths {A x y z} p q : simpl nomatch.

Notation concat := (transitivity (R := @paths _)) (only parsing).

Infix "@" := (@transitivity _ _ _ _ _ _) (at level 20).

The inverse of a path.

Declaring this as simpl nomatch prevents the tactic simpl from expanding it out into match statements. We only want inverse to simplify when applied to an identity path.

Arguments inverse {A x y} p : simpl nomatch.

Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.

Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.

Note that you can use the built-in Coq tactics reflexivity and transitivity when working with paths, but not symmetry, because it is too smart for its own good. Instead, you can write apply symmetry or eapply symmetry.
The identity path.

The composition of two paths.

The inverse of a path.

An alternative notation which puts each path on its own line. Useful as a temporary device during proofs of equalities between very long composites; to turn it on inside a section, say Open Scope long_path_scope.

Notation "p @' q" := (concat p q) (at level 21, left associativity,

format "'[v' p '/' '@'' q ']'") : long_path_scope.

format "'[v' p '/' '@'' q ']'") : long_path_scope.

An important instance of paths_rect is that given any dependent type, one can
transport P p u transports u : P x to P y along p : x = y.

*transport*elements of instances of the type along equalities in the base.
Definition transport {A : Type} (P : A → Type) {x y : A} (p : x = y) (u : P x) : P y :=

match p with idpath ⇒ u end.

match p with idpath ⇒ u end.

See above for the meaning of simpl nomatch.

Transport is very common so it is worth introducing a parsing notation for it. However, we do not use the notation for output because it hides the fibration, and so makes it very hard to read involved transport expression.

Delimit Scope fib_scope with fib.

Local Open Scope fib_scope.

Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.

Local Open Scope fib_scope.

Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.

Having defined transport, we can use it to talk about what a homotopy theorist might see as "paths in a fibration over paths in the base"; and what a type theorist might see as "heterogeneous eqality in a dependent type".
We will first see this appearing in the type of apD.
Functions act on paths: if f : A → B and p : x = y is a path in A, then ap f p : f x = f y.
We typically pronounce ap as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths".

Definition ap {A B:Type} (f:A → B) {x y:A} (p:x = y) : f x = f y

:= match p with idpath ⇒ idpath end.

We introduce the convention that apKN denotes the application of a K-path between
functions to an N-path between elements, where a 0-path is simply a function or an
element. Thus, ap is a shorthand for ap01.

Notation ap01 := ap (only parsing).

Definition pointwise_paths {A} {P:A→Type} (f g:∀ x:A, P x)

:= ∀ x:A, f x = g x.

Hint Unfold pointwise_paths : typeclass_instances.

Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.

Definition apD10 {A} {B:A→Type} {f g : ∀ x, B x} (h:f=g)

: f == g

:= fun x ⇒ match h with idpath ⇒ 1 end.

Definition ap10 {A B} {f g:A→B} (h:f=g) : f == g

:= apD10 h.

Definition ap11 {A B} {f g:A→B} (h:f=g) {x y:A} (p:x=y) : f x = g y.

Proof.

case h, p; reflexivity.

Defined.

See above for the meaning of simpl nomatch.

Similarly, dependent functions act on paths; but the type is a bit more subtle. If f : ∀ a:A, B a and p : x = y is a path in A, then apD f p should somehow be a path between f x : B x and f y : B y. Since these live in different types, we use transport along p to make them comparable: apD f p : p # f x = f y.
The type p # f x = f y can profitably be considered as a heterogeneous or dependent equality type, of "paths from f x to f y over p".

Definition apD {A:Type} {B:A→Type} (f:∀ a:A, B a) {x y:A} (p:x=y):

p # (f x) = f y

:=

match p with idpath ⇒ idpath end.

See above for the meaning of simpl nomatch.

## Equivalences

A typeclass that includes the data making f into an adjoint equivalence.

Class IsEquiv {A B : Type} (f : A → B) := BuildIsEquiv {

equiv_inv : B → A ;

eisretr : Sect equiv_inv f;

eissect : Sect f equiv_inv;

eisadj : ∀ x : A, eisretr (f x) = ap f (eissect x)

}.

Arguments eisretr {A B} f {_} _.

Arguments eissect {A B} f {_} _.

Arguments eisadj {A B} f {_} _.

equiv_inv : B → A ;

eisretr : Sect equiv_inv f;

eissect : Sect f equiv_inv;

eisadj : ∀ x : A, eisretr (f x) = ap f (eissect x)

}.

Arguments eisretr {A B} f {_} _.

Arguments eissect {A B} f {_} _.

Arguments eisadj {A B} f {_} _.

A record that includes all the data of an adjoint equivalence.

Record Equiv A B := BuildEquiv {

equiv_fun :> A → B ;

equiv_isequiv :> IsEquiv equiv_fun

}.

Existing Instance equiv_isequiv.

Arguments equiv_fun {A B} _ _.

Arguments equiv_isequiv {A B} _.

Delimit Scope equiv_scope with equiv.

Local Open Scope equiv_scope.

Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.

equiv_fun :> A → B ;

equiv_isequiv :> IsEquiv equiv_fun

}.

Existing Instance equiv_isequiv.

Arguments equiv_fun {A B} _ _.

Arguments equiv_isequiv {A B} _.

Delimit Scope equiv_scope with equiv.

Local Open Scope equiv_scope.

Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.

A notation for the inverse of an equivalence. We can apply this to a function as long as there is a typeclass instance asserting it to be an equivalence. We can also apply it to an element of A <~> B, since there is an implicit coercion to A → B and also an existing instance of IsEquiv.

## Contractibility and truncation levels

- We prefer to reason about IsTrunc (S n) A rather than IsTrunc n (@paths A a b). Whenever we see a statement (or goal) about truncation of paths, we try to turn it into a statement (or goal) about truncation of a (non-paths) type. We do not allow typeclass resolution to go in the reverse direction from IsTrunc (S n) A to ∀ a b : A, IsTrunc n (a = b).
- We prefer to reason about syntactically smaller types. That is, typeclass instances should turn goals of type IsTrunc n (∀ a : A, P a) into goals of type ∀ a : A, IsTrunc n (P a); and goals of type IsTrunc n (A × B) into the pair of goals of type IsTrunc n A and IsTrunc n B; rather than the other way around. Ideally, we would add similar rules to transform hypotheses in the cases where we can do so. This rule is not always the one we want, but it seems to heuristically capture the shape of most cases that we want the typeclass machinery to automatically infer. That is, we often want to infer IsTrunc n (A × B) from IsTrunc n A and IsTrunc n B, but we (probably) don't often need to do other simple things with IsTrunc n (A × B) which are broken by that reduction.

### Contractibility

Class Contr_internal (A : Type) := BuildContr {

center : A ;

contr : (∀ y : A, center = y)

}.

Arguments center A {_}.

center : A ;

contr : (∀ y : A, center = y)

}.

Arguments center A {_}.

### Truncation levels

We will use Notation for trunc_indexes, so define a scope for them here.

Delimit Scope trunc_scope with trunc.

Bind Scope trunc_scope with trunc_index.

Arguments trunc_S _%trunc_scope.

Fixpoint nat_to_trunc_index (n : nat) : trunc_index

:= match n with

| 0 ⇒ trunc_S (trunc_S minus_two)

| S n' ⇒ trunc_S (nat_to_trunc_index n')

end.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=

match n with

| minus_two ⇒ Contr_internal A

| trunc_S n' ⇒ ∀ (x y : A), IsTrunc_internal n' (x = y)

end.

Notation minus_one:=(trunc_S minus_two).

Bind Scope trunc_scope with trunc_index.

Arguments trunc_S _%trunc_scope.

Fixpoint nat_to_trunc_index (n : nat) : trunc_index

:= match n with

| 0 ⇒ trunc_S (trunc_S minus_two)

| S n' ⇒ trunc_S (nat_to_trunc_index n')

end.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=

match n with

| minus_two ⇒ Contr_internal A

| trunc_S n' ⇒ ∀ (x y : A), IsTrunc_internal n' (x = y)

end.

Notation minus_one:=(trunc_S minus_two).

Include the basic numerals, so we don't need to go through the coercion from nat, and so that we get the right binding with trunc_scope.

Notation "0" := (trunc_S minus_one) : trunc_scope.

Notation "1" := (trunc_S 0) : trunc_scope.

Notation "2" := (trunc_S 1) : trunc_scope.

Arguments IsTrunc_internal n A : simpl nomatch.

Class IsTrunc (n : trunc_index) (A : Type) : Type :=

Trunc_is_trunc : IsTrunc_internal n A.

Notation "1" := (trunc_S 0) : trunc_scope.

Notation "2" := (trunc_S 1) : trunc_scope.

Arguments IsTrunc_internal n A : simpl nomatch.

Class IsTrunc (n : trunc_index) (A : Type) : Type :=

Trunc_is_trunc : IsTrunc_internal n A.

We use the priciple that we should always be doing typeclass resolution on truncation of non-equality types. We try to change the hypotheses and goals so that they never mention something like IsTrunc n (_ = _) and instead say IsTrunc (S n) _. If you're evil enough that some of your paths a = b are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore.

Typeclasses Opaque IsTrunc.

Arguments IsTrunc : simpl never.

Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)

: IsTrunc n (x = y)

:= H x y.

Hint Extern 0 ⇒ progress change IsTrunc_internal with IsTrunc in × : typeclass_instances.

Picking up the ∀ x y, IsTrunc n (x = y) instances in the hypotheses is much tricker. We could do something evil where we declare an empty typeclass like IsTruncSimplification and use the typeclass as a proxy for allowing typeclass machinery to factor nested ∀s into the IsTrunc via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases. It should be clear how to extend the pattern.

Hint Extern 10 ⇒

progress match goal with

| [ H : ∀ x y : ?T, IsTrunc ?n (x = y) |- _ ]

⇒ change (IsTrunc (trunc_S n) T) in H

| [ H : ∀ (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ a : A, IsTrunc (trunc_S n) (T a)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a), IsTrunc (trunc_S n) (T a b)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a) (c : C a b), IsTrunc (trunc_S n) (T a b c)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc (trunc_S n) (T a b c d)) in H; cbv beta in H

end.

Notation Contr := (IsTrunc minus_two).

Notation IsHProp := (IsTrunc minus_one).

Notation IsHSet := (IsTrunc 0).

Hint Extern 0 ⇒ progress change Contr_internal with Contr in × : typeclass_instances.

progress match goal with

| [ H : ∀ x y : ?T, IsTrunc ?n (x = y) |- _ ]

⇒ change (IsTrunc (trunc_S n) T) in H

| [ H : ∀ (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ a : A, IsTrunc (trunc_S n) (T a)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a), IsTrunc (trunc_S n) (T a b)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a) (c : C a b), IsTrunc (trunc_S n) (T a b c)) in H; cbv beta in H

| [ H : ∀ (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]

⇒ change (∀ (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc (trunc_S n) (T a b c d)) in H; cbv beta in H

end.

Notation Contr := (IsTrunc minus_two).

Notation IsHProp := (IsTrunc minus_one).

Notation IsHSet := (IsTrunc 0).

Hint Extern 0 ⇒ progress change Contr_internal with Contr in × : typeclass_instances.

### Function extensionality

# That's not technically true; it might be possible to get non-parametric universe polymorphism using Modules and (Module) Functors; we can use functors to quantify over a Module Type which requires a polymorphic proof of a given hypothesis, and then use that hypothesis polymorphically in any theorem we prove in our new Module Functor. But that is far beyond the scope of this file.

Monomorphic Axiom dummy_funext_type : Type0.

Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.

Axiom isequiv_apD10 : ∀ `{Funext} (A : Type) (P : A → Type) f g, IsEquiv (@apD10 A P f g).

Global Existing Instance isequiv_apD10.

Definition path_forall `{Funext} {A : Type} {P : A → Type} (f g : ∀ x : A, P x) :

f == g → f = g

:=

(@apD10 A P f g)^-1.

Definition path_forall2 `{Funext} {A B : Type} {P : A → B → Type} (f g : ∀ x y, P x y) :

(∀ x y, f x y = g x y) → f = g

:=

(fun E ⇒ path_forall f g (fun x ⇒ path_forall (f x) (g x) (E x))).

Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.

Axiom isequiv_apD10 : ∀ `{Funext} (A : Type) (P : A → Type) f g, IsEquiv (@apD10 A P f g).

Global Existing Instance isequiv_apD10.

Definition path_forall `{Funext} {A : Type} {P : A → Type} (f g : ∀ x : A, P x) :

f == g → f = g

:=

(@apD10 A P f g)^-1.

Definition path_forall2 `{Funext} {A B : Type} {P : A → B → Type} (f g : ∀ x y, P x y) :

(∀ x y, f x y = g x y) → f = g

:=

(fun E ⇒ path_forall f g (fun x ⇒ path_forall (f x) (g x) (E x))).

### Tactics

Hint Resolve

@idpath @inverse

: path_hints.

Hint Resolve @idpath : core.

Ltac path_via mid :=

apply @concat with (y := mid); auto with path_hints.

@idpath @inverse

: path_hints.

Hint Resolve @idpath : core.

Ltac path_via mid :=

apply @concat with (y := mid); auto with path_hints.

We put Empty here, instead of in Empty.v, because Ltac done uses it. HoTT/coq is broken and somehow interprets Type1 as Prop with regard to elimination schemes.

Unset Elimination Schemes.

Inductive Empty : Type1 := .

Scheme Empty_rect := Induction for Empty Sort Type.

Scheme Empty_rec := Induction for Empty Sort Set.

Scheme Empty_ind := Induction for Empty Sort Prop.

Set Elimination Schemes.

Definition not (A:Type) : Type := A → Empty.

Notation "~ x" := (not x) : type_scope.

Hint Unfold not: core.

Notation "x <> y :> T" := (not (x = y :> T))

(at level 70, y at next level, no associativity) : type_scope.

Notation "x <> y" := (x ≠ y :> _) (at level 70, no associativity) : type_scope.

Definition complement {A} (R : relation A) : relation A :=

fun x y ⇒ ¬ (R x y).

Typeclasses Opaque complement.

Class Irreflexive {A} (R : relation A) :=

irreflexivity : Reflexive (complement R).

Class Asymmetric {A} (R : relation A) :=

asymmetry : ∀ {x y}, R x y → (complement R y x : Type).

Inductive Empty : Type1 := .

Scheme Empty_rect := Induction for Empty Sort Type.

Scheme Empty_rec := Induction for Empty Sort Set.

Scheme Empty_ind := Induction for Empty Sort Prop.

Set Elimination Schemes.

Definition not (A:Type) : Type := A → Empty.

Notation "~ x" := (not x) : type_scope.

Hint Unfold not: core.

Notation "x <> y :> T" := (not (x = y :> T))

(at level 70, y at next level, no associativity) : type_scope.

Notation "x <> y" := (x ≠ y :> _) (at level 70, no associativity) : type_scope.

Definition complement {A} (R : relation A) : relation A :=

fun x y ⇒ ¬ (R x y).

Typeclasses Opaque complement.

Class Irreflexive {A} (R : relation A) :=

irreflexivity : Reflexive (complement R).

Class Asymmetric {A} (R : relation A) :=

asymmetry : ∀ {x y}, R x y → (complement R y x : Type).

Class IsPointed (A : Type) := point : A.

Definition pointedType := { u : Type & IsPointed u }.

Arguments point A {_}.

Definition pointedType := { u : Type & IsPointed u }.

Arguments point A {_}.

Ssreflect tactics, adapted by Robbert Krebbers

Ltac done :=

trivial; intros; solve

[ repeat first

[ solve [trivial]

| solve [symmetry; trivial]

| reflexivity

| contradiction

| split ]

| match goal with

H : ¬ _ |- _ ⇒ solve [destruct H; trivial]

end ].

Tactic Notation "by" tactic(tac) :=

tac; done.

trivial; intros; solve

[ repeat first

[ solve [trivial]

| solve [symmetry; trivial]

| reflexivity

| contradiction

| split ]

| match goal with

H : ¬ _ |- _ ⇒ solve [destruct H; trivial]

end ].

Tactic Notation "by" tactic(tac) :=

tac; done.

A convenient tactic for using function extensionality.

Ltac by_extensionality x :=

intros; unfold compose;

match goal with

| [ |- ?f = ?g ] ⇒ eapply path_forall; intro x;

match goal with

| [ |- ∀ (_ : prod _ _), _ ] ⇒ intros [? ?]

| [ |- ∀ (_ : sigT _ _), _ ] ⇒ intros [? ?]

| _ ⇒ intros

end;

simpl; auto with path_hints

end.

intros; unfold compose;

match goal with

| [ |- ?f = ?g ] ⇒ eapply path_forall; intro x;

match goal with

| [ |- ∀ (_ : prod _ _), _ ] ⇒ intros [? ?]

| [ |- ∀ (_ : sigT _ _), _ ] ⇒ intros [? ?]

| _ ⇒ intros

end;

simpl; auto with path_hints

end.

Removed auto. We can write "by (path_induction;auto with path_hints)"
if we want to.

Ltac path_induction :=

intros; repeat progress (

match goal with

| [ p : _ = _ |- _ ] ⇒ induction p

| _ ⇒ idtac

end

).

intros; repeat progress (

match goal with

| [ p : _ = _ |- _ ] ⇒ induction p

| _ ⇒ idtac

end

).

The tactic f_ap is a replacement for the previously existing standard library tactic f_equal. This tactic works by repeatedly applying the fact that f = g → x = y → f x = g y to turn, e.g., f x y = f z w first into f x = f z and y = w, and then turns the first of these into f = f and x = z. The done tactic is used to detect the f = f case and finish, and the trivial is used to solve, e.g., x = x when using f_ap on f y x = f z x. This tactic only works for non-dependently-typed functions; we cannot express y = w in the first example if y and w have different types. If and when Arnaud's new-tacticals branch lands, and we can have a goal which depends on the term used to discharge another goal, then this tactic should probably be generalized to deal with dependent functions.

Ltac f_ap :=

idtac;

lazymatch goal with

| [ |- ?f ?x = ?g ?x ] ⇒ apply (@apD10 _ _ f g);

try (done || f_ap)

| _ ⇒ apply ap11;

[ done || f_ap

| trivial ]

end.

idtac;

lazymatch goal with

| [ |- ?f ?x = ?g ?x ] ⇒ apply (@apD10 _ _ f g);

try (done || f_ap)

| _ ⇒ apply ap11;

[ done || f_ap

| trivial ]

end.

expand replaces both terms of an equality (either paths or pointwise_paths in the goal with their head normal forms

Ltac expand :=

idtac;

match goal with

| [ |- ?X = ?Y ] ⇒

let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')

| [ |- ?X == ?Y ] ⇒

let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')

end; simpl.

idtac;

match goal with

| [ |- ?X = ?Y ] ⇒

let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')

| [ |- ?X == ?Y ] ⇒

let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')

end; simpl.

Test if a tactic succeeds, but always roll-back the results

Tactic Notation "test" tactic3(tac) :=

try (first [ tac | fail 2 tac "does not succeed" ]; fail tac "succeeds"; []).

try (first [ tac | fail 2 tac "does not succeed" ]; fail tac "succeeds"; []).

not tac is equivalent to fail tac "succeeds" if tac succeeds, and is equivalent to idtac if tac fails

Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").

atomic x is the same as idtac if x is a variable or hypothesis, but is fail 0 if x has internal structure.

Ltac atomic x :=

idtac;

match x with

| ?f _ ⇒ fail 1 x "is not atomic"

| (fun _ ⇒ _) ⇒ fail 1 x "is not atomic"

| ∀ _, _ ⇒ fail 1 x "is not atomic"

| _ ⇒ idtac

end.

idtac;

match x with

| ?f _ ⇒ fail 1 x "is not atomic"

| (fun _ ⇒ _) ⇒ fail 1 x "is not atomic"

| ∀ _, _ ⇒ fail 1 x "is not atomic"

| _ ⇒ idtac

end.

transparent assert (H : T) is like assert (H : T), but leaves the body transparent. Since binders don't respect fresh, we use a name unlikely to be reused.

Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=

refine (let __transparent_assert_hypothesis := (_ : type) in _);

[

| (

let H := match goal with H := _ |- _ ⇒ constr:(H) end in

rename H into name) ].

refine (let __transparent_assert_hypothesis := (_ : type) in _);

[

| (

let H := match goal with H := _ |- _ ⇒ constr:(H) end in

rename H into name) ].

transparent eassert is like transparent assert, but allows holes in the type, which will be turned into evars.

Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" "by" tactic3(tac) := let name := fresh "H" in transparent assert (name : type); [ solve [ tac ] | ].

Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" := transparent assert (name : type).

Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" "by" tactic3(tac) := transparent assert (name : type) by tac.

Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" := transparent assert (name : type).

Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" "by" tactic3(tac) := transparent assert (name : type) by tac.