Mercurial > cpdt > repo

changeset 574:1dc1d41620b6 tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents c3d77f2bb92c
children
files .hgignore src/CpdtTactics.v src/DataStruct.v src/DepList.v src/GeneralRec.v src/InductiveTypes.v src/Large.v src/LogicProg.v src/MoreDep.v src/Universes.v
diffstat 10 files changed, 45 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Sun Feb 02 10:51:18 2020 -0500
+++ b/.hgignore	Sun Jul 31 14:48:22 2022 -0400
@@ -42,3 +42,4 @@
 *.out
 src/.coq-native
 .coqdeps.d
+*.cache
--- a/src/CpdtTactics.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/CpdtTactics.v	Sun Jul 31 14:48:22 2022 -0400
@@ -7,7 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-Require Import Eqdep List Omega.
+Require Import Eqdep List Lia.
 
 Set Implicit Arguments.
 
@@ -196,8 +196,8 @@
           repeat (simplHyp invOne; intuition)); un_done
       end;
       sintuition; rewriter; sintuition;
-      (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
-      try omega; try (elimtype False; omega)).
+      (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *)
+      try lia; try (elimtype False; lia)).
 
 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
 Ltac crush := crush' false fail.
--- a/src/DataStruct.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/DataStruct.v	Sun Jul 31 14:48:22 2022 -0400
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Arguments Nil [A].
-Arguments First [n].
+Arguments Nil {A}.
+Arguments First {n}.
 
 (** A few examples show how to make use of these definitions. *)
 
@@ -242,10 +242,10 @@
 End hlist.
 
 (* begin thide *)
-Arguments HNil [A B].
+Arguments HNil {A B}.
 Arguments HCons [A B x ls] _ _.
 
-Arguments HFirst [A elm ls].
+Arguments HFirst {A elm ls}.
 Arguments HNext [A elm x ls] _.
 (* end thide *)
 
@@ -302,7 +302,7 @@
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
 
-Arguments Const [ts].
+Arguments Const {ts}.
 
 (** We write a simple recursive function to translate [type]s into [Set]s. *)
 
--- a/src/DepList.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/DepList.v	Sun Jul 31 14:48:22 2022 -0400
@@ -107,8 +107,8 @@
   End fold.
 End ilist.
 
-Arguments INil [A].
-Arguments First [n].
+Arguments INil {A}.
+Arguments First {n}.
 
 Section imap.
   Variables A B : Type.
@@ -197,11 +197,11 @@
   Qed.
 End hlist.
 
-Arguments HNil [A B].
+Arguments HNil {A B}.
 Arguments HCons [A B x ls] _ _.
 Arguments hmake [A B] f ls.
 
-Arguments HFirst [A elm ls].
+Arguments HFirst {A elm ls}.
 Arguments HNext [A elm x ls] _.
 
 Infix ":::" := HCons (right associativity, at level 60).
--- a/src/GeneralRec.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/GeneralRec.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import Arith List Omega.
+Require Import Arith List Lia.
 
 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
 
@@ -163,7 +163,9 @@
   (** We must prove that the relation is truly well-founded.  To save some space in the rest of this chapter, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts to Part III of the book.  Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *)
 
   Hint Constructors Acc.
-
+  Hint Extern 2 (Acc _ _) => lia.
+  Hint Extern 2 (_ <= _) => lia.
+  
   Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
     unfold lengthOrder; induction len; crush.
   Defined.
@@ -506,7 +508,7 @@
 
   (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
 
-  Hint Extern 1 (_ >= _) => omega.
+  Hint Extern 1 (_ >= _) => lia.
   Hint Unfold leq.
 
   Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
--- a/src/InductiveTypes.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/InductiveTypes.v	Sun Jul 31 14:48:22 2022 -0400
@@ -479,7 +479,7 @@
 (* end thide *)
 End list.
 
-Arguments Nil [T].
+Arguments Nil {T}.
 
 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 
--- a/src/Large.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/Large.v	Sun Jul 31 14:48:22 2022 -0400
@@ -258,9 +258,9 @@
    eval e1 * eval e3 * eval e4 = eval e1 * eval e2
    ]]
 
-   The [crush] tactic does not know how to finish this goal.  We could finish the proof manually. *)
+   The [crush] tactic does not know how to finish this goal.  We could finish the proof manually.  Just kidding, the standard library got smarter, and the following is now redundant! *)
 
