add(named): free variable invariance of the C equivalence (M5 metatheory)

graphs/dependency.dot

@@ -85,6 +85,9 @@ digraph theorem_deps {
   nred_core_fv [label="nred_core_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_core_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   nplug_esub_fv [label="nplug_esub_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nplug_esub_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   nred_fv [label="nred_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  in_filter_neq_iff [label="in_filter_neq_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_filter_neq_iff theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_fv_both [label="Es_fv_both", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_fv_both theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_fv [label="Es_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -203,6 +206,9 @@ digraph theorem_deps {
   nplug_esub_fv -> nred_fv;
   nplug_fv_mono -> nred_fv;
   nplug_fv_upper -> nred_fv;
+  in_filter_neq_iff -> Es_fv_both;
+  nplug_fv_mono -> Es_fv_both;
+  Es_fv_both -> Es_fv;
   par_red1_iff -> par_to_red1_or_eq;
   par_red1_iff -> red1_or_eq_to_par;
   has_red_spec -> check_term_true;

graphs/index.txt

@@ -1,5 +1,7 @@
 status	milestone	kind	name	file
 proved	M0	infra	Es_ctx_any	theory/NamedMeta.v
+proved	M0	infra	Es_fv	theory/NamedMeta.v
+proved	M0	infra	Es_fv_both	theory/NamedMeta.v
 proved	M0	infra	Es_refl_any	theory/NamedMeta.v
 proved	M0	infra	Es_sym_any	theory/NamedMeta.v
 proved	M0	infra	Es_trans_any	theory/NamedMeta.v
@@ -7,6 +9,7 @@ proved	M0	infra	Plus_mred_of_Plus_red1	theory/Metaterm.v
 proved	M0	infra	eqC_in_Es	theory/NamedMeta.v
 proved	M0	infra	filter_neq_in	theory/NamedMeta.v
 proved	M0	infra	in_filter_neq	theory/NamedMeta.v
+proved	M0	infra	in_filter_neq_iff	theory/NamedMeta.v
 proved	M0	infra	isubst_meta_in	theory/NamedMeta.v
 proved	M0	infra	isubst_meta_notin	theory/NamedMeta.v
 proved	M0	infra	mfvs_close_m	theory/Metaterm.v

graphs/theorems.json

@@ -879,6 +879,41 @@
         "nplug_fv_upper"
       ]
     },
+    {
+      "id": "in_filter_neq_iff",
+      "label": "in_filter_neq_iff",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "Es_fv_both",
+      "label": "Es_fv_both",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": [
+        "in_filter_neq_iff",
+        "nplug_fv_mono"
+      ]
+    },
+    {
+      "id": "Es_fv",
+      "label": "Es_fv",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": [
+        "Es_fv_both"
+      ]
+    },
     {
       "id": "par_red1_iff",
       "label": "par_red1_iff",

theory/NamedMeta.v

@@ -300,3 +300,58 @@ Qed.
 
 Print Assumptions nplug_esub_fv.
 Print Assumptions nred_fv.
+
+Lemma in_filter_neq_iff : forall z a l,
+  In z (filter (fun w => negb (Nat.eqb w a)) l) <-> In z l /\ z <> a.
+Proof.
+  intros z a l. split.
+  - intro H. apply filter_In in H. destruct H as [Hl Hp]. split; [exact Hl |].
+    apply Nat.eqb_neq. destruct (Nat.eqb z a) eqn:E; [| reflexivity].
+    simpl in Hp. discriminate Hp.
+  - intros [Hl Hne]. apply filter_In. split; [exact Hl |].
+    apply Nat.eqb_neq in Hne. rewrite Hne. reflexivity.
+Qed.
+
+Lemma Es_fv_both : forall t u, Es t u ->
+  incl (nfv t) (nfv u) /\ incl (nfv u) (nfv t).
+Proof.
+  apply Es_ind.
+  - intros t0. split; unfold incl; auto.
+  - intros t0 u0 H1 IH1. split.
+    + apply (proj2 IH1).
+    + apply (proj1 IH1).
+  - intros t0 u0 v0 H1 H2 IH1 IH2. split.
+    + intros z Hz. apply (proj1 IH2). apply (proj1 H2). exact Hz.
+    + intros z Hz. apply (proj2 H2). apply (proj2 IH2). exact Hz.
+  - intros t0 x0 u0 y0 v0 Hyx Hyu Hxv. split; unfold incl; intros z Hz; simpl in *;
+    apply in_app_iff in Hz as [Hz|Hz].
+    + apply in_filter_neq_iff in Hz as [Hz Hy]. apply in_app_iff in Hz as [Hz|Hz].
+      * apply in_filter_neq_iff in Hz as [Hz Hx].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [| exact Hx].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [exact Hz | exact Hy].
+      * apply in_app_iff. right. exact Hz.
+    + apply in_app_iff. left. apply in_filter_neq_iff. split; [| ].
+      * apply in_app_iff. right. exact Hz.
+      * intro E. apply Hxv. subst z. exact Hz.
+    + apply in_filter_neq_iff in Hz as [Hz Hx]. apply in_app_iff in Hz as [Hz|Hz].
+      * apply in_filter_neq_iff in Hz as [Hz Hy].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [| exact Hy].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [exact Hz | exact Hx].
+      * apply in_app_iff. right. exact Hz.
+    + apply in_app_iff. left. apply in_filter_neq_iff. split; [| ].
+      * apply in_app_iff. right. exact Hz.
+      * intro E. apply Hyu. subst z. exact Hz.
+  - intros C0 t0 t0' H1 IH1. split; apply nplug_fv_mono.
+    + apply (proj1 IH1).
+    + apply (proj2 IH1).
+Qed.
+
+Lemma Es_fv : forall t u, Es t u -> forall z, In z (nfv t) <-> In z (nfv u).
+Proof.
+  intros t u H z. destruct (Es_fv_both t u H) as [Htu Hut]. split.
+  - apply Htu.
+  - apply Hut.
+Qed.
+
+Print Assumptions in_filter_neq_iff.
+Print Assumptions Es_fv.