coq: Update for 8.12, 8.13 compatibility

Closes GH-8.

README.rst

@@ -30,14 +30,9 @@ Installing dependencies and building from source
 
 * OCaml 4.07 through 4.09, `opam <https://opam.ocaml.org/doc/Install.html>`_ 2.0 or later, GNU make.
 
-* Coq 8.9, 8.10, or 8.11::
+* Coq 8.11 through 8.13::
 
-    opam install coq=8.10.2
-
-* Coq's Ltac2 plugin, if using Coq < 8.9 or 8.10 (newer versions have it built-in)::
-
-    opam repo add coq-released https://coq.inria.fr/opam/released
-    opam install coq-ltac2
+    opam install coq=8.12.2
 
 * Dune 2.5 or later::
 

coq/CircuitOptimization.v

@@ -42,7 +42,7 @@ Section CircuitOptimizer.
 
     Fixpoint unannot {sz} (c: circuit sz) : circuit sz :=
       match c with
-      | CAnnot annot c => unannot c
+      | CAnnot _ c => unannot c
       | c => c
       end.
 
@@ -55,7 +55,7 @@ Section CircuitOptimizer.
     Definition asconst {sz} (c: circuit sz) : option (bits sz) :=
       match unannot c with
       | CConst cst => Some cst
-      | c => None
+      | _ => None
       end.
 
     Definition isconst {sz} (c: circuit sz) (cst: bits sz) :=
@@ -368,7 +368,7 @@ Section CircuitOptimizer.
         if select ~~ b1 then fun _ => c1
         else if select ~~ b0 then fun _ => c2
              else fun c0 => c0
-      | c => fun c0 => c0
+      | _ => fun c0 => c0
       end c.
 
     (** This pass performs the following simplification:

coq/Common.v

@@ -1,5 +1,6 @@
 (*! Utilities | Shared utilities !*)
-Require Export Coq.omega.Omega.
+Require Export Coq.micromega.Lia.
+Require Export Coq.Arith.Arith.
 Require Export Coq.Lists.List Coq.Bool.Bool Coq.Strings.String.
 Require Export Koika.EqDec Koika.Vect Koika.FiniteType Koika.Show.
 
@@ -288,7 +289,7 @@ Section Lists.
       skipn n (List.app l1 l2) = List.app (skipn n l1) l2.
   Proof.
     induction l1; destruct n; cbn; try (inversion 1; reflexivity).
-    - intros; apply IHl1; omega.
+    - intros; apply IHl1; lia.
   Qed.
 
   Lemma forallb_pointwise {A} :

coq/Environments.v

@@ -375,7 +375,7 @@ Section Folds.
       | CtxCons k v ctx => cfoldl ctx (f k v init)
       end.
 
-    Fixpoint cfoldl' {sig} (ctx: context V sig) (init: T) :=
+    Definition cfoldl' {sig} (ctx: context V sig) (init: T) :=
       match sig return context V sig -> T with
       | [] => fun _ => init
       | k :: sig => fun ctx => cfoldl (ctl ctx) (f k (chd ctx) init)

coq/EqDec.v

@@ -19,9 +19,8 @@ Qed.
 Lemma beq_dec_false_iff {A} (EQ: EqDec A) a1 a2 :
   beq_dec a1 a2 = false <-> a1 <> a2.
 Proof.
-  unfold beq_dec; destruct eq_dec; subst.
-  - firstorder.
-  - split; intro; (eauto || congruence).
+  unfold beq_dec; destruct eq_dec; subst;
+    intuition congruence.
 Qed.
 
 Hint Extern 1 (EqDec _) => econstructor; decide equality : typeclass_instances.

coq/FiniteType.v

@@ -1,6 +1,7 @@
 (*! Utilities | Finiteness typeclass !*)
 Require Import Coq.Lists.List.
-Require Import Coq.omega.Omega.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Arith.Arith.
 Import ListNotations.
 
 Class FiniteType {T} :=
@@ -41,15 +42,15 @@ Proof.
   induction l; intros n H n' Hle Habs.
   - auto.
   - apply Bool.andb_true_iff in H; destruct H; apply PeanoNat.Nat.ltb_lt in H.
-    destruct Habs as [ ? | ? ]; subst; try omega.
-    eapply IHl; [ eassumption | .. | eassumption ]; omega.
+    destruct Habs as [ ? | ? ]; subst; try lia.
+    eapply IHl; [ eassumption | .. | eassumption ]; lia.
 Qed.
 
 Lemma increasing_not_In' :
   forall l n, increasing (n :: l) = true -> forall n', n' <? n = true -> ~ In n' (n :: l).
 Proof.
   unfold not; intros l n Hincr n' Hlt [ -> | Hin ]; apply PeanoNat.Nat.ltb_lt in Hlt.
-  - omega.
+  - lia.
   - eapply increasing_not_In;
       [ eassumption | apply Nat.lt_le_incl | eassumption ]; eauto.
 Qed.

coq/IndexUtils.v

@@ -143,8 +143,8 @@ Lemma list_sum_member_le:
     list_sum l.
 Proof.
   induction l; destruct idx.
-  - cbn; omega.
-  - specialize (IHl a0); unfold list_sum, list_sum' in *; cbn; omega.
+  - cbn; lia.
+  - specialize (IHl a0); unfold list_sum, list_sum' in *; cbn; lia.
 Qed.
 
 Instance Show_index (n: nat) : Show (index n) :=

coq/Interop.v

@@ -215,7 +215,7 @@ Section Compilation.
              (s: @koika_package_t pos_t var_t fn_name_t rule_name_t reg_t ext_fn_t)
              (opt: let circuit sz := circuit (lower_R s.(koika_reg_types))
                                             (lower_Sigma s.(koika_ext_fn_types)) sz in
-                   forall {sz}, circuit sz -> circuit sz)
+                   forall sz, circuit sz -> circuit sz)
     : circuit_package_t :=
     let _ := s.(koika_reg_finite) in
     let _ := s.(koika_var_names) in