-  rewrite <- IHe2; crush.
+  (*rewrite <- IHe2; crush.*)
 
   (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
 
@@ -460,7 +460,8 @@
   (** What is [t] doing to get us to this point?  The %\index{tactics!info}%[info] command can help us answer this kind of question.  (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *)
 
   Undo.
-  info t.
+  (*info*) t.
+  (* Too bad: recent Coq versions removed [info]. *)
 
   (* begin hide *)
   (* begin thide *)
@@ -515,7 +516,7 @@
 
   Undo.
 
-  info autorewrite with core in *.
+  (*info*) autorewrite with core in *.
   (** %\vspace{-.15in}%[[
  == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
               (confounder (reassoc e1) e3 e4)).
@@ -566,7 +567,7 @@
 
 (* begin thide *)
     Restart.
-    info eauto 6.
+    (*info*) eauto 6.
     (** %\vspace{-.15in}%[[
  == intro x; intro y; intro H; intro H0; intro H4;
        simple eapply trans_eq.
--- a/src/LogicProg.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/LogicProg.v	Sun Jul 31 14:48:22 2022 -0400
@@ -9,7 +9,7 @@
 
 (* begin hide *)
 
-Require Import List Omega.
+Require Import List Lia.
 
 Require Import Cpdt.CpdtTactics.
 
@@ -152,7 +152,7 @@
 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical.  (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon.  The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *)
 
 Restart.
-  info auto 6.
+  info_auto 6.
 (** %\vspace{-.15in}%[[
  == apply PlusS; apply PlusS; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusO.
@@ -220,7 +220,7 @@
 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will.  It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *)
 
 Restart.
-  info eauto 6.
+  info_eauto 6.
 (** %\vspace{-.15in}%[[
  == eapply ex_intro; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusS; apply PlusO.
@@ -431,7 +431,7 @@
   -> y = 2
   -> exists z, z + x = 3.
 (* begin thide *)
-  info eauto with slow.
+  info_eauto with slow.
 (** %\vspace{-.2in}%[[
  == intro x; intro y; intro H; intro H0; simple eapply ex_intro; 
     apply plusS; simple eapply eq_trans.
@@ -672,9 +672,9 @@
 
 Hint Resolve EvalPlus'.
 
-(** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic.  Via [Hint Extern], we ask for use of [omega] on any equality goal.  The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
+(** Further, we instruct [eauto] to apply %\index{tactics!lia}%[lia], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic.  Via [Hint Extern], we ask for use of [lia] on any equality goal.  The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
 
-Hint Extern 1 (_ = _) => abstract omega.
+Hint Extern 1 (_ = _) => abstract lia.
 (* end thide *)
 
 (** Now we can return to [eval1'] and prove it automatically. *)
@@ -696,7 +696,7 @@
 ]]
 *)
 
-(** The lemma [eval1'_subproof] was generated by [abstract omega].
+(** The lemma [eval1'_subproof] was generated by [abstract lia].
 
    Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *)
 
--- a/src/MoreDep.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/MoreDep.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import Arith Bool List Omega.
+Require Import Arith Bool List Lia.
 
 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
 
@@ -871,6 +871,7 @@
 (* end hide *)
 
 (** A few auxiliary functions help us in our final matcher definition.  The function [split] will be used to implement the regexp concatenation case. *)
+Hint Extern 1 (_ <= _) => lia.
 
 Section split.
   Variables P1 P2 : string -> Prop.
@@ -938,7 +939,7 @@
   induction s; substring.
 Qed.
 
-Hint Rewrite substring_self substring_empty using omega.
+Hint Rewrite substring_self substring_empty using lia.
 
 Lemma substring_split' : forall s n m,
   substring n m s ++ substring (n + m) (length s - (n + m)) s
@@ -986,7 +987,7 @@
       | [ |- ?N >= _ ] => destruct N; crush
     end;
     match goal with
-      [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
+      [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | lia ]
     end.
 Qed.
 
@@ -998,19 +999,19 @@
 Qed.
 
 Hint Rewrite substring_stack substring_stack' substring_suffix
-  using omega.
+  using lia.
 
 Lemma minus_minus : forall n m1 m2,
   m1 + m2 <= n
   -> n - m1 - m2 = n - (m1 + m2).
-  intros; omega.
+  intros; lia.
 Qed.
 
 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
-  intros; omega.
+  intros; lia.
 Qed.
 
-Hint Rewrite minus_minus using omega.
+Hint Rewrite minus_minus using lia.
 (* end hide *)
 
 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *)
@@ -1099,7 +1100,8 @@
     (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *)
 
     (** Now we come to [dec_star''] itself.  It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split'].  The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *)
-
+    Hint Extern 2 (_ \/ _) => lia.
+    
     Definition dec_star'' : forall l : nat,
       {exists l', S l' <= l
         /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
--- a/src/Universes.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/Universes.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,9 @@
  *)
 
 (* begin hide *)
-Require Import List.
+Require Import List Lia.
+Hint Extern 2 False => lia.
+Hint Extern 2 (@eq nat _ _) => lia.
 
 Require Import DepList Cpdt.CpdtTactics.