Using exfalso and Nat.add for Coq 8.19

src/DeBruijn.v

@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Generalizable All Variables.
 Require Import Arith.
 Require Import Lia.
 Require Import Dblib.DblibTactics.
 
 (* ---------------------------------------------------------------------------- *)
@@ -640,10 +640,10 @@
    meta-variable. *)
 
 Ltac plus_0_r :=
-  repeat match goal with |- context[?x + 0] => rewrite (plus_0_r x) end.
+  repeat match goal with |- context[?x + 0] => rewrite (Nat.add_0_r x) end.
 
 Ltac plus_0_r_in h :=
-  repeat match type of h with context[?x + 0] => rewrite (plus_0_r x) in h end.
+  repeat match type of h with context[?x + 0] => rewrite (Nat.add_0_r x) in h end.
 
 (* It is worth noting that instead of writing:
      traverse (fun l x => var (lift w (l + k) x)) 0 t
@@ -673,11 +673,11 @@
 
 Ltac recognize_lift :=
   rewrite recognize_lift by eauto with typeclass_instances;
-  repeat rewrite plus_0_l. (* useful when [k1] is zero *)
+  repeat rewrite Nat.add_0_l. (* useful when [k1] is zero *)
 
 Ltac recognize_lift_in h :=
   rewrite recognize_lift in h by eauto with typeclass_instances;
-  repeat rewrite plus_0_l in h. (* useful when [k1] is zero *)
+  repeat rewrite Nat.add_0_l in h. (* useful when [k1] is zero *)
 
 (* The tactic [simpl_lift] is used to simplify an application of [lift] to a
    concrete term, such as [TApp t ...], where [TApp] is a user-defined
@@ -713,7 +713,7 @@
     match type of _traverse with (nat -> nat -> ?V) -> nat -> ?T -> ?T =>
       repeat rewrite (@recognize_lift V _ T _ _) by eauto with typeclass_instances
     end;
-    repeat rewrite plus_0_l (* useful when [k1] is zero and we are at a leaf *)
+    repeat rewrite Nat.add_0_l (* useful when [k1] is zero and we are at a leaf *)
 
   (* Case: [_traverse] appears in a hypothesis. *)
   (* this binds the meta-variable [_traverse] to the user's [traverse_term] *)
@@ -728,7 +728,7 @@
     match type of _traverse with (nat -> nat -> ?V) -> nat -> ?T -> ?T =>
       repeat rewrite (@recognize_lift V _ T _ _)  in h by eauto with typeclass_instances
     end;
-    repeat rewrite plus_0_l in h (* useful when [k1] is zero and we are at a leaf *)
+    repeat rewrite Nat.add_0_l in h (* useful when [k1] is zero and we are at a leaf *)
 
   end.
 
@@ -802,7 +802,7 @@
   constructor. unfold lift, Lift_Traverse. intros w k. intros.
   eapply traverse_var_injective with (f := fun l x => lift w (l + k) x).
   eauto using lift_injective.
   eassumption.
 Qed.
 
 Instance LiftLift_Traverse:
@@ -886,12 +886,12 @@
 Ltac recognize_subst :=
   rewrite recognize_subst by eauto with typeclass_instances;
   try rewrite lift_zero; (* useful when [k1] is zero *)
-  repeat rewrite plus_0_l. (* useful when [k1] is zero *)
+  repeat rewrite Nat.add_0_l. (* useful when [k1] is zero *)
 
 Ltac recognize_subst_in h :=
   rewrite recognize_subst in h by eauto with typeclass_instances;
   try rewrite lift_zero in h; (* useful when [k1] is zero *)
-  repeat rewrite plus_0_l in h. (* useful when [k1] is zero *)
+  repeat rewrite Nat.add_0_l in h. (* useful when [k1] is zero *)
 
 (* This tactic is used to simplify an application of [subst] to a concrete
    term, such as [TApp t1 t2], where [TApp] is a user-defined constructor of
@@ -917,7 +917,7 @@
     match type of _traverse with (nat -> nat -> ?V) -> nat -> ?T -> ?T =>
       repeat rewrite (@recognize_subst V _ _ T _ _ _ _ _) by eauto with typeclass_instances
     end;
-    repeat rewrite plus_0_l; (* useful when [k1] is zero and we are at a leaf *)
+    repeat rewrite Nat.add_0_l; (* useful when [k1] is zero and we are at a leaf *)
     repeat rewrite lift_zero (* useful when [k1] is zero and we are at a leaf *)
 
   (* Case: [_traverse] appears in a hypothesis. *)
@@ -933,7 +933,7 @@
     match type of _traverse with (nat -> nat -> ?V) -> nat -> ?T -> ?T =>
       repeat rewrite (@recognize_subst V _ _ T _ _ _ _ _) in h by eauto with typeclass_instances
     end;
-    repeat rewrite plus_0_l in h; (* useful when [k1] is zero and we are at a leaf *)
+    repeat rewrite Nat.add_0_l in h; (* useful when [k1] is zero and we are at a leaf *)
     repeat rewrite lift_zero in h (* useful when [k1] is zero and we are at a leaf *)
 
   end.
@@ -1660,7 +1660,7 @@
   intros.
   rewrite <- lift_lift_fuse_successor.
   rewrite lift_lift by lia.
-  rewrite plus_0_r.
+  rewrite Nat.add_0_r.
   apply subst_lift.
 Qed.
 

src/Environments.v

@@ -216,14 +216,14 @@ Lemma lookup_insert_old:
 (* Hence, [lookup x (insert y a e) = lookup (x - 1) e]. *)
 Proof.
   (* Induction over [x], which is non-zero. *)
-  induction x; intros; [ elimtype False; lia | replace (S x - 1) with x by lia ].
+  induction x; intros; [ exfalso; lia | replace (S x - 1) with x by lia ].
   - { (* Case analysis. *)
       destruct y; destruct e; simpl; try solve [ eauto ].
       - (* One troublesome case. *)
         rewrite lookup_empty_None. erewrite <- lookup_empty_None. intuition.
       - (* Another troublesome case. *)
         destruct x; intros;
-        [ elimtype False; lia | replace (S x - 1) with x in * by lia ].
+        [ exfalso; lia | replace (S x - 1) with x in * by lia ].
         simpl lookup at 2.
         intuition.
     }
@@ -323,7 +323,7 @@ Lemma insert_insert:
 Proof.
   intros ? k s. generalize s k; clear s k. induction s; intros.
   - (* Case [s = 0]. *)
-    destruct k; [ | elimtype False; lia ]. reflexivity.
+    destruct k; [ | exfalso; lia ]. reflexivity.
   - (* Case [s > 0]. *)
     { destruct k.
       - (* Sub-case [k = 0]. *)
@@ -457,8 +457,8 @@ Proof.
           generalize (IHx1 _ _ _ _ _ h xx); intros [ e [ y1 [ y2 [ ? [ ? [ ? ? ]]]]]]
         end.
         (* [e1] and [e2] must be non-nil. *)
-        { destruct e1; simpl tl in *; [ elimtype False; eauto using insert_nil | ].
-        - destruct e2; simpl tl in *; [ elimtype False; eauto using insert_nil | ].
+        { destruct e1; simpl tl in *; [ exfalso; eauto using insert_nil | ].
+        - destruct e2; simpl tl in *; [ exfalso; eauto using insert_nil | ].
         + exists (o :: e). exists (S y1). exists (S y2).
           split. simpl. congruence.
           split. simpl. congruence.
@@ -804,14 +804,14 @@ Lemma agree_empty_left:
   forall A (e : env A),
   agree (@empty _) e 0.
 Proof.
-  unfold agree. intros. elimtype False. lia.
+  unfold agree. intros. exfalso. lia.
 Qed.
 
 Lemma agree_empty_right:
   forall A (e : env A),
   agree e (@empty _) 0.
 Proof.
-  unfold agree. intros. elimtype False. lia.
+  unfold agree. intros. exfalso. lia.
 Qed.
 
 (* If two environments that agree up to [k] are extended with a new variable,
@@ -897,7 +897,7 @@ Section Subsume.
   Proof.
     intros. destruct o1.
     - eauto.
-    - elimtype False. eauto using osub_None_Some.
+    - exfalso. eauto using osub_None_Some.
   Qed.
 
   (* Then, it is extended pointwise to environments. *)
@@ -1002,7 +1002,7 @@ Section Subsume.
     (* Really painful. *)
     induction e1; simpl; intros.
     - (* Base. *)
-      elimtype False.
+      exfalso.
       match goal with h: subsume nil _ |- _ =>
         generalize (h x); clear h; intro h;
         rewrite lookup_insert_bingo in h by reflexivity;