coq/LoweredSyntaxFunctions.v

@@ -35,7 +35,7 @@ Section LoweredSyntaxFunctions.
     Definition action_footprint {sig tau} (a: action sig tau) :=
       action_footprint' [] a.
 
-    Fixpoint action_registers {sig tau} {EQ: EqDec reg_t} (a: action sig tau) : list reg_t :=
+    Definition action_registers {sig tau} {EQ: EqDec reg_t} (a: action sig tau) : list reg_t :=
       dedup [] (List.map (fun '(rs, _) => rs) (action_footprint a)).
 
     Context (rules: rule_name_t -> rule).

coq/Member.v

@@ -234,7 +234,7 @@ Proof.
     + exact (MemberTl k k' (sig ++ infix ++ sig') (minfix _ infix sig sig' k m')).
 Defined.
 
-Fixpoint mprefix_pair {K sig} (k: K) (p: {k': K & member k' sig})
+Definition mprefix_pair {K sig} (k: K) (p: {k': K & member k' sig})
   : {k': K & member k' (k :: sig)} :=
   let '(existT _ k' m) := p in
   existT _ k' (MemberTl k' k _ m).

coq/Parsing.v

@@ -44,8 +44,8 @@ Notation "'()'"  := nil (in custom koika_args).
 (* Notation "'( )'"  := nil (in custom koika_args). *)
 Notation "'(' x ')'"  := x (in custom koika_args, x custom koika_middle_args).
 (* Koika_var *)
-Notation "a" := (ident_to_string a) (in custom koika_var at level 0, a constr at level 0, format "'[' a ']'",only parsing).
-Notation "a" := (a) (in custom koika_var at level 0, a constr at level 0, format "'[' a ']'",only printing).
+Notation "a" := (ident_to_string a) (in custom koika_var at level 0, a constr at level 0, only parsing).
+Notation "a" := (a) (in custom koika_var at level 0, a constr at level 0, format "'[' a ']'", only printing).
 
 (* Koika_types *)
 Notation " '(' x ':' y ')'" := (cons (prod_of_argsig {| arg_name := x%string; arg_type := y |}) nil) (in custom koika_types at level 60, x custom koika_var at level 0, y constr at level 12 ).

coq/PrimitiveProperties.v

