Réparation conflit

Meta.v

@@ -15,61 +15,55 @@ Implicit Type f : formula.
 
 (** Properties of [lift] *)
 
-Lemma level_lift t : level (lift t) <= S (level t).
+Lemma level_lift k t : level (lift k t) <= S (level t).
 Proof.
  induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
- rewrite map_map.
- apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
- rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
+ - case Nat.leb_spec; auto.
+ - rewrite map_map.
+   apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
+   rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
 Qed.
 
-Lemma lift_nop t : BClosed t -> lift t = t.
+Lemma lift_nop_le k t : level t <= k -> lift k t = t.
 Proof.
- unfold BClosed.
  induction t as [ | | f l IH] using term_ind'; cbn; auto.
- - easy.
- - rewrite list_max_map_0. intros H. f_equal. apply map_id_iff; auto.
+ - case Nat.leb_spec; auto. omega.
+ - rewrite list_max_map_le. intros H. f_equal. apply map_id_iff; auto.
 Qed.
 
-Lemma check_lift sign t :
- check sign (lift t) = check sign t.
+Lemma lift_nop k t : BClosed t -> lift k t = t.
 Proof.
- induction t as [ | | f l IH] using term_ind'; cbn; auto.
- destruct funsymbs; auto.
- rewrite map_length. case eqb; auto.
- apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
- split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
+ unfold BClosed. intros H. apply lift_nop_le. rewrite H; omega.
 Qed.
 
-Lemma lift_fvars t : fvars (lift t) = fvars t.
+Lemma check_lift sign k t :
+ check sign (lift k t) = check sign t.
 Proof.
- induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
- induction l; simpl; auto.
- rewrite IH, IHl; simpl; auto.
- intros x Hx. apply IH. simpl; auto.
+ induction t as [ | | f l IH] using term_ind'; cbn; auto.
+ - case Nat.leb_spec; auto.
+ - destruct funsymbs; auto.
+   rewrite map_length. case eqb; auto.
+   apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
+   split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
 Qed.
 
-(** Properties of [lift_above] *)
-
-Lemma level_lift_above t k :
-  level (lift_above k t) <= S (level t).
+Lemma fvars_lift k t : fvars (lift k t) = fvars t.
 Proof.
-  induction t using term_ind'; cbn; auto with arith.
-  + destruct (k <=? n); cbn; omega.
-  + rewrite map_map.
-    apply list_max_map_le. intros. transitivity (S (level a)); auto.
-    rewrite<- Nat.succ_le_mono. now apply list_max_map_in.
+ induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
+ - case Nat.leb_spec; auto.
+ - induction l; simpl; auto.
+   rewrite IH, IHl; simpl; auto.
+   intros x Hx. apply IH. simpl; auto.
 Qed.
 
-Lemma level_lift_form_above f k :
-  level (lift_form_above k f) <= S (level f).
+Lemma level_lift_form k f : level (lift k f) <= S (level f).
 Proof.
   revert k. induction f; intro; cbn; auto with arith.
   + rewrite map_map.
     rewrite list_max_map_le.
     intros.
     transitivity (S (level a)).
-    - apply level_lift_above.
+    - apply level_lift.
     - apply-> Nat.succ_le_mono.
       apply list_max_map_in.
       assumption.
@@ -80,46 +74,25 @@ Proof.
     omega.
 Qed.
 
-Lemma check_lift_above sign t k :
-  check sign (lift_above k t) = check sign t.
-Proof.
-  induction t as [ | | f l IH] using term_ind'; cbn; auto.
-  + destruct (k <=? n); auto.
-  + destruct funsymbs; auto.
-    rewrite map_length. case eqb; auto.
-    apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
-    split; intros H x Hx. rewrite<- IH; auto. rewrite IH; auto.
-Qed.
-
-Lemma check_lift_form_above sign f k :
-  check sign (lift_form_above k f) = check sign f.
+Lemma check_lift_form sign f k :
+  check sign (lift k f) = check sign f.
 Proof.
   revert k. induction f; cbn; auto.
   + destruct (predsymbs sign p); auto.
     intro. rewrite map_length. case eqb; auto.
     apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
     split; intros.
