### lift is now lift_above

`  Moreover, it works both on term and formulas thanks to Class overloading`
parent 934da1dd
 ... ... @@ -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.
 ... ... @@ -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.
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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
 ... ... @@ -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. ... ...
 ... ... @@ -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 ∈ #3 /\ lift_form_above 2 A))). ∃∀ (#0 ∈ #2 -> ∃ (#0 ∈ #3 /\ 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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!