semantics.base.overture

Overture

Standard imports, flags, definitions and notations, which do not require any axioms.

Import ssreflect

Import setoid rewriting and tactics

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 *)

Flags

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.*)

Execute a tactic without introducing fresh assumptions

Tactic Notation "nointr" tactic(t) :=
  let m := fresh "marker" in
  pose (m := tt);
  t; revert_until m; clear m.

Path Types


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.

Dependent Pairs


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").

Predicates and relations


Definition Pred (T : Type) := T -> Prop.
Definition Rel (T : Type) := T -> Pred T.

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.

Indexed products

This is a hack for canonical structures.
Definition iprod {A : Type} (P : A -> Type) := forall x, P x.

Mere propositions


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.

Equivalence of types

Definitions and notations


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.

For hprops, iff and equiv coincide


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.

Identity equivalence


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).

Inverse of an equivalence


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).

Composition of equivalences

(* 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).