add more morphisms (#148)

* add more morphisms * change arrows
Beluga-lang · Aug 1, 2024 · 946b8c4 · 946b8c4
1 parent 9fa1a23
commit 946b8c4
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 1 deletion.
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
@@ -51,7 +51,7 @@ Proof.
     pose proof (wf_ctx_sub_length _ _ Hτ).
     transitivity {{{#(length Γ1) [Id]}}}; [mauto 3 |].
     rewrite H1, var_arith, H.
-    bulky_rewrite. mauto 3.
+    bulky_rewrite.
   - pose proof (app_ctx_vlookup _ _ _ _ HΔ0 eq_refl).
     pose proof (app_ctx_lookup Γ1 T0 Γ2 _ eq_refl).
     gen_presup H2.

diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
@@ -64,3 +64,39 @@ Proof.
   - eauto using ctx_eq_sym.
   - eauto using ctx_eq_trans.
 Qed.
+
+
+
+Add Parametric Morphism : wf_exp
+  with signature wf_ctx_eq ==> eq ==> eq ==> iff as ctxeq_exp_morphism.
+Proof.
+  intros. split; mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_exp_eq
+  with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as ctxeq_exp_eq_morphism.
+Proof.
+  intros. split; mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_sub
+  with signature wf_ctx_eq ==> eq ==> eq ==> iff as ctxeq_sub_morphism.
+Proof.
+  intros. split; mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_sub_eq
+  with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as ctxeq_sub_eq_morphism.
+Proof.
+  intros. split; mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_subtyping
+  with signature wf_ctx_eq ==> eq ==> eq ==> iff as ctxeq_subtyping_morphism.
+Proof.
+  intros. split; mauto 3.
+Qed.
diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v
@@ -112,3 +112,31 @@ Add Parametric Morphism : wf_exp
 Proof.
   cbv. intros. mauto 3.
 Qed.
+
+
+Add Parametric Morphism : wf_exp_eq
+  with signature wf_ctx_sub --> eq ==> eq ==> eq ==> Basics.impl as ctxsub_exp_eq_morphism.
+Proof.
+  cbv. intros. mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_sub
+  with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_sub_morphism.
+Proof.
+  cbv. intros. mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_sub_eq
+  with signature wf_ctx_sub --> eq ==> eq ==> eq ==> Basics.impl as ctxsub_sub_eq_morphism.
+Proof.
+  cbv. intros. mauto 3.
+Qed.
+
+
+Add Parametric Morphism : wf_subtyping
+  with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_subtyping_morphism.
+Proof.
+  cbv. intros. mauto 3.
+Qed.