@@ -7,7 +7,7 @@ Ltac min_t :=
   repeat match goal with
          | [ |- context[Min.min ?x ?y] ] =>
            first [rewrite (Min.min_l x y) by min_t | rewrite (Min.min_r x y) by min_t ]
-         | _ => omega
+         | _ => lia
          end.
 
 Lemma slice_end :
@@ -18,7 +18,7 @@ Proof.
   apply vect_to_list_inj.
   unfold Bits.slice, vect_skipn_plus, vect_extend_end_firstn, vect_extend_end.
   autorewrite with vect_to_list.
-  min_t; rewrite Nat.sub_diag by omega; cbn.
+  min_t; rewrite Nat.sub_diag by lia; cbn.
   rewrite app_nil_r.
   rewrite firstn_skipn.
   rewrite firstn_all2 by (rewrite vect_to_list_length; reflexivity).
@@ -72,10 +72,10 @@ Proof.
   unfold Bits.slice_subst, vect_skipn_plus, vect_firstn_plus, vect_extend_end_firstn, vect_extend_end.
   autorewrite with vect_to_list.
   rewrite !firstn_app.
-  rewrite firstn_length_le by (rewrite vect_to_list_length; omega).
+  rewrite firstn_length_le by (rewrite vect_to_list_length; lia).
   rewrite !minus_plus, vect_to_list_length, Nat.sub_diag; cbn.
-  rewrite firstn_firstn by omega; min_t.
-  rewrite (firstn_all2 (n := sz)) by (rewrite vect_to_list_length; omega).
+  rewrite firstn_firstn by lia; min_t.
+  rewrite (firstn_all2 (n := sz)) by (rewrite vect_to_list_length; lia).
   rewrite app_nil_r; reflexivity.
 Qed.
 
@@ -91,19 +91,19 @@ Proof.
     unfold Bits.slice_subst, vect_skipn_plus, vect_firstn_plus, vect_extend_end_firstn, vect_extend_end.
   autorewrite with vect_to_list.
   rewrite !firstn_app.
-  rewrite firstn_length_le by (rewrite vect_to_list_length; omega).
+  rewrite firstn_length_le by (rewrite vect_to_list_length; lia).
   rewrite vect_to_list_length; cbn.
   rewrite !firstn_firstn; repeat min_t.
-  rewrite firstn_length_le by (rewrite vect_to_list_length; omega).
+  rewrite firstn_length_le by (rewrite vect_to_list_length; lia).
   rewrite <- !app_assoc.
   rewrite skipn_firstn, firstn_firstn.
   min_t.
-  rewrite !(firstn_all2 (vect_to_list bs)) by (rewrite vect_to_list_length; omega).
-  replace (sz0 + sz - offset - width) with (sz0 + sz - (offset + width)) by omega.
-  replace (sz0 - offset - width) with (sz0 - (offset + width)) by omega.
+  rewrite !(firstn_all2 (vect_to_list bs)) by (rewrite vect_to_list_length; lia).
+  replace (sz0 + sz - offset - width) with (sz0 + sz - (offset + width)) by lia.
+  replace (sz0 - offset - width) with (sz0 - (offset + width)) by lia.
   rewrite <- !skipn_firstn.
-  rewrite (firstn_all2 (n := sz0 + sz)) by (rewrite vect_to_list_length; omega).
-  rewrite <- skipn_app by (rewrite firstn_length, vect_to_list_length; min_t; omega).
+  rewrite (firstn_all2 (n := sz0 + sz)) by (rewrite vect_to_list_length; lia).
+  rewrite <- skipn_app by (rewrite firstn_length, vect_to_list_length; min_t; lia).
   rewrite List.firstn_skipn.
   reflexivity.
 Qed.
@@ -237,7 +237,7 @@ Ltac vect_to_list_t_step :=
   | _ => progress (autounfold with vect_to_list)
   | _ => progress autorewrite with vect_to_list vect_to_list_cleanup
   | [ |- context[match ?x with _ => _ end] ] => destruct x
-  | _ => repeat rewrite ?Min.min_l, ?Min.min_r by omega
+  | _ => repeat rewrite ?Min.min_l, ?Min.min_r by lia
   end.
 
 Ltac vect_to_list_t :=
