Pr and Valid without BClosed in All_e, Ex_i

Equiv2.v

@@ -159,12 +159,8 @@ Proof.
    + rewrite V. symmetry. apply nam2mix_bsubst0_var.
    + rewrite U, V, nam2mix_ctx_fvars.
      rewrite nam2mix_fvars. simpl. namedec.
- - rewrite nam2mix_subst_bsubst0.
-   rewrite nam2mix_term_bclosed, eqb_refl.
-   apply andb_true_r.
- - rewrite nam2mix_subst_bsubst0.
-   rewrite nam2mix_term_bclosed, eqb_refl.
-   apply andb_true_r.
+ - rewrite nam2mix_subst_bsubst0; auto.
+ - rewrite nam2mix_subst_bsubst0; auto.
  - cbn.
    apply eq_true_iff_eq.
    rewrite !andb_true_iff.

Meta.v

@@ -1397,13 +1397,11 @@ Proof.
       f_equal. apply restrict_bsubst.
   - rewrite restrict_bsubst.
     constructor.
-    + now apply restrict_term_bclosed.
     + apply IHValid; namedec.
-    + unfold Claim. rewrite claim_restrict. now rewrite H2.
+    + unfold Claim. rewrite claim_restrict. now rewrite H1.
   - constructor.
-    + now apply restrict_term_bclosed.
     + apply IHValid; namedec.
-    + unfold Claim. rewrite claim_restrict. rewrite H2.
+    + unfold Claim. rewrite claim_restrict. rewrite H1.
       cbn. now rewrite restrict_bsubst.
   - apply V_Ex_e with (restrict sign x A).
     + cbn. rewrite restrict_ctx_fvars, !restrict_form_fvars. namedec.
@@ -1521,10 +1519,6 @@ Definition forcelevel_ctx x (c:context) :=
 Definition forcelevel_seq x '(c ⊢ f) :=
  forcelevel_ctx x c ⊢ forcelevel 0 x f.
 
-(** Normally the witnesses in [rule_kind] are already BClosed,
-    at least for valid derivations. Forcing it nonetheless
-    allow to write a few lemmas below without preconditions. *)
-
 Definition forcelevel_rule x r :=
  match r with
  | All_e wit => All_e (forcelevel_term 0 x wit)
@@ -1717,26 +1711,25 @@ Proof.
  - f_equal. rewrite !map_map. apply map_ext_iff; auto.
 Qed.
 
-Lemma forcelevel_bsubst_term' n x (u t:term) :
-  level u <= n ->
-  forcelevel_term n x (bsubst n u t) =
-  bsubst n u (forcelevel_term (S n) x t).
+Lemma forcelevel_lift n x u :
+  forcelevel_term (S n) x (lift u) = lift (forcelevel_term n x u).
 Proof.
- intros Hu.
- rewrite forcelevel_bsubst_term. f_equal.
- now apply forcelevel_term_id.
+ induction u using term_ind'; simpl; auto.
+ - change (S n0 <? S n) with (n0 <? n).
+   case Nat.ltb_spec; simpl; auto.
+ - f_equal. rewrite !map_map. apply map_ext_in; auto.
 Qed.
 
 Lemma forcelevel_bsubst n x u f :
-  level u <= n ->
   forcelevel n x (bsubst n u f) =
-  bsubst n u (forcelevel (S n) x f).
+  bsubst n (forcelevel_term n x u) (forcelevel (S n) x f).
 Proof.
  revert n u.
  induction f; cbn; intros; f_equal; auto.
- rewrite !map_map. apply map_ext_iff.
- auto using forcelevel_bsubst_term'.
- apply IHf. transitivity (S (level u)). apply level_lift. omega.
+ - rewrite !map_map. apply map_ext_iff.
+   auto using forcelevel_bsubst_term.
+ - rewrite IHf.
+   f_equal. apply forcelevel_lift.
 Qed.
 
 Ltac solver' :=