-    - destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
-    - destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
+    - destruct H with (x := x); auto. rewrite check_lift. reflexivity.
+    - destruct H with (x := x); auto. rewrite check_lift. reflexivity.
   + intro. rewrite IHf1. rewrite IHf2. reflexivity.
 Qed.
 
-Lemma fvars_lift_above t k :
-  fvars (lift_above k t) = fvars t.
-Proof.
-  induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
-  - destruct (k <=? n); auto.
-  - induction l; simpl; auto.
-    rewrite IH, IHl; simpl; auto.
-    intros x Hx. apply IH. simpl; auto.
-Qed.
-
-Lemma fvars_lift_form_above f k :
-  fvars (lift_form_above k f) = fvars f.
+Lemma fvars_lift_form f k :
+  fvars (lift k f) = fvars f.
 Proof.
   revert k. induction f; intro; cbn; auto with *.
   - induction l; simpl; auto.
-    rewrite fvars_lift_above, IHl; simpl; auto.
+    rewrite fvars_lift, IHl; simpl; auto.
   - rewrite IHf1. rewrite IHf2. auto.
 Qed.
 
@@ -172,8 +145,8 @@ Proof.
  induction f; intros; cbn -[Nat.max]; auto with arith.
  - apply (level_bsubst_term_max n u (Fun "" l)).
  - specialize (IHf1 n u). specialize (IHf2 n u). omega with *.
- - assert (H := level_lift u).
-   specialize (IHf (S n) (lift u)). omega with *.
+ - assert (H := level_lift 0 u).
+   specialize (IHf (S n) (lift 0 u)). omega with *.
 Qed.
 
 Lemma level_bsubst_term n (u t:term) :
@@ -234,7 +207,7 @@ Proof.
  induction f; cbn; intros; auto with *.
  - apply (bsubst_term_fvars n u (Fun "" l)).
  - rewrite IHf1, IHf2. namedec.
- - rewrite IHf. now rewrite lift_fvars.
+ - rewrite IHf. now rewrite fvars_lift.
 Qed.
 
 Lemma bsubst_ctx_fvars n u (c:context) :
@@ -494,16 +467,17 @@ Qed.
 Definition BClosed_sub (h:variable->term) :=
  forall v, BClosed (h v).
 
-Lemma lift_vmap (h:variable->term) t :
- lift (vmap h t) = vmap (fun v => lift (h v)) (lift t).
+Lemma lift_vmap (h:variable->term) k t :
+ lift k (vmap h t) = vmap (fun v => lift k (h v)) (lift k t).
 Proof.
  induction t as [ | | f l IH] using term_ind'; cbn; auto.
- f_equal. rewrite !map_map. apply map_ext_iff; auto.
+ - case Nat.leb_spec; auto.
+ - f_equal. rewrite !map_map. apply map_ext_iff; auto.
 Qed.
 
-Lemma lift_vmap' (h:variable->term) t :
+Lemma lift_vmap' (h:variable->term) k t :
  BClosed_sub h ->
- lift (vmap h t) = vmap h (lift t).
+ lift k (vmap h t) = vmap h (lift k t).
 Proof.
  intros CL. rewrite lift_vmap.
  apply term_vmap_ext. intros v _. now apply lift_nop.
@@ -1398,8 +1372,8 @@ Proof.
 Qed.
 
 Lemma fclosed_lift_above n f :
-  form_fclosed (lift_form_above n f) = form_fclosed f.
+  form_fclosed (lift n f) = form_fclosed f.
 Proof.
  apply eq_true_iff_eq. rewrite !form_fclosed_spec.
- unfold FClosed. now rewrite fvars_lift_form_above.
+ unfold FClosed. now rewrite fvars_lift_form.
 Qed.

Mix.v

@@ -106,6 +106,10 @@ Arguments fvars {_} {_} !_.
 Class VMap (A : Type) := vmap : (variable -> term) -> A -> A.
 Arguments vmap {_} {_} _ !_.
 