@@ -249,11 +249,11 @@ Lemma slice_subst_impl_correct :
     slice_subst_impl offset a1 a2.
 Proof.
   intros; vect_to_list_t.
-  - rewrite (firstn_all2 (n := sz - offset)) by (autorewrite with vect_to_list; omega).
+  - rewrite (firstn_all2 (n := sz - offset)) by (autorewrite with vect_to_list; lia).
     reflexivity.
-  - rewrite (skipn_all2 (n := offset + width)) by (autorewrite with vect_to_list; omega).
+  - rewrite (skipn_all2 (n := offset + width)) by (autorewrite with vect_to_list; lia).
     autorewrite with vect_to_list_cleanup; reflexivity.
-  - rewrite (firstn_all2 (n := sz)) by (autorewrite with vect_to_list; omega).
+  - rewrite (firstn_all2 (n := sz)) by (autorewrite with vect_to_list; lia).
     reflexivity.
 Qed.
 
@@ -262,7 +262,7 @@ Lemma slice_full {sz}:
     Bits.slice 0 sz bs = bs.
 Proof.
   intros; vect_to_list_t.
-  rewrite (firstn_all2 (n := sz)) by (autorewrite with vect_to_list; omega);
+  rewrite (firstn_all2 (n := sz)) by (autorewrite with vect_to_list; lia);
     reflexivity.
 Qed.
 
@@ -271,7 +271,7 @@ Lemma slice_concat_l {sz1 sz2} :
     Bits.slice 0 sz1 (bs1 ++ bs2)%vect = bs1.
 Proof.
   intros; vect_to_list_t.
-  rewrite (firstn_all2 (n := sz1)) by (autorewrite with vect_to_list; omega);
+  rewrite (firstn_all2 (n := sz1)) by (autorewrite with vect_to_list; lia);
     reflexivity.
 Qed.
 
@@ -280,9 +280,9 @@ Lemma slice_concat_r {sz1 sz2} :
     Bits.slice sz1 sz2 (bs1 ++ bs2)%vect = bs2.
 Proof.
   intros; vect_to_list_t.
-  rewrite (skipn_all2 (n := sz1)) by (autorewrite with vect_to_list; omega).
+  rewrite (skipn_all2 (n := sz1)) by (autorewrite with vect_to_list; lia).
   vect_to_list_t.
-  rewrite (firstn_all2 (n := sz2)) by (autorewrite with vect_to_list; omega).
+  rewrite (firstn_all2 (n := sz2)) by (autorewrite with vect_to_list; lia).
   reflexivity.
 Qed.
 
@@ -333,6 +333,11 @@ Section Arithmetic.
       apply N.log2_lt_pow2; lia.
   Qed.
 
+  Lemma pow2_nz :
+    forall n, N.pow 2 n <> 0%N.
+  Proof. intros; apply N.pow_nonzero; lia. Qed.
+  Hint Resolve pow2_nz: core.
+
   Lemma to_N_vect_unsnoc :
     forall sz (x: bits (S sz)),
       (Bits.to_N (snd (vect_unsnoc x)) = Bits.to_N x mod (2 ^ N.of_nat sz))%N.
@@ -342,7 +347,8 @@ Section Arithmetic.
     - simpl.
       destruct x. destruct vtl. cbn.
       destruct_match; reflexivity.
-    - destruct x.
+    - pose proof pow2_nz (N.of_nat sz).
+      destruct x.
       rewrite Nat2N.inj_succ, N.pow_succ_r'. cbn.
       specialize (IHsz vtl).
       destruct (vect_unsnoc vtl) eqn:H_unsnoc_vtl.
@@ -351,17 +357,13 @@ Section Arithmetic.
       rewrite (N.mod_small (if vhd then 1 else 0)).
       + rewrite (N.mod_small _ (2 * 2 ^ N.of_nat sz)).
         * f_equal.
-          rewrite N.mul_mod_distr_l by (destruct sz; cbn; lia).
-          reflexivity.
+          rewrite N.mul_mod_distr_l by lia;
+            reflexivity.
         * destruct vhd.