@@ -1760,16 +1753,14 @@ Proof.
    + apply IHValid. namedec.
    + unfold Claim; rewrite claim_forcelevel, H2. cbn. f_equal.
      rewrite forcelevel_bsubst; auto.
- - rewrite forcelevel_bsubst by now rewrite H0.
-   rewrite forcelevel_term_id by now rewrite H0.
+ - rewrite forcelevel_bsubst.
    constructor; auto.
    + apply IHValid; namedec.
-   + unfold Claim. now rewrite claim_forcelevel, H2.
- - rewrite forcelevel_term_id by now rewrite H0.
-   constructor; auto.
+   + unfold Claim. now rewrite claim_forcelevel, H1.
+ - constructor; auto.
    + apply IHValid. namedec.
-   + unfold Claim; rewrite claim_forcelevel, H2. cbn. f_equal.
-     apply forcelevel_bsubst; now rewrite H0.
+   + unfold Claim; rewrite claim_forcelevel, H1. cbn. f_equal.
+     apply forcelevel_bsubst.
  - apply V_Ex_e with (forcelevel 1 x A).
    + cbn. rewrite forcelevel_ctx_fvars, !forcelevel_fvars. namedec.
    + apply IHValid1. namedec.
@@ -1840,4 +1831,4 @@ Proof.
  - apply restrict_forcelevel_seq.
  - rewrite !map_map. apply map_ext_iff.
    rewrite Forall_forall in IH; auto.
-Qed.
+Qed.
\ No newline at end of file

Mix.v

@@ -329,8 +329,8 @@ Instance form_level : Level formula :=
     Note : we try to do something sensible when [t] has itself some
     bounded variables (we lift them when entering [f]'s quantifiers).
     But this situtation is nonetheless to be used with caution.
-    Actually, we'll almost always use [bsubst] when [t] is [BClosed],
-    except in [Peano.v]. *)
+    Actually, we'll mostly use [bsubst] when [t] is [BClosed].
+    Notable exception : induction schema in Peano.v *)
 
 Instance form_bsubst : BSubst formula :=
  fix form_bsubst n t f :=
@@ -514,22 +514,26 @@ Instance vmap_rule : VMap rule_kind :=
 (** Validity of a derivation : is it using correct rules
     of classical logic (resp. intuitionistic logic) ? *)
 
