semantics.base.overture
Overture
Import ssreflect
Require Export Coq.Program.Basics. (* flip *)
Require Export Coq.Setoids.Setoid. (* required for rewrite *)
Require Export Coq.Classes.Morphisms.
Require Import Program.Tactics. (* revert until *)
Require Export Coq.Setoids.Setoid. (* required for rewrite *)
Require Export Coq.Classes.Morphisms.
Require Import Program.Tactics. (* revert until *)
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.
(* This is too buggy at the moment in combination with ssreflect. *)
(*Global Set Universe Polymorphism.*)
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.
(* This is too buggy at the moment in combination with ssreflect. *)
(*Global Set Universe Polymorphism.*)
Tactic Notation "nointr" tactic(t) :=
let m := fresh "marker" in
pose (m := tt);
t; revert_until m; clear m.
let m := fresh "marker" in
pose (m := tt);
t; revert_until m; clear m.
Definition J {A : Type} {a : A} (P : forall b, a = b -> Type) (h : P a erefl)
(b : A) (p : a = b) : P b p := match p with erefl => h end.
Definition transport {A : Type} {x y : A} (p : x = y) {P : A -> Type} : P x -> P y := J id p.
Notation "p # x" := (transport p x) (right associativity, at level 65).
Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y :=
match p with erefl => erefl end.
Lemma transport_const {A B : Type} (x y : A) (a : B) (p : x = y) : p # a = a.
Proof. by destruct p. Qed.
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Bind Scope fibration_scope with sigT.
Open Scope fibration_scope.
We rebind ssreflect's .1/.2 notation to refer to sigT and add the missing coercions. This makes type inference for the notation more difficult, but makes it work in more cases.
Notation "p .1" := (tag p)
(at level 2, left associativity, format "p .1") : fibration_scope.
Notation "p .2" := (tagged p)
(at level 2, left associativity, format "p .2") : fibration_scope.
Coercion pair_to_sigT (A B : Type) (p : A * B) := (fst p; snd p).
Equality in dependent pair types
Lemma sigT_eq (A : Type) (P : A -> Type) (a b : A) (pa : P a) (pb : P b) :
forall p : a = b, p # pa = pb -> (a; pa) = (b; pb).
Proof. destruct 1; by destruct p. Defined.
Arguments sigT_eq {A P a b pa pb} p q.
Definition sigT_eq_pr1 (A : Type) (P : A -> Type) (a b : sigT P) :
a = b -> a.1 = b.1 := ap tag.
Definition sigT_eq_pr2 (A : Type) (P : A -> Type) (a b : sigT P) (p : a = b) :
sigT_eq_pr1 p # a.2 = b.2 := match p with erefl => erefl end.
Notation "p ..1" := (sigT_eq_pr1 p)
(at level 2, left associativity, format "p ..1").
Notation "p ..2" := (sigT_eq_pr2 p)
(at level 2, left associativity, format "p ..2").
Redefine some things from ssreflect for Prop valued relations.
Definition reflexive {T} (R : Rel T) := forall x, R x x.
Definition symmetric {T} (R : Rel T) := forall x y, R x y -> R y x.
Definition antisymmetric {T} (R : Rel T) := forall x y, R x y -> R y x -> x = y.
Definition transitive {T} (R : Rel T) := forall x y z, R x y -> R y z -> R x z.
Definition is_prop (A : Type) := forall a b : A, a = b.
Structure hprop := mk_hprop {
hprop_type :> Type;
hprop_is_prop : is_prop hprop_type
}.
Arguments mk_hprop A h : rename, clear implicits.
Definition hpropP (A : hprop) (a b : A) : a = b.
Proof. exact: hprop_is_prop. Qed.
Lemma tag_injective (A : Type) (P : A -> hprop) : injective (tag : sigT P -> A).
Proof. move=> [x xp] [y yp] /= E. apply: sigT_eq (E) _. exact: hpropP. Qed.
Lemma sigT_is_hprop (A : hprop) (P : A -> hprop) : is_prop (sigT P).
Proof. move=> [x px] [y py]. apply: sigT_eq (hpropP x y) _. exact: hpropP. Qed.
Canonical Structure sigT_hprop (A : hprop) (P : A -> hprop) :=
mk_hprop (sigT P) (@sigT_is_hprop A P).
Lemma unit_is_hprop : is_prop unit.
Proof. by move=> [] []. Qed.
Canonical Structure unit_hprop := mk_hprop unit unit_is_hprop.
Section Equivalence.
Variable (A B : Type).
Structure is_equiv (f : A -> B) := mk_is_equiv {
inverse :> B -> A;
inverse_cl : forall x : A, inverse (f x) = x;
inverse_cr : forall x : B, f (inverse x) = x
}.
Structure equiv := mk_equiv {
equivmap :> A -> B;
equivmap_is_equiv : is_equiv equivmap
}.
End Equivalence.
Arguments mk_is_equiv {A B f} inverse inverse_cl inverse_cr.
Arguments mk_equiv {A B} equivmap equivmap_is_equiv.
Notation "A <~> B" := (equiv A B) (at level 85) : type_scope.
Definition equiv_inverse {A B : Type} {f : A <~> B} of phantom (A -> B) f : B -> A :=
inverse (equivmap_is_equiv f).
Notation "f ^-1" := (equiv_inverse (Phantom (_ -> _) f)).
Lemma equiv_retr {A B} (f : A <~> B) (x : B) : f (f^-1 x) = x.
Proof. exact: (inverse_cr (equivmap_is_equiv f)). Qed.
Lemma equiv_sect {A B} (f : A <~> B) (x : A) : f^-1 (f x) = x.
Proof. exact: (inverse_cl (equivmap_is_equiv f)). Qed.
Section EquivProp.
Variables (A B : hprop).
Definition prop_is_equiv (f : A -> B) (g : B -> A) : is_equiv f.
Proof. apply: (mk_is_equiv g _ _) => x; exact: hpropP. Defined.
Definition prop_equiv (f : A -> B) (g : B -> A) : A <~> B :=
mk_equiv f (prop_is_equiv f g).
End EquivProp.
Definition is_equiv_idfun A : is_equiv (@idfun A) :=
mk_is_equiv id (fun _ => erefl) (fun _ => erefl).
Canonical Structure equiv_refl A := mk_equiv idfun (@is_equiv_idfun A).
Definition is_equiv_inv {A B} (f : A <~> B) : is_equiv f^-1 :=
mk_is_equiv f (equiv_retr f) (equiv_sect f).
Canonical Structure equiv_sym A B (f : A <~> B) := mk_equiv f^-1 (is_equiv_inv f).
(* Note: There's a weird universe bug when writing this definition using Program.
Giving the proof term directly is unproblematic, though... *)
Definition is_equiv_comp {A B C} (f : A <~> B) (g : B <~> C) :
is_equiv (g \o f) := mk_is_equiv (f^-1 \o g^-1)
(fun x => eq_trans (ap f^-1 (equiv_sect g (f x))) (equiv_sect f x))
(fun x => eq_trans (ap g (equiv_retr f (g^-1 x))) (equiv_retr g x)).
Canonical Structure equiv_trans A B C (f : A <~> B) (g : B <~> C) :=
mk_equiv (g \o f) (is_equiv_comp f g).
Giving the proof term directly is unproblematic, though... *)
Definition is_equiv_comp {A B C} (f : A <~> B) (g : B <~> C) :
is_equiv (g \o f) := mk_is_equiv (f^-1 \o g^-1)
(fun x => eq_trans (ap f^-1 (equiv_sect g (f x))) (equiv_sect f x))
(fun x => eq_trans (ap g (equiv_retr f (g^-1 x))) (equiv_retr g x)).
Canonical Structure equiv_trans A B C (f : A <~> B) (g : B <~> C) :=
mk_equiv (g \o f) (is_equiv_comp f g).