-          -- rewrite N.mul_mod_distr_l by (destruct sz; cbn; lia).
-             apply N.mul_2_mono_l.
-             apply N.mod_lt. destruct sz; cbn; lia.
-          -- apply N.mod_lt. destruct sz; cbn; lia.
-      + destruct vhd.
-        * apply N.lt_1_mul_pos. lia.
-          destruct sz; cbn; lia.
-        * destruct sz; cbn; lia.
+          -- rewrite N.mul_mod_distr_l by lia.
+             eauto using N.mul_2_mono_l, N.mod_lt.
+          -- apply N.mod_lt; lia.
+      + destruct vhd; lia.
   Qed.
 
   Lemma to_N_lsl1 :
@@ -374,9 +376,10 @@ Section Arithmetic.
       destruct x.
       reflexivity.
     - intros.
+      pose proof pow2_nz (N.of_nat sz).
       rewrite Nat2N.inj_succ, N.pow_succ_r'.
       cbn. rewrite (N.mul_comm _ 2).
-      rewrite N.mul_mod_distr_l by (destruct sz; cbn; lia).
+      rewrite N.mul_mod_distr_l by lia.
       f_equal.
       apply to_N_vect_unsnoc.
   Qed.
@@ -392,7 +395,7 @@ Section Arithmetic.
     - rewrite Nat2N.inj_succ, N.pow_succ_r'.
       cbn.
       rewrite IHn, to_N_lsl1.
-      rewrite N.mul_mod_idemp_l by (destruct sz; cbn; lia).
+      rewrite N.mul_mod_idemp_l by (pose proof pow2_nz (N.of_nat sz); lia).
       f_equal. ring.
   Qed.
 

coq/SyntaxMacros.v

@@ -168,7 +168,7 @@ Module Display.
          int_retSig := unit_t;
          int_body := display_utf8 "\n" |}.
 
-    Fixpoint extend_printer f (offset: nat) (printer: intfun) : intfun :=
+    Definition extend_printer f (offset: nat) (printer: intfun) : intfun :=
       let opts :=
           {| display_newline := false; display_strings := false; display_style := dFull |} in
       let display_value arg :=

coq/TypeInference.v

@@ -76,7 +76,7 @@ Section TypeInference.
 
     Notation EX Px := (existT _ _ Px).
 
-    Fixpoint actpos {reg_t ext_fn_t} pos (e: uaction reg_t ext_fn_t) :=
+    Definition actpos {reg_t ext_fn_t} pos (e: uaction reg_t ext_fn_t) :=
       match e with
       | UAPos p _ => p
       | _ => pos

coq/TypedSyntaxFunctions.v

@@ -62,7 +62,7 @@ Section TypedSyntaxFunctions.
         dedup acc l
       end.
 
-    Fixpoint action_registers {sig tau} {EQ: EqDec reg_t} (a: action sig tau) : list reg_t :=
+    Definition action_registers {sig tau} {EQ: EqDec reg_t} (a: action sig tau) : list reg_t :=
       dedup [] (List.map (fun '(rs, _) => rs) (action_footprint a)).
 
     Context (rules: rule_name_t -> rule).
@@ -431,13 +431,13 @@ Section TypedSyntaxFunctions.
     | MemberTl (k, _) (k', _) sig' m' => beq_dec k k' || member_mentions_shadowed_binding m'
     end.
 
-  Fixpoint action_mentions_shadowed_var {EQ: EqDec var_t} {sig tau} (a: action sig tau) :=
+  Definition action_mentions_shadowed_var {EQ: EqDec var_t} {sig tau} (a: action sig tau) :=
     existsb_subterm (fun a => match a with
                            | AnyAction (Var m) => member_mentions_shadowed_binding m
                            | _ => false
                            end) a.
 
-  Fixpoint action_mentions_var {EQ: EqDec var_t} {sig tau} (k: var_t) (a: action sig tau) :=
+  Definition action_mentions_var {EQ: EqDec var_t} {sig tau} (k: var_t) (a: action sig tau) :=
     existsb_subterm (fun a => match a with
                            | AnyAction (@Var _ _ _ _ _ _ _ _ k' _ m) => beq_dec k k'
                            | _ => false