-(** Note that we require the witness terms in rules ∀e and ∃i
-    to be [BClosed] (i.e. without any [BVar]). Otherwise
-    awkward things may happen due to our implementation
-    of [bsubst].
-
-    For instance think of [∀ ∃ ~(Pred "=" [#0;#1])] i.e.
+(** Note : this validity notion does *not* ensure that
+    the terms and formulas in this derivation are well-formed
+    (i.e. have no unbound [BVar] variables and properly use
+    the symbols of a signature). We will see later how to
+    "force" a derivation to be well-formed (see [Meta.forcelevel]
+    and [Meta.restrict]).
+
+    In particular, forcing here all formulas to be [BClosed] would
+    be tedious. See for instance [Fa_e] below, any formula can be
+    deduced from [False], even non-well-formed ones. In a former
+    version of this work, [BClosed] conditions were imposed on
+    [All_e] and [Ex_i] witnesses [t], but this isn't mandatory
+    anymore now that [subst] incorporates a [lift] operation.
+
+    Example of earlier issue : consider [∀ ∃ ~(Pred "=" [#0;#1])] i.e.
     [∀x∃y,x≠y], a possible way of saying that the world isn't
-    a singleton. With an unrestricted ∀e, we could deduce
-    [bsubst 0 (#0) (∃ ~(Pred "=" [#0;#1]))] which reduces
-    to [∃ ~(Pred "=" [#0;#0])], a formula negating the reflexivity
-    of equality !
-
-    Apart from these witnesses, the rest of the derivation
-    could technically have unbounded variables, even though
-    we intend all derivations to be [BClosed]. We will be able
-    to force this later on (see [Meta.forcelevel])
+    a singleton. By [∀e] we can deduce
+    [bsubst 0 (#0) (∃ ~(Pred "=" [#0;#1]))], and without [lift] this
+    was reducing to [∃ ~(Pred "=" [#0;#0])], a formula negating
+    the reflexivity of equality !
 *)
 
 Definition valid_deriv_step logic '(Rule r s ld) :=
@@ -555,9 +559,9 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
      (Γ =? Γ') &&& (A' =? bsubst 0 (FVar x) A)
      &&& negb (Names.mem x (fvars (Γ⊢A)))
   | All_e t, (Γ ⊢ B), [Γ'⊢ ∀A] =>
-    (Γ =? Γ') &&& (B =? bsubst 0 t A) &&& (level t =? 0)
+    (Γ =? Γ') &&& (B =? bsubst 0 t A)
   | Ex_i t,  (Γ ⊢ ∃A), [Γ'⊢B] =>
-    (Γ =? Γ') &&& (B =? bsubst 0 t A) &&& (level t =? 0)
+    (Γ =? Γ') &&& (B =? bsubst 0 t A)
   | Ex_e x,  s, [Γ⊢∃A; A'::Γ'⊢B] =>
      (s =? (Γ ⊢ B)) &&& (Γ' =? Γ)
      &&& (A' =? bsubst 0 (FVar x) A)
@@ -765,10 +769,10 @@ Inductive Valid (l:logic) : derivation -> Prop :=
      Valid l d -> Claim d (Γ ⊢ bsubst 0 (FVar x) A) ->
      Valid l (Rule (All_i x) (Γ ⊢ ∀A) [d])
  | V_All_e t d Γ A :
-     BClosed t -> Valid l d -> Claim d (Γ ⊢ ∀A) ->
+     Valid l d -> Claim d (Γ ⊢ ∀A) ->
      Valid l (Rule (All_e t) (Γ ⊢ bsubst 0 t A) [d])
  | V_Ex_i t d Γ A :
-     BClosed t -> Valid l d -> Claim d (Γ ⊢ bsubst 0 t A) ->
+     Valid l d -> Claim d (Γ ⊢ bsubst 0 t A) ->
      Valid l (Rule (Ex_i t) (Γ ⊢ ∃A) [d])
  | V_Ex_e x d1 d2 Γ A B :
      ~Names.In x (fvars (A::Γ⊢B)) ->
@@ -879,10 +883,8 @@ Inductive Pr (l:logic) : sequent -> Prop :=
  | R_All_i x Γ A : ~Names.In x (fvars (Γ ⊢ A)) ->
                    Pr l (Γ ⊢ bsubst 0 (FVar x) A) ->
                    Pr l (Γ ⊢ ∀A)
- | R_All_e t Γ A : BClosed t -> Pr l (Γ ⊢ ∀A) ->
-                   Pr l (Γ ⊢ bsubst 0 t A)
- | R_Ex_i t Γ A : BClosed t -> Pr l (Γ ⊢ bsubst 0 t A) ->
-                  Pr l (Γ ⊢ ∃A)
+ | R_All_e t Γ A : Pr l (Γ ⊢ ∀A) -> Pr l (Γ ⊢ bsubst 0 t A)
+ | R_Ex_i t Γ A : Pr l (Γ ⊢ bsubst 0 t A) -> Pr l (Γ ⊢ ∃A)
  | R_Ex_e x Γ A B : ~Names.In x (fvars (A::Γ⊢B)) ->
       Pr l (Γ ⊢ ∃A) -> Pr l ((bsubst 0 (FVar x) A)::Γ ⊢ B) ->
       Pr l (Γ ⊢ B)
@@ -1011,4 +1013,4 @@ Qed.
 Lemma any_classic d lg : Valid lg d -> Valid Classic d.
 Proof.
  destruct lg. trivial. apply intuit_classic.
-Qed.
+Qed.
\ No newline at end of file

Models.v

@@ -631,17 +631,16 @@ Proof.
  intros WFt (WFA & axs & F & P).
  split. apply Wf_bsubst; auto.
  exists axs. split; auto.
- apply R_All_e; auto. apply WFt.
 Qed.
 
-Lemma thm_ex_i logic A t : Wf th (∃A) -> Wf_term th t ->
+Lemma thm_ex_i logic A t : Wf th (∃A) ->
  IsTheorem logic th (bsubst 0 t A) ->
  IsTheorem logic th (∃A).
 Proof.
- intros WFA WFt (_ & axs & F & P).
+ intros WFA (_ & axs & F & P).
  split; auto.
  exists axs. split; auto.
- apply R_Ex_i with t; auto. apply WFt.
+ apply R_Ex_i with t; auto.
 Qed.
 
 

Peano.v

@@ -107,76 +107,76 @@ Definition PeanoTheory :=
 
 Import PeanoAx.
 
-Lemma Symmetry : forall logic A B Γ, BClosed A -> BClosed B -> In ax2 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = A).
+Lemma Symmetry : forall logic A B Γ, BClosed A -> In ax2 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = A).
 Proof.
   intros.
   apply R_Imp_e with (A := A = B); [ | assumption ].
   assert (AX2 : Pr logic (Γ ⊢ ax2)).
-  { apply R_Ax. exact H1. }
+  { apply R_Ax. exact H0. }
   unfold ax2 in AX2.
-  apply R_All_e with (t := A) in AX2; [ | assumption ].
-  apply R_All_e with (t := B) in AX2; [ | assumption ].
+  apply R_All_e with (t := A) in AX2.
+  apply R_All_e with (t := B) in AX2.
   cbn in AX2.
   assert (bsubst 0 B (lift A) = A).
-  { assert (lift A = A). { apply lift_nop. exact H. } rewrite H3. apply bclosed_bsubst_id. exact H. }
-  rewrite H3 in AX2.
+  { assert (lift A = A). { apply lift_nop. exact H. } rewrite H2. apply bclosed_bsubst_id. exact H. }
+  rewrite H2 in AX2.
   exact AX2.
 Qed.
 
-Lemma Transitivity : forall logic A B C Γ, BClosed A -> BClosed B -> BClosed C -> In ax3 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = C) -> Pr logic (Γ ⊢ A = C).
+Lemma Transitivity : forall logic A B C Γ, BClosed A -> BClosed B -> In ax3 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = C) -> Pr logic (Γ ⊢ A = C).
 Proof.
   intros.
   apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ].
   assert (AX3 : Pr logic (Γ ⊢ ax3)).
-  { apply R_Ax. exact H2. }
+  { apply R_Ax. exact H1. }
   unfold ax3 in AX3.
-  apply R_All_e with (t := A) in AX3; [ | assumption ].
-  apply R_All_e with (t := B) in AX3; [ | assumption ].
-  apply R_All_e with (t := C) in AX3; [ | assumption ].
+  apply R_All_e with (t := A) in AX3.
+  apply R_All_e with (t := B) in AX3.
+  apply R_All_e with (t := C) in AX3.
   cbn in AX3.
   assert (bsubst 0 C (lift B) = B).
-  { assert (lift B = B). {apply lift_nop. assumption. } rewrite H5. apply bclosed_bsubst_id. assumption. }
-  rewrite H5 in AX3.
+  { assert (lift B = B). {apply lift_nop. assumption. } rewrite H4. apply bclosed_bsubst_id. assumption. }
+  rewrite H4 in AX3.
   assert (bsubst 0 C (bsubst 1 (lift B) (lift (lift A))) = A).
-  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H6. rewrite H6.
-    assert (lift B = B). { apply lift_nop. assumption. } rewrite H7.
-    assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H8.
+  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5.
+    assert (lift B = B). { apply lift_nop. assumption. } rewrite H6.
+    assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H7.
     apply bclosed_bsubst_id. assumption. }
-  rewrite H6 in AX3.
+  rewrite H5 in AX3.
   assumption.
 Qed.
 
-Lemma Hereditarity : forall logic A B Γ, BClosed A -> BClosed B -> In ax4 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ Succ A = Succ B).
+Lemma Hereditarity : forall logic A B Γ, BClosed A -> In ax4 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ Succ A = Succ B).
 Proof.
   intros.
   apply R_Imp_e with (A := A = B); [ | assumption ].
   assert (AX4 : Pr logic (Γ ⊢ ax4)).
   { apply R_Ax. assumption. }
   unfold ax4 in AX4.
-  apply R_All_e with (t := A) in AX4; [ | assumption ].
-  apply R_All_e with (t := B) in AX4; [ | assumption ].
+  apply R_All_e with (t := A) in AX4.
+  apply R_All_e with (t := B) in AX4.
   cbn in AX4.
   assert (bsubst 0 B (lift A) = A).
-  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H3.
+  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2.
     apply bclosed_bsubst_id. assumption. }
-  rewrite H3 in AX4.
+  rewrite H2 in AX4.
   assumption.
 Qed.
 
-Lemma AntiHereditarity : forall logic A B Γ, BClosed A -> BClosed B -> In ax13 Γ -> Pr logic (Γ ⊢ Succ A = Succ B) -> Pr logic (Γ ⊢ A = B).
+Lemma AntiHereditarity : forall logic A B Γ, BClosed A -> In ax13 Γ -> Pr logic (Γ ⊢ Succ A = Succ B) -> Pr logic (Γ ⊢ A = B).
 Proof.
   intros.
   apply R_Imp_e with (A := Succ A = Succ B); [ | assumption ].
   assert (AX13 : Pr logic (Γ ⊢ ax13)).
   { apply R_Ax. assumption. }
   unfold ax13 in AX13.
-  apply R_All_e with (t := A) in AX13; [ | assumption ].
-  apply R_All_e with (t := B) in AX13; [ | assumption ].
+  apply R_All_e with (t := A) in AX13.
+  apply R_All_e with (t := B) in AX13.
   cbn in AX13.
   assert (bsubst 0 B (lift A) = A).
-  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H3.
+  { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2.
     apply bclosed_bsubst_id. assumption. }
-  rewrite H3 in AX13.
+  rewrite H2 in AX13.
   assumption.
 Qed.
 
@@ -235,7 +235,7 @@ Ltac calc :=
 Ltac inst H l :=
   match l with
   | [] => idtac
-  | (?u::?l) => apply R_All_e with (t := u) in H; [ inst H l | calc ]
+  | (?u::?l) => apply R_All_e with (t := u) in H; inst H l
   end.
 
 Ltac axiom ax name :=

PreModels.v

@@ -403,15 +403,21 @@ Qed.
 Lemma coherence logic : CoqRequirements logic ->
  forall (d:derivation),
  Valid logic d ->
- BClosed d ->
  ~Claim d ([]⊢False).
 Proof.
- intros CR d VD CL E.
- red in E.
+ intros CR d VD E.
+ destruct (exist_fresh (fvars d)) as (x,Hx).
+ assert (VD' := forcelevel_deriv_valid logic x d Hx VD).
+ assert (BC' := forcelevel_deriv_bclosed x d).
+ set (d' := forcelevel_deriv x d) in *.
+ assert (E' : Claim d' ([] ⊢ False)).
+ { unfold d', Claim. now rewrite claim_forcelevel, E. }
+ clearbody d'.
+ red in E'.
  set (genv := fun (_:variable) => Mo.(someone)).
- assert (interp_seq genv [] (claim d)).
+ assert (interp_seq genv [] (claim d')).
  { apply correctness with logic; auto. }
- rewrite E in H. cbn in *. apply H. intros A. destruct 1.
+ rewrite E' in H. cbn in *. apply H. intros A. destruct 1.
 Qed.
 
 End PREMODEL.