+(** Lifting of bound variables that are above some threshold *)
+Class Lift (A : Type) := lift : nat -> A -> A.
+Arguments lift {_} {_} _ !_.
+
 (** Some generic definitions based on the previous ones *)
 
 Definition BClosed {A}`{Level A} (a:A) := level a = 0.
@@ -218,20 +222,15 @@ Instance term_eqb : Eqb term :=
   | _, _ => false
   end.
 
-Fixpoint lift t :=
- match t with
- | BVar n => BVar (S n)
- | FVar v => FVar v
- | Fun f args => Fun f (List.map lift args)
- end.
+(** [lift k] adds 1 to [BVar] indices that are >= k *)
 
-(* +1 sur les dB >= k *)
-Fixpoint lift_above k t :=
- match t with
- | BVar n => if (k <=? n)%nat then BVar (S n) else t
- | FVar v => FVar v
- | Fun f args => Fun f (List.map (lift_above k) args)
- end.
+Instance term_lift : Lift term :=
+ fix term_lift k t :=
+  match t with
+  | BVar n => if k <=? n then BVar (S n) else t
+  | FVar v => FVar v
+  | Fun f args => Fun f (List.map (term_lift k) args)
+  end.
 
 (** Formulas *)
 
@@ -347,7 +346,7 @@ Instance form_bsubst : BSubst formula :=
   | Pred p args => Pred p (List.map (bsubst n t) args)
   | Not f => Not (form_bsubst n t f)
   | Op o f f' => Op o (form_bsubst n t f) (form_bsubst n t f')
-  | Quant q f' => Quant q (form_bsubst (S n) (lift t) f')
+  | Quant q f' => Quant q (form_bsubst (S n) (lift 0 t) f')
  end.
 
 Instance form_fvars : FVars formula :=
@@ -391,14 +390,17 @@ Compute eqb
         (∀ (Pred "A" [ #0 ] -> Pred "A" [ #0 ]))%form
         (∀ (Pred "A" [FVar "z"] -> Pred "A" [FVar "z"]))%form.
 
-(* +1 sur les dB >= k *)
-Fixpoint lift_form_above k f :=
+(** [lift k f] adds 1 to [BVar] indices that are >= k.
+    Note that this threshold is increased when entering a quantifier. *)
+
+Instance form_lift : Lift formula :=
+ fix form_lift k f :=
  match f with
  | True | False => f
- | Pred p l => Pred p (map (lift_above k) l)
- | Not f => Not (lift_form_above k f)
- | Op o f f' => Op o (lift_form_above k f) (lift_form_above k f')
- | Quant q f => Quant q (lift_form_above (S k) f)
+ | Pred p l => Pred p (map (lift k) l)
+ | Not f => Not (form_lift k f)
+ | Op o f f' => Op o (form_lift k f) (form_lift k f')
+ | Quant q f => Quant q (form_lift (S k) f)
  end.
 
 (** Contexts *)
@@ -970,4 +972,4 @@ Fixpoint form_fclosed f :=
   | Not f => form_fclosed f
   | Op _ f1 f2 => form_fclosed f1 &&& form_fclosed f2
   | Quant _ f => form_fclosed f
-  end.
\ No newline at end of file
+  end.

NameProofs.v

@@ -365,7 +365,7 @@ Proof.
 Qed.
 
 Lemma fresh_loop_ok names id n :
- (cardinal names < n + String.length id)%nat ->
+ cardinal names < n + String.length id ->
  Subset (strict_prefixes id) names ->
  ~In (fresh_loop names id n) names.
 Proof.

Peano.v

@@ -111,8 +111,8 @@ Proof.
   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 H2. apply bclosed_bsubst_id. exact H. }
+  assert (bsubst 0 B (lift 0 A) = A).
+  { assert (lift 0 A = A). { apply lift_nop. exact H. } rewrite H2. apply bclosed_bsubst_id. exact H. }
   rewrite H2 in AX2.
   exact AX2.
 Qed.
@@ -130,12 +130,12 @@ Proof.
   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 H4. apply bclosed_bsubst_id. assumption. }
+  assert (bsubst 0 C (lift 0 B) = B).
+  { assert (lift 0 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 H5. rewrite H5.
-    assert (lift B = B). { apply lift_nop. assumption. } rewrite H6.
+  assert (bsubst 0 C (bsubst 1 (lift 0 B) (lift 0 (lift 0 A))) = A).
+  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5.
+    assert (lift 0 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 H5 in AX3.
@@ -154,8 +154,8 @@ Proof.
   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 H2.
+  assert (bsubst 0 B (lift 0 A) = A).
+  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H2.
     apply bclosed_bsubst_id. assumption. }
   rewrite H2 in AX4.
   assumption.
@@ -173,8 +173,8 @@ Proof.
   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 H2.
+  assert (bsubst 0 B (lift 0 A) = A).
+  { assert (lift 0 A = A). { apply lift_nop. assumption. } rewrite H2.
     apply bclosed_bsubst_id. assumption. }
   rewrite H2 in AX13.
   assumption.

PreModels.v

@@ -211,7 +211,7 @@ Proof.
 Qed.
 
 Lemma interp_lift genv lenv m t :
- interp_term genv (m :: lenv) (lift t) = interp_term genv lenv t.
+ interp_term genv (m :: lenv) (lift 0 t) = interp_term genv lenv t.
 Proof.
  induction t as [ | |f l IH] using term_ind'; cbn; auto.
  case (funs Mo f) as [(k,fk)|]; cbn; auto. f_equal.

Restrict.v

@@ -171,14 +171,15 @@ Proof.
    f_equal. rewrite !map_map. apply map_ext_iff; auto.
 Qed.
 
-Lemma restrict_lift sign x t :
- restrict_term sign x (lift t) = lift (restrict_term sign x t).
+Lemma restrict_lift sign x t k :
+ restrict_term sign x (lift k t) = lift k (restrict_term sign x t).
 Proof.
  induction t as [ | |f l IH] using term_ind'; cbn; auto.
- destruct funsymbs; cbn; auto with *.
- rewrite map_length.
- case eqbspec; cbn; auto.
- intros _. f_equal. rewrite !map_map. apply map_ext_iff; auto.
+ - case Nat.leb_spec; auto.
+ - destruct funsymbs; cbn; auto with *.
+   rewrite map_length.
+   case eqbspec; cbn; auto.
+   intros _. f_equal. rewrite !map_map. apply map_ext_iff; auto.
 Qed.
 
 Lemma restrict_bsubst sign x n t f :
@@ -532,12 +533,12 @@ Proof.
  - f_equal. rewrite !map_map. apply map_ext_iff; auto.
 Qed.
 
-Lemma forcelevel_lift n x u :
-  forcelevel_term (S n) x (lift u) = lift (forcelevel_term n x u).
+Lemma forcelevel_lift0 n x u :
+  forcelevel_term (S n) x (lift 0 u) = lift 0 (forcelevel_term n x u).
 Proof.
- induction u using term_ind'; simpl; auto.
+ induction u using term_ind'; cbn -[Nat.ltb]; auto.
  - change (S n0 <? S n) with (n0 <? n).
-   case Nat.ltb_spec; simpl; auto.
+   case Nat.ltb_spec; cbn; auto.
  - f_equal. rewrite !map_map. apply map_ext_in; auto.
 Qed.
 
@@ -550,7 +551,7 @@ Proof.
  - rewrite !map_map. apply map_ext_iff.
    auto using forcelevel_bsubst_term.
  - rewrite IHf.
-   f_equal. apply forcelevel_lift.
+   f_equal. apply forcelevel_lift0.
 Qed.
 
 Ltac solver' :=

StringUtils.v

@@ -49,7 +49,7 @@ Proof.
 Qed.
 
 Lemma Prefix_length s s' :
-  Prefix s s' -> (String.length s <= String.length s')%nat.
+  Prefix s s' -> String.length s <= String.length s'.
 Proof.
  induction 1; simpl; auto with arith.
 Qed.

ZF.v

@@ -75,8 +75,8 @@ Notation "x ∉ y" := (~ x ∈ y) (at level 70) : formula_scope.
 Module ZFAx.
 Local Open Scope formula_scope.
 
-Definition zero s := ∀ #0 ∉ lift s.
-Definition succ x y := ∀ (#0 ∈ lift y <-> #0 = lift x \/ #0 ∈ lift x).
+Definition zero s := ∀ #0 ∉ lift 0 s.
+Definition succ x y := ∀ (#0 ∈ lift 0 y <-> #0 = lift 0 x \/ #0 ∈ lift 0 x).
 
 Definition eq_refl := ∀ (#0 = #0).
 Definition eq_sym := ∀∀ (#1 = #0 -> #0 = #1).
@@ -93,32 +93,16 @@ Definition infinity := ∃ (∃ ((#0 ∈ #1 /\ zero (#0)) /\ ∀ (#0 ∈ #1 -> (
 Definition axioms_list :=
  [ eq_refl; eq_sym; eq_trans; compat_left; compat_right; ext; pairing; union; powerset; infinity ].
 
-Fixpoint occur_term n t :=
-  match t with
-  | BVar m => n =? m
-  | FVar _ => false
-  | Fun _ l => existsb (occur_term n) l
-  end.
-
-Fixpoint occur_form n f :=
-  match f with
-    | True | False => false
-    | Pred _ l => existsb (occur_term n) l
-    | Not f' => occur_form n f'
-    | Op _ f1 f2 => (occur_form n f1) &&& (occur_form n f2)
-    | Quant _ f' => occur_form (S n) f'
-  end.
-
 (* POUR SEPARATION:
   dB dans A :  0=>x 1=>a n>=2:z_i
   dB dans (lift_above 1 A) 0=>x ... 2=>a (n>=3:z_i) *)
 Definition separation_schema A :=
   nForall
     ((level A) - 2)
-    (∀∃∀ (#0 ∈ #1 <-> (#0 ∈ #2 /\ lift_form_above 1 A))).
+    (∀∃∀ (#0 ∈ #1 <-> (#0 ∈ #2 /\ lift 1 A))).
 
 Definition exists_uniq A :=
-∃ (A /\ ∀ (lift_form_above 1 A -> #0 = #1)).
+∃ (A /\ ∀ (lift 1 A -> #0 = #1)).
 
 (* POUR REPLACEMENT:
    dB dans A :  0=>y 1=>x 2=>a n>=3:z_i
@@ -127,7 +111,7 @@ Definition replacement_schema A :=
   nForall
     ((level A) - 3)
     (∀ (∀ (#0 ∈ #1 -> exists_uniq A)) ->
-       ∃∀ (#0 ∈ #2 -> ∃ (#0 ∈ #2 /\ lift_form_above 2 A))).
+       ∃∀ (#0 ∈ #2 -> ∃ (#0 ∈ #2 /\ lift 2 A))).
 
 Local Close Scope formula_scope.
 
@@ -155,25 +139,25 @@ Proof.
    simpl in IN. intuition; subst; reflexivity.
  - repeat split; unfold separation_schema; cbn.
    + rewrite nForall_check. cbn.
-     rewrite !check_lift_form_above, HB.
+     rewrite !check_lift_form, HB.
      easy.
    + red. rewrite nForall_level.
      cbn -[Nat.max].
      rewrite !pred_max. simpl.
-     assert (H := level_lift_form_above B 1).
+     assert (H := level_lift_form 1 B).
      apply Nat.sub_0_le.
      repeat apply Nat.max_lub; omega with *.
    + 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.
+     rewrite !check_lift_form, HC.
      easy.
    + red. rewrite nForall_level.
      cbn -[Nat.max].
      rewrite !pred_max. simpl.
-     assert (H := level_lift_form_above C 1).
-     assert (H' := level_lift_form_above C 2).
+     assert (H := level_lift_form 1 C).
+     assert (H' := level_lift_form 2 C).
      apply Nat.sub_0_le.
      repeat apply Nat.max_lub; omega with *.
    + apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
@@ -366,4 +350,4 @@ Lemma Successor : IsTheorem Intuiti ZF (∀∃ succ (#1) (#0)).
 Proof.
   apply ModusPonens with (A := ∀∀∃∀ #0 ∈ #1 <-> #0 ∈ #3 \/ #0 ∈ #2); [ | apply unionset ].
   apply ModusPonens with (A := ∀∃∀ #0 ∈ #1 <-> #0 = #2); [ apply Succ | apply singleton ].
-Qed.
\ No newline at end of file
+Qed.