Commit 9c31f9cc authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Compat coq 8.13 (omega -> lia)

parent 9fff058a
......@@ -66,10 +66,10 @@ Proof.
- now inversion 2.
- destruct n as [|n]; intros Hn Hn'; trivial.
cbn - [base]. rewrite Nat.sub_0_r. f_equal. apply IH.
transitivity n; [|omega].
apply Nat.div_le_upper_bound; unfold base; auto with *.
transitivity n; [|omega].
apply Nat.div_le_upper_bound; unfold base; auto with *.
+ transitivity n; [|lia].
apply Nat.div_le_upper_bound; unfold base; lia.
+ transitivity n; [|lia].
apply Nat.div_le_upper_bound; unfold base; lia.
Qed.
Lemma N_of_digits_bound l :
......@@ -79,7 +79,7 @@ Proof.
- now compute.
- cbn - [N.mul N.pow N.of_nat].
rewrite Nat2N.inj_succ, N.pow_succ_r'.
destruct a; omega with *.
destruct a; lia.
Qed.
Lemma N_of_ascii_bound c : (N_of_ascii c < 2^8)%N.
......@@ -109,7 +109,7 @@ Proof.
rewrite Nat.div_small by apply nat_of_ascii_bound; simpl.
rewrite <- IH at 3.
apply string_enum_indep; auto.
unfold base. omega with *.
unfold base. lia.
Qed.
Lemma countable_variables : Countable variable.
......@@ -145,7 +145,7 @@ Proof.
rewrite (Nat.add_succ_r n), !Nat.add_0_r;
rewrite <- ?(Nat.add_1_r k), <- ?Nat.add_assoc; simpl;
rewrite !Nat.mul_add_distr_r, !Nat.mul_add_distr_l; simpl;
omega with *.
lia.
Qed.
Lemma tri_incr_iff k l : k<l <-> k * S k < l * S l.
......@@ -154,16 +154,16 @@ Proof.
{ intros. apply Nat.mul_lt_mono; auto with *. }
split; auto.
destruct (Nat.compare_spec k l); auto.
- subst. omega with *.
- apply H in H0. omega with *.
- subst. lia.
- apply H in H0. lia.
Qed.
Lemma tri_inj k l : k = l <-> k * S k = l * S l.
Proof.
split; [now intros ->|].
destruct (Nat.compare_spec k l); auto.
apply tri_incr_iff in H; omega.
apply tri_incr_iff in H; omega.
apply tri_incr_iff in H; lia.
apply tri_incr_iff in H; lia.
Qed.
Lemma inv_tri_carac_aux n k l:
......@@ -173,10 +173,10 @@ Proof.
rewrite !Nat.add_succ_r, !Nat.add_0_r.
intros Hk Hl.
assert (k < S l).
{ apply tri_incr_iff. omega. }
{ apply tri_incr_iff. lia. }
assert (l < S k).
{ apply tri_incr_iff. omega. }
omega.
{ apply tri_incr_iff. lia. }
lia.
Qed.
Lemma inv_tri_carac n k :
......@@ -212,14 +212,11 @@ Proof.
assert (2*(z*S z/2) = z * S z).
{ symmetry. apply Nat.div_exact; auto with *. }
rewrite H.
rewrite Nat.add_1_r.
split; try omega.
rewrite Nat.mul_add_distr_l.
rewrite (Nat.mul_comm z (S z)). omega with *. }
rewrite Nat.add_1_r. lia. }
rewrite H.
clear k H.
rewrite Nat.add_1_r.
f_equal; omega with *.
f_equal; lia.
Qed.
Lemma countable_nat2 : Countable (nat*nat).
......@@ -348,7 +345,7 @@ Proof.
destruct (Hf (fun n => S (f n n))) as (a,Ha).
set (fa := fun n : nat => S (f n n)) in *.
assert (f a a = fa a) by now rewrite Ha.
unfold fa in H. omega.
unfold fa in H. lia.
Qed.
(** Same for [nat->A] as soon as [A] has at least two elements *)
......
......@@ -4,7 +4,7 @@
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Export Setoid Morphisms RelationClasses Arith Omega Bool String
Require Export Setoid Morphisms RelationClasses Arith Lia Bool String
MSetRBT StringOrder List Utils.
Require DecimalString.
Import ListNotations.
......
......@@ -29,8 +29,8 @@ Lemma add_compat G x x' y y' :
Proof.
intros Hx Hx' Hy IN3 IN5 IN6 Hxx' Hyy'.
trans (x' + y); auto.
- red. red in Hx, Hy. cbn. omega with *.
- red. red in Hx', Hy. cbn. omega with *.
- red. red in Hx, Hy. cbn. lia.
- red. red in Hx', Hy. cbn. lia.
- eapply R_Imp_e; [ | exact Hxx'].
inst_axiom ax5 [x; x'; y]. revert H. cbn.
rewrite !(lift_nop _ x), !lift_nop by auto.
......@@ -50,8 +50,8 @@ Lemma mul_compat G x x' y y' :
Proof.
intros Hx Hx' Hy IN3 IN5 IN6 Hxx' Hyy'.
trans (x' * y); auto.
- red. red in Hx, Hy. cbn. omega with *.
- red. red in Hx', Hy. cbn. omega with *.
- red. red in Hx, Hy. cbn. lia.
- red. red in Hx', Hy. cbn. lia.
- eapply R_Imp_e; [ | exact Hxx'].
inst_axiom ax7 [x; x'; y]. revert H. cbn.
rewrite !(lift_nop _ x), !lift_nop by auto.
......@@ -82,10 +82,10 @@ Proof.
destruct l as [|x [| ]]; try easy. cbn in *.
rewrite andb_true_r in C.
ahered.
* red; red in Hu. cbn in Hu. omega with *.
* red; red in Hu. cbn in Hu. lia.
* apply IH; auto.
{ red; red in Hu. cbn in Hu. omega with *. }
{ red; red in Hu'. cbn in Hu'. omega with *. }
{ red; red in Hu. cbn in Hu. lia. }
{ red; red in Hu'. cbn in Hu'. lia. }
+ (* + *)
intros Hl -> _ _ C.
destruct l as [|x [|y [| ]]]; try easy. cbn in *.
......@@ -159,31 +159,31 @@ Proof.
* apply Pr_pop. apply Leibniz_term; intuition.
* trans Y'; auto. apply R'_Ax.
apply Pr_pop. sym; auto. apply Leibniz_term; intuition.
- cbn. apply ContraIff. apply IHN; auto. cbn in HN. omega.
- cbn. apply ContraIff. apply IHN; auto. cbn in HN. lia.
- cbn. red in Hu,Hu'. cbn in Hu,Hu'. rewrite !max_0 in *.
destruct Hu as (Hu1 & Hu2), Hu' as (Hu1' & Hu2').
cbn in HA. rewrite <- andb_lazy_alt, andb_true_iff in HA.
cbn in HN. apply OpIff; apply IHN; intuition; omega with *.
cbn in HN. apply OpIff; apply IHN; intuition; lia.
- cbn. red in Hu,Hu'. cbn in Hu,Hu'. rewrite pred_0 in Hu,Hu'.
apply QuantIff.
All_i_fresh. clear Hv.
cbn. reIff.
destruct (level_subst_inv (S n) (lift 0 u) A).
+ omega with *.
+ lia.
+ rewrite !(form_level_bsubst_id (S n)); auto.
apply R_And_i; apply R_Imp_i, R'_Ax.
+ destruct (level_subst_inv (S n) (lift 0 u') A).
* omega with *.
* lia.
* rewrite !(form_level_bsubst_id (S n)); auto.
apply R_And_i; apply R_Imp_i, R'_Ax.
* assert (BClosed u).
{ red. generalize (lift_incrlevel 0 u). omega. }
{ red. generalize (lift_incrlevel 0 u). lia. }
assert (BClosed u').
{ red. generalize (lift_incrlevel 0 u'). omega. }
{ red. generalize (lift_incrlevel 0 u'). lia. }
rewrite !lift_nop in * by auto.
rewrite !(swap_bsubst 0); auto.
apply IHN; auto.
{ rewrite height_bsubst. cbn in HN. omega. }
{ rewrite height_bsubst. cbn in HN. lia. }
{ cbn in HA. apply check_bsubst; auto. }
{ apply Nat.le_0_r. now rewrite swap_bsubst, level_bsubst. }
{ apply Nat.le_0_r. now rewrite swap_bsubst, level_bsubst. }
......@@ -194,7 +194,7 @@ Lemma Leibniz_Pr A :
Pr Intuiti (axioms_list ∀∀ #0 = #1 -> A -> bsubst 0 (#1) A).
Proof.
intros (HA,HA'). cbn in HA. red in HA'. cbn in HA'.
assert (HA'' : level A <= 1) by omega with *.
assert (HA'' : level A <= 1) by lia.
All_i_fresh. cbn.
All_i_fresh. cbn. clear Hv Hv0.
rewrite (form_level_bsubst_id 1 _ A) by easy.
......@@ -217,7 +217,7 @@ Proof.
+ cbn. now rewrite check_bsubst, CA.
+ red. cbn -[Nat.max]. rewrite !pred_max. cbn.
generalize (level_bsubst_max 0 (#1) A). cbn - [Nat.max].
red in LA. cbn in LA. omega with *.
red in LA. cbn in LA. lia.
+ rewrite <- form_fclosed_spec in *. cbn in *.
rewrite fclosed_bsubst; auto. now rewrite FA.
- exists axioms_list. split.
......
......@@ -67,7 +67,7 @@ Proof.
revert t.
fix IH 1. destruct t; cbn.
- destruct (list_index v stack) eqn:E; cbn; auto with arith.
apply list_index_lt_length in E. omega.
apply list_index_lt_length in E. lia.
- clear f. revert l.
fix IH' 1. destruct l as [|t l]; cbn; auto with arith.
apply Nat.max_lub; auto.
......@@ -80,14 +80,14 @@ Proof.
induction f; intros stack; cbn; auto with arith.
- apply (nam2mix_term_level stack (Nam.Fun "" l)).
- apply Nat.max_lub; auto.
- specialize (IHf (v::stack)). cbn in *. omega.
- specialize (IHf (v::stack)). cbn in *. lia.
Qed.
Lemma nam2mix_term_bclosed t :
Mix.BClosed (nam2mix_term [] t).
Proof.
unfold Mix.BClosed.
generalize (nam2mix_term_level [] t); simpl; omega.
generalize (nam2mix_term_level [] t); simpl; lia.
Qed.
Lemma nam2mix_bclosed f :
......@@ -251,7 +251,7 @@ Proof.
+ rewrite list_index_app_l' by (simpl; intuition).
destruct (list_index v stk) eqn:E; cbn; auto.
apply list_index_lt_length in E.
case eqbspec; intros; subst; auto; omega.
case eqbspec; intros; subst; auto; lia.
- f_equal; clear f.
rewrite !map_map. apply map_ext_in. auto.
Qed.
......@@ -379,7 +379,7 @@ Proof.
+ intros NE.
rewrite lift_nop.
2:{ unfold Mix.BClosed.
generalize (nam2mix_term_level [] u). simpl. omega. }
generalize (nam2mix_term_level [] u). simpl. lia. }
destruct (Names.mem v (Term.vars u)) eqn:IN; simpl.
* f_equal.
setfresh vars z Hz.
......@@ -649,9 +649,9 @@ Proof.
fix IHl 1. destruct l as [|t l]; simpl; trivial.
intros LE FR.
f_equal.
+ apply IH; auto. omega with *.
+ apply IH; auto. lia.
intros v IN. apply FR in IN. namedec.
+ apply IHl; auto. omega with *.
+ apply IHl; auto. lia.
intros v IN. apply FR in IN. namedec.
Qed.
......@@ -667,15 +667,15 @@ Proof.
injection (mix_nam_mix_term_gen stack (Mix.Fun "" l)); auto.
- f_equal. auto.
- cbn in *. f_equal.
+ apply IHf1; auto. omega with *.
+ apply IHf1; auto. lia.
intros v IN. apply FR in IN. namedec.
+ apply IHf2; auto. omega with *.
+ apply IHf2; auto. lia.
intros v IN. apply FR in IN. namedec.
- cbn in *. f_equal.
apply IHf; auto.
+ constructor; auto.
setfresh vars z Hz. rewrite <- names_of_list_in. namedec.
+ simpl. omega with *.
+ simpl. lia.
+ simpl.
intros v [<-|IN].
* setfresh vars z Hz. namedec.
......
......@@ -386,7 +386,7 @@ Proof.
- simpl.
cbn in HA. apply Nat.succ_lt_mono in HA.
assert (L : level A <= 1).
{ unfold WF,BClosed in W. cbn in W. omega. }
{ unfold WF,BClosed in W. cbn in W. lia. }
assert (HA' : forall t, height (bsubst 0 t A) < h).
{ intro. now rewrite height_bsubst. }
destruct q; split.
......
......@@ -156,7 +156,7 @@ Proof.
inversion_clear ND.
rewrite InA_In in H.
rewrite IH; clear IH; auto.
rewrite NamesP.add_cardinal_2. omega.
rewrite NamesP.add_cardinal_2. lia.
apply Hf'; auto.
intros x Hx. nameiff. intros [Eq|IN].
apply Hf in Eq; auto. congruence.
......@@ -309,7 +309,7 @@ Proof.
apply NamesP.subset_antisym; auto.
intros x IN.
destruct (NamesP.In_dec x u) as [H|H]; auto.
generalize (NamesP.subset_cardinal_lt SU IN H). omega.
generalize (NamesP.subset_cardinal_lt SU IN H). lia.
Qed.
Lemma string_app_length s s' :
......@@ -359,9 +359,9 @@ Proof.
- right. apply Prefix_refl.
- assert (String.length (x++String a "") = String.length x).
{ now f_equal. }
rewrite string_app_length in *. simpl in *. omega.
rewrite string_app_length in *. simpl in *. lia.
- apply Prefix_length in H.
rewrite string_app_length in *. simpl in *. omega.
rewrite string_app_length in *. simpl in *. lia.
Qed.
Lemma fresh_loop_ok names id n :
......@@ -375,7 +375,7 @@ Proof.
assert (E : cardinal (strict_prefixes id) = cardinal vars).
{ apply NamesP.subset_cardinal in SU.
rewrite strict_prefixes_cardinal in *.
omega. }
lia. }
apply subset_equal in E; auto. clear SU.
rewrite <- E.
unfold strict_prefixes. nameiff. intuition.
......@@ -383,7 +383,7 @@ Proof.
destruct (mem id vars) eqn:ME; simpl.
+ rewrite mem_spec in ME.
apply IHn.
* rewrite string_app_length. simpl. omega.
* rewrite string_app_length. simpl. lia.
* rewrite strict_prefixes_more; auto.
{ intros x. red in SU. nameiff. intuition. }
+ rewrite <- mem_spec. now destruct mem.
......@@ -393,7 +393,7 @@ Lemma fresh_ok names :
~In (fresh names) names.
Proof.
unfold fresh. apply fresh_loop_ok.
simpl. omega.
simpl. lia.
change "x" with (""++String "x" "").
rewrite strict_prefixes_more.
unfold strict_prefixes. simpl. namedec.
......
......@@ -80,7 +80,7 @@ Proof.
{ apply level_bsubst'. auto. }
assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
{ apply level_bsubst'. auto. }
omega with *.
lia.
+ apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
cbn. now rewrite !fclosed_bsubst, HB'.
Qed.
......@@ -450,7 +450,7 @@ Proof.
unfold PeanoTheory. simpl.
unfold PeanoAx.IsAx.
intros [IN|(B & -> & CK & CL)] G.
- compute in IN. intuition; subst; cbn; intros; subst; omega.
- compute in IN. intuition; subst; cbn; intros; subst; lia.
- unfold PeanoAx.induction_schema.
apply interp_nforall.
intros stk Len. rewrite app_nil_r. cbn.
......
......@@ -145,7 +145,7 @@ Proof.
- setoid_rewrite Nat.max_lt_iff in EL. apply IHA1; eauto with set.
- setoid_rewrite Nat.max_lt_iff in EL. apply IHA2; eauto with set.
- intros m. apply IHA; eauto with set.
destruct k; cbn; auto. intros H. apply EL. omega.
destruct k; cbn; auto. intros H. apply EL. lia.
Qed.
Lemma cinterp_ext G L G' L' (c:context) :
......@@ -228,9 +228,9 @@ Proof.
rewrite Nat.sub_diag; simpl. f_equal. rewrite <- Hu. symmetry.
apply tinterp_bclosed; auto.
- intro k. rewrite Nat.lt_gt_cases. intros [LT|GT].
+ rewrite nth_error_app1; auto. omega.
+ rewrite !(proj2 (nth_error_None _ _)); simpl; auto. omega.
rewrite app_length; simpl. omega.
+ rewrite nth_error_app1; auto. lia.
+ rewrite !(proj2 (nth_error_None _ _)); simpl; auto. lia.
rewrite app_length; simpl. lia.
Qed.
Lemma finterp_bsubst_gen G L L' u m n A :
......@@ -261,9 +261,9 @@ Proof.
rewrite Nat.sub_diag; simpl. f_equal. rewrite <- Hu. symmetry.
apply tinterp_bclosed; auto.
- intro k. rewrite Nat.lt_gt_cases. intros [LT|GT].
+ rewrite nth_error_app1; auto. omega.
+ rewrite !(proj2 (nth_error_None _ _)); simpl; auto. omega.
rewrite app_length; simpl. omega.
+ rewrite nth_error_app1; auto. lia.
+ rewrite !(proj2 (nth_error_None _ _)); simpl; auto. lia.
rewrite app_length; simpl. lia.
Qed.
Lemma finterp_bsubst0 G u m A :
......@@ -340,20 +340,20 @@ Proof.
cbn in CL; rewrite ?eqb_eq, ?max_0 in CL;
instlevel; cbn in *; try (tryinstG; intuition eauto 3; fail).
- intros m.
rewrite finterp_bsubst_adhoc with (x:=x) by auto with *.
rewrite finterp_bsubst_adhoc with (x:=x) by (auto with *; lia).
apply IHValid.
rewrite <- (cinterp_ext G); eauto with *.
- rewrite <- finterp_bsubst0 with (u:=t); auto with *.
destruct d as (?,s,?); cbn in *; subst s; cbn in *; omega with *.
- rewrite <- finterp_bsubst0 with (u:=t); auto with *; try easy.
destruct d as (?,s,?); cbn in *; subst s; cbn in *; lia.
- exists (tinterp G [] t).
rewrite finterp_bsubst0 with (u:=t); auto with *.
rewrite finterp_bsubst0 with (u:=t); auto; try easy. lia.
- destruct (IHValid1 G) as (m & Hm); auto.
rewrite finterp_bsubst_adhoc with (x:=x) in Hm; [ | | namedec].
erewrite finterp_ext.
eapply IHValid2; eauto.
apply cinterp_cons. apply Hm.
rewrite <- (cinterp_ext G); eauto. prove_ext. prove_ext. auto.
destruct d1 as (?,s,?); cbn in *; subst s; cbn in *; omega with *.
destruct d1 as (?,s,?); cbn in *; subst s; cbn in *; lia.
- subst logic.
destruct (CR (finterp G [] A)); auto.
destruct (IHValid G); auto.
......@@ -409,7 +409,7 @@ Lemma nForall_level n A :
level (nForall n A) = level A - n.
Proof.
induction n; cbn; auto with arith.
rewrite IHn. omega.
rewrite IHn. lia.
Qed.
Lemma interp_nforall {sign}{M}(Mo : PreModel M sign) G L n A :
......@@ -429,7 +429,7 @@ Proof.
rewrite <- app_assoc. simpl. apply IHn; auto.
+ intros H m. apply IHn. intros stk Len.
change (m::L) with ([m]++L)%list. rewrite app_assoc.
apply H. rewrite app_length. simpl. omega.
apply H. rewrite app_length. simpl. lia.
Qed.
(** Premodel extension *)
......
......@@ -87,13 +87,13 @@ Qed.
Lemma restrict_term_bclosed sign x t :
BClosed t -> BClosed (restrict_term sign x t).
Proof.
unfold BClosed. assert (H := restrict_term_level sign x t). auto with *.
unfold BClosed. assert (H := restrict_term_level sign x t). lia.
Qed.
Lemma restrict_level sign x f :
level (restrict sign x f) <= level f.
Proof.
induction f; cbn; auto using Nat.max_le_compat with *.
induction f; cbn; auto using Nat.max_le_compat with *; try lia.
destruct predsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear p a.
......@@ -104,7 +104,7 @@ Qed.
Lemma restrict_bclosed sign x f :
BClosed f -> BClosed (restrict sign x f).
Proof.
unfold BClosed. assert (H := restrict_level sign x f). auto with *.
unfold BClosed. assert (H := restrict_level sign x f). lia.
Qed.
Lemma restrict_term_fvars sign x t :
......@@ -421,7 +421,7 @@ Proof.
- rewrite map_map. apply list_max_map_le.
auto using forcelevel_term_level.
- apply max_le; auto.
- specialize (IHf (S n)). auto with *.
- specialize (IHf (S n)). lia.
Qed.
Lemma forcelevel_bclosed x f :
......@@ -472,7 +472,7 @@ Lemma forcelevel_term_id n x t :
Proof.
induction t as [ | | f l IH] using term_ind';
cbn - [Nat.ltb]; intros H; auto with *.
- case Nat.ltb_spec; cbn; auto; omega.
- case Nat.ltb_spec; cbn; auto; lia.
- f_equal.
rewrite list_max_map_le in H.
apply map_id_iff; auto.
......@@ -482,9 +482,10 @@ Lemma forcelevel_id n x f :
level f <= n -> forcelevel n x f = f.
Proof.
revert n.
induction f; cbn; intros; rewrite ?max_le in *; f_equal; intuition.
induction f; cbn; intros; rewrite ?max_le in *; f_equal; trivial;
(apply IHf || apply IHf1 || apply IHf2 || idtac); try lia.
apply map_id_iff. rewrite list_max_map_le in H.
auto using forcelevel_term_id.
auto using forcelevel_term_id.
Qed.
Lemma forcelevel_ctx_id x c :
......@@ -534,14 +535,14 @@ Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case eqbspec.
+ intros; subst.
case Nat.leb_spec; try omega. cbn. now rewrite eqb_refl.
case Nat.leb_spec; try lia. cbn. now rewrite eqb_refl.
+ simpl.
case Nat.leb_spec.
* intros LE NE. cbn - [Nat.ltb].
case eqbspec; [intros; exfalso; omega|intros _].
case Nat.ltb_spec; auto; omega.
case eqbspec; [intros; exfalso; lia|intros _].
case Nat.ltb_spec; auto; lia.
* intros LT _. cbn - [Nat.ltb].
case Nat.ltb_spec; auto; omega.
case Nat.ltb_spec; auto; lia.
- f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
......
......@@ -43,8 +43,8 @@ Proof.
intros. set (m := S n) in *.
assert (IH : level (downvars m) = S m) by now apply IHn.
clearbody m. clear IHn.
cbn -[Nat.max]. change (list_max _) with (level (downvars m)).
rewrite IH. omega with *.
cbn -[Nat.max]. change (Utils.list_max _) with (level (downvars m)).
rewrite IH. lia.
Qed.
Lemma level_downvars_le n : level (downvars n) <= S n.
......@@ -101,7 +101,7 @@ Proof.
- unfold BClosed in *. rewrite nForall_level in *.
cbn in LA.
apply Nat.sub_0_le. rewrite level_bsubst_max.
apply Nat.max_lub; try omega with *.
apply Nat.max_lub; try lia.
apply level_downvars_le.
- rewrite <- nForall_fclosed in *.
rewrite <- form_fclosed_spec in *.
......
......@@ -636,7 +636,7 @@ Proof.
+ red; red in FC. cbn in *. namedec.
- exists []; split; auto.
subst logic. apply ExEx.
assert (Nat.pred (level A) = 0) by apply CL. omega.
assert (Nat.pred (level A) = 0) by apply CL. lia.
Qed.
Fixpoint term_funs t :=
......@@ -893,12 +893,12 @@ Proof.
right; left. rewrite H.
cbn. f_equal. f_equal. symmetry.
apply form_level_bsubst_id.
assert (pred (level f) = 0) by apply W. omega.
assert (pred (level f) = 0) by apply W. lia.
* intros [H|[H|H]]; auto.
right. rewrite <- H.
cbn. f_equal. f_equal. symmetry.
apply form_level_bsubst_id.
assert (pred (level f) = 0) by apply W. omega.
assert (pred (level f) = 0) by apply W. lia.
+ intros A [HA|HA].
* cbn. apply signext_wc with th; auto using WCAxiom.
rewrite Hm. apply delcst_HenkinAll_signext.
......@@ -1077,7 +1077,7 @@ Lemma ax_completion_grows th n m : n <= m ->
Proof.
intros LE A.
rewrite !ax_completion_carac. intros [H|(k & Hk & H)]; auto.
right. exists k; auto with *.
right. exists k. intuition; lia.
Qed.
Lemma ax_completion_init th :
......
......@@ -34,20 +34,20 @@ Qed.
Lemma lift_nop_le k t : level t <= k -> lift k t = t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case Nat.leb_spec; auto. omega.
- case Nat.leb_spec; auto. lia.
- rewrite list_max_map_le. intros H. f_equal. apply map_id_iff; auto.
Qed.
Lemma lift_nop k t : BClosed t -> lift k t = t.
Proof.
unfold BClosed. intros H. apply lift_nop_le. rewrite H; omega.
unfold BClosed. intros H. apply lift_nop_le. rewrite H; lia.
Qed.
Lemma lift_incrlevel k t : k < level t -> level (lift k t) = S (level t).
Proof.
revert t. fix IH 1; destruct t; cbn.
- inversion 1.
- case Nat.leb_spec; cbn; omega.
- case Nat.leb_spec; cbn; lia.
- revert l; fix IHl 1; destruct l as [|t l]; cbn.
+ inversion 1.