Strengthen In_size lemma

erasure/theories/EConstructorsAsBlocks.v

@@ -67,7 +67,7 @@ Section transform_blocks.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
     - change (fun x => size (id x)) with size in H.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H.
@@ -82,6 +82,8 @@ Section transform_blocks.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - eapply (In_size dbody size) in H; lia.
+    - eapply (In_size dbody size) in H; lia.
     - now eapply InPrim_size in H.
   Qed.
 

erasure/theories/EEtaExpanded.v

@@ -79,23 +79,18 @@ Section isEtaExp.
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
-    all:try apply (In_size); tea.
-    all:try lia.
-    - now apply (In_size id size).
-    - rewrite size_mkApps.
-      eapply (In_size id size) in H.
-      change (fun x => size (id x)) with size in H. unfold id in *; cbn.
-      lia.
-    - now eapply size_mkApps_f.
-    - change (fun x => size (id x)) with size in H.
-      eapply (In_size id size) in H. unfold id in H.
-      change (fun x => size x) with size in H.
-      pose proof (size_mkApps_l napp nnil). lia.
+    3:now eapply size_mkApps_f.
+    3:{ pose proof (size_mkApps_l napp nnil).
+        setoid_rewrite <- (In_size id size H) in H0. unfold id in H0. lia. }
+    all:try rewrite size_mkApps.
+    all:try setoid_rewrite <- (In_size id size H); unfold id.
+    all: try (cbn; lia).
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; intuition eauto.
       subst. lia.
-      eapply (In_size id size) in H0. unfold id in H0.
-      change (fun x => size x) with size in H0. lia.
+      setoid_rewrite <- (In_size id size H0); unfold id. lia.
   Qed.
 
 End isEtaExp.

erasure/theories/EEtaExpandedFix.v

@@ -301,7 +301,8 @@ Section isEtaExp.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite (In_size id size); tea. unfold id.
+      now change (fun x => size x) with size.
     - rewrite size_mkApps. cbn.
       apply (In_size id size) in H.
       unfold id in H. change (fun x => size x) with size in H. lia.
@@ -320,6 +321,7 @@ Section isEtaExp.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; eauto. destruct H; subst; try lia.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H. lia.

erasure/theories/EImplementBox.v

@@ -59,9 +59,11 @@ Section implement_box.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
-    - now eapply (In_size id size).
-    - eapply (In_size snd size) in H. cbn in *. lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size snd size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
     - now eapply InPrim_size in H.
   Qed.
 

erasure/theories/ERemoveParams.v

@@ -63,7 +63,8 @@ Section strip.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
-    - now eapply (In_size id size).
+    - eapply (In_size id size) in H. unfold id in H.
+      change (fun x => size x) with size in *. lia.
     - rewrite size_mkApps.
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H.  cbn. lia.
     - rewrite size_mkApps.
@@ -72,6 +73,8 @@ Section strip.
     - pose proof (size_mkApps_l napp nnil).
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H. lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
     - destruct p as [? []]; cbn in H; eauto.
       intuition auto; subst; cbn; try lia.
       eapply (In_size id size) in H0. unfold id in H0.

utils/theories/MCArith.v

@@ -58,3 +58,26 @@ Proof.
   rewrite Pos2Nat.inj_1. reflexivity.
   rewrite Pos2Nat.inj_succ. cbn. f_equal. lia.
 Qed.
+
+(* Missing rewriting theory on natural number orders *)
+
+Require Import Morphisms Morphisms_Prop.
+#[export] Instance proper_S_lt : Morphisms.Proper (lt ==> lt)%signature S.
+Proof. red. intros x y h. lia. Qed.
+#[export] Instance proper_add_lt_r : Morphisms.Proper (eq ==> lt ==> lt)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+#[export] Instance proper_add_lt_l : Morphisms.Proper (lt ==> eq ==> lt)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+
+#[export] Instance proper_S_le : Morphisms.Proper (le ==> le)%signature S.
+Proof. red. intros x y h. lia. Qed.
+#[export] Instance proper_add_le_r : Morphisms.Proper (eq ==> le ==> le)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+#[export] Instance proper_add_le_l : Morphisms.Proper (le ==> eq ==> le)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+
+#[export] Instance subrel_eq_le : subrelation eq le.
+Proof. red. now intros ?? ->. Qed.
+
+#[export] Instance subrel_lt_le : subrelation lt le.
+Proof. red. intros ???. lia. Qed.

utils/theories/MCList.v

@@ -1406,7 +1406,7 @@ Proof.
 Qed.
 
 Lemma In_size {A B} {x : A} {l : list A} (proj : A -> B) (size : B -> nat) :
-  In x l -> size (proj x) < S (list_size (size ∘ proj) l).
+  In x l -> size (proj x) < (list_size (size ∘ proj) l).
 Proof.
   induction l; cbn => //.
   intros [->|hin]. lia. specialize (IHl hin); lia.