Library Beroal.Equality

Equality in Intensional Type Theory

Shorthands for eq elimination


Section subst.
Variable t:Type.
Definition subst_as_in := fun (v0:t)
        (type_fun : forall right_eq:t, v0=right_eq -> Type)
        (v1:t) (eq0:v0=v1) (value : type_fun v0 (refl_equal v0))
        => match eq0 as as0 in _=right_eq
                return type_fun right_eq as0
                with refl_equal => value end.
Definition subst_in := fun (type_fun:t -> Type) (v0 v1:t)
        (eq0:v0=v1) (value:type_fun v0)
        => match eq0 in _=right_eq return type_fun right_eq
                with refl_equal => value end.
Definition subst := fun (t0 t1:Type) (eq0:t0=t1) (value:t0)
        => match eq0 in _=right_eq return right_eq
                with refl_equal => value end.
End subst.
Implicit Arguments subst_as_in [t v0 v1].
Implicit Arguments subst_in [t v0 v1].
Implicit Arguments subst [t0 t1].
Ltac subst_tac_in type_fun eq0 := refine (subst_in eq0 type_fun _).
Ltac subst_tac_as_in type_fun eq0:= refine (subst_as_in eq0 type_fun _).

eq is a groupoid with:

  • objects: formulas;
  • morphisms: proofs of identity of formulas;
  • identity morphism: refl_equal;
  • composition of morphisms: trans_eq;
  • inverse morphism: sym_eq.
Section groupoid.
Variable (t0:Type) (v0 v1 v2 v3:t0)
        (eq01:v0=v1) (eq12:v1=v2) (eq23:v2=v3).

sym_eq is an inverse to itself

Definition sym_eq_inv_self : eq01 = sym_eq (sym_eq eq01).

sym_eq gives an opposite

Definition sym_eq_opp_right : refl_equal _ = trans_eq eq01 (sym_eq eq01).

Definition sym_eq_opp_left : refl_equal _ = trans_eq (sym_eq eq01) eq01.

refl_equal gives an identity

Check (refl_equal _) : eq01 = trans_eq eq01 (refl_equal _).

Definition refl_equal_identity_left : eq01 = trans_eq (refl_equal _) eq01.

trans_eq is associative
Definition trans_eq_assoc : trans_eq (trans_eq eq01 eq12) eq23
        = trans_eq eq01 (trans_eq eq12 eq23).

End groupoid.

Subst is a functor from groupoid eq to a category of types and functions between types

Section subst_functor.
Variable (sort0:Type) (type_fun:sort0->Type) (t0 t1 t2:sort0)
        (v0:type_fun t0) (eq01:t0=t1) (eq12:t1=t2).
Definition subst0 := subst_in type_fun.
Implicit Arguments subst0 [v0 v1].

subst preserves identity
Definition subst_pres_id : v0 = subst0 (refl_equal _) v0.

subst preserves composition
Definition subst_pres_comp : subst0 (trans_eq eq01 eq12) v0
        = subst0 eq12 (subst0 eq01 v0).

End subst_functor.

Section subst_mix.
Variable (t0:Type) (v0 v1:t0) (eq01:v0=v1).
Definition subst_mix0
        : refl_equal v1 = eq_rect _ (fun v => v=v1) eq01 _ eq01.

Definition subst_mix1
        : refl_equal v0 = eq_rect _ (fun v => v0=v) eq01 _ (sym_eq eq01).
End subst_mix.

subst may be moved around a polymorphic function


Section subst_pair_fr.
Definition pair_fr_ob := fun t:Type => prod t t.
Definition pair_fr_mor := fun (t0 t1:Type) (f:t0->t1) p
        => match p with (a,b) => (f a, f b) end.
Variable (t0 t1:Type) (v0:prod t0 t0) (eq01:t0=t1).
Definition subst_pair_fr
        : subst_in pair_fr_ob eq01 v0 = pair_fr_mor _ _ (subst eq01) v0.
End subst_pair_fr.

Section subst_comm_f.
Variable (t0 t1:Type) (eqt:t0=t1) (v0:t0).
Definition f := fun (t:Type) (a:t) => (a, a) : prod t t.
Implicit Arguments f [t].

Definition subst_prod := subst_in (fun t:Type => prod t t).
Implicit Arguments subst_prod [v0 v1].
Definition subst_comm_f : f (subst eqt v0) = subst_prod eqt (f v0).

End subst_comm_f.

Section JMeq.
Require Import Coq.Logic.JMeq.
Variable (t0 t1 t2:Type).

Definition JMeq_constr_diff_types : forall (a:t0) (eqt:t0=t1),
        @JMeq t0 a t1 (subst eqt a).

End JMeq.