Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 7cc2810b authored by Léo Gourdin's avatar Léo Gourdin
Browse files

replacing omega with lia in some file

parent 9a0bf569
......@@ -192,6 +192,8 @@ build_rv64:
script:
- ./config_rv64.sh
- make -j "$NJOBS"
- export LD_LIBRARY_PATH=/usr/riscv64-linux-gnu/lib
- sudo ln -s /usr/riscv64-linux-gnu/lib/ld-linux-riscv64-lp64d.so.1 /lib
- make -C test CCOMPOPTS=-static SIMU='qemu-riscv64' EXECUTE='qemu-riscv64' all test
- ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
rules:
......
......@@ -37,6 +37,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
Require Import Locations Conventions.
Require Stacklayout.
Require Import OptionMonad Asm.
Require Import Lia.
Require Export Asm.
Local Open Scope option_monad_scope.
......@@ -437,7 +438,7 @@ Qed.
Lemma size_positive (b:bblock): size b > 0.
Proof.
unfold size. destruct b as [hd bdy ex cor]. cbn.
destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega);
destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia);
unfold non_empty_bblockb in cor; simpl in cor.
inversion cor.
Qed.
......
......@@ -19,6 +19,7 @@ Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock IterList.
Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
Require Import Lia.
Module MB := Machblock.
Module AB := Asmblock.
......@@ -71,7 +72,7 @@ Lemma transf_function_no_overflow:
transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
Proof.
intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
omega.
lia.
Qed.
Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
......@@ -298,8 +299,8 @@ Proof.
split. unfold goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
auto. omega.
generalize (transf_function_no_overflow _ _ H0). omega.
auto. lia.
generalize (transf_function_no_overflow _ _ H0). lia.
intros. apply Pregmap.gso; auto.
Qed.
......@@ -389,7 +390,7 @@ Lemma mbsize_eqz:
Proof.
intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
remember (length _) as a. remember (length_opt _) as b.
assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
inv H0. inv H1. destruct bdy; destruct ex; auto.
all: try discriminate.
Qed.
......@@ -1452,11 +1453,11 @@ Proof.
rewrite Pregmap.gso; auto. rewrite V; auto.
} destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
exploit exec_straight_steps_2; eauto using functions_transl.
simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
intros (ofs' & X & Y).
left; exists (State rs3' m3'); split.
eapply exec_straight_steps_1; eauto.
simpl fn_blocks. simpl fn_blocks in g. omega.
simpl fn_blocks. simpl fn_blocks in g. lia.
constructor.
econstructor; eauto.
rewrite X; econstructor; eauto.
......@@ -1495,7 +1496,7 @@ Local Transparent destroyed_at_function_entry.
- (* return *)
inv MS.
inv STACKS. simpl in *.
right. split. omega. split. auto.
right. split. lia. split. auto.
rewrite <- ATPC in H5.
econstructor; eauto. congruence.
Qed.
......
......@@ -38,6 +38,7 @@ Require Import Asmblockgen.
Require Import Conventions1.
Require Import Axioms.
Require Import Asmblockprops.
Require Import Lia.
Module MB:=Machblock.
Module AB:=Asmblock.
......@@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
Lemma code_tail_pos:
forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
Proof.
induction 1. omega. generalize (size_positive bi); intros; omega.
induction 1. lia. generalize (size_positive bi); intros; lia.
Qed.
Lemma find_bblock_tail:
......@@ -405,10 +406,10 @@ Lemma find_bblock_tail:
Proof.
induction c1; simpl; intros.
inversion H.
destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
destruct (zeq pos 0). subst pos.
inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
eauto.
Qed.
......@@ -422,13 +423,13 @@ Proof.
induction 1; intros.
- subst; eauto.
- replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
omega.
lia.
Qed.
Lemma size_blocks_pos c: 0 <= size_blocks c.
Proof.
induction c as [| a l ]; simpl; try omega.
generalize (size_positive a); omega.
induction c as [| a l ]; simpl; try lia.
generalize (size_positive a); lia.
Qed.
Remark code_tail_positive:
......@@ -436,15 +437,15 @@ Remark code_tail_positive:
code_tail ofs fn c -> 0 <= ofs.
Proof.
induction 1; intros; simpl.
- omega.
- generalize (size_positive bi). omega.
- lia.
- generalize (size_positive bi). lia.
Qed.
Remark code_tail_size:
forall fn ofs c,
code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
Proof.
induction 1; intros; simpl; try omega.
induction 1; intros; simpl; try lia.
Qed.
Remark code_tail_bounds fn ofs c:
......@@ -453,7 +454,7 @@ Proof.
intro H;
exploit code_tail_size; eauto.
generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
omega.
lia.
Qed.
Local Hint Resolve code_tail_next: core.
......@@ -470,8 +471,8 @@ Proof.
intros.
rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
- rewrite Ptrofs.unsigned_repr; eauto.
omega.
- rewrite Ptrofs.unsigned_repr; omega.
lia.
- rewrite Ptrofs.unsigned_repr; lia.
Qed.
(** The [find_label] function returns the code tail starting at the
......@@ -505,12 +506,12 @@ Proof.
simpl; intros until c'.
case (is_label lbl a).
- intros. inv H. exists pos. split; auto. split.
replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
generalize (size_blocks_pos c). generalize (size_positive a). omega.
replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
generalize (size_blocks_pos c). generalize (size_positive a). lia.
- intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
exists pos'. split. auto. split.
replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
constructor. auto. generalize (size_positive a). omega.
replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
constructor. auto. generalize (size_positive a). lia.
Qed.
(** Predictor for return addresses in generated Asm code.
......@@ -589,7 +590,7 @@ Proof.
exists (Ptrofs.repr ofs). red; intros.
rewrite Ptrofs.unsigned_repr. congruence.
exploit code_tail_bounds; eauto.
intros; apply transf_function_len in TF. omega.
intros; apply transf_function_len in TF. lia.
+ exists Ptrofs.zero; red; intros. congruence.
Qed.
......@@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
Remark code_tail_no_bigger:
forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
Proof.
induction 1; simpl; omega.
induction 1; simpl; lia.
Qed.
Remark code_tail_unique:
......@@ -621,8 +622,8 @@ Remark code_tail_unique:
code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
Proof.
induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
f_equal. eauto.
Qed.
......
......@@ -21,6 +21,7 @@ Require Import Asmblockprops.
Require Import PostpassScheduling.
Require Import Asmblockgenproof.
Require Import Axioms.
Require Import Lia.
Local Open Scope error_monad_scope.
......@@ -171,7 +172,7 @@ Proof.
induction tc.
- intros. simpl in H. discriminate.
- intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+ inv H. assert (k = k') by omega. subst. reflexivity.
+ inv H. assert (k = k') by lia. subst. reflexivity.
+ pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.
......
......@@ -620,7 +620,7 @@ Proof.
destruct a; simpl in H10; try discriminate; simpl; trivial.
rewrite negb_false_iff in H8.
eapply Mem.load_storebytes_other. eauto.
rewrite H6. rewrite Z2Nat.id by omega.
rewrite H6. rewrite Z2Nat.id by lia.
eapply pdisjoint_sound. eauto.
unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
erewrite <- regs_valnums_sound by eauto. eauto with va.
......
......@@ -89,7 +89,7 @@ Qed.
Obligation 2.
Proof.
simpl in BOUND.
omega.
lia.
Qed.
Program Definition bounded_nth_S_statement : Prop :=
......@@ -104,14 +104,14 @@ Lemma bounded_nth_proof_irr :
(BOUND1 BOUND2 : (k < List.length l)%nat),
(bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
Proof.
induction k; destruct l; simpl; intros; trivial; omega.
induction k; destruct l; simpl; intros; trivial; lia.
Qed.
Lemma bounded_nth_S : bounded_nth_S_statement.
Proof.
unfold bounded_nth_S_statement.
induction k; destruct l; simpl; intros; trivial.
1, 2: omega.
1, 2: lia.
apply bounded_nth_proof_irr.
Qed.
......@@ -121,7 +121,7 @@ Lemma inject_list_injected:
Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
Proof.
induction l; simpl; intros.
- omega.
- lia.
- simpl.
destruct k as [ | k]; simpl pos_add_nat.
+ simpl bounded_nth.
......
......@@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
Require Import Compopts AST.
Require Import Values Memory Globalenvs Builtins Events.
Require Import Registers RTL.
Require Import Lia.
(** The abstract domains for value analysis *)
......@@ -2822,8 +2823,8 @@ Proof.
generalize (Int.unsigned_range_2 j); intros RANGE.
assert (Int.unsigned j <> 0).
{ red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
}
intros until y.
intros HX HY.
......
......@@ -25,6 +25,7 @@ Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Builtins.
Require Import Lia.
(** * Events and traces *)
......@@ -1443,7 +1444,7 @@ Proof.
econstructor; eauto.
red; intros; congruence.
(* trace length *)
- inv H; simpl; omega.
- inv H; simpl; lia.
(* receptive *)
- inv H; inv H0. exists Vundef, m1; constructor.
(* determ *)
......
......@@ -23,6 +23,7 @@ Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Lia.
(** * Properties of memory chunks *)
......@@ -48,7 +49,7 @@ Definition largest_size_chunk := 8.
Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
Proof.
destruct chunk; simpl; omega.
destruct chunk; simpl; lia.
Qed.
Lemma size_chunk_pos:
......
......@@ -20,6 +20,7 @@ Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Lia.
Definition block : Type := positive.
Definition eq_block := peq.
......@@ -1535,14 +1536,14 @@ Proof.
replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
replace (Int.ltu n Int.iwordsize) with true.
f_equal; apply Int.shrx_shr_2; assumption.
symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
symmetry; apply zlt_true. change (Int.unsigned n < 32); lia.
symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
assert (Int.unsigned n <> 0).
{ red; intros; elim H.
rewrite <- (Int.repr_unsigned n), H0. auto. }
rewrite Int.unsigned_repr.
change (Int.unsigned Int.iwordsize) with 32; omega.
assert (32 < Int.max_unsigned) by reflexivity. omega.
change (Int.unsigned Int.iwordsize) with 32; lia.
assert (32 < Int.max_unsigned) by reflexivity. lia.
Qed.
Theorem or_rolm:
......@@ -1848,12 +1849,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
replace (Int.ltu n Int64.iwordsize') with true.
f_equal; apply Int64.shrx'_shr_2; assumption.
symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
symmetry; apply zlt_true. change (Int.unsigned n < 64); lia.
symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
rewrite Int.unsigned_repr.
change (Int.unsigned Int64.iwordsize') with 64; omega.
assert (64 < Int.max_unsigned) by reflexivity. omega.
change (Int.unsigned Int64.iwordsize') with 64; lia.
assert (64 < Int.max_unsigned) by reflexivity. lia.
Qed.
Theorem negate_cmp_bool:
......
......@@ -5,7 +5,7 @@ branch=`git rev-parse --abbrev-ref HEAD`
date=`date -I`
if test "x$CCOMP_INSTALL_PREFIX" = "x" ;
then CCOMP_INSTALL_PREFIX=/opt/CompCert ;
then CCOMP_INSTALL_PREFIX=/home/yuki/Work/VERIMAG/CompCert ;
fi
./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch
......@@ -29,6 +29,7 @@ Require Stacklayout.
Require Import Conventions.
Require Import Errors.
Require Export Asmvliw.
Require Import Lia.
(* Notations necessary to hook Asmvliw definitions *)
Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs.
......@@ -212,7 +213,7 @@ Qed.
Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
Proof.
intros. destruct l; try (contradict H; auto; fail).
cbn. omega.
cbn. lia.
Qed.
Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
......@@ -226,7 +227,7 @@ Qed.
Lemma size_positive (b:bblock): size b > 0.
Proof.
unfold size. destruct b as [hd bdy ex cor]. cbn.
destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega).
destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia).
inversion cor; contradict H; cbn; auto.
Qed.
......
......@@ -21,6 +21,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock.
Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
Require Import Axioms.
Require Import Lia.
Module MB := Machblock.
Module AB := Asmvliw.
......@@ -72,7 +73,7 @@ Lemma transf_function_no_overflow:
transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
Proof.
intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
omega.
lia.
Qed.
Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
......@@ -247,8 +248,8 @@ Proof.
split. unfold goto_label. unfold par_goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
auto. omega.
generalize (transf_function_no_overflow _ _ H0). omega.
auto. lia.
generalize (transf_function_no_overflow _ _ H0). lia.
intros. apply Pregmap.gso; auto.
Qed.
......@@ -1374,7 +1375,7 @@ Lemma mbsize_eqz:
Proof.
intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
remember (length _) as a. remember (length_opt _) as b.
assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
inv H0. inv H1. destruct bdy; destruct ex; auto.
all: try discriminate.
Qed.
......@@ -1706,11 +1707,11 @@ Proof.
+ contradiction.
} destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
exploit exec_straight_steps_2; eauto using functions_transl.
simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
intros (ofs' & X & Y).
left; exists (State rs3' m3'); split.
eapply exec_straight_steps_1; eauto.
simpl fn_blocks. simpl fn_blocks in g. omega.
simpl fn_blocks. simpl fn_blocks in g. lia.
constructor.
econstructor; eauto.
rewrite X; econstructor; eauto.
......@@ -1756,7 +1757,7 @@ Local Transparent destroyed_at_function_entry.
- (* return *)
inv MS.
inv STACKS. simpl in *.
right. split. omega. split. auto.
right. split. lia. split. auto.
rewrite <- ATPC in H5.
econstructor; eauto. congruence.
Qed.
......
......@@ -37,6 +37,7 @@ Require Import Asmblockgen.
Require Import Conventions1.
Require Import Axioms.
Require Import Asmblockprops.
Require Import Lia.
Module MB:=Machblock.
Module AB:=Asmblock.
......@@ -410,7 +411,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
Lemma code_tail_pos:
forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
Proof.
induction 1. omega. generalize (size_positive bi); intros; omega.
induction 1. lia. generalize (size_positive bi); intros; lia.
Qed.
Lemma find_bblock_tail:
......@@ -420,10 +421,10 @@ Lemma find_bblock_tail:
Proof.
induction c1; simpl; intros.
inversion H.
destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
destruct (zeq pos 0). subst pos.
inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
eauto.
Qed.
......@@ -438,13 +439,13 @@ Proof.
induction 1; intros.
- subst; eauto.
- replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
omega.
lia.
Qed.
Lemma size_blocks_pos c: 0 <= size_blocks c.
Proof.
induction c as [| a l ]; simpl; try omega.
generalize (size_positive a); omega.
induction c as [| a l ]; simpl; try lia.
generalize (size_positive a); lia.
Qed.
Remark code_tail_positive:
......@@ -452,15 +453,15 @@ Remark code_tail_positive:
code_tail ofs fn c -> 0 <= ofs.
Proof.
induction 1; intros; simpl.
- omega.
- generalize (size_positive bi). omega.
- lia.
- generalize (size_positive bi). lia.
Qed.
Remark code_tail_size:
forall fn ofs c,
code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
Proof.
induction 1; intros; simpl; try omega.
induction 1; intros; simpl; try lia.
Qed.
Remark code_tail_bounds fn ofs c:
......@@ -469,7 +470,7 @@ Proof.
intro H;
exploit code_tail_size; eauto.
generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
omega.
lia.
Qed.
Local Hint Resolve code_tail_next: core.
......@@ -486,8 +487,8 @@ Proof.
intros.
rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
- rewrite Ptrofs.unsigned_repr; eauto.
omega.
- rewrite Ptrofs.unsigned_repr; omega.
lia.
- rewrite Ptrofs.unsigned_repr; lia.
Qed.
(** Predictor for return addresses in generated Asm code.
......@@ -566,7 +567,7 @@ Proof.
exists (Ptrofs.repr ofs). red; intros.
rewrite Ptrofs.unsigned_repr. congruence.
exploit code_tail_bounds; eauto.
intros; apply transf_function_len in TF. omega.
intros; apply transf_function_len in TF. lia.
+ exists Ptrofs.zero; red; intros. congruence.
Qed.
......@@ -590,7 +591,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
Remark code_tail_no_bigger:
forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
Proof.
induction 1; simpl; omega.
induction 1; simpl; lia.
Qed.
Remark code_tail_unique:
......@@ -598,8 +599,8 @@ Remark code_tail_unique:
code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
Proof.
induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
f_equal. eauto.
Qed.
......@@ -638,12 +639,12 @@ Proof.
simpl; intros until c'.
case (is_label lbl a).
- intros. inv H. exists pos. split; auto. split.
replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
generalize (size_blocks_pos c). generalize (size_positive a). omega.
replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
generalize (size_blocks_pos c). generalize (size_positive a). lia.
- intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
exists pos'. split. auto. split.
replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
constructor. auto. generalize (size_positive a). omega.
replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
constructor. auto. generalize (size_positive a). lia.
Qed.
(** Helper lemmas to reason about
......