From f53a011ac83fa820faba970109485780715e153f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 23 Jan 2019 15:16:39 +0100 Subject: Pass some files to strict focusing mode. ie default goal selector ! How to do this: - change the default value of default goal selector in goal_select.ml - eval the emacs code in this commit message - compile Coq and in each erroring file repeatedly run [C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer) until there are no errors (NB the first [C-c f] has no effect). You need to watch for 2 cases: - overly deep proofs where the bullets need to go beyond the list in my/bullet-stack (6 layers is enough the vast majority of the time though). The system will give you an error and you need to finish the lemma manually. - weird indentation when a bullet starts in the middle of a line and doesn't end in that line. Just reindent as you like then go to the next error and continue. ~~~emacs-lisp (defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**") "Which bullets should be used, in order.") (defvar-local my/bullet-count nil "The value in the car indicates how many goals remain in the bullet at (length-1), and so on recursively. nil means we haven't started bulleting the current proof.") (defvar-local my/last-seen-qed nil) (defun my/get-maybe-bullet-error () "Extract the number of focused goals from the ! selector error message." (when-let* ((rbuf (get-buffer "*response*")) (str (with-current-buffer "*response*" (buffer-string))) (_ (string-match (rx "Error: Expected a single focused goal but " (group (+ digit))) str)) (ngoals (string-to-number (match-string 1 str)))) ngoals)) (defun my/bullet-fix-indent () "Auto indent until the next Qed/Defined, and update my/last-seen-qed." ;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count)) (when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t)))) (set-marker my/last-seen-qed qed) (indent-region (- (point) 1) qed))) (defun my/nth-bullet (n) "Get nth bullet, erroring if n >= length my/bullet-stack" (or (nth n my/bullet-stack) (error "Too many bullets."))) (defun my/maybe-fix-bullet-error (&optional arg) "Main function for porting a file to strict focusing. Repeatedly process your file in proof general until you get a focusing error, then run this function. Once there are no more errors you're done. Indentation commonly looks bad in the middle of fixing a proof, but will be fixed unless you start a bullet in the middle of a line and don't finish it in that line. ie in 'tac1. - tac2.\n tac3.' tac3 will get indented to align with tac2, but if tac2 finished the bullet the next action will reindent. This is a stateful process. The state is automatically reset when you get to the next proof, but if you get an error or take manual action which breaks the algorithm's expectation you can call with prefix argument to reset." (interactive "P") (unless my/last-seen-qed (setq my/last-seen-qed (set-marker (make-marker) 0))) (when (or arg (> (point) my/last-seen-qed)) (setq my/bullet-count nil) (set-marker my/last-seen-qed 0)) (when-let ((ngoals (my/get-maybe-bullet-error))) (setq my/prev-count (format "%s %s" ngoals my/bullet-count)) (if (= ngoals 0) (progn (while (and my/bullet-count (= (car my/bullet-count) 0)) (pop my/bullet-count)) (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " ")) (setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count))) (my/bullet-fix-indent)) (setq my/bullet-count (cons (- ngoals 1) my/bullet-count)) (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " ")) (my/bullet-fix-indent)))) (bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map) ~~~ --- theories/Structures/Equalities.v | 10 +++-- theories/Structures/GenericMinMax.v | 90 ++++++++++++++++++++----------------- theories/Structures/Orders.v | 54 +++++++++++----------- theories/Structures/OrdersFacts.v | 6 +-- 4 files changed, 86 insertions(+), 74 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 4143dba547..346c300ee5 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -158,8 +158,10 @@ Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E. Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. Proof. intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. - auto with *. - split. discriminate. intro EQ; elim NEQ; auto. + - auto with *. + - split. + + discriminate. + + intro EQ; elim NEQ; auto. Qed. End HasEqDec2Bool. @@ -168,8 +170,8 @@ Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E. Proof. intros x y. assert (H:=F.eqb_eq x y). destruct (F.eqb x y); [left|right]. - apply -> H; auto. - intro EQ. apply H in EQ. discriminate. + - apply -> H; auto. + - intro EQ. apply H in EQ. discriminate. Defined. End HasEqBool2Dec. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 4d04667c01..c314f3f982 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -47,8 +47,8 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. - transitivity y; auto. - rewrite H in H'; auto. + - transitivity y; auto. + - rewrite H in H'; auto. Qed. Lemma max_l x y : y<=x -> max x y == x. @@ -142,8 +142,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. (** *** Semi-lattice algebraic properties of [max] *) @@ -194,7 +194,11 @@ Proof. Qed. Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m. -Proof. split. apply max_le. solve_max. Qed. +Proof. + split. + - apply max_le. + - solve_max. +Qed. Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m. Proof. @@ -282,8 +286,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. Lemma min_id n : min n n == n. @@ -330,7 +334,11 @@ Proof. Qed. Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p. -Proof. split. apply min_le. solve_min. Qed. +Proof. + split. + - apply min_le. + - solve_min. +Qed. Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p. Proof. @@ -377,16 +385,16 @@ Lemma min_max_absorption n m : max n (min n m) == n. Proof. intros. destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E. - apply max_l. order. - destruct (max_spec n m); intuition; order. + - apply max_l. order. + - destruct (max_spec n m); intuition; order. Qed. Lemma max_min_absorption n m : min n (max n m) == n. Proof. intros. destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. - apply min_l; auto. order. + - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. + - apply min_l; auto. order. Qed. (** Distributivity *) @@ -395,16 +403,16 @@ Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p). Proof. symmetry. apply min_mono. - eauto with *. - repeat red; intros. apply max_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply max_le_compat_l; auto. Qed. Lemma min_max_distr n m p : min n (max m p) == max (min n m) (min n p). Proof. symmetry. apply max_mono. - eauto with *. - repeat red; intros. apply min_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply min_le_compat_l; auto. Qed. (** Modularity *) @@ -415,8 +423,8 @@ Proof. rewrite <- max_min_distr. destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed. Lemma min_max_modular n m p : @@ -425,8 +433,8 @@ Proof. intros. rewrite <- min_max_distr. destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. - rewrite 2 min_l; try order. rewrite max_le_iff; auto. + - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. + - rewrite 2 min_l; try order. rewrite max_le_iff; auto. Qed. (** Disassociativity *) @@ -448,8 +456,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. Lemma min_max_antimono f : @@ -460,8 +468,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. End MinMaxLogicalProperties. @@ -479,12 +487,12 @@ Lemma max_case_strong n m (P:t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply max_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply max_l; auto. Defined. Lemma max_case n m (P:t -> Type) : @@ -508,12 +516,12 @@ Lemma min_case_strong n m (P:O.t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply min_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined. Lemma min_case n m (P:O.t -> Type) : @@ -624,11 +632,11 @@ Module TOMaxEqDec_to_Compare Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. intros; unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. - absurd (x==y); auto. transitivity (max x y); auto. - symmetry. apply max_l. rewrite le_lteq; intuition. - destruct (lt_total y x); auto. - absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. + - destruct (lt_total x y); auto. + absurd (x==y); auto. transitivity (max x y); auto. + symmetry. apply max_l. rewrite le_lteq; intuition. + - destruct (lt_total y x); auto. + absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. Qed. End TOMaxEqDec_to_Compare. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 310a22a0a4..7fcf517457 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -143,8 +143,8 @@ Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O. Proof. unfold eqb. intros x y. destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). Qed. End Compare2EqBool. @@ -252,9 +252,11 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). - destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT. + - discriminate. + - intros LE. elim (StrictOrder_Irreflexive x). + destruct LE as [LT|EQ]. + + now transitivity y. + + now rewrite <- EQ in GT. Qed. Lemma leb_total : forall x y, leb x y \/ leb y x. @@ -267,10 +269,10 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros x y z. rewrite !leb_le, !le_lteq. intros [Hxy|Hxy] [Hyz|Hyz]. - left; transitivity y; auto. - left; rewrite <- Hyz; auto. - left; rewrite Hxy; auto. - right; transitivity y; auto. + - left; transitivity y; auto. + - left; rewrite <- Hyz; auto. + - left; rewrite Hxy; auto. + - right; transitivity y; auto. Qed. Definition t := t. @@ -302,10 +304,10 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Proof. intros. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). - constructor. split; auto. - constructor. split; congruence. - constructor. destruct (leb_total x y); split; congruence. + - case_eq (y <=? x). + + constructor. split; auto. + + constructor. split; congruence. + - constructor. destruct (leb_total x y); split; congruence. Qed. Definition eqb x y := (x <=? y) && (y <=? x). @@ -321,19 +323,19 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Instance eq_equiv : Equivalence eq. Proof. split. - intros x; unfold eq, le. destruct (leb_total x x); auto. - intros x y; unfold eq, le. intuition. - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. + - intros x; unfold eq, le. destruct (leb_total x x); auto. + - intros x y; unfold eq, le. intuition. + - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. Qed. Instance lt_strorder : StrictOrder lt. Proof. split. - intros x. unfold lt; red; intuition. - intros x y z; unfold lt, le. intuition. - apply leb_trans with y; auto. - absurd (z <=? y); auto. - apply leb_trans with x; auto. + - intros x. unfold lt; red; intuition. + - intros x y z; unfold lt, le. intuition. + + apply leb_trans with y; auto. + + absurd (z <=? y); auto. + apply leb_trans with x; auto. Qed. Instance lt_compat : Proper (eq ==> eq ==> iff) lt. @@ -341,11 +343,11 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy' H. unfold eq, lt, le in *. intuition. - apply leb_trans with x; auto. - apply leb_trans with y; auto. - absurd (y <=? x); auto. - apply leb_trans with x'; auto. - apply leb_trans with y'; auto. + - apply leb_trans with x; auto. + apply leb_trans with y; auto. + - absurd (y <=? x); auto. + apply leb_trans with x'; auto. + apply leb_trans with y'; auto. Qed. Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 1fb0a37e16..182b781fe1 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -290,9 +290,9 @@ Module Type CompareBasedOrderFacts Lemma compare_spec x y : CompareSpec (x==y) (x x==y. -- cgit v1.2.3