Library rm0
Preserving eq0
Lemma ka_eq_eq0 : Proper (ka_eq ==> Logic.eq) eq0.
Theorem eq_eq0 ax :
Proper (ax ==> Logic.eq) eq0 → Proper (eq ax ==> Logic.eq) eq0.
Lemma ka_eq_t_eq0 : Proper (ka_eq_t ==> Logic.eq) eq0.
Lemma ka_eq_u_eq0 : Proper (ka_eq_u ==> Logic.eq) eq0.
Lemma zero_ka_t_eq0 : Proper (zero_ka_t ==> Logic.eq) eq0.
Lemma zero_ka_u_eq0 : Proper (zero_ka_u ==> Logic.eq) eq0.
Lemma zero_perm_t_eq0 : Proper (zero_perm_t ==> Logic.eq) eq0.
Lemma zero_perm_u_eq0 : Proper (zero_perm_u ==> Logic.eq) eq0.
Lemma zero_nom_t_eq0 : Proper (zero_nom_t ==> Logic.eq) eq0.
Lemma zero_nom_u_eq0 : Proper (zero_nom_u ==> Logic.eq) eq0.
Lemma eq_nom_typed_p_eq0 : Proper (eq_nom_typed_p ==> Logic.eq) eq0.
Lemma eq_nom_typed_np_eq0 : Proper (eq_nom_typed_np ==> Logic.eq) eq0.
Lemma eq_nom_typed_eq0 : Proper (eq_nom_typed ==> Logic.eq) eq0.
Lemma eq_nom_untyped_p_eq0 : Proper (eq_nom_untyped_p ==> Logic.eq) eq0.
Lemma eq_nom_untyped_np_eq0 :
Proper (eq_nom_untyped_np ==> Logic.eq) eq0.
Lemma eq_nom_untyped_eq0 : Proper (eq_nom_untyped ==> Logic.eq) eq0.
Lemma eq_perm_elim_eq0 : Proper (eq_perm_elim ==> Logic.eq) eq0.
Lemma eq_ν_smpl_eq0: Proper (eq_ν_smpl ==> Logic.eq) eq0.
Lemma eq_ω_smpl_eq0: Proper (eq_ω_smpl ==> Logic.eq) eq0.
Lemma eq_perm_eq0 : Proper (eq_perm ==> Logic.eq) eq0.
Lemma eq_perm_ω_eq0 : Proper (eq_perm_ω ==> Logic.eq) eq0.
Lemma zero_eq_u_eq0 : Proper (zero_eq_u ==> Logic.eq) eq0.
Lemma zero_eq_t_eq0 : Proper (zero_eq_t ==> Logic.eq) eq0.
Theorem eq_eq0 ax :
Proper (ax ==> Logic.eq) eq0 → Proper (eq ax ==> Logic.eq) eq0.
Lemma ka_eq_t_eq0 : Proper (ka_eq_t ==> Logic.eq) eq0.
Lemma ka_eq_u_eq0 : Proper (ka_eq_u ==> Logic.eq) eq0.
Lemma zero_ka_t_eq0 : Proper (zero_ka_t ==> Logic.eq) eq0.
Lemma zero_ka_u_eq0 : Proper (zero_ka_u ==> Logic.eq) eq0.
Lemma zero_perm_t_eq0 : Proper (zero_perm_t ==> Logic.eq) eq0.
Lemma zero_perm_u_eq0 : Proper (zero_perm_u ==> Logic.eq) eq0.
Lemma zero_nom_t_eq0 : Proper (zero_nom_t ==> Logic.eq) eq0.
Lemma zero_nom_u_eq0 : Proper (zero_nom_u ==> Logic.eq) eq0.
Lemma eq_nom_typed_p_eq0 : Proper (eq_nom_typed_p ==> Logic.eq) eq0.
Lemma eq_nom_typed_np_eq0 : Proper (eq_nom_typed_np ==> Logic.eq) eq0.
Lemma eq_nom_typed_eq0 : Proper (eq_nom_typed ==> Logic.eq) eq0.
Lemma eq_nom_untyped_p_eq0 : Proper (eq_nom_untyped_p ==> Logic.eq) eq0.
Lemma eq_nom_untyped_np_eq0 :
Proper (eq_nom_untyped_np ==> Logic.eq) eq0.
Lemma eq_nom_untyped_eq0 : Proper (eq_nom_untyped ==> Logic.eq) eq0.
Lemma eq_perm_elim_eq0 : Proper (eq_perm_elim ==> Logic.eq) eq0.
Lemma eq_ν_smpl_eq0: Proper (eq_ν_smpl ==> Logic.eq) eq0.
Lemma eq_ω_smpl_eq0: Proper (eq_ω_smpl ==> Logic.eq) eq0.
Lemma eq_perm_eq0 : Proper (eq_perm ==> Logic.eq) eq0.
Lemma eq_perm_ω_eq0 : Proper (eq_perm_ω ==> Logic.eq) eq0.
Lemma zero_eq_u_eq0 : Proper (zero_eq_u ==> Logic.eq) eq0.
Lemma zero_eq_t_eq0 : Proper (zero_eq_t ==> Logic.eq) eq0.
Misc.
Lemma eq0_proof_untyped :
∀ e, untyped e → eq0 e = true →
zero_eq_u ⊢ e ≡ 0.
Lemma eq0_untyped_refl :
∀ e, untyped e →reflect (zero_eq_u ⊢ e ≡ 0) (eq0 e).
Lemma eq0_proof_typed :
∀ e A, A ⊨ e → eq0 e = true →
zero_eq_t ⊢ e ≡ ⊥ A.
∀ e, untyped e → eq0 e = true →
zero_eq_u ⊢ e ≡ 0.
Lemma eq0_untyped_refl :
∀ e, untyped e →reflect (zero_eq_u ⊢ e ≡ 0) (eq0 e).
Lemma eq0_proof_typed :
∀ e A, A ⊨ e → eq0 e = true →
zero_eq_t ⊢ e ≡ ⊥ A.
rm0 preserves the semantics.
Lemma rm0_eq_untyped :
∀ e, untyped e →
(zero_eq_u ∨ ka_eq_u) ⊢ e ≡ rm0 e.
Lemma rm0_eq_typed :
∀ e A, A ⊨ e →
(zero_eq_t ∨ ka_eq_t) ⊢ e ≡ rm0 e.
∀ e, untyped e →
(zero_eq_u ∨ ka_eq_u) ⊢ e ≡ rm0 e.
Lemma rm0_eq_typed :
∀ e A, A ⊨ e →
(zero_eq_t ∨ ka_eq_t) ⊢ e ≡ rm0 e.
If e and f are related by zero axioms then rm0 e and rm0 f are equal in a minimal setting.
Lemma rm0_zero_eq_u :
Proper (ut ∧ zero_eq_u ==> eq_expr) rm0.
Lemma rm0_zero_eq_t :
Proper (ty'∧ zero_eq_t ==> eq_expr) rm0.
Proper (ut ∧ zero_eq_u ==> eq_expr) rm0.
Lemma rm0_zero_eq_t :
Proper (ty'∧ zero_eq_t ==> eq_expr) rm0.
Axiom bundles preserve rm0.
Lemma rm0_eq_ν_smpl_typed :
Proper (ty'∧ eq_ν_smpl ==> eq eq_ν_smpl) rm0.
Lemma rm0_eq_ν_smpl_untyped :
Proper (ut ∧ eq_ν_smpl ==> eq eq_ν_smpl) rm0.
Lemma rm0_eq_ω_smpl_typed :
Proper (ty'∧ eq_ω_smpl ==> eq eq_ω_smpl) rm0.
Lemma rm0_eq_perm_elim :
Proper ((eq_perm_elim∨eq_perm)
==> (Logic.eq∨eq_perm_elim∨eq_perm)) rm0.
Lemma rm0_eq_perm_ω :
Proper ((eq_perm_ω)
==> (Logic.eq∨eq_perm_ω)) rm0.
Lemma rm0_t_ka_eq :
Proper (ty'∧ (ka_eq∨ka_eq_t) ==> eq ka_eq_t) rm0.
Lemma rm0_u_ka_eq :
Proper (ut ∧ (ka_eq∨ka_eq_u) ==> eq ka_eq_u) rm0.
Lemma rm0_eq_nom_untyped_p :
Proper (ut ∧ (eq_nom_untyped_p) ==> eq eq_nom_untyped_p) rm0.
Lemma rm0_eq_nom_untyped_np :
Proper (ut ∧ (eq_nom_untyped_np) ==> eq eq_nom_untyped_np) rm0.
Lemma rm0_eq_nom_untyped :
Proper (ut ∧ (eq_nom_untyped) ==> eq eq_nom_untyped) rm0.
Lemma rm0_eq_nom_typed :
Proper (ty'∧ (eq_nom_typed) ==> eq eq_nom_typed) rm0.
Lemma rm0_eq_nom_typed_p :
Proper (eq_nom_typed_p ==> eq eq_nom_typed_p) rm0.
Lemma stronger_Ty_eq_nom_typed_np :
eq_nom_typed_np ⇒ ty'∧ eq_nom_typed_np.
Lemma rm0_eq_nom_typed_np :
Proper (eq_nom_typed_np ==> eq (eq_nom_typed_np)) rm0.
Lemma untyped_impl_rm0 (ax ax0 :expr → expr → Prop):
(Proper ((ax∨ax0) ==> iff) untyped) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_u ⇒ ax →
(Proper (ut ∧ ax ==> eq ax) rm0) →
(Proper (ut ∧ ax0 ==> eq_expr) rm0) →
(Proper (ut ∧ (eq (ax∨ax0)) ==> eq (ut ∧ ax)) rm0).
Lemma typed_impl_rm0 (ax ax0 :expr → expr → Prop):
(∀ A,Proper ((ax∨ax0) ==> iff) ( has_type A)) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_t ⇒ ax →
(Proper (ty'∧ ax ==> eq ax) rm0) →
(Proper (ty'∧ ax0 ==> eq_expr) rm0) →
(Proper (ty'∧ (eq (ax∨ax0)) ==> eq (ty'∧ ax)) rm0).
Theorem typed_equiv_rm0 (ax ax0 :expr → expr → Prop):
(∀ A,Proper ((ax∨ax0) ==> iff) ( has_type A)) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_t ⇒ ax → zero_eq_t ⇒ ax0 →
(Proper (ty'∧ ax ==> eq ax) rm0) →
(Proper (ty'∧ ax0 ==> eq_expr) rm0) →
∀ e f, (∃ A,A ⊨ e) → (∃ A, A ⊨ f) →
((ax∨ax0) ⊢ e ≡ f ↔ ax ⊢ (rm0 e) ≡ (rm0 f)).
Theorem untyped_equiv_rm0 (ax ax0 :expr → expr → Prop):
(Proper ((ax∨ax0) ==> iff) untyped) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_u ⇒ ax → zero_eq_u ⇒ ax0 →
(Proper (ut ∧ ax ==> eq ax) rm0) →
(Proper (ut ∧ ax0 ==> eq_expr) rm0) →
∀ e f, untyped e → untyped f →
((ax∨ax0) ⊢ e ≡ f ↔ ax ⊢ (rm0 e) ≡ (rm0 f)).
Proper (ty'∧ eq_ν_smpl ==> eq eq_ν_smpl) rm0.
Lemma rm0_eq_ν_smpl_untyped :
Proper (ut ∧ eq_ν_smpl ==> eq eq_ν_smpl) rm0.
Lemma rm0_eq_ω_smpl_typed :
Proper (ty'∧ eq_ω_smpl ==> eq eq_ω_smpl) rm0.
Lemma rm0_eq_perm_elim :
Proper ((eq_perm_elim∨eq_perm)
==> (Logic.eq∨eq_perm_elim∨eq_perm)) rm0.
Lemma rm0_eq_perm_ω :
Proper ((eq_perm_ω)
==> (Logic.eq∨eq_perm_ω)) rm0.
Lemma rm0_t_ka_eq :
Proper (ty'∧ (ka_eq∨ka_eq_t) ==> eq ka_eq_t) rm0.
Lemma rm0_u_ka_eq :
Proper (ut ∧ (ka_eq∨ka_eq_u) ==> eq ka_eq_u) rm0.
Lemma rm0_eq_nom_untyped_p :
Proper (ut ∧ (eq_nom_untyped_p) ==> eq eq_nom_untyped_p) rm0.
Lemma rm0_eq_nom_untyped_np :
Proper (ut ∧ (eq_nom_untyped_np) ==> eq eq_nom_untyped_np) rm0.
Lemma rm0_eq_nom_untyped :
Proper (ut ∧ (eq_nom_untyped) ==> eq eq_nom_untyped) rm0.
Lemma rm0_eq_nom_typed :
Proper (ty'∧ (eq_nom_typed) ==> eq eq_nom_typed) rm0.
Lemma rm0_eq_nom_typed_p :
Proper (eq_nom_typed_p ==> eq eq_nom_typed_p) rm0.
Lemma stronger_Ty_eq_nom_typed_np :
eq_nom_typed_np ⇒ ty'∧ eq_nom_typed_np.
Lemma rm0_eq_nom_typed_np :
Proper (eq_nom_typed_np ==> eq (eq_nom_typed_np)) rm0.
Lemma untyped_impl_rm0 (ax ax0 :expr → expr → Prop):
(Proper ((ax∨ax0) ==> iff) untyped) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_u ⇒ ax →
(Proper (ut ∧ ax ==> eq ax) rm0) →
(Proper (ut ∧ ax0 ==> eq_expr) rm0) →
(Proper (ut ∧ (eq (ax∨ax0)) ==> eq (ut ∧ ax)) rm0).
Lemma typed_impl_rm0 (ax ax0 :expr → expr → Prop):
(∀ A,Proper ((ax∨ax0) ==> iff) ( has_type A)) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_t ⇒ ax →
(Proper (ty'∧ ax ==> eq ax) rm0) →
(Proper (ty'∧ ax0 ==> eq_expr) rm0) →
(Proper (ty'∧ (eq (ax∨ax0)) ==> eq (ty'∧ ax)) rm0).
Theorem typed_equiv_rm0 (ax ax0 :expr → expr → Prop):
(∀ A,Proper ((ax∨ax0) ==> iff) ( has_type A)) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_t ⇒ ax → zero_eq_t ⇒ ax0 →
(Proper (ty'∧ ax ==> eq ax) rm0) →
(Proper (ty'∧ ax0 ==> eq_expr) rm0) →
∀ e f, (∃ A,A ⊨ e) → (∃ A, A ⊨ f) →
((ax∨ax0) ⊢ e ≡ f ↔ ax ⊢ (rm0 e) ≡ (rm0 f)).
Theorem untyped_equiv_rm0 (ax ax0 :expr → expr → Prop):
(Proper ((ax∨ax0) ==> iff) untyped) →
(Proper ((ax∨ax0) ==> Logic.eq) eq0) →
ka_eq_u ⇒ ax → zero_eq_u ⇒ ax0 →
(Proper (ut ∧ ax ==> eq ax) rm0) →
(Proper (ut ∧ ax0 ==> eq_expr) rm0) →
∀ e f, untyped e → untyped f →
((ax∨ax0) ⊢ e ≡ f ↔ ax ⊢ (rm0 e) ≡ (rm0 f)).