Dedicated boolean functions term_fclosed and form_closed (easier that Names.Empty ...)

Meta.v

@@ -1988,3 +1988,48 @@ Proof.
   + apply R_And_e2 with (A := (~f1)%form). apply R_Ax. apply in_eq.
   + apply R_And_e1 with (B := f1). apply R_Ax. apply in_eq.
 Qed.
+
+(** Properties of [term_fclosed] and [form_fclosed] *)
+
+Lemma term_fclosed_spec t : term_fclosed t = true <-> FClosed t.
+Proof.
+ unfold FClosed.
+ induction t using term_ind'; cbn.
+ - rewrite <- Names.is_empty_spec. namedec.
+ - rewrite <- Names.is_empty_spec. reflexivity.
+ - rewrite forallb_forall. unfold Names.Empty.
+   setoid_rewrite unionmap_in. split.
+   + intros F a (t & IN & IN').
+     specialize (F t IN'). rewrite H in F; auto. now apply (F a).
+   + intros G x Hx. rewrite H; auto. intros a Ha. apply (G a).
+     now exists x.
+Qed.
+
+Lemma form_fclosed_spec f : form_fclosed f = true <-> FClosed f.
+Proof.
+ unfold FClosed.
+ induction f; cbn; auto.
+ - rewrite <- Names.is_empty_spec. namedec.
+ - rewrite <- Names.is_empty_spec. namedec.
+ - apply (term_fclosed_spec (Fun "" l)).
+ - rewrite <- andb_lazy_alt, andb_true_iff, IHf1, IHf2.
+   intuition.
+Qed.
+
+Lemma fclosed_bsubst n t f :
+ term_fclosed t = true -> form_fclosed (bsubst n t f) = form_fclosed f.
+Proof.
+ intros E. apply eq_true_iff_eq. rewrite !form_fclosed_spec.
+ rewrite term_fclosed_spec in E. unfold FClosed in *.
+ assert (Names.Equal (fvars (bsubst n t f)) (fvars f)).
+ { intros a. split. rewrite bsubst_fvars. namedec.
+   apply bsubst_fvars'. }
+ now rewrite H.
+Qed.
+
+Lemma fclosed_lift_above n f :
+  form_fclosed (lift_form_above n f) = form_fclosed f.
+Proof.
+ apply eq_true_iff_eq. rewrite !form_fclosed_spec.
+ unfold FClosed. now rewrite fvars_lift_form_above.
+Qed.

Mix.v

@@ -952,3 +952,22 @@ Lemma any_classic d lg : Valid lg d -> Valid Classic d.
 Proof.
  destruct lg. trivial. apply intuit_classic.
 Qed.
+
+(** A direct boolean version of [FClosed], easier to use than
+    [Names.is_empty (fvars ...)] *)
+
+Fixpoint term_fclosed t :=
+  match t with
+  | BVar _ => true
+  | FVar _ => false
+  | Fun _ l => forallb term_fclosed l
+  end.
+
+Fixpoint form_fclosed f :=
+  match f with
+  | True | False => true
+  | Pred _ l => forallb term_fclosed l
+  | Not f => form_fclosed f
+  | Op _ f1 f2 => form_fclosed f1 &&& form_fclosed f2
+  | Quant _ f => form_fclosed f
+  end.

Peano.v

@@ -81,16 +81,8 @@ Proof.
      assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
      { apply level_bsubst'. auto. }
      omega with *.
-   + apply nForall_fclosed. red. cbn.
-     assert (FClosed (bsubst 0 Zero B)).
-     { red. rewrite bsubst_fvars.
-       intro x. rewrite Names.union_spec. cbn. red in HB'. intuition. }
-     assert (FClosed (bsubst 0 (Succ(BVar 0)) B)).
-     { red. rewrite bsubst_fvars.
-       intro x. rewrite Names.union_spec. cbn - [Names.union].
-       rewrite Names.union_spec.
-       generalize (HB' x) (@Names.empty_spec x). intuition. }
-     unfold FClosed in *. intuition.
+   + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
+     cbn. now rewrite !fclosed_bsubst, HB'.
 Qed.
 
 End PeanoAx.

Theories.v

@@ -20,16 +20,16 @@ Definition Wf (sign:signature) (A:formula) :=
 Hint Unfold Wf.
 
 Definition isWf sign (A:formula) :=
-  check sign A && (level A =? 0) && Names.is_empty (fvars A).
+  check sign A && (level A =? 0) && form_fclosed A.
 
 Lemma Wf_spec sign A : reflect (Wf sign A) (isWf sign A).
 Proof.
- unfold Wf, isWf, BClosed, FClosed.
+ unfold Wf, isWf, BClosed.
  destruct check; simpl; [ | constructor; easy].
  case eqbspec; simpl; intros; [ | constructor; easy ].
- destruct (Names.is_empty (fvars A)) eqn:E.
- - rewrite Names.is_empty_spec in E. now constructor.
- - constructor. rewrite <- Names.is_empty_spec, E. easy.
+ destruct (form_fclosed A) eqn:E.
+ - rewrite form_fclosed_spec in E. now constructor.
+ - constructor. rewrite <- form_fclosed_spec, E. easy.
 Qed.
 
 Lemma Wf_iff sign A : Wf sign A <-> isWf sign A = true.
@@ -1417,4 +1417,4 @@ Proof.
  - now apply supercomplete_complete.
 Qed.
 
-End SomeLogic.
\ No newline at end of file
+End SomeLogic.

ZF.v

@@ -146,11 +146,6 @@ Proof.
 symmetry. apply Nat.max_monotone. red. red. auto with *.
 Qed.
 
-Lemma empty_alt a : Names.Empty a <-> Names.eq a Names.empty.
-Proof.
-unfold Names.eq. intuition.
-Qed.
-
 Lemma WfAx A : IsAx A -> Wf ZFSign A.
 Proof.
  intros [ IN | [ (B & -> & HB & HB') | (C & -> & HC & HC') ] ].
@@ -167,12 +162,8 @@ Proof.
      assert (H := level_lift_form_above B 1).
      apply Nat.sub_0_le.
      repeat apply Nat.max_lub; omega with *.
-   + apply nForall_fclosed. red.
-     apply-> Names.is_empty_spec. cbn -[Names.union].
-     rewrite fvars_lift_form_above.
-     apply empty_alt in HB'.
-     rewrite HB'.
-     reflexivity.
+   + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
+     cbn. now rewrite fclosed_lift_above, HB'.
  - repeat split; unfold replacement_schema; cbn.
    + rewrite nForall_check. cbn.
      rewrite !check_lift_form_above, HC.
@@ -184,13 +175,8 @@ Proof.
      assert (H' := level_lift_form_above C 2).
      apply Nat.sub_0_le.
      repeat apply Nat.max_lub; omega with *.
-   + apply nForall_fclosed. red.
-     apply-> Names.is_empty_spec. cbn -[Names.union].
-     rewrite fvars_lift_form_above.
-     apply empty_alt in HC'.
-     assert (H := fvars_lift_form_above C 2).
-     rewrite H, !HC'.
-     reflexivity.
+   + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
+     cbn. now rewrite !fclosed_lift_above, HC'.
 Qed.
 
 End ZFAx.
@@ -255,4 +241,4 @@ Proof.
 Qed.
 
 Lemma union : IsTheorem Intuiti ZF (∀∀∃∀ (#0 ∈ #1 <-> #0 ∈ #2 \/ #0 ∈ #3)).
-Admitted.
\ No newline at end of file
+Admitted.