(** 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). Proof. refine (subst_as_in (fun _ as0 => as0 = sym_eq (sym_eq as0)) eq01 _). simpl. refine (refl_equal _). Defined. (** [sym_eq] gives an opposite *) Definition sym_eq_opp_right : refl_equal _ = trans_eq eq01 (sym_eq eq01). Proof. refine (subst_as_in (fun _ as0 => _ = trans_eq as0 (sym_eq as0)) eq01 _). simpl. refine (refl_equal _). Defined. Definition sym_eq_opp_left : refl_equal _ = trans_eq (sym_eq eq01) eq01. Proof. refine (subst_as_in (fun _ as0 => refl_equal _ = trans_eq (sym_eq as0) as0) eq01 _). simpl. refine (refl_equal _). Defined. (** [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. Proof. refine (subst_as_in (fun _ as0 => as0 = trans_eq (refl_equal _) as0) eq01 _). simpl. refine (refl_equal _). Defined. (** [trans_eq] is associative *) Definition trans_eq_assoc : trans_eq (trans_eq eq01 eq12) eq23 = trans_eq eq01 (trans_eq eq12 eq23). Proof. refine (subst_as_in (fun _ as0 => trans_eq (trans_eq eq01 eq12) as0 = trans_eq eq01 (trans_eq eq12 as0)) eq23 _). simpl. refine (refl_equal _). Defined. 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. Proof. simpl. refine (refl_equal _). Qed. (** subst preserves composition *) Definition subst_pres_comp : subst0 (trans_eq eq01 eq12) v0 = subst0 eq12 (subst0 eq01 v0). Proof. refine (subst_as_in (fun _ as0 => subst0 (trans_eq eq01 as0) _ = subst0 as0 (subst0 eq01 _)) eq12 _). simpl. refine (refl_equal _). Qed. 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. Proof. refine (subst_as_in (fun vv as0 => refl_equal vv = eq_rect _ (fun v => v=vv) as0 _ as0) eq01 _). simpl. refine (refl_equal _). Qed. Definition subst_mix1 : refl_equal v0 = eq_rect _ (fun v => v0=v) eq01 _ (sym_eq eq01). Proof. refine (subst_as_in (fun _ as0 => refl_equal v0 = eq_rect _ (fun v => v0=v) as0 _ (sym_eq as0)) eq01 _). simpl. refine (refl_equal _). Qed. 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. Proof. refine (subst_as_in (fun _ as0 => subst_in pair_fr_ob as0 v0 = pair_fr_mor _ _ (subst as0) v0) eq01 _). unfold pair_fr_ob, pair_fr_mor. simpl. destruct v0. refine (refl_equal _). Qed. 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]. (* subst commutes with f *) Definition subst_comm_f : f (subst eqt v0) = subst_prod eqt (f v0). Proof. refine (subst_as_in (fun _ as0 => f (subst as0 _) = subst_prod as0 _) eqt _). simpl. refine (refl_equal _). Defined. End subst_comm_f. Section JMeq. Require Import Coq.Logic.JMeq. Set Printing Implicit. Variable (t0 t1 t2:Type). (* compare 'JMeq_constr_diff_types s (Q:S=T)' to '{s || Q:S = T} : (s : S) = (s [Q:S = T⟩ : T)' in "Altenkirch, McBride, Swierstra. Observational Equality, Now!" and to 'JMSubst2' in "Oury. Extensionality in the Calculus of Constructions" *) Definition JMeq_constr_diff_types : forall (a:t0) (eqt:t0=t1), @JMeq t0 a t1 (subst eqt a). Proof. refine (fun a eqt => _). refine (subst_as_in (fun t2 eqt0 => @JMeq t0 a t2 (subst eqt0 a)) eqt _). simpl. refine (JMeq_refl _). Qed. End JMeq.